diff options
| -rw-r--r-- | arm/Machregs.v | 6 | ||||
| -rw-r--r-- | arm/PrintOp.ml | 1 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 2 | ||||
| -rw-r--r-- | backend/RTLgen.v | 21 | ||||
| -rw-r--r-- | backend/Regalloc.ml | 5 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 35 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 18 | ||||
| -rw-r--r-- | driver/Driver.ml | 9 | ||||
| -rw-r--r-- | extraction/extraction.v | 12 | ||||
| -rw-r--r-- | ia32/Asm.v | 25 | ||||
| -rw-r--r-- | ia32/Asmgen.v | 8 | ||||
| -rw-r--r-- | ia32/Asmgenproof1.v | 108 | ||||
| -rw-r--r-- | ia32/Machregs.v | 6 | ||||
| -rw-r--r-- | ia32/TargetPrinter.ml | 4 | ||||
| -rw-r--r-- | lib/Coqlib.v | 8 | ||||
| -rw-r--r-- | lib/Decidableplus.v | 77 | ||||
| -rw-r--r-- | lib/Integers.v | 92 | ||||
| -rw-r--r-- | powerpc/Machregs.v | 6 |
18 files changed, 272 insertions, 171 deletions
diff --git a/arm/Machregs.v b/arm/Machregs.v index b43f9be6..e97df790 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -58,7 +58,7 @@ Proof. Qed. Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - + Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete @@ -161,6 +161,9 @@ Definition destroyed_by_setstack (ty: typ): list mreg := nil. Definition destroyed_at_function_entry: list mreg := R12 :: nil. +Definition destroyed_at_indirect_call: list mreg := + R0 :: R1 :: R2 :: R3 :: nil. + Definition temp_for_parent_frame: mreg := R12. @@ -177,6 +180,7 @@ Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame + destroyed_at_indirect_call mregs_for_operation mregs_for_builtin. (** Two-address operations. Return [true] if the first argument and diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index 71e1dfc3..642fff80 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -120,6 +120,7 @@ let print_operation reg pp = function | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1 | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1 + | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1 | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1 | Ointuofsingle, [r1] -> fprintf pp "intuofsingle(%a)" reg r1 | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1 diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 95cae3f7..6d194369 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -382,7 +382,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end | (fr, Single, sr) :: act -> let n = fixup_incoming oc act in - if fr = sr then n else begin + if (2*fr) = sr then n else begin fprintf oc " vmov.f32 s%d, s%d\n" (2*fr) sr; 1 + n end diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 49d79fb2..11da630b 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -23,7 +23,7 @@ Require Import Registers. Require Import CminorSel. Require Import RTL. -Open Local Scope string_scope. +Local Open Scope string_scope. (** * Translation environments and state *) @@ -112,16 +112,13 @@ Implicit Arguments Error [A s]. Definition mon (A: Type) : Type := forall (s: state), res A s. -Definition ret (A: Type) (x: A) : mon A := +Definition ret {A: Type} (x: A) : mon A := fun (s: state) => OK x s (state_incr_refl s). -Implicit Arguments ret [A]. -Definition error (A: Type) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg. +Definition error {A: Type} (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg. -Implicit Arguments error [A]. - -Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B := +Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := fun (s: state) => match f s with | Error msg => Error msg @@ -132,27 +129,21 @@ Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B := end end. -Implicit Arguments bind [A B]. - -Definition bind2 (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C) : mon C := +Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C := bind f (fun xy => g (fst xy) (snd xy)). -Implicit Arguments bind2 [A B C]. - Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) (at level 200, X ident, Y ident, A at level 100, B at level 200). -Definition handle_error (A: Type) (f g: mon A) : mon A := +Definition handle_error {A: Type} (f g: mon A) : mon A := fun (s: state) => match f s with | OK a s' i => OK a s' i | Error _ => g s end. -Implicit Arguments handle_error [A]. - (** ** Operations on state *) (** The initial state (empty CFG). *) diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 0013d91a..b91bad27 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -657,9 +657,12 @@ let add_interfs_instr g instr live = | Xstore(chunk, addr, args, src) -> add_interfs_destroyed g live (destroyed_by_store chunk addr) | Xcall(sg, vos, args, res) -> + begin match vos with + | Coq_inl v -> List.iter (fun r -> IRC.add_interf g (vmreg r) v) destroyed_at_indirect_call + | _ -> () end; add_interfs_destroyed g (vset_removelist res live) destroyed_at_call | Xtailcall(sg, Coq_inl v, args) -> - List.iter (fun r -> IRC.add_interf g (vmreg r) v) int_callee_save_regs + List.iter (fun r -> IRC.add_interf g (vmreg r) v) (int_callee_save_regs @ destroyed_at_indirect_call) | Xtailcall(sg, Coq_inr id, args) -> () | Xbuiltin(ef, args, res) -> diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index bf88e033..b7329a4d 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -15,6 +15,7 @@ Require Import String. Require Import Axioms. Require Import Classical. +Require Import Decidableplus. Require Import Coqlib. Require Import Errors. Require Import Maps. @@ -473,39 +474,11 @@ Definition memcpy_args_ok /\ (sz > 0 -> (al | odst)) /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc). -Remark memcpy_check_args: - forall sz al bdst odst bsrc osrc, - {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}. -Proof with try (right; intuition omega). - intros. - assert (X: {al = 1 \/ al = 2 \/ al = 4 \/ al = 8} + {~(al = 1 \/ al = 2 \/ al = 4 \/ al = 8)}). - destruct (zeq al 1); auto. destruct (zeq al 2); auto. - destruct (zeq al 4); auto. destruct (zeq al 8); auto... - unfold memcpy_args_ok. destruct X... - assert (al > 0) by (intuition omega). - destruct (zle 0 sz)... - destruct (Zdivide_dec al sz); auto... - assert(U: forall x, {sz > 0 -> (al | x)} + {~(sz > 0 -> (al | x))}). - intros. destruct (zeq sz 0). - left; intros; omegaContradiction. - destruct (Zdivide_dec al x); auto. right; red; intros. elim n0. apply H0. omega. - destruct (U osrc); auto... - destruct (U odst); auto... - assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc} - +{~(bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc)}). - destruct (eq_block bsrc bdst); auto. - destruct (zeq osrc odst); auto. - destruct (zle (osrc + sz) odst); auto. - destruct (zle (odst + sz) osrc); auto. - right; intuition omega. - destruct Y... left; intuition omega. -Defined. - Definition do_ef_memcpy (sz al: Z) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match vargs with | Vptr bdst odst :: Vptr bsrc osrc :: nil => - if memcpy_check_args sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc) then + if decide (memcpy_args_ok sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc)) then do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz; do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes; Some(w, E0, Vundef, m') @@ -581,7 +554,7 @@ Proof with try congruence. split. econstructor; eauto. omega. constructor. (* EF_memcpy *) unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... - destruct v... destruct vargs... mydestr. red in m0. + destruct v... destruct vargs... mydestr. apply Decidable_sound in Heqb1. red in Heqb1. split. econstructor; eauto; tauto. constructor. (* EF_annot *) unfold do_ef_annot. mydestr. @@ -623,7 +596,7 @@ Proof. inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega. (* EF_memcpy *) inv H; unfold do_ef_memcpy. - inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto. + inv H0. rewrite Decidable_complete, H7, H8. auto. red. tauto. (* EF_annot *) inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index bfdd8ab9..71b67f67 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -25,7 +25,7 @@ Require Import Cop. Require Import Csyntax. Require Import Clight. -Open Local Scope string_scope. +Local Open Scope string_scope. (** State and error monad for generating fresh identifiers. *) @@ -43,17 +43,13 @@ Implicit Arguments Res [A g]. Definition mon (A: Type) := forall (g: generator), result A g. -Definition ret (A: Type) (x: A) : mon A := +Definition ret {A: Type} (x: A) : mon A := fun g => Res x g (Ple_refl (gen_next g)). -Implicit Arguments ret [A]. - -Definition error (A: Type) (msg: Errors.errmsg) : mon A := +Definition error {A: Type} (msg: Errors.errmsg) : mon A := fun g => Err msg. -Implicit Arguments error [A]. - -Definition bind (A B: Type) (x: mon A) (f: A -> mon B) : mon B := +Definition bind {A B: Type} (x: mon A) (f: A -> mon B) : mon B := fun g => match x g with | Err msg => Err msg @@ -64,13 +60,9 @@ Definition bind (A B: Type) (x: mon A) (f: A -> mon B) : mon B := end end. -Implicit Arguments bind [A B]. - -Definition bind2 (A B C: Type) (x: mon (A * B)) (f: A -> B -> mon C) : mon C := +Definition bind2 {A B C: Type} (x: mon (A * B)) (f: A -> B -> mon C) : mon C := bind x (fun p => f (fst p) (snd p)). -Implicit Arguments bind2 [A B C]. - Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200) : gensym_monad_scope. diff --git a/driver/Driver.ml b/driver/Driver.ml index 8b0cd7ac..b89d93c1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -23,6 +23,7 @@ let dump_options = ref false (* Optional sdump suffix *) let sdump_suffix = ref ".json" +let sdump_folder = ref "" (* Dump Asm code in asm format for the validator *) @@ -59,8 +60,11 @@ let compile_c_ast sourcename csyntax ofile = eprintf "%s: %a" sourcename print_error msg; exit 2 in (* Dump Asm in binary and JSON format *) - if !option_sdump then - dump_jasm asm sourcename (output_filename sourcename ".c" !sdump_suffix); + if !option_sdump then begin + let sf = output_filename sourcename ".c" !sdump_suffix in + let csf = Filename.concat !sdump_folder sf in + dump_jasm asm sourcename csf + end; (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm; @@ -457,6 +461,7 @@ let cmdline_actions = dump_options:=true); Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); + Exact "-sdump-folder", String (fun s -> sdump_folder := s); Exact "-doptions", Set dump_options; (* General options *) Exact "-v", Set option_v; diff --git a/extraction/extraction.v b/extraction/extraction.v index e7f2e2fc..8e13264c 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -12,6 +12,7 @@ Require Coqlib. Require Wfsimpl. +Require DecidableClass Decidableplus. Require AST. Require Iteration. Require Floats. @@ -39,6 +40,12 @@ Require Import ExtrOcamlString. (* Coqlib *) Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". +(* Decidable *) + +Extraction Inline DecidableClass.Decidable_witness DecidableClass.decide + Decidableplus.Decidable_and Decidableplus.Decidable_or + Decidableplus.Decidable_not Decidableplus.Decidable_implies. + (* Wfsimpl *) Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. @@ -159,12 +166,13 @@ Separate Extraction Ctyping.typecheck_program Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr Ctypes.make_program - Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs - Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs + Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs + Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs Conventions1.dummy_int_reg Conventions1.dummy_float_reg RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg + Machregs.destroyed_at_indirect_call AST.signature_main Floats.Float32.from_parsed Floats.Float.from_parsed Globalenvs.Senv.invert_symbol @@ -151,6 +151,7 @@ Inductive instruction: Type := | Pimul_ri (rd: ireg) (n: int) | Pimul_r (r1: ireg) | Pmul_r (r1: ireg) + | Pcltd | Pdiv (r1: ireg) | Pidiv (r1: ireg) | Pand_rr (rd: ireg) (r1: ireg) @@ -618,17 +619,25 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmul_r r1 => Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1) #EDX <- (Val.mulhu rs#EAX rs#r1))) m + | Pcltd => + Next (nextinstr_nf (rs#EDX <- (Val.shr rs#EAX (Vint (Int.repr 31))))) m | Pdiv r1 => - let vn := rs#EAX in let vd := (rs#EDX <- Vundef)#r1 in - match Val.divu vn vd, Val.modu vn vd with - | Some vq, Some vr => Next (nextinstr_nf (rs#EAX <- vq #EDX <- vr)) m - | _, _ => Stuck + match rs#EDX, rs#EAX, rs#r1 with + | Vint nh, Vint nl, Vint d => + match Int.divmodu2 nh nl d with + | Some(q, r) => Next (nextinstr_nf (rs#EAX <- (Vint q) #EDX <- (Vint r))) m + | None => Stuck + end + | _, _, _ => Stuck end | Pidiv r1 => - let vn := rs#EAX in let vd := (rs#EDX <- Vundef)#r1 in - match Val.divs vn vd, Val.mods vn vd with - | Some vq, Some vr => Next (nextinstr_nf (rs#EAX <- vq #EDX <- vr)) m - | _, _ => Stuck + match rs#EDX, rs#EAX, rs#r1 with + | Vint nh, Vint nl, Vint d => + match Int.divmods2 nh nl d with + | Some(q, r) => Next (nextinstr_nf (rs#EAX <- (Vint q) #EDX <- (Vint r))) m + | None => Stuck + end + | _, _, _ => Stuck end | Pand_rr rd r1 => Next (nextinstr_nf (rs#rd <- (Val.and rs#rd rs#r1))) m diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index fd0d5bc5..1d718c26 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -315,22 +315,22 @@ Definition transl_op assertion (mreg_eq a1 AX); assertion (mreg_eq a2 CX); assertion (mreg_eq res AX); - OK(Pidiv ECX :: k) + OK(Pcltd :: Pidiv ECX :: k) | Odivu, a1 :: a2 :: nil => assertion (mreg_eq a1 AX); assertion (mreg_eq a2 CX); assertion (mreg_eq res AX); - OK(Pdiv ECX :: k) + OK(Pxor_r EDX :: Pdiv ECX :: k) | Omod, a1 :: a2 :: nil => assertion (mreg_eq a1 AX); assertion (mreg_eq a2 CX); assertion (mreg_eq res DX); - OK(Pidiv ECX :: k) + OK(Pcltd :: Pidiv ECX :: k) | Omodu, a1 :: a2 :: nil => assertion (mreg_eq a1 AX); assertion (mreg_eq a2 CX); assertion (mreg_eq res DX); - OK(Pdiv ECX :: k) + OK(Pxor_r EDX :: Pdiv ECX :: k) | Oand, a1 :: a2 :: nil => assertion (mreg_eq a1 res); do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pand_rr r r2 :: k) diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 60cc266e..9703d419 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -121,28 +121,44 @@ Qed. (** Properties of division *) -Remark divs_mods_exist: +Lemma divu_modu_exists: forall v1 v2, - match Val.divs v1 v2, Val.mods v1 v2 with - | Some _, Some _ => True - | None, None => True - | _, _ => False - end. + Val.divu v1 v2 <> None \/ Val.modu v1 v2 <> None -> + exists n d q r, + v1 = Vint n /\ v2 = Vint d + /\ Int.divmodu2 Int.zero n d = Some(q, r) + /\ Val.divu v1 v2 = Some (Vint q) /\ Val.modu v1 v2 = Some (Vint r). Proof. - intros. unfold Val.divs, Val.mods. destruct v1; auto. destruct v2; auto. - destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); auto. + intros v1 v2; unfold Val.divu, Val.modu. + destruct v1; try (intuition discriminate). + destruct v2; try (intuition discriminate). + predSpec Int.eq Int.eq_spec i0 Int.zero ; try (intuition discriminate). + intros _. exists i, i0, (Int.divu i i0), (Int.modu i i0); intuition auto. + apply Int.divmodu2_divu_modu; auto. Qed. -Remark divu_modu_exist: +Lemma divs_mods_exists: forall v1 v2, - match Val.divu v1 v2, Val.modu v1 v2 with - | Some _, Some _ => True - | None, None => True - | _, _ => False - end. + Val.divs v1 v2 <> None \/ Val.mods v1 v2 <> None -> + exists nh nl d q r, + Val.shr v1 (Vint (Int.repr 31)) = Vint nh /\ v1 = Vint nl /\ v2 = Vint d + /\ Int.divmods2 nh nl d = Some(q, r) + /\ Val.divs v1 v2 = Some (Vint q) /\ Val.mods v1 v2 = Some (Vint r). Proof. - intros. unfold Val.divu, Val.modu. destruct v1; auto. destruct v2; auto. - destruct (Int.eq i0 Int.zero); auto. + intros v1 v2; unfold Val.divs, Val.mods. + destruct v1; try (intuition discriminate). + destruct v2; try (intuition discriminate). + destruct (Int.eq i0 Int.zero + || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:OK; + try (intuition discriminate). + intros _. + InvBooleans. + exists (Int.shr i (Int.repr 31)), i, i0, (Int.divs i i0), (Int.mods i i0); intuition auto. + rewrite Int.shr_lt_zero. apply Int.divmods2_divs_mods. + red; intros; subst i0; rewrite Int.eq_true in H; discriminate. + revert H0. predSpec Int.eq Int.eq_spec i (Int.repr Int.min_signed); auto. + predSpec Int.eq Int.eq_spec i0 Int.mone; auto. + discriminate. Qed. (** Smart constructor for [shrx] *) @@ -1031,32 +1047,52 @@ Transparent destroyed_by_op. apply SAME. TranslOp. destruct H1. Simplifs. (* div *) apply SAME. - specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. - destruct (Val.mods (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. - TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. - auto. auto. - simpl in H3. destruct H3; Simplifs. + exploit (divs_mods_exists (rs EAX) (rs ECX)). left; congruence. + intros (nh & nl & d & q & r & A & B & C & D & E & F). + set (rs1 := nextinstr_nf (rs#EDX <- (Vint nh))). + econstructor; split. + eapply exec_straight_two with (rs2 := rs1). simpl. rewrite A. reflexivity. + simpl. change (rs1 EAX) with (rs EAX); rewrite B. + change (rs1 ECX) with (rs ECX); rewrite C. + rewrite D. reflexivity. auto. auto. + split. change (Vint q = v). congruence. + simpl; intros. destruct H2. unfold rs1; Simplifs. (* divu *) apply SAME. - specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0. - destruct (Val.modu (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. - TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. - auto. auto. - simpl in H3. destruct H3; Simplifs. + exploit (divu_modu_exists (rs EAX) (rs ECX)). left; congruence. + intros (n & d & q & r & B & C & D & E & F). + set (rs1 := nextinstr_nf (rs#EDX <- Vzero)). + econstructor; split. + eapply exec_straight_two with (rs2 := rs1). reflexivity. + simpl. change (rs1 EAX) with (rs EAX); rewrite B. + change (rs1 ECX) with (rs ECX); rewrite C. + rewrite D. reflexivity. auto. auto. + split. change (Vint q = v). congruence. + simpl; intros. destruct H2. unfold rs1; Simplifs. (* mod *) apply SAME. - specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. - destruct (Val.divs (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. - TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. - auto. auto. - simpl in H3. destruct H3; Simplifs. + exploit (divs_mods_exists (rs EAX) (rs ECX)). right; congruence. + intros (nh & nl & d & q & r & A & B & C & D & E & F). + set (rs1 := nextinstr_nf (rs#EDX <- (Vint nh))). + econstructor; split. + eapply exec_straight_two with (rs2 := rs1). simpl. rewrite A. reflexivity. + simpl. change (rs1 EAX) with (rs EAX); rewrite B. + change (rs1 ECX) with (rs ECX); rewrite C. + rewrite D. reflexivity. auto. auto. + split. change (Vint r = v). congruence. + simpl; intros. destruct H2. unfold rs1; Simplifs. (* modu *) apply SAME. - specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0. - destruct (Val.divu (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. - TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. - auto. auto. - simpl in H3. destruct H3; Simplifs. + exploit (divu_modu_exists (rs EAX) (rs ECX)). right; congruence. + intros (n & d & q & r & B & C & D & E & F). + set (rs1 := nextinstr_nf (rs#EDX <- Vzero)). + econstructor; split. + eapply exec_straight_two with (rs2 := rs1). reflexivity. + simpl. change (rs1 EAX) with (rs EAX); rewrite B. + change (rs1 ECX) with (rs ECX); rewrite C. + rewrite D. reflexivity. auto. auto. + split. change (Vint r = v). congruence. + simpl; intros. destruct H2. unfold rs1; Simplifs. (* shrximm *) apply SAME. eapply mk_shrximm_correct; eauto. (* lea *) diff --git a/ia32/Machregs.v b/ia32/Machregs.v index fb80a1fd..3a6ae674 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -55,7 +55,7 @@ Proof. Qed. Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - + Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete @@ -166,6 +166,9 @@ Definition destroyed_at_function_entry: list mreg := (* must include [destroyed_by_setstack ty] *) DX :: FP0 :: nil. +Definition destroyed_at_indirect_call: list mreg := + nil. + Definition destroyed_by_setstack (ty: typ): list mreg := match ty with | Tfloat | Tsingle => FP0 :: nil @@ -210,6 +213,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin + destroyed_at_indirect_call destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame mregs_for_operation mregs_for_builtin. diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 979ac800..4ffb701b 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -421,11 +421,11 @@ module Target(System: SYSTEM):TARGET = fprintf oc " imull %a\n" ireg r1 | Pmul_r(r1) -> fprintf oc " mull %a\n" ireg r1 + | Pcltd -> + fprintf oc " cltd\n" | Pdiv(r1) -> - fprintf oc " xorl %%edx, %%edx\n"; fprintf oc " divl %a\n" ireg r1 | Pidiv(r1) -> - fprintf oc " cltd\n"; fprintf oc " idivl %a\n" ireg r1 | Pand_rr(rd, r1) -> fprintf oc " andl %a, %a\n" ireg r1 ireg rd diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 6fa82492..18d4d7e1 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1200,7 +1200,7 @@ Proof. subst; exists b1; auto. exploit IHlist_forall2; eauto. intros (x2 & U & V); exists x2; auto. Qed. - + Lemma list_forall2_in_right: forall x2 l1 l2, list_forall2 l1 l2 -> In x2 l2 -> exists x1, In x1 l1 /\ P x1 x2. @@ -1209,7 +1209,7 @@ Proof. subst; exists a1; auto. exploit IHlist_forall2; eauto. intros (x1 & U & V); exists x1; auto. Qed. - + End FORALL2. Lemma list_forall2_imply: @@ -1277,11 +1277,9 @@ Qed. (** * Definitions and theorems over boolean types *) -Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool := +Definition proj_sumbool {P Q: Prop} (a: {P} + {Q}) : bool := if a then true else false. -Implicit Arguments proj_sumbool [P Q]. - Coercion proj_sumbool: sumbool >-> bool. Lemma proj_sumbool_true: diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 932b885a..3bb6eee7 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -19,56 +19,9 @@ of Coq 8.5 with more instances of decidable properties, including universal and existential quantification over finite types. *) -(** Temporarily and for compatibility with Coq 8.4, this file includes - a copy of the relevant definitions from the Coq 8.5 [DecidableClass] - library. This library is copyright INRIA. *) - +Require Export DecidableClass. Require Import Coqlib. -Class Decidable (P : Prop) := { - Decidable_witness : bool; - Decidable_spec : Decidable_witness = true <-> P -}. - -Lemma Decidable_sound : forall P (H : Decidable P), - Decidable_witness = true -> P. -Proof. - intros. rewrite <- Decidable_spec. auto. -Qed. - -Lemma Decidable_complete : forall P (H : Decidable P), - P -> Decidable_witness = true. -Proof. - intros. rewrite Decidable_spec. auto. -Qed. - -Lemma Decidable_sound_alt : forall P (H : Decidable P), - ~ P -> Decidable_witness = false. -Proof. - intros. destruct Decidable_witness eqn:E; auto. elim H0. eapply Decidable_sound; eauto. -Qed. - -Lemma Decidable_complete_alt : forall P (H : Decidable P), - Decidable_witness = false -> ~ P. -Proof. - intros; red; intros. rewrite (Decidable_complete P H) in H0 by auto. discriminate. -Qed. - -Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H). - -Ltac _decide_ P H := - let b := fresh "b" in - set (b := decide P) in *; - assert (H : decide P = b) by reflexivity; - clearbody b; - destruct b; [apply Decidable_sound in H|apply Decidable_complete_alt in H]. - -Tactic Notation "decide" constr(P) "as" ident(H) := - _decide_ P H. - -Tactic Notation "decide" constr(P) := - let H := fresh "H" in _decide_ P H. - Ltac decide_goal := eapply Decidable_sound; reflexivity. (** Deciding logical connectives *) @@ -169,6 +122,34 @@ Next Obligation. apply Z.ltb_lt. Qed. +Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := { + Decidable_witness := Z.geb x y +}. +Next Obligation. + rewrite Z.geb_le. intuition omega. +Qed. + +Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := { + Decidable_witness := Z.gtb x y +}. +Next Obligation. + rewrite Z.gtb_lt. intuition omega. +Qed. + +Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := { + Decidable_witness := Z.eqb y ((y / x) * x)%Z +}. +Next Obligation. + split. + intros. apply Z.eqb_eq in H. exists (y / x). auto. + intros [k EQ]. apply Z.eqb_eq. + destruct (Z.eq_dec x 0). + subst x. rewrite Z.mul_0_r in EQ. subst y. reflexivity. + assert (k = y / x). + { apply Zdiv_unique_full with 0. red; omega. rewrite EQ; ring. } + congruence. +Qed. + (** Deciding properties over lists *) Program Instance Decidable_forall_in_list : diff --git a/lib/Integers.v b/lib/Integers.v index 316dfb52..16c95e01 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -403,6 +403,18 @@ Definition is_false (x: int) : Prop := x = zero. Definition is_true (x: int) : Prop := x <> zero. Definition notbool (x: int) : int := if eq x zero then one else zero. +(** x86-style extended division and modulus *) + +Definition divmodu2 (nhi nlo: int) (d: int) : option (int * int) := + if eq_dec d zero then None else + (let (q, r) := Z.div_eucl (unsigned nhi * modulus + unsigned nlo) (unsigned d) in + if zle q max_unsigned then Some(repr q, repr r) else None). + +Definition divmods2 (nhi nlo: int) (d: int) : option (int * int) := + if eq_dec d zero then None else + (let (q, r) := Z.quotrem (signed nhi * modulus + unsigned nlo) (signed d) in + if zle min_signed q && zle q max_signed then Some(repr q, repr r) else None). + (** * Properties of integers and integer arithmetic *) (** ** Properties of [modulus], [max_unsigned], etc. *) @@ -1193,6 +1205,86 @@ Proof. rewrite <- neg_mul_distr_l. rewrite mul_mone. rewrite neg_involutive. apply sub_idem. Qed. +Theorem divmodu2_divu_modu: + forall n d, + d <> zero -> divmodu2 zero n d = Some (divu n d, modu n d). +Proof. + unfold divmodu2, divu, modu; intros. + rewrite dec_eq_false by auto. + set (N := unsigned zero * modulus + unsigned n). + assert (E1: unsigned n = N) by (unfold N; rewrite unsigned_zero; ring). rewrite ! E1. + set (D := unsigned d). + set (Q := N / D); set (R := N mod D). + assert (E2: Z.div_eucl N D = (Q, R)). + { unfold Q, R, Z.div, Z.modulo. destruct (Z.div_eucl N D); auto. } + rewrite E2. rewrite zle_true. auto. + assert (unsigned d <> 0). + { red; intros. elim H. rewrite <- (repr_unsigned d). rewrite H0; auto. } + assert (0 < D). + { unfold D. generalize (unsigned_range d); intros. omega. } + assert (0 <= Q <= max_unsigned). + { unfold Q. apply Zdiv_interval_2. + rewrite <- E1; apply unsigned_range_2. + omega. unfold max_unsigned; generalize modulus_pos; omega. omega. } + omega. +Qed. + +Lemma unsigned_signed: + forall n, unsigned n = if lt n zero then signed n + modulus else signed n. +Proof. + intros. unfold lt. rewrite signed_zero. unfold signed. + generalize (unsigned_range n). rewrite half_modulus_modulus. intros. + destruct (zlt (unsigned n) half_modulus). +- rewrite zlt_false by omega. auto. +- rewrite zlt_true by omega. ring. +Qed. + +Theorem divmods2_divs_mods: + forall n d, + d <> zero -> n <> repr min_signed \/ d <> mone -> + divmods2 (if lt n zero then mone else zero) n d = Some (divs n d, mods n d). +Proof. + unfold divmods2, divs, mods; intros. + rewrite dec_eq_false by auto. + set (N := signed (if lt n zero then mone else zero) * modulus + unsigned n). + set (D := signed d). + assert (D <> 0). + { unfold D; red; intros. elim H. rewrite <- (repr_signed d). rewrite H1; auto. } + assert (N = signed n). + { unfold N. rewrite unsigned_signed. destruct (lt n zero). + rewrite signed_mone. ring. + rewrite signed_zero. ring. } + set (Q := Z.quot N D); set (R := Z.rem N D). + assert (E2: Z.quotrem N D = (Q, R)). + { unfold Q, R, Z.quot, Z.rem. destruct (Z.quotrem N D); auto. } + rewrite E2. + assert (min_signed <= N <= max_signed) by (rewrite H2; apply signed_range). + assert (min_signed <= Q <= max_signed). + { unfold Q. destruct (zeq D 1); [ | destruct (zeq D (-1))]. + - (* D = 1 *) + rewrite e. rewrite Z.quot_1_r; auto. + - (* D = -1 *) + rewrite e. change (-1) with (Z.opp 1). rewrite Z.quot_opp_r by omega. + rewrite Z.quot_1_r. + assert (N <> min_signed). + { red; intros; destruct H0. + + elim H0. rewrite <- (repr_signed n). rewrite <- H2. rewrite H4. auto. + + elim H0. rewrite <- (repr_signed d). unfold D in e; rewrite e; auto. } + unfold min_signed, max_signed in *. omega. + - (* |D| > 1 *) + assert (Z.abs (Z.quot N D) < half_modulus). + { rewrite <- Z.quot_abs by omega. apply Zquot_lt_upper_bound. + xomega. xomega. + apply Zle_lt_trans with (half_modulus * 1). + rewrite Z.mul_1_r. unfold min_signed, max_signed in H3; xomega. + apply Zmult_lt_compat_l. generalize half_modulus_pos; omega. xomega. } + rewrite Z.abs_lt in H4. + unfold min_signed, max_signed; omega. + } + unfold proj_sumbool; rewrite ! zle_true by omega; simpl. + unfold Q, R; rewrite H2; auto. +Qed. + (** ** Bit-level properties *) (** ** Properties of bit-level operations over [Z] *) diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 24065254..ce9c3542 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -76,7 +76,7 @@ Proof. Qed. Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - + Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete @@ -210,6 +210,9 @@ Definition destroyed_by_setstack (ty: typ): list mreg := Definition destroyed_at_function_entry: list mreg := nil. +Definition destroyed_at_indirect_call: list mreg := + nil. + Definition temp_for_parent_frame: mreg := R11. @@ -230,6 +233,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin + destroyed_at_indirect_call destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame mregs_for_operation mregs_for_builtin. |