diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-21 09:17:05 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-21 19:39:46 +0200 |
commit | cae21e8816db863bf99f87469c9680e150d28960 (patch) | |
tree | 19fdf188238300245e0e5e7a9b78a94bbb53df93 /riscV | |
parent | 52b4f973646c3b79804fcdddeed5325ab1f3ce7d (diff) | |
download | compcert-kvx-cae21e8816db863bf99f87469c9680e150d28960.tar.gz compcert-kvx-cae21e8816db863bf99f87469c9680e150d28960.zip |
maketotal mod & div
Diffstat (limited to 'riscV')
-rw-r--r-- | riscV/Asmgenproof1.v | 45 | ||||
-rw-r--r-- | riscV/ConstpropOpproof.v | 152 | ||||
-rw-r--r-- | riscV/Op.v | 143 | ||||
-rw-r--r-- | riscV/SelectLongproof.v | 46 | ||||
-rw-r--r-- | riscV/SelectOpproof.v | 62 | ||||
-rw-r--r-- | riscV/ValueAOp.v | 310 |
6 files changed, 593 insertions, 165 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 8678a5dc..d2255e66 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1035,7 +1035,9 @@ Opaque Int.eq. intros (rs' & A & B & C). exists rs'; split; eauto. rewrite B; auto with asmgen. - (* shrximm *) - clear H. exploit Val.shrx_shr_3; eauto. intros E; subst v; clear EV. + destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn. + { + exploit Val.shrx_shr_3; eauto. intros E; subst v. destruct (Int.eq n Int.zero). + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. @@ -1052,6 +1054,24 @@ Opaque Int.eq. eapply exec_straight_step. simpl; reflexivity. auto. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. + } + destruct (Int.eq n Int.zero). ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. ++ destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + - (* longofintu *) econstructor; split. eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto. @@ -1076,7 +1096,27 @@ Opaque Int.eq. intros (rs' & A & B & C). exists rs'; split; eauto. rewrite B; auto with asmgen. - (* shrxlimm *) - clear H. exploit Val.shrxl_shrl_3; eauto. intros E; subst v; clear EV. + destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL. + { + exploit Val.shrxl_shrl_3; eauto. intros E; subst v. + destruct (Int.eq n Int.zero). ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. ++ destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + + * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + } destruct (Int.eq n Int.zero). + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. @@ -1094,6 +1134,7 @@ Opaque Int.eq. eapply exec_straight_step. simpl; reflexivity. auto. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. + - (* cond *) exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. diff --git a/riscV/ConstpropOpproof.v b/riscV/ConstpropOpproof.v index 765aa035..26a50317 100644 --- a/riscV/ConstpropOpproof.v +++ b/riscV/ConstpropOpproof.v @@ -265,52 +265,84 @@ Qed. Lemma make_divimm_correct: forall n r1 r2 v, - Val.divs e#r1 e#r2 = Some v -> + Val.maketotal (Val.divs e#r1 e#r2) = v -> e#r2 = Vint n -> let (op, args) := make_divimm n r1 r2 in exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. - predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. - destruct (e#r1) eqn:?; - try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); - inv H; auto. - destruct (Int.is_power2 n) eqn:?. - destruct (Int.ltu i (Int.repr 31)) eqn:?. - exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. - exists v; auto. - exists v; auto. + predSpec Int.eq Int.eq_spec n Int.one; intros; subst; rewrite H0. + { destruct (e # r1) eqn:Er1. + all: try (cbn; exists (e # r1); split; auto; fail). + rewrite Val.divs_one. + cbn. + rewrite Er1. + exists (Vint i); split; auto. + } + destruct (Int.is_power2 n) eqn:Power2. + { + destruct (Int.ltu i (Int.repr 31)) eqn:iLT31. + { + cbn. + exists (Val.maketotal (Val.shrx e # r1 (Vint i))); split; auto. + destruct (Val.divs e # r1 (Vint n)) eqn:DIVS; cbn; auto. + rewrite Val.divs_pow2 with (y:=v) (n:=n). + cbn. + all: auto. + } + exists (Val.maketotal (Val.divs e # r1 (Vint n))); split; cbn; auto; congruence. + } + exists (Val.maketotal (Val.divs e # r1 (Vint n))); split; cbn; auto; congruence. Qed. Lemma make_divuimm_correct: forall n r1 r2 v, - Val.divu e#r1 e#r2 = Some v -> + Val.maketotal (Val.divu e#r1 e#r2) = v -> e#r2 = Vint n -> let (op, args) := make_divuimm n r1 r2 in exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. - predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. - destruct (e#r1) eqn:?; - try (rewrite Val.divu_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); - inv H; auto. - destruct (Int.is_power2 n) eqn:?. - econstructor; split. simpl; eauto. - rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto. - exists v; auto. + predSpec Int.eq Int.eq_spec n Int.one; intros; subst; rewrite H0. + { destruct (e # r1) eqn:Er1. + all: try (cbn; exists (e # r1); split; auto; fail). + rewrite Val.divu_one. + cbn. + rewrite Er1. + exists (Vint i); split; auto. + } + destruct (Int.is_power2 n) eqn:Power2. + { + cbn. + exists (Val.shru e # r1 (Vint i)); split; auto. + destruct (Val.divu e # r1 (Vint n)) eqn:DIVU; cbn; auto. + rewrite Val.divu_pow2 with (y:=v) (n:=n). + all: auto. + } + exists (Val.maketotal (Val.divu e # r1 (Vint n))); split; cbn; auto; congruence. Qed. Lemma make_moduimm_correct: forall n r1 r2 v, - Val.modu e#r1 e#r2 = Some v -> + Val.maketotal (Val.modu e#r1 e#r2) = v -> e#r2 = Vint n -> let (op, args) := make_moduimm n r1 r2 in exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_moduimm. destruct (Int.is_power2 n) eqn:?. - exists v; split; auto. simpl. decEq. eapply Val.modu_pow2; eauto. congruence. - exists v; auto. + { destruct (Val.modu e # r1 e # r2) eqn:MODU; cbn in H. + { subst v0. + exists v; split; auto. + cbn. decEq. eapply Val.modu_pow2; eauto. congruence. + } + subst v. + eexists; split; auto. + cbn. reflexivity. + } + exists v; split; auto. + cbn. + congruence. Qed. Lemma make_andimm_correct: @@ -444,48 +476,82 @@ Qed. Lemma make_divlimm_correct: forall n r1 r2 v, - Val.divls e#r1 e#r2 = Some v -> + Val.maketotal (Val.divls e#r1 e#r2) = v -> e#r2 = Vlong n -> let (op, args) := make_divlimm n r1 r2 in exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divlimm. - destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?. - rewrite H0 in H. econstructor; split. simpl; eauto. eapply Val.divls_pow2; eauto. auto. - exists v; auto. - exists v; auto. + destruct (Int64.is_power2' n) eqn:Power2. + { + destruct (Int.ltu i (Int.repr 63)) eqn:iLT63. + { + cbn. + exists (Val.maketotal (Val.shrxl e # r1 (Vint i))); split; auto. + rewrite H0 in H. + destruct (Val.divls e # r1 (Vlong n)) eqn:DIVS; cbn in H; auto. + { + subst v0. + rewrite Val.divls_pow2 with (y:=v) (n:=n). + cbn. + all: auto. + } + subst. auto. + } + cbn. subst. rewrite H0. + exists (Val.maketotal (Val.divls e # r1 (Vlong n))); split; auto. + } + cbn. subst. rewrite H0. + exists (Val.maketotal (Val.divls e # r1 (Vlong n))); split; auto. Qed. Lemma make_divluimm_correct: forall n r1 r2 v, - Val.divlu e#r1 e#r2 = Some v -> + Val.maketotal (Val.divlu e#r1 e#r2) = v -> e#r2 = Vlong n -> let (op, args) := make_divluimm n r1 r2 in exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divluimm. destruct (Int64.is_power2' n) eqn:?. + { econstructor; split. simpl; eauto. - rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. - simpl. - erewrite Int64.is_power2'_range by eauto. - erewrite Int64.divu_pow2' by eauto. auto. - exists v; auto. + rewrite H0 in H. destruct (e#r1); inv H. + all: cbn; auto. + { + destruct (Int64.eq n Int64.zero); cbn; auto. + erewrite Int64.is_power2'_range by eauto. + erewrite Int64.divu_pow2' by eauto. auto. + } + } + exists v; split; auto. + cbn. + rewrite H. + reflexivity. Qed. Lemma make_modluimm_correct: forall n r1 r2 v, - Val.modlu e#r1 e#r2 = Some v -> + Val.maketotal (Val.modlu e#r1 e#r2) = v -> e#r2 = Vlong n -> let (op, args) := make_modluimm n r1 r2 in exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_modluimm. destruct (Int64.is_power2 n) eqn:?. - exists v; split; auto. simpl. decEq. - rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. - simpl. erewrite Int64.modu_and by eauto. auto. - exists v; auto. + { + econstructor; split. simpl; eauto. + rewrite H0 in H. destruct (e#r1); inv H. + all: cbn; auto. + { + destruct (Int64.eq n Int64.zero); cbn; auto. + erewrite Int64.modu_and by eauto. auto. + } + } + exists v; split; auto. + cbn. + rewrite H. + reflexivity. Qed. Lemma make_andlimm_correct: @@ -633,14 +699,17 @@ Proof. - (* mul 2*) InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto. - (* divs *) - assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. - apply make_divimm_correct; auto. + assert (e#r2 = Vint n2). { clear H0. InvApproxRegs; SimplVM; auto. } + apply make_divimm_correct; auto. + congruence. - (* divu *) assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_divuimm_correct; auto. + congruence. - (* modu *) assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_moduimm_correct; auto. + congruence. - (* and 1 *) rewrite Val.and_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andimm_correct; auto. - (* and 2 *) @@ -680,12 +749,15 @@ Proof. - (* divl *) assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_divlimm_correct; auto. + congruence. - (* divlu *) assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_divluimm_correct; auto. + congruence. - (* modlu *) assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_modluimm_correct; auto. + congruence. - (* andl 1 *) rewrite Val.andl_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andlimm_correct; auto. - (* andl 2 *) @@ -241,10 +241,10 @@ Definition eval_operation | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2) | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2) | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2) - | Odiv, v1 :: v2 :: nil => Val.divs v1 v2 - | Odivu, v1 :: v2 :: nil => Val.divu v1 v2 - | Omod, v1 :: v2 :: nil => Val.mods v1 v2 - | Omodu, v1 :: v2 :: nil => Val.modu v1 v2 + | Odiv, v1 :: v2 :: nil => Some (Val.maketotal (Val.divs v1 v2)) + | Odivu, v1 :: v2 :: nil => Some (Val.maketotal (Val.divu v1 v2)) + | Omod, v1 :: v2 :: nil => Some (Val.maketotal (Val.mods v1 v2)) + | Omodu, v1 :: v2 :: nil => Some (Val.maketotal (Val.modu v1 v2)) | Oand, v1 :: v2 :: nil => Some (Val.and v1 v2) | Oandimm n, v1 :: nil => Some (Val.and v1 (Vint n)) | Oor, v1 :: v2 :: nil => Some (Val.or v1 v2) @@ -257,7 +257,7 @@ Definition eval_operation | Oshrimm n, v1 :: nil => Some (Val.shr v1 (Vint n)) | Oshru, v1 :: v2 :: nil => Some (Val.shru v1 v2) | Oshruimm n, v1 :: nil => Some (Val.shru v1 (Vint n)) - | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) + | Oshrximm n, v1::nil => Some (Val.maketotal (Val.shrx v1 (Vint n))) | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2) | Olowlong, v1::nil => Some (Val.loword v1) | Ohighlong, v1::nil => Some (Val.hiword v1) @@ -270,10 +270,10 @@ Definition eval_operation | Omull, v1::v2::nil => Some (Val.mull v1 v2) | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2) | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2) - | Odivl, v1::v2::nil => Val.divls v1 v2 - | Odivlu, v1::v2::nil => Val.divlu v1 v2 - | Omodl, v1::v2::nil => Val.modls v1 v2 - | Omodlu, v1::v2::nil => Val.modlu v1 v2 + | Odivl, v1::v2::nil => Some (Val.maketotal (Val.divls v1 v2)) + | Odivlu, v1::v2::nil => Some (Val.maketotal (Val.divlu v1 v2)) + | Omodl, v1::v2::nil => Some (Val.maketotal (Val.modls v1 v2)) + | Omodlu, v1::v2::nil => Some (Val.maketotal (Val.modlu v1 v2)) | Oandl, v1::v2::nil => Some(Val.andl v1 v2) | Oandlimm n, v1::nil => Some (Val.andl v1 (Vlong n)) | Oorl, v1::v2::nil => Some(Val.orl v1 v2) @@ -286,7 +286,7 @@ Definition eval_operation | Oshrlimm n, v1::nil => Some (Val.shrl v1 (Vint n)) | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2) | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n)) - | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n) + | Oshrxlimm n, v1::nil => Some (Val.maketotal (Val.shrxl v1 (Vint n))) | Onegf, v1::nil => Some (Val.negf v1) | Oabsf, v1::nil => Some (Val.absf v1) | Oaddf, v1::v2::nil => Some (Val.addf v1 v2) @@ -539,15 +539,17 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1... - destruct v0; destruct v1... (* div, divu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int.eq i0 Int.zero); inv H2... + - destruct v0; destruct v1; cbn; trivial. + destruct (Int.eq i0 Int.zero + || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn; trivial. + - destruct v0; destruct v1; cbn; trivial. + destruct (Int.eq i0 Int.zero); cbn; trivial. (* mod, modu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int.eq i0 Int.zero); inv H2... + - destruct v0; destruct v1; cbn; trivial. + destruct (Int.eq i0 Int.zero + || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn; trivial. + - destruct v0; destruct v1; cbn; trivial. + destruct (Int.eq i0 Int.zero); cbn; trivial. (* and, andimm *) - destruct v0; destruct v1... - destruct v0... @@ -567,7 +569,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... (* shrx *) - - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 31)); inv H0... + - destruct v0; cbn; trivial. + destruct (Int.ltu n (Int.repr 31)); cbn; trivial. (* makelong, lowlong, highlong *) - destruct v0; destruct v1... - destruct v0... @@ -588,15 +591,19 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1... - destruct v0; destruct v1... (* divl, divlu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int64.eq i0 Int64.zero); inv H2... + - destruct v0; destruct v1; cbn; trivial. + destruct (Int64.eq i0 Int64.zero + || Int64.eq i (Int64.repr (-9223372036854775808)) && + Int64.eq i0 Int64.mone); cbn; trivial. + - destruct v0; destruct v1; cbn; trivial. + destruct (Int64.eq i0 Int64.zero); cbn; trivial. (* modl, modlu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int64.eq i0 Int64.zero); inv H2... + - destruct v0; destruct v1; cbn; trivial. + destruct (Int64.eq i0 Int64.zero + || Int64.eq i (Int64.repr (-9223372036854775808)) && + Int64.eq i0 Int64.mone); cbn; trivial. + - destruct v0; destruct v1; cbn; trivial. + destruct (Int64.eq i0 Int64.zero); cbn; trivial. (* andl, andlimm *) - destruct v0; destruct v1... - destruct v0... @@ -616,7 +623,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... (* shrxl *) - - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0... + - destruct v0; cbn; trivial. + destruct (Int.ltu n (Int.repr 63)); cbn; trivial. (* negf, absf *) - destruct v0... - destruct v0... @@ -669,9 +677,6 @@ Qed. Definition is_trapping_op (op : operation) := match op with - | Odiv | Odivl | Odivu | Odivlu - | Omod | Omodl | Omodu | Omodlu - | Oshrximm _ | Oshrxlimm _ | Ointoffloat | Ointuoffloat | Ointofsingle | Ointuofsingle | Olongoffloat | Olonguoffloat @@ -1033,19 +1038,29 @@ Proof. - inv H4; inv H2; simpl; auto. - inv H4; inv H2; simpl; auto. (* div, divu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H2; cbn. + all: try apply Val.val_inject_undef. destruct (Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. - TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. + || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn. + apply Val.val_inject_undef. + apply Val.inject_int. + - inv H4; inv H2; cbn. + all: try apply Val.val_inject_undef. + destruct (Int.eq i0 Int.zero); cbn. + apply Val.val_inject_undef. + apply Val.inject_int. (* mod, modu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H2; cbn. + all: try apply Val.val_inject_undef. destruct (Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. - TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. + || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn. + apply Val.val_inject_undef. + apply Val.inject_int. + - inv H4; inv H2; cbn. + all: try apply Val.val_inject_undef. + destruct (Int.eq i0 Int.zero); cbn. + apply Val.val_inject_undef. + apply Val.inject_int. (* and, andimm *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1065,8 +1080,10 @@ Proof. - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. (* shrx *) - - inv H4; simpl in H1; try discriminate. simpl. - destruct (Int.ltu n (Int.repr 31)); inv H1. TrivialExists. + - inv H4; cbn; try apply Val.val_inject_undef. + destruct (Int.ltu n (Int.repr 31)); cbn. + apply Val.inject_int. + apply Val.val_inject_undef. (* makelong, highlong, lowlong *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1085,19 +1102,31 @@ Proof. - inv H4; inv H2; simpl; auto. - inv H4; inv H2; simpl; auto. (* divl, divlu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H2; cbn. + all: try apply Val.val_inject_undef. destruct (Int64.eq i0 Int64.zero - || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. - TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists. + || Int64.eq i (Int64.repr (-9223372036854775808)) && + Int64.eq i0 Int64.mone); cbn. + apply Val.val_inject_undef. + apply Val.inject_long. + - inv H4; inv H2; cbn. + all: try apply Val.val_inject_undef. + destruct (Int64.eq i0 Int64.zero); cbn. + apply Val.val_inject_undef. + apply Val.inject_long. (* modl, modlu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H2; cbn. + all: try apply Val.val_inject_undef. destruct (Int64.eq i0 Int64.zero - || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. - TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists. + || Int64.eq i (Int64.repr (-9223372036854775808)) && + Int64.eq i0 Int64.mone); cbn. + apply Val.val_inject_undef. + apply Val.inject_long. + - inv H4; inv H2; cbn. + all: try apply Val.val_inject_undef. + destruct (Int64.eq i0 Int64.zero); cbn. + apply Val.val_inject_undef. + apply Val.inject_long. (* andl, andlimm *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1116,9 +1145,11 @@ Proof. (* shru, shruimm *) - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. - (* shrx *) - - inv H4; simpl in H1; try discriminate. simpl. - destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists. + (* shrx *) + - inv H4; cbn; try apply Val.val_inject_undef. + destruct (Int.ltu n (Int.repr 63)); cbn. + apply Val.inject_long. + apply Val.val_inject_undef. (* negf, absf *) - inv H4; simpl; auto. - inv H4; simpl; auto. diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v index d47b6d64..f5e8edf8 100644 --- a/riscV/SelectLongproof.v +++ b/riscV/SelectLongproof.v @@ -455,6 +455,10 @@ Proof. unfold divls_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_divls_base; eauto. TrivialExists. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls. @@ -462,6 +466,10 @@ Proof. unfold modls_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_modls_base; eauto. TrivialExists. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu. @@ -469,6 +477,10 @@ Proof. unfold divlu_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_divlu_base; eauto. TrivialExists. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu. @@ -476,6 +488,10 @@ Proof. unfold modlu_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_modlu_base; eauto. TrivialExists. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_shrxlimm: @@ -490,33 +506,9 @@ Proof. - subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto. change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto. - TrivialExists. -(* - intros. unfold shrxlimm. destruct Archi.splitlong eqn:SL. -+ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32. -+ destruct x; simpl in H0; try discriminate. - destruct (Int.ltu n (Int.repr 63)) eqn:LTU; inv H0. - predSpec Int.eq Int.eq_spec n Int.zero. - - subst n. exists (Vlong i); split; auto. rewrite Int64.shrx'_zero. auto. - - assert (NZ: Int.unsigned n <> 0). - { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. } - assert (LT: 0 <= Int.unsigned n < 63) by (apply Int.ltu_inv in LTU; assumption). - assert (LTU2: Int.ltu (Int.sub Int64.iwordsize' n) Int64.iwordsize' = true). - { unfold Int.ltu; apply zlt_true. - unfold Int.sub. change (Int.unsigned Int64.iwordsize') with 64. - rewrite Int.unsigned_repr. omega. - assert (64 < Int.max_unsigned) by reflexivity. omega. } - assert (X: eval_expr ge sp e m le - (Eop (Oshrlimm (Int.repr (Int64.zwordsize - 1))) (a ::: Enil)) - (Vlong (Int64.shr' i (Int.repr (Int64.zwordsize - 1))))). - { EvalOp. } - assert (Y: eval_expr ge sp e m le (shrxlimm_inner a n) - (Vlong (Int64.shru' (Int64.shr' i (Int.repr (Int64.zwordsize - 1))) (Int.sub Int64.iwordsize' n)))). - { EvalOp. simpl. rewrite LTU2. auto. } - TrivialExists. - constructor. EvalOp. simpl; eauto. constructor. - simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int64.shrx'_shr_2 by auto. reflexivity. - change (Int.unsigned Int64.iwordsize') with 64; omega. -*) + cbn. + rewrite H0. + reflexivity. Qed. Theorem eval_cmplu: diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 7f2014dc..436cd4f3 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -506,7 +506,12 @@ Theorem eval_divs_base: Val.divs x y = Some z -> exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divs_base. exists z; split. EvalOp. auto. + intros. unfold divs_base. exists z; split. EvalOp. + 2: apply Val.lessdef_refl. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_mods_base: @@ -516,7 +521,12 @@ Theorem eval_mods_base: Val.mods x y = Some z -> exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold mods_base. exists z; split. EvalOp. auto. + intros. unfold mods_base. exists z; split. EvalOp. + 2: apply Val.lessdef_refl. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_divu_base: @@ -526,7 +536,12 @@ Theorem eval_divu_base: Val.divu x y = Some z -> exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divu_base. exists z; split. EvalOp. auto. + intros. unfold divu_base. exists z; split. EvalOp. + 2: apply Val.lessdef_refl. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_modu_base: @@ -536,7 +551,12 @@ Theorem eval_modu_base: Val.modu x y = Some z -> exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold modu_base. exists z; split. EvalOp. auto. + intros. unfold modu_base. exists z; split. EvalOp. + 2: apply Val.lessdef_refl. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_shrximm: @@ -553,34 +573,12 @@ Proof. replace (Int.shrx i Int.zero) with i. auto. unfold Int.shrx, Int.divs. rewrite Int.shl_zero. change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. - econstructor; split. EvalOp. auto. -(* - intros. destruct x; simpl in H0; try discriminate. - destruct (Int.ltu n (Int.repr 31)) eqn:LTU; inv H0. - unfold shrximm. - predSpec Int.eq Int.eq_spec n Int.zero. - - subst n. exists (Vint i); split; auto. - unfold Int.shrx, Int.divs. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto. - - assert (NZ: Int.unsigned n <> 0). - { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. } - assert (LT: 0 <= Int.unsigned n < 31) by (apply Int.ltu_inv in LTU; assumption). - assert (LTU2: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true). - { unfold Int.ltu; apply zlt_true. - unfold Int.sub. change (Int.unsigned Int.iwordsize) with 32. - rewrite Int.unsigned_repr. omega. - assert (32 < Int.max_unsigned) by reflexivity. omega. } - assert (X: eval_expr ge sp e m le - (Eop (Oshrimm (Int.repr (Int.zwordsize - 1))) (a ::: Enil)) - (Vint (Int.shr i (Int.repr (Int.zwordsize - 1))))). - { EvalOp. } - assert (Y: eval_expr ge sp e m le (shrximm_inner a n) - (Vint (Int.shru (Int.shr i (Int.repr (Int.zwordsize - 1))) (Int.sub Int.iwordsize n)))). - { EvalOp. simpl. rewrite LTU2. auto. } - TrivialExists. - constructor. EvalOp. simpl; eauto. constructor. - simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int.shrx_shr_2 by auto. reflexivity. - change (Int.unsigned Int.iwordsize) with 32; omega. -*) + econstructor; split. EvalOp. + cbn. + rewrite H0. + cbn. + reflexivity. + apply Val.lessdef_refl. Qed. Theorem eval_shl: binary_constructor_sound shl Val.shl. diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 5670b5fe..5d1797ae 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -13,6 +13,300 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op RTL ValueDomain. +Require Import Zbits. + +Definition divs_total (v w: aval) := + match w, v with + | I i2, I i1 => + if Int.eq i2 Int.zero + || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone + then ntop + else I (Int.divs i1 i2) + | _, _ => ntop2 v w + end. + +Lemma divs_total_sound1: + forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.divs v w = Some u -> vmatch bc u (divs_total x y). +Proof. + intros until y. + intros HX HY VAL. + inv HX; inv HY; cbn in *. + { destruct (_ || _) eqn:E. + discriminate. + inv VAL. + auto with va. + } + all: try discriminate. + all: destruct (_ || _) eqn:E; inv VAL; unfold ntop2; auto with va. +Qed. + +Lemma divs_total_sound: + forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divs v w)) (divs_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + { destruct (_ || _) eqn:E; cbn; unfold ntop; auto with va. + } + all: unfold ntop2; auto with va. + all: destruct (_ || _) eqn:E; unfold ntop2; cbn; auto with va. +Qed. + +Definition divu_total (v w: aval) := + match w, v with + | I i2, I i1 => + if Int.eq i2 Int.zero + then ntop + else I (Int.divu i1 i2) + | _, _ => ntop2 v w + end. + +Lemma divu_total_sound1: + forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.divu v w = Some u -> vmatch bc u (divu_total x y). +Proof. + intros until y. + intros HX HY VAL. + inv HX; inv HY; cbn in *. + { destruct Int.eq eqn:E. + discriminate. + inv VAL. + auto with va. + } + all: try discriminate. + all: destruct Int.eq eqn:E; inv VAL; unfold ntop2; auto with va. +Qed. + +Lemma divu_total_sound: + forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divu v w)) (divu_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + { destruct Int.eq eqn:E; cbn; unfold ntop; auto with va. + } + all: unfold ntop2; auto with va. + all: destruct Int.eq eqn:E; unfold ntop2; cbn; auto with va. +Qed. + +Definition mods_total (v w: aval) := + match w, v with + | I i2, I i1 => + if Int.eq i2 Int.zero + || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone + then ntop + else I (Int.mods i1 i2) + | _, _ => ntop2 v w + end. + +Lemma mods_total_sound1: + forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.mods v w = Some u -> vmatch bc u (mods x y). +Proof. + intros until y. + intros HX HY VAL. + inv HX; inv HY; cbn in *. + { destruct (_ || _) eqn:E. + discriminate. + inv VAL. + auto with va. + } + all: try discriminate. + all: destruct (_ || _) eqn:E; inv VAL; unfold ntop2; auto with va. +Qed. + +Lemma mods_total_sound: + forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.mods v w)) (mods_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + { destruct (_ || _) eqn:E; cbn; unfold ntop; auto with va. + } + all: unfold ntop2; auto with va. + all: destruct (_ || _) eqn:E; unfold ntop2; cbn; auto with va. +Qed. + +Definition modu_total (v w: aval) := + match w, v with + | I i2, I i1 => + if Int.eq i2 Int.zero + then ntop + else I (Int.modu i1 i2) + | I i2, _ => uns (provenance v) (usize i2) + | _, _ => ntop2 v w + end. + +Lemma modu_total_sound1: + forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.modu v w = Some u -> vmatch bc u (modu x y). +Proof. + assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)). + { + intros. apply is_uns_mon with (usize (Int.modu i j)). + { apply is_uns_usize. + } + unfold usize, Int.size. + apply Zsize_monotone. + generalize (Int.unsigned_range_2 j); intros RANGE. + assert (Int.unsigned j <> 0). + { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. } + exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD. + unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. + } + + intros until y. + intros HX HY VAL. + inv HX; inv HY; cbn in *. + { destruct Int.eq eqn:E. + discriminate. + inv VAL. + auto with va. + } + all: try discriminate. + all: destruct Int.eq eqn:E; inv VAL; unfold ntop2; auto with va. + + all: + apply vmatch_uns; + apply UNS; + generalize (Int.eq_spec i0 Int.zero); + rewrite E; + auto. +Qed. + +Lemma modu_total_sound: + forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.modu v w)) (modu_total x y). +Proof. + assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)). + { + intros. apply is_uns_mon with (usize (Int.modu i j)). + { apply is_uns_usize. + } + unfold usize, Int.size. + apply Zsize_monotone. + generalize (Int.unsigned_range_2 j); intros RANGE. + assert (Int.unsigned j <> 0). + { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. } + exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD. + unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. + } + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + { destruct Int.eq eqn:E; unfold ntop; cbn; auto with va. + } + all: try discriminate. + all: unfold ntop2; auto with va. + all: try (destruct Int.eq eqn:E; cbn; unfold ntop2; auto with va; fail). + all: try apply vmatch_uns_undef. + + all: + generalize (Int.eq_spec i0 Int.zero); + destruct (Int.eq i0 Int.zero); + cbn; + intro. + all: try apply vmatch_uns_undef. + all: apply vmatch_uns; auto. +Qed. + + +Lemma shrx_total_sound: + forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.shrx v w)) (shrx x y). +Proof. + intros until y. intros HX HY. + inv HX; inv HY; cbn. + all: unfold ntop1; auto with va. + all: destruct Int.ltu eqn:LTU; cbn; unfold ntop; auto with va. +Qed. + + +Definition divls_total (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + || Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone + then ntop + else L (Int64.divs i1 i2) + | _, _ => ntop2 v w + end. + +Lemma divls_total_sound: + forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divls v w)) (divls_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + all: unfold ntop2; auto with va. + all: destruct (_ || _) eqn:E; unfold ntop2, ntop; cbn; auto with va. +Qed. + +Definition divlu_total (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + then ntop + else L (Int64.divu i1 i2) + | _, _ => ntop2 v w + end. + +Lemma divlu_total_sound: + forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divlu v w)) (divlu_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + all: unfold ntop2; auto with va. + all: destruct Int64.eq eqn:E; unfold ntop2, ntop; cbn; auto with va. +Qed. + + +Definition modls_total (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + || Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone + then ntop + else L (Int64.mods i1 i2) + | _, _ => ntop2 v w + end. + +Lemma modls_total_sound: + forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.modls v w)) (modls_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + all: unfold ntop2; auto with va. + all: destruct (_ || _) eqn:E; unfold ntop2, ntop; cbn; auto with va. +Qed. + + +Definition modlu_total (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + then ntop + else L (Int64.modu i1 i2) + | _, _ => ntop2 v w + end. + +Lemma modlu_total_sound: + forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.modlu v w)) (modlu_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + all: unfold ntop2; auto with va. + all: destruct Int64.eq eqn:E; cbn; unfold ntop2, ntop; auto with va. +Qed. + +Lemma shrxl_total_sound: + forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.shrxl v w)) (shrxl x y). +Proof. + intros until y. intros HX HY. + inv HX; inv HY; cbn. + all: unfold ntop1; auto with va. + all: destruct Int.ltu eqn:LTU; cbn; unfold ntop; auto with va. +Qed. + +Hint Resolve divu_total_sound divs_total_sound modu_total_sound mods_total_sound shrx_total_sound divlu_total_sound divls_total_sound modlu_total_sound modls_total_sound shrxl_total_sound : va. (** Value analysis for RISC V operators *) @@ -59,10 +353,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omul, v1::v2::nil => mul v1 v2 | Omulhs, v1::v2::nil => mulhs v1 v2 | Omulhu, v1::v2::nil => mulhu v1 v2 - | Odiv, v1::v2::nil => divs v1 v2 - | Odivu, v1::v2::nil => divu v1 v2 - | Omod, v1::v2::nil => mods v1 v2 - | Omodu, v1::v2::nil => modu v1 v2 + | Odiv, v1::v2::nil => divs_total v1 v2 + | Odivu, v1::v2::nil => divu_total v1 v2 + | Omod, v1::v2::nil => mods_total v1 v2 + | Omodu, v1::v2::nil => modu_total v1 v2 | Oand, v1::v2::nil => and v1 v2 | Oandimm n, v1::nil => and v1 (I n) | Oor, v1::v2::nil => or v1 v2 @@ -88,10 +382,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omull, v1::v2::nil => mull v1 v2 | Omullhs, v1::v2::nil => mullhs v1 v2 | Omullhu, v1::v2::nil => mullhu v1 v2 - | Odivl, v1::v2::nil => divls v1 v2 - | Odivlu, v1::v2::nil => divlu v1 v2 - | Omodl, v1::v2::nil => modls v1 v2 - | Omodlu, v1::v2::nil => modlu v1 v2 + | Odivl, v1::v2::nil => divls_total v1 v2 + | Odivlu, v1::v2::nil => divlu_total v1 v2 + | Omodl, v1::v2::nil => modls_total v1 v2 + | Omodlu, v1::v2::nil => modlu_total v1 v2 | Oandl, v1::v2::nil => andl v1 v2 | Oandlimm n, v1::nil => andl v1 (L n) | Oorl, v1::v2::nil => orl v1 v2 |