Commit 3ffda353 authored by xleroy's avatar xleroy
Browse files

Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 06c55ab8
......@@ -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 :=
......
......@@ -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}.
......
......@@ -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
......
......@@ -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.
......
......@@ -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:
......
......@@ -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.
......
*** 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 **)
......@@ -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.
......
#!/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.
......
......@@ -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).
......
......@@ -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.
......
......@@ -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.
......
#!/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
......@@ -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:
......
......@@ -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
......
......@@ -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)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment