diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | arm/Op.v | 3 | ||||
| -rw-r--r-- | backend/CSE.v | 10 | ||||
| -rw-r--r-- | backend/Coloringaux.ml | 5 | ||||
| -rw-r--r-- | backend/Coloringproof.v | 2 | ||||
| -rw-r--r-- | backend/InterfGraph.v | 4 | ||||
| -rw-r--r-- | common/Memory.v | 12 | ||||
| -rw-r--r-- | extraction/Kildall.ml.patch | 21 | ||||
| -rw-r--r-- | extraction/extraction.v | 15 | ||||
| -rwxr-xr-x | extraction/fixextract | 4 | ||||
| -rw-r--r-- | lib/Intv.v | 5 | ||||
| -rw-r--r-- | lib/Lattice.v | 18 | ||||
| -rw-r--r-- | lib/Parmov.v | 2 | ||||
| -rw-r--r-- | lib/UnionFind.v | 14 | ||||
| -rwxr-xr-x | pg | 23 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 10 | ||||
| -rw-r--r-- | test/c/Makefile | 4 | ||||
| -rw-r--r-- | test/raytracer/Makefile | 2 |
18 files changed, 70 insertions, 85 deletions
@@ -95,7 +95,6 @@ proof: $(FILES:.v=.vo) extraction: rm -f extraction/*.ml extraction/*.mli $(COQEXEC) extraction/extraction.v - cd extraction && ./fixextract ccomp: driver/Configuration.ml $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \ @@ -128,6 +128,7 @@ Inductive addressing: Type := Definition eq_shift (x y: shift): {x=y} + {x<>y}. Proof. + revert x y. generalize Int.eq_dec; intro. assert (forall (x y: shift_amount), {x=y}+{x<>y}). destruct x as [x Px]. destruct y as [y Py]. destruct (H x y). @@ -846,7 +847,7 @@ Definition is_shift_amount_aux (n: int) : { Int.ltu n Int.iwordsize = true } + { Int.ltu n Int.iwordsize = false }. Proof. - intro. case (Int.ltu n Int.iwordsize). left; auto. right; auto. + case (Int.ltu n Int.iwordsize). left; auto. right; auto. Defined. Definition is_shift_amount (n: int) : option shift_amount := diff --git a/backend/CSE.v b/backend/CSE.v index 4347c33..45b50d6 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -57,15 +57,7 @@ Definition eq_valnum: forall (x y: valnum), {x=y}+{x<>y} := peq. Definition eq_list_valnum (x y: list valnum) : {x=y}+{x<>y}. Proof. - induction x; intros; case y; intros. - left; auto. - right; congruence. - right; congruence. - case (eq_valnum a v); intros. - case (IHx l); intros. - left; congruence. - right; congruence. - right; congruence. + decide equality. apply eq_valnum. Qed. Definition eq_rhs (x y: rhs) : {x=y}+{x<>y}. diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml index 0420972..02081d5 100644 --- a/backend/Coloringaux.ml +++ b/backend/Coloringaux.ml @@ -169,13 +169,12 @@ end module IntSet = Set.Make(struct type t = int - let compare x y = - if x < y then -1 else if x > y then 1 else 0 + let compare (x:int) (y:int) = compare x y end) module IntPairSet = Set.Make(struct type t = int * int - let compare (x1, y1) (x2, y2) = + let compare ((x1, y1): (int * int)) (x2, y2) = if x1 < x2 then -1 else if x1 > x2 then 1 else if y1 < y2 then -1 else diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index bb97c87..ca0637a 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -658,7 +658,7 @@ Lemma check_coloring_3_correct: Proof. unfold check_coloring_3; intros. exploit Regset.for_all_2; eauto. - red; intros. hnf in H1. congruence. + red; intros. congruence. apply Regset.mem_2. eauto. simpl. intro. elim (andb_prop _ _ H1); intros. split. apply loc_is_acceptable_correct; auto. diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index a73e7d7..ec64e99 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -243,7 +243,7 @@ Proof. apply Regset.add_2; apply Regset.add_2; tauto. intros. rewrite SetRegReg.fold_1. apply H. - intuition. left. apply SetRegReg.elements_1. auto. + intuition. Qed. Lemma in_setregreg_fold': @@ -276,7 +276,7 @@ Proof. apply Regset.add_2; auto. intros. rewrite SetRegMreg.fold_1. apply H with mr2. - intuition. left. apply SetRegMreg.elements_1. auto. + intuition. Qed. Lemma all_interf_regs_correct_1: diff --git a/common/Memory.v b/common/Memory.v index 6de00e7..a6594e4 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -62,7 +62,7 @@ Definition perm_order' (po: option permission) (p: permission) := | None => False end. -Record mem_ : Type := mkmem { +Record mem' : Type := mkmem { mem_contents: block -> Z -> memval; mem_access: block -> Z -> option permission; bounds: block -> Z * Z; @@ -73,7 +73,7 @@ Record mem_ : Type := mkmem { noread_undef: forall b ofs, perm_order' (mem_access b ofs) Readable \/ mem_contents b ofs = Undef }. -Definition mem := mem_. +Definition mem := mem'. Lemma mkmem_ext: forall cont1 cont2 acc1 acc2 bound1 bound2 next1 next2 @@ -2397,7 +2397,7 @@ Qed. the [Vundef] values stored in [m1] by more defined values stored in [m2] at the same locations. *) -Record extends_ (m1 m2: mem) : Prop := +Record extends' (m1 m2: mem) : Prop := mk_extends { mext_next: nextblock m1 = nextblock m2; mext_inj: mem_inj inject_id m1 m2 @@ -2406,7 +2406,7 @@ Record extends_ (m1 m2: mem) : Prop := *) }. -Definition extends := extends_. +Definition extends := extends'. Theorem extends_refl: forall m, extends m m. @@ -2645,7 +2645,7 @@ Qed. - the offsets [delta] are representable with signed machine integers. *) -Record inject_ (f: meminj) (m1 m2: mem) : Prop := +Record inject' (f: meminj) (m1 m2: mem) : Prop := mk_inject { mi_inj: mem_inj f m1 m2; @@ -2666,7 +2666,7 @@ Record inject_ (f: meminj) (m1 m2: mem) : Prop := (Int.min_signed <= low_bound m2 b' /\ high_bound m2 b' <= Int.max_signed) }. -Definition inject := inject_. +Definition inject := inject'. Hint Local Resolve mi_mappedblocks mi_range_offset: mem. diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch deleted file mode 100644 index 6c94854..0000000 --- a/extraction/Kildall.ml.patch +++ /dev/null @@ -1,21 +0,0 @@ -*** kildall.ml.orig 2009-08-16 15:45:21.000000000 +0200 ---- kildall.ml 2009-08-16 15:45:27.000000000 +0200 -*************** -*** 252,259 **** - - (** val basic_block_map : positive list PTree.t -> positive -> bbmap **) - -! let basic_block_map successors entrypoint x = -! is_basic_block_head entrypoint (make_predecessors successors) x - - (** val basic_block_list : - positive list PTree.t -> bbmap -> positive list **) ---- 252,259 ---- - - (** val basic_block_map : positive list PTree.t -> positive -> bbmap **) - -! let basic_block_map successors entrypoint = -! is_basic_block_head entrypoint (make_predecessors successors) - - (** val basic_block_list : - positive list PTree.t -> bbmap -> positive list **) diff --git a/extraction/extraction.v b/extraction/extraction.v index 8e3c1aa..1c14298 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -23,7 +23,7 @@ Extract Inductive unit => "unit" [ "()" ]. Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. Extract Inductive option => "option" [ "Some" "None" ]. -Extract Inductive List.list => "list" [ "[]" "(::)" ]. +Extract Inductive list => "list" [ "[]" "(::)" ]. (* Float *) Extract Inlined Constant Floats.float => "float". @@ -52,6 +52,9 @@ Extract Constant Memdata.big_endian => "Memdataaux.big_endian". (* Memory - work around an extraction bug. *) Extraction NoInline Memory.Mem.valid_pointer. +(* Errors *) +Extraction Inline Errors.bind Errors.bind2. + (* Iteration *) Extract Constant Iteration.dependent_description' => "fun x -> assert false". @@ -64,6 +67,7 @@ Extract Constant Iteration.GenIter.iterate => (* RTLgen *) Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch". Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". +Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2. (* RTLtyping *) Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_environment". @@ -74,6 +78,9 @@ Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring". (* Linearize *) Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". +(* SimplExpr *) +Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2. + (* Compiler *) Extract Constant Compiler.print_Csyntax => "PrintCsyntax.print_if". Extract Constant Compiler.print_Clight => "PrintClight.print_if". @@ -85,12 +92,6 @@ Extract Constant Compiler.print_RTL_constprop => "PrintRTL.print_constprop". Extract Constant Compiler.print_RTL_cse => "PrintRTL.print_cse". Extract Constant Compiler.print_LTLin => "PrintLTLin.print_if". -(* Suppression of stupidly big equality functions *) -Extract Constant Op.eq_operation => "fun (x: operation) (y: operation) -> x = y". -Extract Constant Op.eq_addressing => "fun (x: addressing) (y: addressing) -> x = y". -(*Extract Constant CSE.eq_rhs => "fun (x: rhs) (y: rhs) -> x = y".*) -Extract Constant Machregs.mreg_eq => "fun (x: mreg) (y: mreg) -> x = y". - (* Processor-specific extraction directives *) Load extractionMachdep. diff --git a/extraction/fixextract b/extraction/fixextract deleted file mode 100755 index 86ebdbd..0000000 --- a/extraction/fixextract +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/sh - -echo "Patching files..." -for i in *.patch; do patch < $i; done @@ -248,16 +248,13 @@ Next Obligation. destruct H2. congruence. auto. Qed. Next Obligation. - elim wildcard'0. intros y [A B]. exists y; split; auto. omega. + exists wildcard'0; split; auto. omega. Qed. Next Obligation. exists (hi - 1); split; auto. omega. Qed. Next Obligation. omegaContradiction. -Qed. -Next Obligation. - apply Zwf_well_founded. Defined. End FORALL. diff --git a/lib/Lattice.v b/lib/Lattice.v index c200fc8..51a7976 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -64,11 +64,11 @@ Set Implicit Arguments. Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP. -Inductive t_ : Type := - | Bot_except: PTree.t L.t -> t_ - | Top_except: PTree.t L.t -> t_. +Inductive t' : Type := + | Bot_except: PTree.t L.t -> t' + | Top_except: PTree.t L.t -> t'. -Definition t: Type := t_. +Definition t: Type := t'. Definition get (p: positive) (x: t) : L.t := match x with @@ -611,12 +611,12 @@ End LFSet. Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP. -Inductive t_ : Type := - | Bot: t_ - | Inj: X.t -> t_ - | Top: t_. +Inductive t' : Type := + | Bot: t' + | Inj: X.t -> t' + | Top: t'. -Definition t : Type := t_. +Definition t : Type := t'. Definition eq (x y: t) := (x = y). Definition eq_refl: forall x, eq x x := (@refl_equal t). diff --git a/lib/Parmov.v b/lib/Parmov.v index 493b0bd..fb04310 100644 --- a/lib/Parmov.v +++ b/lib/Parmov.v @@ -1017,7 +1017,7 @@ Lemma split_move_charact: Proof. unfold no_read. intros m r. functional induction (split_move m r). red; simpl. tauto. - rewrite _x. split. reflexivity. simpl;auto. + split. reflexivity. simpl; auto. rewrite e1 in IHo. simpl. intuition. rewrite e1 in IHo. destruct IHo. split. rewrite H. reflexivity. simpl. intuition. diff --git a/lib/UnionFind.v b/lib/UnionFind.v index d74a20a..553d905 100644 --- a/lib/UnionFind.v +++ b/lib/UnionFind.v @@ -635,26 +635,22 @@ Next Obligation. red. auto. Qed. Next Obligation. - destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a' - (find_x_obligation_1 a find_x a' Heq_anonymous))) + (* a <> b*) + destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. apply repr_some_diff. auto. Qed. Next Obligation. - destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a' - (find_x_obligation_1 a find_x a' Heq_anonymous))) - as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. + destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. rewrite B. apply repr_some. auto. Qed. Next Obligation. split. - destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a' - (find_x_obligation_1 a find_x a' Heq_anonymous))) + destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. symmetry. apply repr_some. auto. intros. rewrite repr_compress. - destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a' - (find_x_obligation_1 a find_x a' Heq_anonymous))) + destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. auto. Qed. Next Obligation. @@ -0,0 +1,23 @@ +#!/bin/sh +# Start Proof General with the right -I options +# Use the Makefile to rebuild dependencies if needed +# Recompile the modified file after coqide editing + +PWD=`pwd` +ARCH=$PWD/`sed -n -e 's/^ARCH=//p' Makefile.config` +VARIANT=$ARCH/`sed -n -e 's/^VARIANT=//p' Makefile.config` + + +make -q ${1}o || { + make -n ${1}o | grep -v "\\b${1}\\b" | \ + (while read cmd; do + $cmd || exit 2 + done) +} +COQPROGNAME="coqtop" +COQPROGARGS="\"-I\" \"$PWD/lib\" \"-I\" \"$PWD/common\" \"-I\" \"$VARIANT\" \"-I\" \"$ARCH\" \"-I\" \"$PWD/backend\" \"-I\" \"$PWD/cfrontend\"" + + +emacs --eval "(setq coq-prog-name \"$COQPROGNAME\")" \ + --eval "(setq coq-prog-args '($COQPROGARGS))" $1 \ +&& make ${1}o diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 65c831e..54e454e 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -776,16 +776,16 @@ Proof. unfold rs1. rewrite nextinstr_inv; auto with ppcgen. auto. congruence. intros [rs2 [U [V W]]]. exists rs2; split. - apply exec_straight_step with rs1 m'. + apply exec_straight_step with rs1 m'. simpl. unfold load1. simpl. rewrite gpr_or_zero_not_zero. rewrite <- (sp_val _ _ _ AG). rewrite A. auto. congruence. auto. auto. assert (agree (Regmap.set IT1 Vundef ms) sp rs1). - unfold rs1. eauto with ppcgen. + unfold rs1. change (IR GPR11) with (preg_of IT1). auto with ppcgen. apply agree_exten_2 with (rs1#(preg_of dst) <- v'). - auto with ppcgen. - intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of dst)). - congruence. auto. + auto with ppcgen. + intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of dst)). + congruence. auto. Qed. Lemma exec_Mop_prop: diff --git a/test/c/Makefile b/test/c/Makefile index 7b6d63c..ed70d18 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -30,7 +30,7 @@ all_gcc: $(PROGS:%=%.gcc) %.gcc: %.c $(CC) $(CFLAGS) -o $*.gcc $*.c $(LIBS) -test_compcert: +test: @for i in $(PROGS); do \ if ./$$i.compcert | cmp -s - Results/$$i; \ then echo "$$i: passed"; \ @@ -51,7 +51,7 @@ time_gcc: echo -n "$$i: "; $(TIME) ./$$i.gcc; \ done -time_compcert: +time: @for i in $(PROGS); do \ echo -n "$$i: "; $(TIME) ./$$i.compcert; \ done diff --git a/test/raytracer/Makefile b/test/raytracer/Makefile index 8ba9ede..66dcb0a 100644 --- a/test/raytracer/Makefile +++ b/test/raytracer/Makefile @@ -9,6 +9,8 @@ OBJS=memory.o gmllexer.o gmlparser.o eval.o \ arrays.o vector.o matrix.o object.o intersect.o surface.o light.o \ simplify.o render.o main.o +all: render + render: $(OBJS) $(CC) $(CFLAGS) -o render $(OBJS) $(LIBS) |