diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-02 16:17:51 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-02 16:17:51 +0200 |
commit | f21a6b181dded86ef0e5c7ab94f74e5b960fd510 (patch) | |
tree | 01bb7b59e438c60d12d87d869b6c890095a977f4 /backend | |
parent | a14b9578ee5297d954103e05d7b2d322816ddd8f (diff) | |
download | compcert-f21a6b181dded86ef0e5c7ab94f74e5b960fd510.tar.gz compcert-f21a6b181dded86ef0e5c7ab94f74e5b960fd510.zip |
Improve code generation for 64-bit signed integer division
Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port.
Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
Diffstat (limited to 'backend')
-rw-r--r-- | backend/SelectDiv.vp | 65 | ||||
-rw-r--r-- | backend/SelectDivproof.v | 119 | ||||
-rw-r--r-- | backend/Selection.v | 6 | ||||
-rw-r--r-- | backend/Selectionproof.v | 4 | ||||
-rw-r--r-- | backend/SplitLong.vp | 43 | ||||
-rw-r--r-- | backend/SplitLongproof.v | 133 | ||||
-rw-r--r-- | backend/ValueDomain.v | 18 |
7 files changed, 256 insertions, 132 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index d708afb7..1fc0b689 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -14,12 +14,8 @@ Require Import Coqlib. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. -Require Import SelectOp. +Require Import AST Integers Floats. +Require Import Op CminorSel SelectOp SplitLong SelectLong. Open Local Scope cminorsel_scope. @@ -201,6 +197,63 @@ Nondetfunction mods (e1: expr) (e2: expr) := | _ => mods_base e1 e2 end. +(** 64-bit integer divisions *) + +Section SELECT. + +Context {hf: helper_functions}. + +Definition modl_from_divl (equo: expr) (n: int64) := + subl (Eletvar O) (mullimm n equo). + +Definition divlu (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.divu n1 n2) + | Some n2, _ => + match Int64.is_power2' n2 with + | Some l => shrluimm e1 l + | None => divlu_base e1 e2 + end (* TODO: multiply-high *) + | _, _ => divlu_base e1 e2 + end. + +Definition modlu (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.modu n1 n2) + | Some n2, _ => + match Int64.is_power2 n2 with + | Some l => andl e1 (longconst (Int64.sub n2 Int64.one)) + | None => modlu_base e1 e2 + end + | _, _ => modlu_base e1 e2 + end. + +Definition divls (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.divs n1 n2) + | Some n2, _ => + match Int64.is_power2' n2 with + | Some l => if Int.ltu l (Int.repr 63) then shrxlimm e1 l else divls_base e1 e2 + | None => divls_base e1 e2 + end (* TODO: multiply-high *) + | _, _ => divls_base e1 e2 + end. + +Definition modls (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.mods n1 n2) + | Some n2, _ => + match Int64.is_power2' n2 with + | Some l => if Int.ltu l (Int.repr 63) + then Elet e1 (modl_from_divl (shrxlimm (Eletvar O) l) n2) + else modls_base e1 e2 + | None => modls_base e1 e2 + end + | _, _ => modls_base e1 e2 + end. + +End SELECT. + (** Floating-point division by a constant can also be turned into a FP multiplication by the inverse constant, but only for powers of 2. *) diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 5621acd5..441f69b1 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -15,7 +15,7 @@ Require Import Zquot Coqlib. Require Import AST Integers Floats Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. -Require Import SelectOp SelectOpproof SelectDiv. +Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv. Open Local Scope cminorsel_scope. @@ -321,7 +321,10 @@ Qed. Section CMCONSTRS. -Variable ge: genv. +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. @@ -543,6 +546,118 @@ Proof. - eapply eval_mods_base; eauto. Qed. +Lemma eval_modl_from_divl: + forall le a n x y, + eval_expr ge sp e m le a (Vlong y) -> + nth_error le O = Some (Vlong x) -> + eval_expr ge sp e m le (modl_from_divl a n) (Vlong (Int64.sub x (Int64.mul y n))). +Proof. + unfold modl_from_divl; intros. + exploit eval_mullimm; eauto. instantiate (1 := n). intros (v1 & A1 & B1). + exploit (eval_subl prog sp e m le (Eletvar O)). constructor; eauto. eexact A1. + intros (v2 & A2 & B2). + simpl in B1; inv B1. simpl in B2; inv B2. exact A2. +Qed. + +Theorem eval_divlu: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.divlu x y = Some z -> + exists v, eval_expr ge sp e m le (divlu a b) v /\ Val.lessdef z v. +Proof. + unfold divlu; intros. + destruct (is_longconst b) as [n2|] eqn:N2. +- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y. + destruct (is_longconst a) as [n1|] eqn:N1. ++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x. + simpl in H1. destruct (Int64.eq n2 Int64.zero); inv H1. + econstructor; split. apply eval_longconst. constructor. ++ destruct (Int64.is_power2' n2) as [l|] eqn:POW. +* exploit Val.divlu_pow2; eauto. intros EQ; subst z. apply eval_shrluimm; auto. +* eapply eval_divlu_base; eauto. +- eapply eval_divlu_base; eauto. +Qed. + +Theorem eval_modlu: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.modlu x y = Some z -> + exists v, eval_expr ge sp e m le (modlu a b) v /\ Val.lessdef z v. +Proof. + unfold modlu; intros. + destruct (is_longconst b) as [n2|] eqn:N2. +- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y. + destruct (is_longconst a) as [n1|] eqn:N1. ++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x. + simpl in H1. destruct (Int64.eq n2 Int64.zero); inv H1. + econstructor; split. apply eval_longconst. constructor. ++ destruct (Int64.is_power2 n2) as [l|] eqn:POW. +* exploit Val.modlu_pow2; eauto. intros EQ; subst z. eapply eval_andl; eauto. apply eval_longconst. +* eapply eval_modlu_base; eauto. +- eapply eval_modlu_base; eauto. +Qed. + +Theorem eval_divls: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.divls x y = Some z -> + exists v, eval_expr ge sp e m le (divls a b) v /\ Val.lessdef z v. +Proof. + unfold divls; intros. + destruct (is_longconst b) as [n2|] eqn:N2. +- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y. + destruct (is_longconst a) as [n1|] eqn:N1. ++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x. + simpl in H1. + destruct (Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1. + econstructor; split. apply eval_longconst. constructor. ++ destruct (Int64.is_power2' n2) as [l|] eqn:POW. +* destruct (Int.ltu l (Int.repr 63)) eqn:LT. +** exploit Val.divls_pow2; eauto. intros EQ. eapply eval_shrxlimm; eauto. +** eapply eval_divls_base; eauto. +* eapply eval_divls_base; eauto. +- eapply eval_divls_base; eauto. +Qed. + +Theorem eval_modls: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.modls x y = Some z -> + exists v, eval_expr ge sp e m le (modls a b) v /\ Val.lessdef z v. +Proof. + unfold modls; intros. + destruct (is_longconst b) as [n2|] eqn:N2. +- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y. + destruct (is_longconst a) as [n1|] eqn:N1. ++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x. + simpl in H1. + destruct (Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1. + econstructor; split. apply eval_longconst. constructor. ++ destruct (Int64.is_power2' n2) as [l|] eqn:POW. +* destruct (Int.ltu l (Int.repr 63)) eqn:LT. +**destruct x; simpl in H1; try discriminate. + destruct (Int64.eq n2 Int64.zero + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone) eqn:D; inv H1. + assert (Val.divls (Vlong i) (Vlong n2) = Some (Vlong (Int64.divs i n2))). + { simpl; rewrite D; auto. } + exploit Val.divls_pow2; eauto. intros EQ. + set (le' := Vlong i :: le). + assert (A: eval_expr ge sp e m le' (Eletvar O) (Vlong i)) by (constructor; auto). + exploit eval_shrxlimm; eauto. intros (v1 & A1 & B1). inv B1. + econstructor; split. + econstructor. eauto. eapply eval_modl_from_divl. eexact A1. reflexivity. + rewrite Int64.mods_divs. auto. +**eapply eval_modls_base; eauto. +* eapply eval_modls_base; eauto. +- eapply eval_modls_base; eauto. +Qed. + (** * Floating-point division *) Theorem eval_divf: diff --git a/backend/Selection.v b/backend/Selection.v index 3aff446e..5cb5d119 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -27,7 +27,7 @@ Require Import Coqlib Maps. Require Import AST Errors Integers Globalenvs Switch. Require Cminor. Require Import Op CminorSel. -Require Import SelectOp SelectDiv SplitLong SelectLong. +Require Import SelectOp SplitLong SelectLong SelectDiv. Require Machregs. Local Open Scope cminorsel_scope. @@ -138,9 +138,9 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := | Cminor.Oaddl => addl arg1 arg2 | Cminor.Osubl => subl arg1 arg2 | Cminor.Omull => mull arg1 arg2 - | Cminor.Odivl => divl arg1 arg2 + | Cminor.Odivl => divls arg1 arg2 | Cminor.Odivlu => divlu arg1 arg2 - | Cminor.Omodl => modl arg1 arg2 + | Cminor.Omodl => modls arg1 arg2 | Cminor.Omodlu => modlu arg1 arg2 | Cminor.Oandl => andl arg1 arg2 | Cminor.Oorl => orl arg1 arg2 diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 34157553..90e50338 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -305,9 +305,9 @@ Proof. eapply eval_addl; eauto. eapply eval_subl; eauto. eapply eval_mull; eauto. - eapply eval_divl; eauto. + eapply eval_divls; eauto. eapply eval_divlu; eauto. - eapply eval_modl; eauto. + eapply eval_modls; eauto. eapply eval_modlu; eauto. eapply eval_andl; eauto. eapply eval_orl; eauto. diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index 305e20f3..5891adef 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -255,38 +255,17 @@ Definition mull (e1 e2: expr) := | _, _ => mull_base e1 e2 end. -Definition binop_long (id: ident) (sem: int64 -> int64 -> int64) (e1 e2: expr) := - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (sem n1 n2) - | _, _ => Eexternal id sig_ll_l (e1 ::: e2 ::: Enil) - end. - -Definition divl e1 e2 := binop_long i64_sdiv Int64.divs e1 e2. -Definition modl e1 e2 := binop_long i64_smod Int64.mods e1 e2. - -Definition divlu (e1 e2: expr) := - let default := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil) in - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.divu n1 n2) - | _, Some n2 => - match Int64.is_power2' n2 with - | Some l => shrluimm e1 l - | None => default - end - | _, _ => default - end. - -Definition modlu (e1 e2: expr) := - let default := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil) in - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.modu n1 n2) - | _, Some n2 => - match Int64.is_power2 n2 with - | Some l => andl e1 (longconst (Int64.sub n2 Int64.one)) - | None => default - end - | _, _ => default - end. +Definition shrxlimm (e: expr) (n: int) := + if Int.eq n Int.zero then e else + Elet e (shrlimm (addl (Eletvar O) + (shrluimm (shrlimm (Eletvar O) (Int.repr 63)) + (Int.sub (Int.repr 64) n))) + n). + +Definition divlu_base (e1 e2: expr) := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil). +Definition modlu_base (e1 e2: expr) := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil). +Definition divls_base (e1 e2: expr) := Eexternal i64_sdiv sig_ll_l (e1 ::: e2 ::: Enil). +Definition modls_base (e1 e2: expr) := Eexternal i64_smod sig_ll_l (e1 ::: e2 ::: Enil). Definition cmpl_eq_zero (e: expr) := splitlong e (fun h l => comp Ceq (or h l) (Eop (Ointconst Int.zero) Enil)). diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 1dbe25bd..57fc6b56 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -823,118 +823,79 @@ Proof. - apply eval_mull_base; auto. Qed. -Lemma eval_binop_long: - forall id name sem le a b x y z, - (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) -> - helper_declared prog id name sig_ll_l -> - external_implements name sig_ll_l (x::y::nil) z -> +Theorem eval_shrxlimm: + forall le a n x z, + Archi.ptr64 = false -> eval_expr ge sp e m le a x -> - eval_expr ge sp e m le b y -> - exists v, eval_expr ge sp e m le (binop_long id sem a b) v /\ Val.lessdef z v. + Val.shrxl x (Vint n) = Some z -> + exists v, eval_expr ge sp e m le (shrxlimm a n) v /\ Val.lessdef z v. Proof. - intros. unfold binop_long. - destruct (is_longconst a) as [p|] eqn:LC1. - destruct (is_longconst b) as [q|] eqn:LC2. - exploit is_longconst_sound. eexact LC1. eauto. intros EQ; subst x. - exploit is_longconst_sound. eexact LC2. eauto. intros EQ; subst y. - econstructor; split. EvalOp. erewrite H by eauto. rewrite Int64.ofwords_recompose. auto. - econstructor; split. eapply eval_helper_2; eauto. auto. - econstructor; split. eapply eval_helper_2; eauto. auto. + intros. + apply Val.shrxl_shrl_2 in H1. unfold shrxlimm. + destruct (Int.eq n Int.zero). +- subst z; exists x; auto. +- set (le' := x :: le). + edestruct (eval_shrlimm (Int.repr 63) le' (Eletvar O)) as (v1 & A1 & B1). + constructor. reflexivity. + edestruct (eval_shrluimm (Int.sub (Int.repr 64) n) le') as (v2 & A2 & B2). + eexact A1. + edestruct (eval_addl H le' (Eletvar 0)) as (v3 & A3 & B3). + constructor. reflexivity. eexact A2. + edestruct (eval_shrlimm n le') as (v4 & A4 & B4). eexact A3. + exists v4; split. + econstructor; eauto. + assert (X: forall v1 v2 n, Val.lessdef v1 v2 -> Val.lessdef (Val.shrl v1 (Vint n)) (Val.shrl v2 (Vint n))). + { intros. inv H2; auto. } + assert (Y: forall v1 v2 n, Val.lessdef v1 v2 -> Val.lessdef (Val.shrlu v1 (Vint n)) (Val.shrlu v2 (Vint n))). + { intros. inv H2; auto. } + subst z. eapply Val.lessdef_trans; [|eexact B4]. apply X. + eapply Val.lessdef_trans; [|eexact B3]. apply Val.addl_lessdef; auto. + eapply Val.lessdef_trans; [|eexact B2]. apply Y. + auto. Qed. -Theorem eval_divl: +Theorem eval_divlu_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> - Val.divls x y = Some z -> - exists v, eval_expr ge sp e m le (divl a b) v /\ Val.lessdef z v. + Val.divlu x y = Some z -> + exists v, eval_expr ge sp e m le (divlu_base a b) v /\ Val.lessdef z v. Proof. - intros. eapply eval_binop_long; eauto. - intros; subst; simpl in H1. - destruct (Int64.eq q Int64.zero - || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. - auto. - DeclHelper. UseHelper. + intros; unfold divlu_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. -Theorem eval_modl: +Theorem eval_modlu_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> - Val.modls x y = Some z -> - exists v, eval_expr ge sp e m le (modl a b) v /\ Val.lessdef z v. + Val.modlu x y = Some z -> + exists v, eval_expr ge sp e m le (modlu_base a b) v /\ Val.lessdef z v. Proof. - intros. eapply eval_binop_long; eauto. - intros; subst; simpl in H1. - destruct (Int64.eq q Int64.zero - || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. - auto. - DeclHelper. UseHelper. + intros; unfold modlu_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. -Theorem eval_divlu: +Theorem eval_divsu_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> - Val.divlu x y = Some z -> - exists v, eval_expr ge sp e m le (divlu a b) v /\ Val.lessdef z v. + Val.divls x y = Some z -> + exists v, eval_expr ge sp e m le (divls_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divlu. - set (default := Eexternal i64_udiv sig_ll_l (a ::: b ::: Enil)). - assert (DEFAULT: - exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v). - { - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. - } - destruct (is_longconst a) as [p|] eqn:LC1; - destruct (is_longconst b) as [q|] eqn:LC2. -- exploit (is_longconst_sound le a); eauto. intros EQ; subst x. - exploit (is_longconst_sound le b); eauto. intros EQ; subst y. - econstructor; split. apply eval_longconst. - simpl in H1. destruct (Int64.eq q Int64.zero); inv H1. auto. -- auto. -- destruct (Int64.is_power2' q) as [l|] eqn:P2; auto. - exploit (is_longconst_sound le b); eauto. intros EQ; subst y. - replace z with (Val.shrlu x (Vint l)). - apply eval_shrluimm. auto. - destruct x; simpl in H1; try discriminate. - destruct (Int64.eq q Int64.zero); inv H1. - simpl. erewrite Int64.is_power2'_range by eauto. - erewrite Int64.divu_pow2' by eauto. - auto. -- auto. + intros; unfold divls_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. -Theorem eval_modlu: +Theorem eval_modls_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> - Val.modlu x y = Some z -> - exists v, eval_expr ge sp e m le (modlu a b) v /\ Val.lessdef z v. + Val.modls x y = Some z -> + exists v, eval_expr ge sp e m le (modls_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold modlu. - set (default := Eexternal i64_umod sig_ll_l (a ::: b ::: Enil)). - assert (DEFAULT: - exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v). - { - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. - } - destruct (is_longconst a) as [p|] eqn:LC1; - destruct (is_longconst b) as [q|] eqn:LC2. -- exploit (is_longconst_sound le a); eauto. intros EQ; subst x. - exploit (is_longconst_sound le b); eauto. intros EQ; subst y. - econstructor; split. apply eval_longconst. - simpl in H1. destruct (Int64.eq q Int64.zero); inv H1. auto. -- auto. -- destruct (Int64.is_power2 q) as [l|] eqn:P2; auto. - exploit (is_longconst_sound le b); eauto. intros EQ; subst y. - replace z with (Val.andl x (Vlong (Int64.sub q Int64.one))). - apply eval_andl. auto. apply eval_longconst. - destruct x; simpl in H1; try discriminate. - destruct (Int64.eq q Int64.zero); inv H1. - simpl. - erewrite Int64.modu_and by eauto. auto. -- auto. + intros; unfold modls_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Remark decompose_cmpl_eq_zero: diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 6b314904..bf88a450 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -1938,6 +1938,22 @@ Proof. inv H; inv H0; auto with va. simpl. rewrite E. constructor. Qed. +Definition shrxl (v w: aval) := + match v, w with + | L i, I j => if Int.ltu j (Int.repr 63) then L(Int64.shrx' i j) else ntop + | _, _ => ntop1 v + end. + +Lemma shrxl_sound: + forall v w u x y, vmatch v x -> vmatch w y -> Val.shrxl v w = Some u -> vmatch u (shrxl x y). +Proof. + intros. + destruct v; destruct w; try discriminate; simpl in H1. + destruct (Int.ltu i0 (Int.repr 63)) eqn:LTU; inv H1. + unfold shrxl; inv H; auto with va; inv H0; auto with va. + rewrite LTU; auto with va. +Qed. + (** Floating-point arithmetic operations *) Definition negf := unop_float Float.neg. @@ -4544,7 +4560,7 @@ Hint Resolve cnot_sound symbol_address_sound shll_sound shrl_sound shrlu_sound andl_sound orl_sound xorl_sound notl_sound roll_sound rorl_sound negl_sound addl_sound subl_sound mull_sound - divls_sound divlu_sound modls_sound modlu_sound + divls_sound divlu_sound modls_sound modlu_sound shrxl_sound negf_sound absf_sound addf_sound subf_sound mulf_sound divf_sound negfs_sound absfs_sound |