diff options
Diffstat (limited to 'common')
| -rw-r--r-- | common/AST.v | 219 | ||||
| -rw-r--r-- | common/Errors.v | 167 | ||||
| -rw-r--r-- | common/Events.v | 117 | ||||
| -rw-r--r-- | common/Globalenvs.v | 690 | ||||
| -rw-r--r-- | common/Main.v | 352 | ||||
| -rw-r--r-- | common/Mem.v | 3281 | ||||
| -rw-r--r-- | common/Smallstep.v | 460 | ||||
| -rw-r--r-- | common/Switch.v | 165 | ||||
| -rw-r--r-- | common/Values.v | 64 |
9 files changed, 3426 insertions, 2089 deletions
diff --git a/common/AST.v b/common/AST.v index 5b8c997..403861d 100644 --- a/common/AST.v +++ b/common/AST.v @@ -2,11 +2,14 @@ the abstract syntax trees of many of the intermediate languages. *) Require Import Coqlib. +Require Import Errors. Require Import Integers. Require Import Floats. Set Implicit Arguments. +(** * Syntactic elements *) + (** Identifiers (names of local variables, of global symbols and functions, etc) are represented by the type [positive] of positive integers. *) @@ -14,8 +17,9 @@ Definition ident := positive. Definition ident_eq := peq. -(** The languages are weakly typed, using only two types: [Tint] for - integers and pointers, and [Tfloat] for floating-point numbers. *) +(** The intermediate languages are weakly typed, using only two types: + [Tint] for integers and pointers, and [Tfloat] for floating-point + numbers. *) Inductive typ : Set := | Tint : typ @@ -24,6 +28,9 @@ Inductive typ : Set := Definition typesize (ty: typ) : Z := match ty with Tint => 4 | Tfloat => 8 end. +Lemma typesize_pos: forall ty, typesize ty > 0. +Proof. destruct ty; simpl; omega. Qed. + (** Additionally, function definitions and function calls are annotated by function signatures indicating the number and types of arguments, as well as the type of the returned value if any. These signatures @@ -82,6 +89,14 @@ Record program (F V: Set) : Set := mkprogram { prog_vars: list (ident * list init_data * V) }. +Definition prog_funct_names (F V: Set) (p: program F V) : list ident := + map (@fst ident F) p.(prog_funct). + +Definition prog_var_names (F V: Set) (p: program F V) : list ident := + map (fun x: ident * list init_data * V => fst(fst x)) p.(prog_vars). + +(** * Generic transformations over programs *) + (** We now define a general iterator over programs that applies a given code transformation function to all function descriptions and leaves the other parts of the program unchanged. *) @@ -117,48 +132,63 @@ End TRANSF_PROGRAM. code transformation function can fail and therefore returns an option type. *) +Open Local Scope error_monad_scope. +Open Local Scope string_scope. + Section MAP_PARTIAL. Variable A B C: Set. -Variable f: B -> option C. +Variable prefix_errmsg: A -> errmsg. +Variable f: B -> res C. -Fixpoint map_partial (l: list (A * B)) : option (list (A * C)) := +Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) := match l with - | nil => Some nil + | nil => OK nil | (a, b) :: rem => match f b with - | None => None - | Some c => - match map_partial rem with - | None => None - | Some res => Some ((a, c) :: res) - end + | Error msg => Error (prefix_errmsg a ++ msg)%list + | OK c => + do rem' <- map_partial rem; + OK ((a, c) :: rem') end end. Remark In_map_partial: forall l l' a c, - map_partial l = Some l' -> + map_partial l = OK l' -> In (a, c) l' -> - exists b, In (a, b) l /\ f b = Some c. + exists b, In (a, b) l /\ f b = OK c. Proof. induction l; simpl. - intros. inversion H; subst. elim H0. - destruct a as [a1 b1]. intros until c. + intros. inv H. elim H0. + intros until c. destruct a as [a1 b1]. caseEq (f b1); try congruence. - intros c1 EQ1. caseEq (map_partial l); try congruence. - intros res EQ2 EQ3 IN. inversion EQ3; clear EQ3; subst l'. - elim IN; intro. inversion H; subst. - exists b1; auto. + intro c1; intros. monadInv H0. + elim H1; intro. inv H0. exists b1; auto. exploit IHl; eauto. intros [b [P Q]]. exists b; auto. Qed. +Remark map_partial_forall2: + forall l l', + map_partial l = OK l' -> + list_forall2 + (fun (a_b: A * B) (a_c: A * C) => + fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c)) + l l'. +Proof. + induction l; simpl. + intros. inv H. constructor. + intro l'. destruct a as [a b]. + caseEq (f b). 2: congruence. intro c; intros. monadInv H0. + constructor. simpl. auto. auto. +Qed. + End MAP_PARTIAL. Remark map_partial_total: - forall (A B C: Set) (f: B -> C) (l: list (A * B)), - map_partial (fun b => Some (f b)) l = - Some (List.map (fun a_b => (fst a_b, f (snd a_b))) l). + forall (A B C: Set) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)), + map_partial prefix (fun b => OK (f b)) l = + OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l). Proof. induction l; simpl. auto. @@ -166,8 +196,8 @@ Proof. Qed. Remark map_partial_identity: - forall (A B: Set) (l: list (A * B)), - map_partial (fun b => Some b) l = Some l. + forall (A B: Set) (prefix: A -> errmsg) (l: list (A * B)), + map_partial prefix (fun b => OK b) l = OK l. Proof. induction l; simpl. auto. @@ -177,39 +207,39 @@ Qed. Section TRANSF_PARTIAL_PROGRAM. Variable A B V: Set. -Variable transf_partial: A -> option B. +Variable transf_partial: A -> res B. -Function transform_partial_program (p: program A V) : option (program B V) := - match map_partial transf_partial p.(prog_funct) with - | None => None - | Some fl => Some (mkprogram fl p.(prog_main) p.(prog_vars)) - end. +Definition prefix_funct_name (id: ident) : errmsg := + MSG "In function " :: CTX id :: MSG ":\n" :: nil. + +Definition transform_partial_program (p: program A V) : res (program B V) := + do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct); + OK (mkprogram fl p.(prog_main) p.(prog_vars)). Lemma transform_partial_program_function: forall p tp i tf, - transform_partial_program p = Some tp -> + transform_partial_program p = OK tp -> In (i, tf) tp.(prog_funct) -> - exists f, In (i, f) p.(prog_funct) /\ transf_partial f = Some tf. + exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf. Proof. - intros. functional inversion H. - apply In_map_partial with fl; auto. - inversion H; subst tp; assumption. + intros. monadInv H. simpl in H0. + eapply In_map_partial; eauto. Qed. Lemma transform_partial_program_main: forall p tp, - transform_partial_program p = Some tp -> + transform_partial_program p = OK tp -> tp.(prog_main) = p.(prog_main). Proof. - intros. functional inversion H. reflexivity. + intros. monadInv H. reflexivity. Qed. Lemma transform_partial_program_vars: forall p tp, - transform_partial_program p = Some tp -> + transform_partial_program p = OK tp -> tp.(prog_vars) = p.(prog_vars). Proof. - intros. functional inversion H. reflexivity. + intros. monadInv H. reflexivity. Qed. End TRANSF_PARTIAL_PROGRAM. @@ -221,49 +251,104 @@ End TRANSF_PARTIAL_PROGRAM. Section TRANSF_PARTIAL_PROGRAM2. Variable A B V W: Set. -Variable transf_partial_function: A -> option B. -Variable transf_partial_variable: V -> option W. - -Function transform_partial_program2 (p: program A V) : option (program B W) := - match map_partial transf_partial_function p.(prog_funct) with - | None => None - | Some fl => - match map_partial transf_partial_variable p.(prog_vars) with - | None => None - | Some vl => Some (mkprogram fl p.(prog_main) vl) - end - end. +Variable transf_partial_function: A -> res B. +Variable transf_partial_variable: V -> res W. + +Definition prefix_var_name (id_init: ident * list init_data) : errmsg := + MSG "In global variable " :: CTX (fst id_init) :: MSG ":\n" :: nil. + +Definition transform_partial_program2 (p: program A V) : res (program B W) := + do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct); + do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars); + OK (mkprogram fl p.(prog_main) vl). Lemma transform_partial_program2_function: forall p tp i tf, - transform_partial_program2 p = Some tp -> + transform_partial_program2 p = OK tp -> In (i, tf) tp.(prog_funct) -> - exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = Some tf. + exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf. Proof. - intros. functional inversion H. - apply In_map_partial with fl. auto. subst tp; assumption. + intros. monadInv H. + eapply In_map_partial; eauto. Qed. Lemma transform_partial_program2_variable: forall p tp i tv, - transform_partial_program2 p = Some tp -> + transform_partial_program2 p = OK tp -> In (i, tv) tp.(prog_vars) -> - exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = Some tv. + exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv. Proof. - intros. functional inversion H. - apply In_map_partial with vl. auto. subst tp; assumption. + intros. monadInv H. + eapply In_map_partial; eauto. Qed. Lemma transform_partial_program2_main: forall p tp, - transform_partial_program2 p = Some tp -> + transform_partial_program2 p = OK tp -> tp.(prog_main) = p.(prog_main). Proof. - intros. functional inversion H. reflexivity. + intros. monadInv H. reflexivity. Qed. End TRANSF_PARTIAL_PROGRAM2. +(** The following is a relational presentation of + [transform_program_partial2]. Given relations between function + definitions and between variable information, it defines a relation + between programs stating that the two programs have the same shape + (same global names, etc) and that identically-named function definitions + are variable information are related. *) + +Section MATCH_PROGRAM. + +Variable A B V W: Set. +Variable match_fundef: A -> B -> Prop. +Variable match_varinfo: V -> W -> Prop. + +Definition match_funct_entry (x1: ident * A) (x2: ident * B) := + match x1, x2 with + | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2 + end. + +Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) := + match x1, x2 with + | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2 + end. + +Definition match_program (p1: program A V) (p2: program B W) : Prop := + list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct) + /\ p1.(prog_main) = p2.(prog_main) + /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars). + +End MATCH_PROGRAM. + +Remark transform_partial_program2_match: + forall (A B V W: Set) + (transf_partial_function: A -> res B) + (transf_partial_variable: V -> res W) + (p: program A V) (tp: program B W), + transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp -> + match_program + (fun fd tfd => transf_partial_function fd = OK tfd) + (fun info tinfo => transf_partial_variable info = OK tinfo) + p tp. +Proof. + intros. monadInv H. split. + apply list_forall2_imply with + (fun (ab: ident * A) (ac: ident * B) => + fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)). + eapply map_partial_forall2. eauto. + intros. destruct v1; destruct v2; simpl in *. auto. + split. auto. + apply list_forall2_imply with + (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) => + fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)). + eapply map_partial_forall2. eauto. + intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence. +Qed. + +(** * External functions *) + (** For most languages, the functions composing the program are either internal functions, defined within the language, or external functions (a.k.a. system calls) that emit an event when applied. We define @@ -296,16 +381,12 @@ End TRANSF_FUNDEF. Section TRANSF_PARTIAL_FUNDEF. Variable A B: Set. -Variable transf_partial: A -> option B. +Variable transf_partial: A -> res B. -Definition transf_partial_fundef (fd: fundef A): option (fundef B) := +Definition transf_partial_fundef (fd: fundef A): res (fundef B) := match fd with - | Internal f => - match transf_partial f with - | None => None - | Some f' => Some (Internal f') - end - | External ef => Some (External ef) + | Internal f => do f' <- transf_partial f; OK (Internal f') + | External ef => OK (External ef) end. End TRANSF_PARTIAL_FUNDEF. diff --git a/common/Errors.v b/common/Errors.v new file mode 100644 index 0000000..2c1d752 --- /dev/null +++ b/common/Errors.v @@ -0,0 +1,167 @@ +(** Error reporting and the error monad. *) + +Require Import String. +Require Import Coqlib. + +Close Scope string_scope. + +Set Implicit Arguments. + +(** * Representation of error messages. *) + +(** Compile-time errors produce an error message, represented in Coq + as a list of either substrings or positive numbers encoding + a source-level identifier (see module AST). *) + +Inductive errcode: Set := + | MSG: string -> errcode + | CTX: positive -> errcode. + +Definition errmsg: Set := list errcode. + +Definition msg (s: string) : errmsg := MSG s :: nil. + +(** * The error monad *) + +(** Compilation functions that can fail have return type [res A]. + The return value is either [OK res] to indicate success, + or [Error msg] to indicate failure. *) + +Inductive res (A: Set) : Set := +| OK: A -> res A +| Error: errmsg -> res A. + +Implicit Arguments Error [A]. + +(** To automate the propagation of errors, we use a monadic style + with the following [bind] operation. *) + +Definition bind (A B: Set) (f: res A) (g: A -> res B) : res B := + match f with + | OK x => g x + | Error msg => Error msg + end. + +Definition bind2 (A B C: Set) (f: res (A * B)) (g: A -> B -> res C) : res C := + match f with + | OK (x, y) => g x y + | Error msg => Error msg + end. + +(** The [do] notation, inspired by Haskell's, keeps the code readable. *) + +Notation "'do' X <- A ; B" := (bind A (fun X => B)) + (at level 200, X ident, A at level 100, B at level 200) + : error_monad_scope. + +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) + : error_monad_scope. + +Remark bind_inversion: + forall (A B: Set) (f: res A) (g: A -> res B) (y: B), + bind f g = OK y -> + exists x, f = OK x /\ g x = OK y. +Proof. + intros until y. destruct f; simpl; intros. + exists a; auto. + discriminate. +Qed. + +Remark bind2_inversion: + forall (A B C: Set) (f: res (A*B)) (g: A -> B -> res C) (z: C), + bind2 f g = OK z -> + exists x, exists y, f = OK (x, y) /\ g x y = OK z. +Proof. + intros until z. destruct f; simpl. + destruct p; simpl; intros. exists a; exists b; auto. + intros; discriminate. +Qed. + +Open Local Scope error_monad_scope. + +(** This is the familiar monadic map iterator. *) + +Fixpoint mmap (A B: Set) (f: A -> res B) (l: list A) {struct l} : res (list B) := + match l with + | nil => OK nil + | hd :: tl => do hd' <- f hd; do tl' <- mmap f tl; OK (hd' :: tl') + end. + +Remark mmap_inversion: + forall (A B: Set) (f: A -> res B) (l: list A) (l': list B), + mmap f l = OK l' -> + list_forall2 (fun x y => f x = OK y) l l'. +Proof. + induction l; simpl; intros. + inversion_clear H. constructor. + destruct (bind_inversion _ _ H) as [hd' [P Q]]. + destruct (bind_inversion _ _ Q) as [tl' [R S]]. + inversion_clear S. + constructor. auto. auto. +Qed. + +(** * Reasoning over monadic computations *) + +(** The [monadInv H] tactic below simplifies hypotheses of the form +<< + H: (do x <- a; b) = OK res +>> + By definition of the bind operation, both computations [a] and + [b] must succeed for their composition to succeed. The tactic + therefore generates the following hypotheses: + + x: ... + H1: a = OK x + H2: b x = OK res +*) + +Ltac monadInv1 H := + match type of H with + | (OK _ = OK _) => + inversion H; clear H; try subst + | (Error _ = OK _) => + discriminate + | (bind ?F ?G = OK ?X) => + let x := fresh "x" in ( + let EQ1 := fresh "EQ" in ( + let EQ2 := fresh "EQ" in ( + destruct (bind_inversion F G H) as [x [EQ1 EQ2]]; + clear H; + try (monadInv1 EQ2)))) + | (bind2 ?F ?G = OK ?X) => + let x1 := fresh "x" in ( + let x2 := fresh "x" in ( + let EQ1 := fresh "EQ" in ( + let EQ2 := fresh "EQ" in ( + destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]]; + clear H; + try (monadInv1 EQ2))))) + | (mmap ?F ?L = OK ?M) => + generalize (mmap_inversion F L H); intro + end. + +Ltac monadInv H := + match type of H with + | (OK _ = OK _) => monadInv1 H + | (Error _ = OK _) => monadInv1 H + | (bind ?F ?G = OK ?X) => monadInv1 H + | (bind2 ?F ?G = OK ?X) => monadInv1 H + | (?F _ _ _ _ _ _ _ _ = OK _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ _ _ = OK _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ _ = OK _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ = OK _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ = OK _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ = OK _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ = OK _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ = OK _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + end. + diff --git a/common/Events.v b/common/Events.v index a0559fd..e1a4729 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1,4 +1,4 @@ -(** Representation of (traces of) observable events. *) +(** Representation of observable events and execution traces. *) Require Import Coqlib. Require Import AST. @@ -6,23 +6,77 @@ Require Import Integers. Require Import Floats. Require Import Values. +(** The observable behaviour of programs is stated in terms of + input/output events, which can also be thought of as system calls + to the operating system. An event is generated each time an + external function (see module AST) is invoked. The event records + the name of the external function, the arguments to the function + invocation provided by the program, and the return value provided by + the outside world (e.g. the operating system). Arguments and values + are either integers or floating-point numbers. We currently do not + allow pointers to be exchanged between the program and the outside + world. *) + Inductive eventval: Set := | EVint: int -> eventval | EVfloat: float -> eventval. -Parameter trace: Set. -Parameter E0: trace. -Parameter Eextcall: ident -> list eventval -> eventval -> trace. -Parameter Eapp: trace -> trace -> trace. +Record event : Set := mkevent { + ev_name: ident; + ev_args: list eventval; + ev_res: eventval +}. + +(** The dynamic semantics for programs collect traces of events. + Traces are of two kinds: finite (type [trace]) + or infinite (type [traceinf]). *) + +Definition trace := list event. + +Definition E0 : trace := nil. + +Definition Eextcall + (name: ident) (args: list eventval) (res: eventval) : trace := + mkevent name args res :: nil. + +Definition Eapp (t1 t2: trace) : trace := t1 ++ t2. + +CoInductive traceinf : Set := + | Econsinf: event -> traceinf -> traceinf. + +Fixpoint Eappinf (t: trace) (T: traceinf) {struct t} : traceinf := + match t with + | nil => T + | ev :: t' => Econsinf ev (Eappinf t' T) + end. + +(** Concatenation of traces is written [**] in the finite case + or [***] in the infinite case. *) Infix "**" := Eapp (at level 60, right associativity). +Infix "***" := Eappinf (at level 60, right associativity). -Axiom E0_left: forall t, E0 ** t = t. -Axiom E0_right: forall t, t ** E0 = t. -Axiom Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3). +Lemma E0_left: forall t, E0 ** t = t. +Proof. auto. Qed. + +Lemma E0_right: forall t, t ** E0 = t. +Proof. intros. unfold E0, Eapp. rewrite <- app_nil_end. auto. Qed. + +Lemma Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3). +Proof. intros. unfold Eapp, trace. apply app_ass. Qed. + +Lemma Eappinf_assoc: forall t1 t2 T, (t1 ** t2) *** T = t1 *** (t2 *** T). +Proof. + induction t1; intros; simpl. auto. decEq; auto. +Qed. Hint Rewrite E0_left E0_right Eapp_assoc: trace_rewrite. +Opaque trace E0 Eextcall Eapp. + +(** The following [traceEq] tactic proves equalities between traces + or infinite traces. *) + Ltac substTraceHyp := match goal with | [ H: (@eq trace ?x ?y) |- _ ] => @@ -40,6 +94,11 @@ Ltac decomposeTraceEq := Ltac traceEq := repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq. +(** The predicate [event_match ef vargs t vres] expresses that + the event [t] is generated when invoking external function [ef] + with arguments [vargs], and obtaining [vres] as a return value + from the operating system. *) + Inductive eventval_match: eventval -> typ -> val -> Prop := | ev_match_int: forall i, eventval_match (EVint i) Tint (Vint i) @@ -63,6 +122,10 @@ Inductive event_match: eventval_match eres (proj_sig_res ef.(ef_sig)) vres -> event_match ef vargs (Eextcall ef.(ef_id) eargs eres) vres. +(** The following section shows that [event_match] is stable under + relocation of pointer values, as performed by memory injections + (see module [Mem]). *) + Require Import Mem. Section EVENT_MATCH_INJECT. @@ -101,3 +164,41 @@ Proof. Qed. End EVENT_MATCH_INJECT. + +(** The following section shows that [event_match] is stable under + replacement of [Vundef] values by more defined values. *) + +Section EVENT_MATCH_LESSDEF. + +Remark eventval_match_lessdef: + forall ev ty v1, eventval_match ev ty v1 -> + forall v2, Val.lessdef v1 v2 -> + eventval_match ev ty v2. +Proof. + induction 1; intros; inv H; constructor. +Qed. + +Remark eventval_list_match_moredef: + forall evl tyl vl1, eventval_list_match evl tyl vl1 -> + forall vl2, Val.lessdef_list vl1 vl2 -> + eventval_list_match evl tyl vl2. +Proof. + induction 1; intros. + inversion H; constructor. + inversion H1; constructor. + eapply eventval_match_lessdef; eauto. + eauto. +Qed. + +Lemma event_match_lessdef: + forall ef args1 t res1 args2, + event_match ef args1 t res1 -> + Val.lessdef_list args1 args2 -> + exists res2, event_match ef args2 t res2 /\ Val.lessdef res1 res2. +Proof. + intros. inversion H; subst. exists res1; split. + constructor. eapply eventval_list_match_moredef; eauto. auto. + auto. +Qed. + +End EVENT_MATCH_LESSDEF. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index ccb7b03..623200f 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -19,6 +19,7 @@ system. *) Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. @@ -60,6 +61,34 @@ Module Type GENV. Hypothesis find_funct_find_funct_ptr: forall (F: Set) (ge: t F) (b: block), find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b. + + Hypothesis find_symbol_exists: + forall (F V: Set) (p: program F V) + (id: ident) (init: list init_data) (v: V), + In (id, init, v) (prog_vars p) -> + exists b, find_symbol (globalenv p) id = Some b. + Hypothesis find_funct_ptr_exists: + forall (F V: Set) (p: program F V) (id: ident) (f: F), + list_norepet (prog_funct_names p) -> + list_disjoint (prog_funct_names p) (prog_var_names p) -> + In (id, f) (prog_funct p) -> + exists b, find_symbol (globalenv p) id = Some b + /\ find_funct_ptr (globalenv p) b = Some f. + + Hypothesis find_funct_ptr_inversion: + forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F), + find_funct_ptr (globalenv p) b = Some f -> + exists id, In (id, f) (prog_funct p). + Hypothesis find_funct_inversion: + forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F), + find_funct (globalenv p) v = Some f -> + exists id, In (id, f) (prog_funct p). + Hypothesis find_funct_ptr_symbol_inversion: + forall (F V: Set) (p: program F V) (id: ident) (b: block) (f: F), + find_symbol (globalenv p) id = Some b -> + find_funct_ptr (globalenv p) b = Some f -> + In (id, f) p.(prog_funct). + Hypothesis find_funct_ptr_prop: forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F), (forall id f, In (id, f) (prog_funct p) -> P f) -> @@ -70,24 +99,19 @@ Module Type GENV. (forall id f, In (id, f) (prog_funct p) -> P f) -> find_funct (globalenv p) v = Some f -> P f. - Hypothesis find_funct_ptr_symbol_inversion: - forall (F V: Set) (p: program F V) (id: ident) (b: block) (f: F), - find_symbol (globalenv p) id = Some b -> - find_funct_ptr (globalenv p) b = Some f -> - In (id, f) p.(prog_funct). Hypothesis initmem_nullptr: forall (F V: Set) (p: program F V), let m := init_mem p in valid_block m nullptr /\ m.(blocks) nullptr = empty_block 0 0. - Hypothesis initmem_block_init: - forall (F V: Set) (p: program F V) (b: block), - exists id, (init_mem p).(blocks) b = block_init_data id. - Hypothesis find_funct_ptr_inv: + Hypothesis initmem_inject_neutral: + forall (F V: Set) (p: program F V), + mem_inject_neutral (init_mem p). + Hypothesis find_funct_ptr_negative: forall (F V: Set) (p: program F V) (b: block) (f: F), find_funct_ptr (globalenv p) b = Some f -> b < 0. - Hypothesis find_symbol_inv: + Hypothesis find_symbol_not_fresh: forall (F V: Set) (p: program F V) (id: ident) (b: block), find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p). @@ -95,74 +119,162 @@ Module Type GENV. and operations over global environments. *) Hypothesis find_funct_ptr_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V) (b: block) (f: A), + forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> find_funct_ptr (globalenv (transform_program transf p)) b = Some (transf f). Hypothesis find_funct_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V) (v: val) (f: A), + forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> find_funct (globalenv (transform_program transf p)) v = Some (transf f). Hypothesis find_symbol_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V) (s: ident), + forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (s: ident), find_symbol (globalenv (transform_program transf p)) s = find_symbol (globalenv p) s. Hypothesis init_mem_transf: forall (A B V: Set) (transf: A -> B) (p: program A V), init_mem (transform_program transf p) = init_mem p. + Hypothesis find_funct_ptr_rev_transf: + forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (b : block) (tf : B), + find_funct_ptr (globalenv (transform_program transf p)) b = Some tf -> + exists f : A, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf. + Hypothesis find_funct_rev_transf: + forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (v : val) (tf : B), + find_funct (globalenv (transform_program transf p)) v = Some tf -> + exists f : A, find_funct (globalenv p) v = Some f /\ transf f = tf. (** Commutation properties between partial program transformations and operations over global environments. *) Hypothesis find_funct_ptr_transf_partial: - forall (A B V: Set) (transf: A -> option B) - (p: program A V) (p': program B V), - transform_partial_program transf p = Some p' -> + forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + transform_partial_program transf p = OK p' -> forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> - find_funct_ptr (globalenv p') b = transf f /\ transf f <> None. + exists f', + find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'. Hypothesis find_funct_transf_partial: - forall (A B V: Set) (transf: A -> option B) - (p: program A V) (p': program B V), - transform_partial_program transf p = Some p' -> + forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + transform_partial_program transf p = OK p' -> forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> - find_funct (globalenv p') v = transf f /\ transf f <> None. + exists f', + find_funct (globalenv p') v = Some f' /\ transf f = OK f'. Hypothesis find_symbol_transf_partial: - forall (A B V: Set) (transf: A -> option B) - (p: program A V) (p': program B V), - transform_partial_program transf p = Some p' -> + forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + transform_partial_program transf p = OK p' -> forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Hypothesis init_mem_transf_partial: - forall (A B V: Set) (transf: A -> option B) - (p: program A V) (p': program B V), - transform_partial_program transf p = Some p' -> + forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + transform_partial_program transf p = OK p' -> init_mem p' = init_mem p. + Hypothesis find_funct_ptr_rev_transf_partial: + forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + transform_partial_program transf p = OK p' -> + forall (b : block) (tf : B), + find_funct_ptr (globalenv p') b = Some tf -> + exists f : A, + find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf. + Hypothesis find_funct_rev_transf_partial: + forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + transform_partial_program transf p = OK p' -> + forall (v : val) (tf : B), + find_funct (globalenv p') v = Some tf -> + exists f : A, + find_funct (globalenv p) v = Some f /\ transf f = OK tf. Hypothesis find_funct_ptr_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W) + forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), - transform_partial_program2 transf_fun transf_var p = Some p' -> + transform_partial_program2 transf_fun transf_var p = OK p' -> forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> - find_funct_ptr (globalenv p') b = transf_fun f /\ transf_fun f <> None. + exists f', + find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'. Hypothesis find_funct_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W) + forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), - transform_partial_program2 transf_fun transf_var p = Some p' -> + transform_partial_program2 transf_fun transf_var p = OK p' -> forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> - find_funct (globalenv p') v = transf_fun f /\ transf_fun f <> None. + exists f', + find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. Hypothesis find_symbol_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W) + forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), - transform_partial_program2 transf_fun transf_var p = Some p' -> + transform_partial_program2 transf_fun transf_var p = OK p' -> forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Hypothesis init_mem_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W) + forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + (p: program A V) (p': program B W), + transform_partial_program2 transf_fun transf_var p = OK p' -> + init_mem p' = init_mem p. + Hypothesis find_funct_ptr_rev_transf_partial2: + forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + (p: program A V) (p': program B W), + transform_partial_program2 transf_fun transf_var p = OK p' -> + forall (b : block) (tf : B), + find_funct_ptr (globalenv p') b = Some tf -> + exists f : A, + find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf. + Hypothesis find_funct_rev_transf_partial2: + forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), - transform_partial_program2 transf_fun transf_var p = Some p' -> + transform_partial_program2 transf_fun transf_var p = OK p' -> + forall (v : val) (tf : B), + find_funct (globalenv p') v = Some tf -> + exists f : A, + find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf. + +(** Commutation properties between matching between programs + and operations over global environments. *) + + Hypothesis find_funct_ptr_match: + forall (A B V W: Set) (match_fun: A -> B -> Prop) + (match_var: V -> W -> Prop) (p: program A V) (p': program B W), + match_program match_fun match_var p p' -> + forall (b : block) (f : A), + find_funct_ptr (globalenv p) b = Some f -> + exists tf : B, + find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf. + Hypothesis find_funct_ptr_rev_match: + forall (A B V W: Set) (match_fun: A -> B -> Prop) + (match_var: V -> W -> Prop) (p: program A V) (p': program B W), + match_program match_fun match_var p p' -> + forall (b : block) (tf : B), + find_funct_ptr (globalenv p') b = Some tf -> + exists f : A, + find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf. + Hypothesis find_funct_match: + forall (A B V W: Set) (match_fun: A -> B -> Prop) + (match_var: V -> W -> Prop) (p: program A V) (p': program B W), + match_program match_fun match_var p p' -> + forall (v : val) (f : A), + find_funct (globalenv p) v = Some f -> + exists tf : B, find_funct (globalenv p') v = Some tf /\ match_fun f tf. + Hypothesis find_funct_rev_match: + forall (A B V W: Set) (match_fun: A -> B -> Prop) + (match_var: V -> W -> Prop) (p: program A V) (p': program B W), + match_program match_fun match_var p p' -> + forall (v : val) (tf : B), + find_funct (globalenv p') v = Some tf -> + exists f : A, find_funct (globalenv p) v = Some f /\ match_fun f tf. + Hypothesis find_symbol_match: + forall (A B V W: Set) (match_fun: A -> B -> Prop) + (match_var: V -> W -> Prop) (p: program A V) (p': program B W), + match_program match_fun match_var p p' -> + forall (s : ident), + find_symbol (globalenv p') s = find_symbol (globalenv p) s. + Hypothesis init_mem_match: + forall (A B V W: Set) (match_fun: A -> B -> Prop) + (match_var: V -> W -> Prop) (p: program A V) (p': program B W), + match_program match_fun match_var p p' -> init_mem p' = init_mem p. End GENV. @@ -280,10 +392,10 @@ Lemma initmem_nullptr: forall (p: program F V), let m := init_mem p in valid_block m nullptr /\ - m.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0). + m.(blocks) nullptr = mkblock 0 0 (fun y => Undef). Proof. pose (P := fun m => valid_block m nullptr /\ - m.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0)). + m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)). assert (forall init, P (snd init) -> forall vars, P (snd (add_globals init vars))). induction vars; simpl; intros. auto. @@ -297,25 +409,25 @@ Proof. red; simpl. split. compute. auto. reflexivity. Qed. -Lemma initmem_block_init: - forall (p: program F V) (b: block), - exists id, (init_mem p).(blocks) b = block_init_data id. +Lemma initmem_inject_neutral: + forall (p: program F V), + mem_inject_neutral (init_mem p). Proof. - assert (forall g0 vars g1 m b, + assert (forall g0 vars g1 m, add_globals (g0, Mem.empty) vars = (g1, m) -> - exists id, m.(blocks) b = block_init_data id). - induction vars; simpl. - intros. inversion H. unfold Mem.empty; simpl. - exists (@nil init_data). symmetry. apply Mem.block_init_data_empty. + mem_inject_neutral m). + Opaque alloc_init_data. + induction vars; simpl. + intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H). + simpl in H1. rewrite Mem.getN_init in H1. + replace v with Vundef. auto. destruct chunk; simpl in H1; auto. destruct a as [[id1 init1] info1]. - caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. - intros g m b EQ1. injection EQ1; intros EQ2 EQ3; clear EQ1. - rewrite <- EQ2; simpl. unfold update. - case (zeq b (nextblock m1)); intro. - exists init1; auto. - eauto. - intros. caseEq (globalenv_initmem p). - intros g m EQ. unfold init_mem; rewrite EQ; simpl. + caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. + caseEq (alloc_init_data m1 init1). intros m2 b ALLOC. + intros. inv H. + eapply Mem.alloc_init_data_neutral; eauto. + intros. caseEq (globalenv_initmem p). intros g m EQ. + unfold init_mem; rewrite EQ; simpl. unfold globalenv_initmem in EQ. eauto. Qed. @@ -325,7 +437,7 @@ Proof. induction fns; simpl; intros. omega. unfold Zpred. omega. Qed. -Theorem find_funct_ptr_inv: +Theorem find_funct_ptr_negative: forall (p: program F V) (b: block) (f: F), find_funct_ptr (globalenv p) b = Some f -> b < 0. Proof. @@ -340,7 +452,7 @@ Proof. intros. eauto. Qed. -Theorem find_symbol_inv: +Theorem find_symbol_not_fresh: forall (p: program F V) (id: ident) (b: block), find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p). Proof. @@ -358,6 +470,7 @@ Proof. induction vars; simpl; intros until b. intros. inversion H0. subst g m. simpl. generalize (H fns s b H1). omega. + Transparent alloc_init_data. destruct a as [[id1 init1] info1]. caseEq (add_globals (add_functs empty fns, Mem.empty) vars). intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ. @@ -373,20 +486,125 @@ Qed. End GENV. (* Invariants on functions *) + +Lemma find_symbol_exists: + forall (F V: Set) (p: program F V) + (id: ident) (init: list init_data) (v: V), + In (id, init, v) (prog_vars p) -> + exists b, find_symbol (globalenv p) id = Some b. +Proof. + intros until v. + assert (forall initm vl, In (id, init, v) vl -> + exists b, PTree.get id (@symbols F (fst (add_globals initm vl))) = Some b). + induction vl; simpl; intros. + elim H. + destruct a as [[id0 init0] v0]. + caseEq (add_globals initm vl). intros g1 m1 EQ. simpl. + rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto. + elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto. + intros. unfold globalenv, find_symbol, globalenv_initmem. auto. +Qed. + +Remark find_symbol_above_nextfunction: + forall (F: Set) (id: ident) (b: block) (fns: list (ident * F)), + let g := add_functs (empty F) fns in + PTree.get id g.(symbols) = Some b -> + b > g.(nextfunction). +Proof. + induction fns; simpl. + rewrite PTree.gempty. congruence. + rewrite PTree.gsspec. case (peq id (fst a)); intro. + intro EQ. inversion EQ. unfold Zpred. omega. + intros. generalize (IHfns H). unfold Zpred; omega. +Qed. + +Remark find_symbol_add_globals: + forall (F V: Set) (id: ident) (ge_m: t F * mem) (vars: list (ident * list init_data * V)), + ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) -> + find_symbol (fst (add_globals ge_m vars)) id = + find_symbol (fst ge_m) id. +Proof. + unfold find_symbol; induction vars; simpl; intros. + auto. + destruct a as [[id0 init0] var0]. simpl in *. + caseEq (add_globals ge_m vars); intros ge' m' EQ. + simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars. + apply IHvars. tauto. intuition congruence. +Qed. + +Lemma find_funct_ptr_exists: + forall (F V: Set) (p: program F V) (id: ident) (f: F), + list_norepet (prog_funct_names p) -> + list_disjoint (prog_funct_names p) (prog_var_names p) -> + In (id, f) (prog_funct p) -> + exists b, find_symbol (globalenv p) id = Some b + /\ find_funct_ptr (globalenv p) b = Some f. +Proof. + intros until f. + assert (forall (fns: list (ident * F)), + list_norepet (map (@fst ident F) fns) -> + In (id, f) fns -> + exists b, find_symbol (add_functs (empty F) fns) id = Some b + /\ find_funct_ptr (add_functs (empty F) fns) b = Some f). + unfold find_symbol, find_funct_ptr. induction fns; intros. + elim H0. + destruct a as [id0 f0]; simpl in *. inv H. + unfold add_funct; simpl. + rewrite PTree.gsspec. destruct (peq id id0). + subst id0. econstructor; split. eauto. + replace f0 with f. apply ZMap.gss. + elim H0; intro. congruence. elim H3. + change id with (@fst ident F (id, f)). apply List.in_map. auto. + exploit IHfns; eauto. elim H0; intro. congruence. auto. + intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto. + generalize (find_symbol_above_nextfunction _ _ X). + unfold block; unfold ZIndexed.t; intro; omega. + + intros. exploit H; eauto. assumption. intros [b [X Y]]. + exists b; split. + unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals. + assumption. apply list_disjoint_notin with (prog_funct_names p). assumption. + unfold prog_funct_names. change id with (fst (id, f)). + apply List.in_map; auto. + unfold find_funct_ptr. rewrite functions_globalenv. + assumption. +Qed. + +Lemma find_funct_ptr_inversion: + forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F), + find_funct_ptr (globalenv p) b = Some f -> + exists id, In (id, f) (prog_funct p). +Proof. + intros until f. + assert (forall fns: list (ident * F), + find_funct_ptr (add_functs (empty F) fns) b = Some f -> + exists id, In (id, f) fns). + unfold find_funct_ptr. induction fns; simpl. + rewrite ZMap.gi. congruence. + destruct a as [id0 f0]; simpl. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs (empty F) fns))). + intro. inv H. exists id0; auto. + intro. exploit IHfns; eauto. intros [id A]. exists id; auto. + unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto. +Qed. + Lemma find_funct_ptr_prop: forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F), (forall id f, In (id, f) (prog_funct p) -> P f) -> find_funct_ptr (globalenv p) b = Some f -> P f. Proof. - intros until f. - unfold find_funct_ptr. rewrite functions_globalenv. - generalize (prog_funct p). induction l; simpl. - rewrite ZMap.gi. intros; discriminate. - rewrite ZMap.gsspec. - case (ZIndexed.eq b (nextfunction (add_functs (empty F) l))); intros. - apply H with (fst a). left. destruct a. simpl in *. congruence. - apply IHl. intros. apply H with id. right. auto. auto. + intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto. +Qed. + +Lemma find_funct_inversion: + forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F), + find_funct (globalenv p) v = Some f -> + exists id, In (id, f) (prog_funct p). +Proof. + intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H. + rewrite find_funct_find_funct_ptr in H. + eapply find_funct_ptr_inversion; eauto. Qed. Lemma find_funct_prop: @@ -395,10 +613,7 @@ Lemma find_funct_prop: find_funct (globalenv p) v = Some f -> P f. Proof. - intros until f. unfold find_funct. - destruct v; try (intros; discriminate). - case (Int.eq i Int.zero); [idtac | intros; discriminate]. - intros. eapply find_funct_ptr_prop; eauto. + intros. exploit find_funct_inversion; eauto. intros [id A]. eauto. Qed. Lemma find_funct_ptr_symbol_inversion: @@ -411,15 +626,6 @@ Proof. assert (forall fns, let g := add_functs (empty F) fns in PTree.get id g.(symbols) = Some b -> - b > g.(nextfunction)). - induction fns; simpl. - rewrite PTree.gempty. congruence. - rewrite PTree.gsspec. case (peq id (fst a)); intro. - intro EQ. inversion EQ. unfold Zpred. omega. - intros. generalize (IHfns H). unfold Zpred; omega. - assert (forall fns, - let g := add_functs (empty F) fns in - PTree.get id g.(symbols) = Some b -> ZMap.get b g.(functions) = Some f -> In (id, f) fns). induction fns; simpl. @@ -430,216 +636,336 @@ Proof. intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true. intro EQ2. left. destruct a. simpl in *. congruence. intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto. - generalize (H _ H0). fold g. unfold block. omega. + generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega. assert (forall g0 m0, b < 0 -> forall vars g m, @add_globals F V (g0, m0) vars = (g, m) -> PTree.get id g.(symbols) = Some b -> PTree.get id g0.(symbols) = Some b). induction vars; simpl. - intros. inversion H2. auto. + intros. inv H1. auto. destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars). intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1. unfold add_symbol; intros A B. rewrite <- B. simpl. rewrite PTree.gsspec. case (peq id id1); intros. - assert (b > 0). injection H2; intros. rewrite <- H3. apply nextblock_pos. + assert (b > 0). inv H1. apply nextblock_pos. omegaContradiction. eauto. intros. - generalize (find_funct_ptr_inv _ _ H3). intro. + generalize (find_funct_ptr_negative _ _ H2). intro. pose (g := add_functs (empty F) (prog_funct p)). - apply H0. - apply H1 with Mem.empty (prog_vars p) (globalenv p) (init_mem p). + apply H. + apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p). auto. unfold globalenv, init_mem. rewrite <- surjective_pairing. reflexivity. assumption. rewrite <- functions_globalenv. assumption. Qed. (* Global environments and program transformations. *) -Section TRANSF_PROGRAM_PARTIAL2. +Section MATCH_PROGRAM. Variable A B V W: Set. -Variable transf_fun: A -> option B. -Variable transf_var: V -> option W. +Variable match_fun: A -> B -> Prop. +Variable match_var: V -> W -> Prop. Variable p: program A V. Variable p': program B W. -Hypothesis transf_OK: - transform_partial_program2 transf_fun transf_var p = Some p'. +Hypothesis match_prog: + match_program match_fun match_var p p'. -Lemma add_functs_transf: +Lemma add_functs_match: forall (fns: list (ident * A)) (tfns: list (ident * B)), - map_partial transf_fun fns = Some tfns -> + list_forall2 (match_funct_entry match_fun) fns tfns -> let r := add_functs (empty A) fns in let tr := add_functs (empty B) tfns in nextfunction tr = nextfunction r /\ symbols tr = symbols r /\ forall (b: block) (f: A), ZMap.get b (functions r) = Some f -> - ZMap.get b (functions tr) = transf_fun f /\ transf_fun f <> None. + exists tf, ZMap.get b (functions tr) = Some tf /\ match_fun f tf. Proof. - induction fns; simpl. + induction 1; simpl. - intros; injection H; intro; subst tfns. - simpl. split. reflexivity. split. reflexivity. + split. reflexivity. split. reflexivity. intros b f; repeat (rewrite ZMap.gi). intros; discriminate. - intro tfns. destruct a. caseEq (transf_fun a). intros a' TA. - caseEq (map_partial transf_fun fns). intros l TPP EQ. - injection EQ; intro; subst tfns. - clear EQ. simpl. - generalize (IHfns l TPP). - intros [HR1 [HR2 HR3]]. - rewrite HR1. rewrite HR2. - split. reflexivity. - split. reflexivity. + destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. + simpl. red in H. destruct H. + destruct IHlist_forall2 as [X [Y Z]]. + rewrite X. rewrite Y. + split. auto. + split. congruence. intros b f. - case (zeq b (nextfunction (add_functs (empty A) fns))); intro. - subst b. repeat (rewrite ZMap.gss). - intro EQ; injection EQ; intro; subst f; clear EQ. - rewrite TA. split. auto. discriminate. - repeat (rewrite ZMap.gso; auto). + repeat (rewrite ZMap.gsspec). + destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))). + intro EQ; inv EQ. exists fn2; auto. + auto. +Qed. - intros; discriminate. - intros; discriminate. +Lemma add_functs_rev_match: + forall (fns: list (ident * A)) (tfns: list (ident * B)), + list_forall2 (match_funct_entry match_fun) fns tfns -> + let r := add_functs (empty A) fns in + let tr := add_functs (empty B) tfns in + nextfunction tr = nextfunction r /\ + symbols tr = symbols r /\ + forall (b: block) (tf: B), + ZMap.get b (functions tr) = Some tf -> + exists f, ZMap.get b (functions r) = Some f /\ match_fun f tf. +Proof. + induction 1; simpl. + + split. reflexivity. split. reflexivity. + intros b f; repeat (rewrite ZMap.gi). intros; discriminate. + + destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. + simpl. red in H. destruct H. + destruct IHlist_forall2 as [X [Y Z]]. + rewrite X. rewrite Y. + split. auto. + split. congruence. + intros b f. + repeat (rewrite ZMap.gsspec). + destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))). + intro EQ; inv EQ. exists fn1; auto. + auto. Qed. -Lemma mem_add_globals_transf: +Lemma mem_add_globals_match: forall (g1: genv A) (g2: genv B) (m: mem) (vars: list (ident * list init_data * V)) (tvars: list (ident * list init_data * W)), - map_partial transf_var vars = Some tvars -> + list_forall2 (match_var_entry match_var) vars tvars -> snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars). Proof. - induction vars; simpl. - intros. inversion H. reflexivity. - intro. destruct a as [[id1 init1] info1]. - caseEq (transf_var info1); try congruence. - intros tinfo1 EQ1. - caseEq (map_partial transf_var vars); try congruence. - intros tvars' EQ2 EQ3. - inversion EQ3. simpl. - generalize (IHvars _ EQ2). - destruct (add_globals (g1, m) vars). - destruct (add_globals (g2, m) tvars'). + induction 1; simpl. + auto. + destruct a1 as [[id1 init1] info1]. + destruct b1 as [[id2 init2] info2]. + red in H. destruct H as [X [Y Z]]. subst id2 init2. + generalize IHlist_forall2. + destruct (add_globals (g1, m) al). + destruct (add_globals (g2, m) bl). simpl. intro. subst m1. auto. Qed. -Lemma symbols_add_globals_transf: +Lemma symbols_add_globals_match: forall (g1: genv A) (g2: genv B) (m: mem), symbols g1 = symbols g2 -> forall (vars: list (ident * list init_data * V)) (tvars: list (ident * list init_data * W)), - map_partial transf_var vars = Some tvars -> + list_forall2 (match_var_entry match_var) vars tvars -> symbols (fst (add_globals (g1, m) vars)) = symbols (fst (add_globals (g2, m) tvars)). Proof. - induction vars; simpl. - intros. inversion H0. assumption. - intro. destruct a as [[id1 init1] info1]. - caseEq (transf_var info1); try congruence. intros tinfo1 EQ1. - caseEq (map_partial transf_var vars); try congruence. - intros tvars' EQ2 EQ3. inversion EQ3; simpl. - generalize (IHvars _ EQ2). - generalize (mem_add_globals_transf g1 g2 m vars EQ2). - destruct (add_globals (g1, m) vars). - destruct (add_globals (g2, m) tvars'). + induction 2; simpl. + auto. + destruct a1 as [[id1 init1] info1]. + destruct b1 as [[id2 init2] info2]. + red in H0. destruct H0 as [X [Y Z]]. subst id2 init2. + generalize IHlist_forall2. + generalize (mem_add_globals_match g1 g2 m H1). + destruct (add_globals (g1, m) al). + destruct (add_globals (g2, m) bl). simpl. intros. congruence. Qed. -(* -Lemma prog_funct_transf_OK: - transf_partial_program transf p.(prog_funct) = Some p'.(prog_funct). +Theorem find_funct_ptr_match: + forall (b: block) (f: A), + find_funct_ptr (globalenv p) b = Some f -> + exists tf, find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf. Proof. - generalize transf_OK; unfold transform_partial_program. - case (transf_partial_program transf (prog_funct p)); simpl; intros. - injection transf_OK0; intros; subst p'. reflexivity. - discriminate. + intros until f. destruct match_prog as [X [Y Z]]. + destruct (add_functs_match X) as [P [Q R]]. + unfold find_funct_ptr. repeat rewrite functions_globalenv. + auto. Qed. -*) -Theorem find_funct_ptr_transf_partial2: - forall (b: block) (f: A), - find_funct_ptr (globalenv p) b = Some f -> - find_funct_ptr (globalenv p') b = transf_fun f /\ transf_fun f <> None. +Theorem find_funct_ptr_rev_match: + forall (b: block) (tf: B), + find_funct_ptr (globalenv p') b = Some tf -> + exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf. Proof. - intros until f. functional inversion transf_OK. - destruct (add_functs_transf _ H0) as [P [Q R]]. - unfold find_funct_ptr. repeat rewrite functions_globalenv. simpl. + intros until tf. destruct match_prog as [X [Y Z]]. + destruct (add_functs_rev_match X) as [P [Q R]]. + unfold find_funct_ptr. repeat rewrite functions_globalenv. auto. Qed. -Theorem find_funct_transf_partial2: +Theorem find_funct_match: forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> - find_funct (globalenv p') v = transf_fun f /\ transf_fun f <> None. + exists tf, find_funct (globalenv p') v = Some tf /\ match_fun f tf. Proof. intros until f. unfold find_funct. case v; try (intros; discriminate). intros b ofs. case (Int.eq ofs Int.zero); try (intros; discriminate). - apply find_funct_ptr_transf_partial2. + apply find_funct_ptr_match. Qed. -Lemma symbols_init_transf2: +Theorem find_funct_rev_match: + forall (v: val) (tf: B), + find_funct (globalenv p') v = Some tf -> + exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf. +Proof. + intros until tf. unfold find_funct. + case v; try (intros; discriminate). + intros b ofs. + case (Int.eq ofs Int.zero); try (intros; discriminate). + apply find_funct_ptr_rev_match. +Qed. + +Lemma symbols_init_match: symbols (globalenv p') = symbols (globalenv p). Proof. unfold globalenv. unfold globalenv_initmem. - functional inversion transf_OK. - destruct (add_functs_transf _ H0) as [P [Q R]]. - simpl. symmetry. apply symbols_add_globals_transf. auto. auto. + destruct match_prog as [X [Y Z]]. + destruct (add_functs_match X) as [P [Q R]]. + simpl. symmetry. apply symbols_add_globals_match. auto. auto. Qed. -Theorem find_symbol_transf_partial2: +Theorem find_symbol_match: forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. intros. unfold find_symbol. - rewrite symbols_init_transf2. auto. + rewrite symbols_init_match. auto. +Qed. + +Theorem init_mem_match: + init_mem p' = init_mem p. +Proof. + unfold init_mem. unfold globalenv_initmem. + destruct match_prog as [X [Y Z]]. + symmetry. apply mem_add_globals_match. auto. +Qed. + +End MATCH_PROGRAM. + +Section TRANSF_PROGRAM_PARTIAL2. + +Variable A B V W: Set. +Variable transf_fun: A -> res B. +Variable transf_var: V -> res W. +Variable p: program A V. +Variable p': program B W. +Hypothesis transf_OK: + transform_partial_program2 transf_fun transf_var p = OK p'. + +Remark prog_match: + match_program + (fun fd tfd => transf_fun fd = OK tfd) + (fun info tinfo => transf_var info = OK tinfo) + p p'. +Proof. + apply transform_partial_program2_match; auto. +Qed. + +Theorem find_funct_ptr_transf_partial2: + forall (b: block) (f: A), + find_funct_ptr (globalenv p) b = Some f -> + exists f', + find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'. +Proof. + intros. + exploit find_funct_ptr_match. eexact prog_match. eauto. + intros [tf [X Y]]. exists tf; auto. +Qed. + +Theorem find_funct_ptr_rev_transf_partial2: + forall (b: block) (tf: B), + find_funct_ptr (globalenv p') b = Some tf -> + exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf. +Proof. + intros. + exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto. +Qed. + +Theorem find_funct_transf_partial2: + forall (v: val) (f: A), + find_funct (globalenv p) v = Some f -> + exists f', + find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. +Proof. + intros. + exploit find_funct_match. eexact prog_match. eauto. + intros [tf [X Y]]. exists tf; auto. +Qed. + +Theorem find_funct_rev_transf_partial2: + forall (v: val) (tf: B), + find_funct (globalenv p') v = Some tf -> + exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf. +Proof. + intros. + exploit find_funct_rev_match. eexact prog_match. eauto. auto. +Qed. + +Theorem find_symbol_transf_partial2: + forall (s: ident), + find_symbol (globalenv p') s = find_symbol (globalenv p) s. +Proof. + intros. eapply find_symbol_match. eexact prog_match. Qed. Theorem init_mem_transf_partial2: init_mem p' = init_mem p. Proof. - unfold init_mem. unfold globalenv_initmem. - functional inversion transf_OK. - simpl. symmetry. apply mem_add_globals_transf. auto. + intros. eapply init_mem_match. eexact prog_match. Qed. End TRANSF_PROGRAM_PARTIAL2. - Section TRANSF_PROGRAM_PARTIAL. Variable A B V: Set. -Variable transf: A -> option B. +Variable transf: A -> res B. Variable p: program A V. Variable p': program B V. -Hypothesis transf_OK: transform_partial_program transf p = Some p'. +Hypothesis transf_OK: transform_partial_program transf p = OK p'. Remark transf2_OK: - transform_partial_program2 transf (fun x => Some x) p = Some p'. + transform_partial_program2 transf (fun x => OK x) p = OK p'. Proof. rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program. - destruct (map_partial transf (prog_funct p)); auto. + destruct (map_partial prefix_funct_name transf (prog_funct p)); auto. rewrite map_partial_identity; auto. Qed. Theorem find_funct_ptr_transf_partial: forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> - find_funct_ptr (globalenv p') b = transf f /\ transf f <> None. + exists f', + find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'. Proof. exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). Qed. +Theorem find_funct_ptr_rev_transf_partial: + forall (b: block) (tf: B), + find_funct_ptr (globalenv p') b = Some tf -> + exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf. +Proof. + exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). +Qed. + Theorem find_funct_transf_partial: forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> - find_funct (globalenv p') v = transf f /\ transf f <> None. + exists f', + find_funct (globalenv p') v = Some f' /\ transf f = OK f'. Proof. exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). Qed. +Theorem find_funct_rev_transf_partial: + forall (v: val) (tf: B), + find_funct (globalenv p') v = Some tf -> + exists f, find_funct (globalenv p) v = Some f /\ transf f = OK tf. +Proof. + exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). +Qed. + Theorem find_symbol_transf_partial: forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. @@ -663,7 +989,7 @@ Variable p: program A V. Let tp := transform_program transf p. Remark transf_OK: - transform_partial_program (fun x => Some (transf x)) p = Some tp. + transform_partial_program (fun x => OK (transf x)) p = OK tp. Proof. unfold tp, transform_program, transform_partial_program. rewrite map_partial_total. reflexivity. @@ -676,7 +1002,16 @@ Theorem find_funct_ptr_transf: Proof. intros. destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK _ _ H) - as [X Y]. auto. + as [f' [X Y]]. congruence. +Qed. + +Theorem find_funct_ptr_rev_transf: + forall (b: block) (tf: B), + find_funct_ptr (globalenv tp) b = Some tf -> + exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf. +Proof. + intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto. + intros [f [X Y]]. exists f; split. auto. congruence. Qed. Theorem find_funct_transf: @@ -686,7 +1021,16 @@ Theorem find_funct_transf: Proof. intros. destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK _ _ H) - as [X Y]. auto. + as [f' [X Y]]. congruence. +Qed. + +Theorem find_funct_rev_transf: + forall (v: val) (tf: B), + find_funct (globalenv tp) v = Some tf -> + exists f, find_funct (globalenv p) v = Some f /\ transf f = tf. +Proof. + intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto. + intros [f [X Y]]. exists f; split. auto. congruence. Qed. Theorem find_symbol_transf: diff --git a/common/Main.v b/common/Main.v index f472ec3..33bc783 100644 --- a/common/Main.v +++ b/common/Main.v @@ -1,40 +1,48 @@ -(** The compiler back-end and its proof of semantic preservation *) +(** The whole compiler and its proof of semantic preservation *) (** Libraries. *) Require Import Coqlib. Require Import Maps. +Require Import Errors. Require Import AST. Require Import Values. +Require Import Smallstep. (** Languages (syntax and semantics). *) Require Csyntax. Require Csem. Require Csharpminor. Require Cminor. +Require CminorSel. Require RTL. Require LTL. +Require LTLin. Require Linear. Require Mach. Require PPC. (** Translation passes. *) Require Cshmgen. Require Cminorgen. +Require Selection. Require RTLgen. Require Constprop. Require CSE. Require Allocation. Require Tunneling. Require Linearize. +Require Reload. Require Stacking. Require PPCgen. (** Type systems. *) Require Ctyping. Require RTLtyping. Require LTLtyping. +Require LTLintyping. Require Lineartyping. Require Machtyping. (** Proofs of semantic preservation and typing preservation. *) Require Cshmgenproof3. Require Cminorgenproof. +Require Selectionproof. Require RTLgenproof. Require Constpropproof. Require CSEproof. @@ -44,266 +52,234 @@ Require Tunnelingproof. Require Tunnelingtyping. Require Linearizeproof. Require Linearizetyping. +Require Reloadproof. +Require Reloadtyping. Require Stackingproof. Require Stackingtyping. -Require Machabstr2mach. +Require Machabstr2concr. Require PPCgenproof. +Open Local Scope string_scope. + (** * Composing the translation passes *) (** We first define useful monadic composition operators, along with funny (but convenient) notations. *) -Definition apply_total (A B: Set) (x: option A) (f: A -> B) : option B := - match x with None => None | Some x1 => Some (f x1) end. +Definition apply_total (A B: Set) (x: res A) (f: A -> B) : res B := + match x with Error msg => Error msg | OK x1 => OK (f x1) end. Definition apply_partial (A B: Set) - (x: option A) (f: A -> option B) : option B := - match x with None => None | Some x1 => f x1 end. + (x: res A) (f: A -> res B) : res B := + match x with Error msg => Error msg | OK x1 => f x1 end. Notation "a @@@ b" := (apply_partial _ _ a b) (at level 50, left associativity). Notation "a @@ b" := (apply_total _ _ a b) (at level 50, left associativity). -(** We define two translation functions for whole programs: one starting with - a C program, the other with a Cminor program. Both - translations produce PPC programs ready for pretty-printing and - assembling. +(** We define three translation functions for whole programs: one + starting with a C program, one with a Cminor program, one with an + RTL program. The three translations produce PPC programs ready for + pretty-printing and assembling. - There are two ways to compose the compiler passes. The first translates - every function from the Cminor program from Cminor to RTL, then to LTL, etc, - all the way to PPC, and iterates this transformation for every function. - The second translates the whole Cminor program to a RTL program, then to - an LTL program, etc. We follow the first approach because it has lower - memory requirements. + There are two ways to compose the compiler passes. The first + translates every function from the Cminor program from Cminor to + RTL, then to LTL, etc, all the way to PPC, and iterates this + transformation for every function. The second translates the whole + Cminor program to a RTL program, then to an LTL program, etc. + Between Cminor and PPC, we follow the first approach because it has + lower memory requirements. The translation from Clight to PPC + follows the second approach. - The translation of a Cminor function to a PPC function is as follows. *) + The translation of an RTL function to a PPC function is as follows. *) -Definition transf_cminor_fundef (f: Cminor.fundef) : option PPC.fundef := - Some f - @@@ RTLgen.transl_fundef +Definition transf_rtl_fundef (f: RTL.fundef) : res PPC.fundef := + OK f @@ Constprop.transf_fundef @@ CSE.transf_fundef @@@ Allocation.transf_fundef @@ Tunneling.tunnel_fundef @@ Linearize.transf_fundef + @@ Reload.transf_fundef @@@ Stacking.transf_fundef @@@ PPCgen.transf_fundef. +(* Here is the translation of a Cminor function to a PPC function. *) + +Definition transf_cminor_fundef (f: Cminor.fundef) : res PPC.fundef := + OK f + @@ Selection.sel_fundef + @@@ RTLgen.transl_fundef + @@@ transf_rtl_fundef. + (** The corresponding translations for whole program follow. *) -Definition transf_cminor_program (p: Cminor.program) : option PPC.program := +Definition transf_rtl_program (p: RTL.program) : res PPC.program := + transform_partial_program transf_rtl_fundef p. + +Definition transf_cminor_program (p: Cminor.program) : res PPC.program := transform_partial_program transf_cminor_fundef p. -Definition transf_c_program (p: Csyntax.program) : option PPC.program := +Definition transf_c_program (p: Csyntax.program) : res PPC.program := match Ctyping.typecheck_program p with - | false => None + | false => + Error (msg "Ctyping: type error") | true => - Some p + OK p @@@ Cshmgen.transl_program @@@ Cminorgen.transl_program @@@ transf_cminor_program end. -(** * Equivalence with whole program transformations *) - -(** To prove semantic preservation for the whole compiler, it is easier to reason - over the second way to compose the compiler pass: the one that translate - whole programs through each compiler pass. We now define this second translation - and prove that it produces the same PPC programs as the first translation. *) - -Definition transf_cminor_program2 (p: Cminor.program) : option PPC.program := - Some p - @@@ RTLgen.transl_program - @@ Constprop.transf_program - @@ CSE.transf_program - @@@ Allocation.transf_program - @@ Tunneling.tunnel_program - @@ Linearize.transf_program - @@@ Stacking.transf_program - @@@ PPCgen.transf_program. +(** The following lemmas help reason over compositions of passes. *) Lemma map_partial_compose: forall (X A B C: Set) - (f1: A -> option B) (f2: B -> option C) - (p: list (X * A)), - map_partial f1 p @@@ map_partial f2 = - map_partial (fun f => f1 f @@@ f2) p. + (ctx: X -> errmsg) + (f1: A -> res B) (f2: B -> res C) + (pa: list (X * A)) (pc: list (X * C)), + map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc -> + exists pb, map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc. Proof. - induction p. simpl. auto. - simpl. destruct a. destruct (f1 a). - simpl. simpl in IHp. destruct (map_partial f1 p). - simpl. simpl in IHp. destruct (f2 b). - destruct (map_partial f2 l). - rewrite <- IHp. auto. - rewrite <- IHp. auto. - auto. - simpl. rewrite <- IHp. simpl. destruct (f2 b); auto. - simpl. auto. + induction pa; simpl. + intros. inv H. econstructor; eauto. + intro pc. destruct a as [x a]. + caseEq (f1 a); simpl; try congruence. intros b F1. + caseEq (f2 b); simpl; try congruence. intros c F2 EQ. + monadInv EQ. exploit IHpa; eauto. intros [pb [P Q]]. + rewrite P; simpl. + exists ((x, b) :: pb); split. auto. simpl. rewrite F2. rewrite Q. auto. Qed. -(* -Lemma transform_partial_program2_compose: - forall (A B C V W X: Set) - (f1: A -> option B) (g1: V -> option W) - (f2: B -> option C) (g2: W -> option X) - (p: program A V), - transform_partial_program2 f1 g1 p @@@ - (fun p' => transform_partial_program2 f2 g2 p') = - transform_partial_program2 (fun x => f1 x @@@ f2) (fun x => g1 x @@@ g2) p. +Lemma transform_partial_program_compose: + forall (A B C V: Set) + (f1: A -> res B) (f2: B -> res C) + (pa: program A V) (pc: program C V), + transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc -> + exists pb, transform_partial_program f1 pa = OK pb /\ + transform_partial_program f2 pb = OK pc. Proof. - unfold transform_partial_program2; intros. - rewrite <- map_partial_compose; simpl. - rewrite <- map_partial_compose; simpl. - destruct (map_partial f1 (prog_funct p)); simpl; auto. - destruct (map_partial g1 (prog_vars p)); simpl; auto. - destruct (map_partial f2 l); auto. + intros. monadInv H. + exploit map_partial_compose; eauto. intros [xb [P Q]]. + exists (mkprogram xb (prog_main pa) (prog_vars pa)); split. + unfold transform_partial_program. rewrite P; auto. + unfold transform_partial_program. simpl. rewrite Q; auto. Qed. -Lemma transform_program_partial2_partial: - forall (A B V: Set) (f: A -> option B) (p: program A V), - transform_partial_program f p = - transform_partial_program2 f (fun x => Some x) p. +Lemma transform_program_partial_program: + forall (A B V: Set) (f: A -> B) (p: program A V) (tp: program B V), + transform_partial_program (fun x => OK (f x)) p = OK tp -> + transform_program f p = tp. Proof. - intros. unfold transform_partial_program, transform_partial_program2. - rewrite map_partial_identity. auto. + intros until tp. unfold transform_partial_program. + rewrite map_partial_total. simpl. intros. inv H. auto. Qed. -Lemma apply_partial_transf_program: - forall (A B V: Set) (f: A -> option B) (x: option (program A V)), - x @@@ (fun p => transform_partial_program f p) = - x @@@ (fun p => transform_partial_program2 f (fun x => Some x) p). -Proof. - intros. unfold apply_partial. - destruct x. apply transform_program_partial2_partial. auto. -Qed. -*) -Lemma transform_partial_program_compose: +Lemma transform_program_compose: forall (A B C V: Set) - (f1: A -> option B) (f2: B -> option C) - (p: program A V), - transform_partial_program f1 p @@@ - (fun p' => transform_partial_program f2 p') = - transform_partial_program (fun f => f1 f @@@ f2) p. + (f1: A -> res B) (f2: B -> C) + (pa: program A V) (pc: program C V), + transform_partial_program (fun f => f1 f @@ f2) pa = OK pc -> + exists pb, transform_partial_program f1 pa = OK pb /\ + transform_program f2 pb = pc. Proof. - unfold transform_partial_program; intros. - rewrite <- map_partial_compose. simpl. - destruct (map_partial f1 (prog_funct p)); simpl. - auto. auto. + intros. + replace (fun f : A => f1 f @@ f2) + with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H. + exploit transform_partial_program_compose; eauto. + intros [pb [X Y]]. exists pb; split. auto. + apply transform_program_partial_program. auto. + apply extensionality; intro. destruct(f1 x); auto. Qed. -Lemma transform_program_partial_total: - forall (A B V: Set) (f: A -> B) (p: program A V), - Some (transform_program f p) = - transform_partial_program (fun x => Some (f x)) p. +Lemma transform_partial_program_identity: + forall (A V: Set) (pa pb: program A V), + transform_partial_program (@OK A) pa = OK pb -> + pa = pb. Proof. - intros. unfold transform_program, transform_partial_program. - rewrite map_partial_total. auto. + intros until pb. unfold transform_partial_program. + replace (@OK A) with (fun b => @OK A b). + rewrite map_partial_identity. simpl. destruct pa; simpl; congruence. + apply extensionality; auto. Qed. -Lemma apply_total_transf_program: - forall (A B V: Set) (f: A -> B) (x: option (program A V)), - x @@ (fun p => transform_program f p) = - x @@@ (fun p => transform_partial_program (fun x => Some (f x)) p). -Proof. - intros. unfold apply_total, apply_partial. - destruct x. apply transform_program_partial_total. auto. -Qed. +(** * Semantic preservation *) -Lemma transf_cminor_program_equiv: - forall p, transf_cminor_program2 p = transf_cminor_program p. -Proof. - intro. unfold transf_cminor_program, transf_cminor_program2, transf_cminor_fundef. - simpl. - unfold RTLgen.transl_program, - Constprop.transf_program, RTL.program. - rewrite apply_total_transf_program. - rewrite transform_partial_program_compose. - unfold CSE.transf_program, RTL.program. - rewrite apply_total_transf_program. - rewrite transform_partial_program_compose. - unfold Allocation.transf_program, - LTL.program, RTL.program. - rewrite transform_partial_program_compose. - unfold Tunneling.tunnel_program, LTL.program. - rewrite apply_total_transf_program. - rewrite transform_partial_program_compose. - unfold Linearize.transf_program, LTL.program, Linear.program. - rewrite apply_total_transf_program. - rewrite transform_partial_program_compose. - unfold Stacking.transf_program, Linear.program, Mach.program. - rewrite transform_partial_program_compose. - unfold PPCgen.transf_program, Mach.program, PPC.program. - rewrite transform_partial_program_compose. - reflexivity. -Qed. +(** We prove that the [transf_program] translations preserve semantics. + The proof composes the semantic preservation results for each pass. + This establishes the correctness of the whole compiler! *) -(* -Lemma transf_csharpminor_program_equiv: - forall p, transf_csharpminor_program2 p = transf_csharpminor_program p. +Theorem transf_rtl_program_correct: + forall p tp beh, + transf_rtl_program p = OK tp -> + RTL.exec_program p beh -> + PPC.exec_program tp beh. Proof. - intros. - unfold transf_csharpminor_program2, transf_csharpminor_program, transf_csharpminor_fundef. - simpl. - replace transf_cminor_program2 with transf_cminor_program. - unfold transf_cminor_program, Cminorgen.transl_program, Cminor.program, PPC.program. - rewrite apply_partial_transf_program. - rewrite transform_partial_program2_compose. - reflexivity. - symmetry. apply extensionality. exact transf_cminor_program_equiv. -Qed. -*) + intros. unfold transf_rtl_program, transf_rtl_fundef in H. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p7 [H7 P7]]. + clear H. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H7) as [p6 [H6 P6]]. + clear H7. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H6) as [p5 [H5 P5]]. + clear H6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H5) as [p4 [H4 P4]]. + clear H5. generalize (transform_program_partial_program _ _ _ _ _ _ P4). clear P4. intro P4. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H4) as [p3 [H3 P3]]. + clear H4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]]. + clear H3. + destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]]. + clear H2. + destruct (transform_program_compose _ _ _ _ _ _ _ _ H1) as [p0 [H00 P0]]. + clear H1. + generalize (transform_partial_program_identity _ _ _ _ H00). clear H00. intro. subst p0. -(** * Semantic preservation *) + assert (WT3 : LTLtyping.wt_program p3). + apply Alloctyping.program_typing_preserved with p2. auto. + assert (WT4 : LTLtyping.wt_program p4). + subst p4. apply Tunnelingtyping.program_typing_preserved. auto. + assert (WT5 : LTLintyping.wt_program p5). + subst p5. apply Linearizetyping.program_typing_preserved. auto. + assert (WT6 : Lineartyping.wt_program p6). + subst p6. apply Reloadtyping.program_typing_preserved. auto. + assert (WT7: Machtyping.wt_program p7). + apply Stackingtyping.program_typing_preserved with p6. auto. auto. -(** We prove that the [transf_program] translations preserve semantics. The proof - composes the semantic preservation results for each pass. - This establishes the correctness of the whole compiler! *) + apply PPCgenproof.transf_program_correct with p7; auto. + apply Machabstr2concr.exec_program_equiv; auto. + apply Stackingproof.transf_program_correct with p6; auto. + subst p6; apply Reloadproof.transf_program_correct; auto. + subst p5; apply Linearizeproof.transf_program_correct; auto. + subst p4; apply Tunnelingproof.transf_program_correct. + apply Allocproof.transf_program_correct with p2; auto. + subst p2; apply CSEproof.transf_program_correct. + subst p1; apply Constpropproof.transf_program_correct. auto. +Qed. Theorem transf_cminor_program_correct: forall p tp t n, - transf_cminor_program p = Some tp -> + transf_cminor_program p = OK tp -> Cminor.exec_program p t (Vint n) -> - PPC.exec_program tp t (Vint n). + PPC.exec_program tp (Terminates t n). Proof. - intros until n. - rewrite <- transf_cminor_program_equiv. - unfold transf_cminor_program2. - simpl. caseEq (RTLgen.transl_program p). intros p1 EQ1. - simpl. set (p2 := CSE.transf_program (Constprop.transf_program p1)). - caseEq (Allocation.transf_program p2). intros p3 EQ3. - simpl. set (p4 := Tunneling.tunnel_program p3). - set (p5 := Linearize.transf_program p4). - caseEq (Stacking.transf_program p5). intros p6 EQ6. - simpl. intros EQTP EXEC. - assert (WT3 : LTLtyping.wt_program p3). - apply Alloctyping.program_typing_preserved with p2. auto. - assert (WT4 : LTLtyping.wt_program p4). - unfold p4. apply Tunnelingtyping.program_typing_preserved. auto. - assert (WT5 : Lineartyping.wt_program p5). - unfold p5. apply Linearizetyping.program_typing_preserved. auto. - assert (WT6: Machtyping.wt_program p6). - apply Stackingtyping.program_typing_preserved with p5. auto. auto. - apply PPCgenproof.transf_program_correct with p6; auto. - apply Machabstr2mach.exec_program_equiv; auto. - apply Stackingproof.transl_program_correct with p5; auto. - unfold p5; apply Linearizeproof.transf_program_correct. - unfold p4; apply Tunnelingproof.transf_program_correct. - apply Allocproof.transl_program_correct with p2; auto. - unfold p2; apply CSEproof.transf_program_correct; - apply Constpropproof.transf_program_correct. - apply RTLgenproof.transl_program_correct with p; auto. - simpl; intros; discriminate. - simpl; intros; discriminate. - simpl; intros; discriminate. + intros. unfold transf_cminor_program, transf_cminor_fundef in H. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [H3 P3]]. + clear H. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]]. + clear H3. + destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]]. + generalize (transform_partial_program_identity _ _ _ _ H1). clear H1. intro. subst p1. + apply transf_rtl_program_correct with p3. auto. + apply RTLgenproof.transl_program_correct with p2; auto. + rewrite <- P1. apply Selectionproof.sel_program_correct; auto. Qed. Theorem transf_c_program_correct: forall p tp t n, - transf_c_program p = Some tp -> + transf_c_program p = OK tp -> Csem.exec_program p t (Vint n) -> - PPC.exec_program tp t (Vint n). + PPC.exec_program tp (Terminates t n). Proof. intros until n; unfold transf_c_program; simpl. caseEq (Ctyping.typecheck_program p); try congruence; intro. diff --git a/common/Mem.v b/common/Mem.v index 679c41e..6b66d9d 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -1,11 +1,11 @@ (** This file develops the memory model that is used in the dynamic - semantics of all the languages of the compiler back-end. + semantics of all the languages used in the compiler. It defines a type [mem] of memory states, the following 4 basic operations over memory states, and their properties: -- [alloc]: allocate a fresh memory block; -- [free]: invalidate a memory block; - [load]: read a memory chunk at a given address; -- [store]: store a memory chunk at a given address. +- [store]: store a memory chunk at a given address; +- [alloc]: allocate a fresh memory block; +- [free]: invalidate a memory block. *) Require Import Coqlib. @@ -15,12 +15,6 @@ Require Import Integers. Require Import Floats. Require Import Values. -(** * Structure of memory states *) - -(** A memory state is organized in several disjoint blocks. Each block - has a low and a high bound that defines its size. Each block map - byte offsets to the contents of this byte. *) - Definition update (A: Set) (x: Z) (v: A) (f: Z -> A) : Z -> A := fun y => if zeq y x then v else f y. @@ -40,32 +34,32 @@ Proof. intros; unfold update. apply zeq_false; auto. Qed. +(** * Structure of memory states *) + +(** A memory state is organized in several disjoint blocks. Each block + has a low and a high bound that defines its size. Each block map + byte offsets to the contents of this byte. *) + (** The possible contents of a byte-sized memory cell. To give intuitions, a 4-byte value [v] stored at offset [d] will be represented by - the content [Datum32 v] at offset [d] and [Cont] at offsets [d+1], + the content [Datum(4, v)] at offset [d] and [Cont] at offsets [d+1], [d+2] and [d+3]. The [Cont] contents enable detecting future writes - that would overlap partially the 4-byte value. *) + that would partially overlap the 4-byte value. *) Inductive content : Set := - | Undef: content (**r undefined contents *) - | Datum8: val -> content (**r a value that fits in 1 byte *) - | Datum16: val -> content (**r first byte of a 2-byte value *) - | Datum32: val -> content (**r first byte of a 4-byte value *) - | Datum64: val -> content (**r first byte of a 8-byte value *) - | Cont: content. (**r continuation bytes for a multi-byte value *) + | Undef: content (**r undefined contents *) + | Datum: nat -> val -> content (**r first byte of a value *) + | Cont: content. (**r continuation bytes for a multi-byte value *) Definition contentmap : Set := Z -> content. (** A memory block comprises the dimensions of the block (low and high bounds) - plus a mapping from byte offsets to contents. For technical reasons, - we also carry around a proof that the mapping is equal to [Undef] - outside the range of allowed byte offsets. *) + plus a mapping from byte offsets to contents. *) Record block_contents : Set := mkblock { low: Z; high: Z; - contents: contentmap; - undef_outside: forall ofs, ofs < low \/ ofs >= high -> contents ofs = Undef + contents: contentmap }. (** A memory state is a mapping from block addresses (represented by [Z] @@ -82,49 +76,43 @@ Record mem : Set := mkmem { (** Memory reads and writes are performed by quantities called memory chunks, encoding the type, size and signedness of the chunk being addressed. - It is useful to extract only the size information as given by the - following [memory_size] type. *) - -Inductive memory_size : Set := - | Size8: memory_size - | Size16: memory_size - | Size32: memory_size - | Size64: memory_size. - -Definition size_mem (sz: memory_size) := - match sz with - | Size8 => 1 - | Size16 => 2 - | Size32 => 4 - | Size64 => 8 + The following functions extract the size information from a chunk. *) + +Definition size_chunk (chunk: memory_chunk) : Z := + match chunk with + | Mint8signed => 1 + | Mint8unsigned => 1 + | Mint16signed => 2 + | Mint16unsigned => 2 + | Mint32 => 4 + | Mfloat32 => 4 + | Mfloat64 => 8 end. -Definition mem_chunk (chunk: memory_chunk) := +Definition pred_size_chunk (chunk: memory_chunk) : nat := match chunk with - | Mint8signed => Size8 - | Mint8unsigned => Size8 - | Mint16signed => Size16 - | Mint16unsigned => Size16 - | Mint32 => Size32 - | Mfloat32 => Size32 - | Mfloat64 => Size64 + | Mint8signed => 0%nat + | Mint8unsigned => 0%nat + | Mint16signed => 1%nat + | Mint16unsigned => 1%nat + | Mint32 => 3%nat + | Mfloat32 => 3%nat + | Mfloat64 => 7%nat end. -Definition size_chunk (chunk: memory_chunk) := size_mem (mem_chunk chunk). +Lemma size_chunk_pred: + forall chunk, size_chunk chunk = 1 + Z_of_nat (pred_size_chunk chunk). +Proof. + destruct chunk; auto. +Qed. (** The initial store. *) Remark one_pos: 1 > 0. Proof. omega. Qed. -Remark undef_undef_outside: - forall lo hi ofs, ofs < lo \/ ofs >= hi -> (fun y => Undef) ofs = Undef. -Proof. - auto. -Qed. - Definition empty_block (lo hi: Z) : block_contents := - mkblock lo hi (fun y => Undef) (undef_undef_outside lo hi). + mkblock lo hi (fun y => Undef). Definition empty: mem := mkmem (fun x => empty_block 0 0) 1 one_pos. @@ -200,8 +188,16 @@ Fixpoint check_cont (n: nat) (p: Z) (m: contentmap) {struct n} : bool := end end. -Definition getN (n: nat) (p: Z) (m: contentmap) : content := - if check_cont n (p + 1) m then m p else Undef. +Definition eq_nat: forall (p q: nat), {p=q} + {p<>q}. +Proof. decide equality. Defined. + +Definition getN (n: nat) (p: Z) (m: contentmap) : val := + match m p with + | Datum n' v => + if eq_nat n n' && check_cont n (p + 1) m then v else Vundef + | _ => + Vundef + end. Fixpoint set_cont (n: nat) (p: Z) (m: contentmap) {struct n} : contentmap := match n with @@ -209,54 +205,47 @@ Fixpoint set_cont (n: nat) (p: Z) (m: contentmap) {struct n} : contentmap := | S n1 => update p Cont (set_cont n1 (p + 1) m) end. -Definition setN (n: nat) (p: Z) (v: content) (m: contentmap) : contentmap := - update p v (set_cont n (p + 1) m). +Definition setN (n: nat) (p: Z) (v: val) (m: contentmap) : contentmap := + update p (Datum n v) (set_cont n (p + 1) m). -Lemma check_cont_true: - forall n p m, - (forall q, p <= q < p + Z_of_nat n -> m q = Cont) -> - check_cont n p m = true. +Lemma check_cont_spec: + forall n m p, + if check_cont n p m + then (forall q, p <= q < p + Z_of_nat n -> m q = Cont) + else (exists q, p <= q < p + Z_of_nat n /\ m q <> Cont). Proof. induction n; intros. - reflexivity. - simpl. rewrite H. apply IHn. - intros. apply H. rewrite inj_S. omega. - rewrite inj_S. omega. + simpl. intros; omegaContradiction. + simpl check_cont. repeat rewrite inj_S. caseEq (m p); intros. + exists p; split. omega. congruence. + exists p; split. omega. congruence. + generalize (IHn m (p + 1)). case (check_cont n (p + 1) m). + intros. assert (p = q \/ p + 1 <= q < p + Zsucc (Z_of_nat n)) by omega. + elim H2; intro. congruence. apply H0; omega. + intros [q [A B]]. exists q; split. omega. auto. Qed. -Hint Resolve check_cont_true. - -Lemma check_cont_inv: - forall n p m, - check_cont n p m = true -> - (forall q, p <= q < p + Z_of_nat n -> m q = Cont). +Lemma check_cont_true: + forall n m p, + (forall q, p <= q < p + Z_of_nat n -> m q = Cont) -> + check_cont n p m = true. Proof. - induction n; intros until m. - unfold Z_of_nat. intros. omegaContradiction. - unfold check_cont; fold check_cont. - caseEq (m p); intros; try discriminate. - assert (p = q \/ p + 1 <= q < (p + 1) + Z_of_nat n). - rewrite inj_S in H1. omega. - elim H2; intro. - subst q. auto. - apply IHn with (p + 1); auto. + intros. generalize (check_cont_spec n m p). + destruct (check_cont n p m). auto. + intros [q [A B]]. elim B; auto. Qed. -Hint Resolve check_cont_inv. - Lemma check_cont_false: - forall n p q m, - p <= q < p + Z_of_nat n -> - m q <> Cont -> + forall n m p q, + p <= q < p + Z_of_nat n -> m q <> Cont -> check_cont n p m = false. Proof. - intros. caseEq (check_cont n p m); intro. - generalize (check_cont_inv _ _ _ H1 q H). intro. contradiction. + intros. generalize (check_cont_spec n m p). + destruct (check_cont n p m). + intros. elim H0; auto. auto. Qed. -Hint Resolve check_cont_false. - Lemma set_cont_inside: forall n p m q, p <= q < p + Z_of_nat n -> @@ -273,8 +262,6 @@ Proof. red; intro; subst q. omega. Qed. -Hint Resolve set_cont_inside. - Lemma set_cont_outside: forall n p m q, q < p \/ p + Z_of_nat n <= q -> @@ -286,160 +273,133 @@ Proof. rewrite update_o. apply IHn. omega. omega. Qed. -Hint Resolve set_cont_outside. - Lemma getN_setN_same: forall n p v m, getN n p (setN n p v m) = v. Proof. - intros. unfold getN, setN. - rewrite check_cont_true. apply update_s. + intros. unfold getN, setN. rewrite update_s. + rewrite check_cont_true. unfold proj_sumbool. + rewrite dec_eq_true. auto. intros. rewrite update_o. apply set_cont_inside. auto. omega. Qed. -Hint Resolve getN_setN_same. - Lemma getN_setN_other: forall n1 n2 p1 p2 v m, p1 + Z_of_nat n1 < p2 \/ p2 + Z_of_nat n2 < p1 -> getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m. Proof. intros. unfold getN, setN. - caseEq (check_cont n2 (p2 + 1) m); intro. - rewrite check_cont_true. rewrite update_o. - apply set_cont_outside. omega. omega. - intros. rewrite update_o. rewrite set_cont_outside. - eapply check_cont_inv. eauto. auto. + generalize (check_cont_spec n2 m (p2 + 1)); + destruct (check_cont n2 (p2 + 1) m); intros. + rewrite check_cont_true. + rewrite update_o. rewrite set_cont_outside. auto. omega. omega. - caseEq (check_cont n2 (p2 + 1) (update p1 v (set_cont n1 (p1 + 1) m))); intros. - assert (check_cont n2 (p2 + 1) m = true). - apply check_cont_true. intros. - generalize (check_cont_inv _ _ _ H1 q H2). - rewrite update_o. rewrite set_cont_outside. auto. omega. omega. - rewrite H0 in H2; discriminate. - auto. -Qed. - -Hint Resolve getN_setN_other. + intros. rewrite update_o. rewrite set_cont_outside. auto. + omega. omega. + destruct H0 as [q [A B]]. + rewrite (check_cont_false n2 (update p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) q). + rewrite update_o. rewrite set_cont_outside. auto. + omega. omega. omega. + rewrite update_o. rewrite set_cont_outside. auto. + omega. omega. +Qed. Lemma getN_setN_overlap: forall n1 n2 p1 p2 v m, p1 <> p2 -> p1 + Z_of_nat n1 >= p2 -> p2 + Z_of_nat n2 >= p1 -> - v <> Cont -> - getN n2 p2 (setN n1 p1 v m) = Cont \/ - getN n2 p2 (setN n1 p1 v m) = Undef. -Proof. - intros. unfold getN. - caseEq (check_cont n2 (p2 + 1) (setN n1 p1 v m)); intro. - case (zlt p2 p1); intro. - assert (p2 + 1 <= p1 < p2 + 1 + Z_of_nat n2). omega. - generalize (check_cont_inv _ _ _ H3 p1 H4). - unfold setN. rewrite update_s. intro. contradiction. - left. unfold setN. rewrite update_o. - apply set_cont_inside. omega. auto. - right; auto. -Qed. - -Hint Resolve getN_setN_overlap. + getN n2 p2 (setN n1 p1 v m) = Vundef. +Proof. + intros. unfold getN, setN. + rewrite update_o; auto. + destruct (zlt p2 p1). + (* [p1] belongs to [[p2, p2 + n2 - 1]], + therefore [check_cont n2 (p2 + 1) ...] is false. *) + rewrite (check_cont_false n2 (update p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) p1). + destruct (set_cont n1 (p1 + 1) m p2); auto. + destruct (eq_nat n2 n); auto. + omega. + rewrite update_s. congruence. + (* [p2] belongs to [[p1 + 1, p1 + n1 - 1]], + therefore [set_cont n1 (p1 + 1) m p2] is [Cont]. *) + rewrite set_cont_inside. auto. omega. +Qed. Lemma getN_setN_mismatch: forall n1 n2 p v m, - getN n2 p (setN n1 p v m) = v \/ getN n2 p (setN n1 p v m) = Undef. + n1 <> n2 -> + getN n2 p (setN n1 p v m) = Vundef. Proof. - intros. unfold getN. - caseEq (check_cont n2 (p + 1) (setN n1 p v m)); intro. - left. unfold setN. apply update_s. - right. auto. + intros. unfold getN, setN. rewrite update_s. + unfold proj_sumbool; rewrite dec_eq_false; simpl. auto. auto. Qed. -Hint Resolve getN_setN_mismatch. +Lemma getN_setN_characterization: + forall m v n1 p1 n2 p2, + getN n2 p2 (setN n1 p1 v m) = v + \/ getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m + \/ getN n2 p2 (setN n1 p1 v m) = Vundef. +Proof. + intros. destruct (zeq p1 p2). subst p2. + destruct (eq_nat n1 n2). subst n2. + left; apply getN_setN_same. + right; right; apply getN_setN_mismatch; auto. + destruct (zlt (p1 + Z_of_nat n1) p2). + right; left; apply getN_setN_other; auto. + destruct (zlt (p2 + Z_of_nat n2) p1). + right; left; apply getN_setN_other; auto. + right; right; apply getN_setN_overlap; omega. +Qed. Lemma getN_init: forall n p, - getN n p (fun y => Undef) = Undef. + getN n p (fun y => Undef) = Vundef. Proof. - intros. unfold getN. - case (check_cont n (p + 1) (fun y => Undef)); auto. + intros. auto. Qed. -Hint Resolve getN_init. +(** [valid_access m chunk b ofs] holds if a memory access (load or store) + of the given chunk is possible in [m] at address [b, ofs]. *) + +Inductive valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) : Prop := + | valid_access_intro: + valid_block m b -> + low_bound m b <= ofs -> + ofs + size_chunk chunk <= high_bound m b -> + valid_access m chunk b ofs. (** The following function checks whether accessing the given memory chunk at the given offset in the given block respects the bounds of the block. *) -Definition in_bounds (chunk: memory_chunk) (ofs: Z) (c: block_contents) : - {c.(low) <= ofs /\ ofs + size_chunk chunk <= c.(high)} - + {c.(low) > ofs \/ ofs + size_chunk chunk > c.(high)} := - match zle c.(low) ofs, zle (ofs + size_chunk chunk) c.(high) with - | left P1, left P2 => left _ (conj P1 P2) - | left P1, right P2 => right _ (or_intror _ P2) - | right P1, _ => right _ (or_introl _ P1) - end. - -Lemma in_bounds_holds: - forall (chunk: memory_chunk) (ofs: Z) (c: block_contents) - (A: Set) (a b: A), - c.(low) <= ofs -> ofs + size_chunk chunk <= c.(high) -> - (if in_bounds chunk ofs c then a else b) = a. +Definition in_bounds (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) : + {valid_access m chunk b ofs} + {~valid_access m chunk b ofs}. Proof. - intros. case (in_bounds chunk ofs c); intro. - auto. - omegaContradiction. -Qed. + intros. + destruct (zlt b m.(nextblock)). + destruct (zle (low_bound m b) ofs). + destruct (zle (ofs + size_chunk chunk) (high_bound m b)). + left; constructor; auto. + right; red; intro V; inv V; omega. + right; red; intro V; inv V; omega. + right; red; intro V; inv V; contradiction. +Defined. -Lemma in_bounds_exten: - forall (chunk: memory_chunk) (ofs: Z) (c: block_contents) (x: contentmap) P, - in_bounds chunk ofs (mkblock (low c) (high c) x P) = - in_bounds chunk ofs c. +Lemma in_bounds_true: + forall m chunk b ofs (A: Set) (a1 a2: A), + valid_access m chunk b ofs -> + (if in_bounds m chunk b ofs then a1 else a2) = a1. Proof. - intros; reflexivity. + intros. destruct (in_bounds m chunk b ofs). auto. contradiction. Qed. -Hint Resolve in_bounds_holds in_bounds_exten. - (** [valid_pointer] holds if the given block address is valid and the given offset falls within the bounds of the corresponding block. *) Definition valid_pointer (m: mem) (b: block) (ofs: Z) : bool := - if zlt b m.(nextblock) then - (let c := m.(blocks) b in - if zle c.(low) ofs then if zlt ofs c.(high) then true else false - else false) - else false. - -(** Read a quantity of size [sz] at offset [ofs] in block contents [c]. - Return [Vundef] if the requested size does not match that of the - current contents, or if the following offsets do not contain [Cont]. - The first check captures a size mismatch between the read and the - latest write at this offset. The second check captures partial overwriting - of the latest write at this offset by a more recent write at a nearby - offset. *) - -Definition load_contents (sz: memory_size) (c: contentmap) (ofs: Z) : val := - match sz with - | Size8 => - match getN 0%nat ofs c with - | Datum8 n => n - | _ => Vundef - end - | Size16 => - match getN 1%nat ofs c with - | Datum16 n => n - | _ => Vundef - end - | Size32 => - match getN 3%nat ofs c with - | Datum32 n => n - | _ => Vundef - end - | Size64 => - match getN 7%nat ofs c with - | Datum64 n => n - | _ => Vundef - end - end. + zlt b m.(nextblock) && + zle (low_bound m b) ofs && + zlt ofs (high_bound m b). (** [load chunk m b ofs] perform a read in memory state [m], at address [b] and offset [ofs]. [None] is returned if the address is invalid @@ -447,15 +407,25 @@ Definition load_contents (sz: memory_size) (c: contentmap) (ofs: Z) : val := Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) : option val := - if zlt b m.(nextblock) then - (let c := m.(blocks) b in - if in_bounds chunk ofs c - then Some (Val.load_result chunk - (load_contents (mem_chunk chunk) c.(contents) ofs)) - else None) + if in_bounds m chunk b ofs then + Some (Val.load_result chunk + (getN (pred_size_chunk chunk) ofs (contents (blocks m b)))) else None. +Lemma load_inv: + forall chunk m b ofs v, + load chunk m b ofs = Some v -> + valid_access m chunk b ofs /\ + v = Val.load_result chunk + (getN (pred_size_chunk chunk) ofs (contents (blocks m b))). +Proof. + intros until v; unfold load. + destruct (in_bounds m chunk b ofs); intros. + split. auto. congruence. + congruence. +Qed. + (** [loadv chunk m addr] is similar, but the address and offset are given as a single value [addr], which must be a pointer value. *) @@ -465,90 +435,17 @@ Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val := | _ => None end. -Theorem load_in_bounds: - forall (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z), - valid_block m b -> - low_bound m b <= ofs -> - ofs + size_chunk chunk <= high_bound m b -> - exists v, load chunk m b ofs = Some v. -Proof. - intros. unfold load. rewrite zlt_true; auto. - rewrite in_bounds_holds. - exists (Val.load_result chunk - (load_contents (mem_chunk chunk) - (contents (m.(blocks) b)) - ofs)). - auto. - exact H0. exact H1. -Qed. - -Lemma load_inv: - forall (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val), - load chunk m b ofs = Some v -> - let c := m.(blocks) b in - b < m.(nextblock) /\ - c.(low) <= ofs /\ - ofs + size_chunk chunk <= c.(high) /\ - Val.load_result chunk (load_contents (mem_chunk chunk) c.(contents) ofs) = v. -Proof. - intros until v; unfold load. - case (zlt b (nextblock m)); intro. - set (c := m.(blocks) b). - case (in_bounds chunk ofs c). - intuition congruence. - intros; discriminate. - intros; discriminate. -Qed. -Hint Resolve load_in_bounds load_inv. - -(* Write the value [v] with size [sz] at offset [ofs] in block contents [c]. - Return updated block contents. [Cont] contents are stored at the following - offsets. *) - -Definition store_contents (sz: memory_size) (c: contentmap) - (ofs: Z) (v: val) : contentmap := - match sz with - | Size8 => - setN 0%nat ofs (Datum8 v) c - | Size16 => - setN 1%nat ofs (Datum16 v) c - | Size32 => - setN 3%nat ofs (Datum32 v) c - | Size64 => - setN 7%nat ofs (Datum64 v) c - end. - -Remark store_contents_undef_outside: - forall sz c ofs v lo hi, - lo <= ofs /\ ofs + size_mem sz <= hi -> - (forall x, x < lo \/ x >= hi -> c x = Undef) -> - (forall x, x < lo \/ x >= hi -> - store_contents sz c ofs v x = Undef). -Proof. - intros until hi; intros [LO HI] UO. - assert (forall n d x, - ofs + (1 + Z_of_nat n) <= hi -> - x < lo \/ x >= hi -> - setN n ofs d c x = Undef). - intros. unfold setN. rewrite update_o. - transitivity (c x). apply set_cont_outside. omega. - apply UO. omega. omega. - unfold store_contents; destruct sz; unfold size_mem in HI; - intros; apply H; auto; simpl Z_of_nat; auto. -Qed. +(* The memory state [m] after a store of value [v] at offset [ofs] + in block [b]. *) Definition unchecked_store (chunk: memory_chunk) (m: mem) (b: block) - (ofs: Z) (v: val) - (P: (m.(blocks) b).(low) <= ofs /\ - ofs + size_chunk chunk <= (m.(blocks) b).(high)) : mem := + (ofs: Z) (v: val) : mem := let c := m.(blocks) b in mkmem (update b (mkblock c.(low) c.(high) - (store_contents (mem_chunk chunk) c.(contents) ofs v) - (store_contents_undef_outside (mem_chunk chunk) c.(contents) - ofs v _ _ P c.(undef_outside))) + (setN (pred_size_chunk chunk) ofs v c.(contents))) m.(blocks)) m.(nextblock) m.(nextblock_pos). @@ -560,13 +457,21 @@ Definition unchecked_store Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val) : option mem := - if zlt b m.(nextblock) then - match in_bounds chunk ofs (m.(blocks) b) with - | left P => Some(unchecked_store chunk m b ofs v P) - | right _ => None - end - else - None. + if in_bounds m chunk b ofs + then Some(unchecked_store chunk m b ofs v) + else None. + +Lemma store_inv: + forall chunk m b ofs v m', + store chunk m b ofs v = Some m' -> + valid_access m chunk b ofs /\ + m' = unchecked_store chunk m b ofs v. +Proof. + intros until m'; unfold store. + destruct (in_bounds m chunk b ofs); intros. + split. auto. congruence. + congruence. +Qed. (** [storev chunk m addr v] is similar, but the address and offset are given as a single value [addr], which must be a pointer value. *) @@ -577,63 +482,21 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := | _ => None end. -Theorem store_in_bounds: - forall (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val), - valid_block m b -> - low_bound m b <= ofs -> - ofs + size_chunk chunk <= high_bound m b -> - exists m', store chunk m b ofs v = Some m'. -Proof. - intros. unfold store. - rewrite zlt_true; auto. - case (in_bounds chunk ofs (blocks m b)); intro P. - exists (unchecked_store chunk m b ofs v P). reflexivity. - unfold low_bound in H0. unfold high_bound in H1. omegaContradiction. -Qed. - -Lemma store_inv: - forall (chunk: memory_chunk) (m m': mem) (b: block) (ofs: Z) (v: val), - store chunk m b ofs v = Some m' -> - let c := m.(blocks) b in - b < m.(nextblock) /\ - c.(low) <= ofs /\ - ofs + size_chunk chunk <= c.(high) /\ - m'.(nextblock) = m.(nextblock) /\ - exists P, m'.(blocks) = - update b (mkblock c.(low) c.(high) - (store_contents (mem_chunk chunk) c.(contents) ofs v) P) - m.(blocks). -Proof. - intros until v; unfold store. - case (zlt b (nextblock m)); intro. - set (c := m.(blocks) b). - case (in_bounds chunk ofs c). - intros; injection H; intro; subst m'. simpl. - intuition. fold c. - exists (store_contents_undef_outside (mem_chunk chunk) - (contents c) ofs v (low c) (high c) a (undef_outside c)). - auto. - intros; discriminate. - intros; discriminate. -Qed. - -Hint Resolve store_in_bounds store_inv. - (** Build a block filled with the given initialization data. *) Fixpoint contents_init_data (pos: Z) (id: list init_data) {struct id}: contentmap := match id with | nil => (fun y => Undef) | Init_int8 n :: id' => - store_contents Size8 (contents_init_data (pos + 1) id') pos (Vint n) + setN 0%nat pos (Vint n) (contents_init_data (pos + 1) id') | Init_int16 n :: id' => - store_contents Size16 (contents_init_data (pos + 2) id') pos (Vint n) + setN 1%nat pos (Vint n) (contents_init_data (pos + 1) id') | Init_int32 n :: id' => - store_contents Size32 (contents_init_data (pos + 4) id') pos (Vint n) + setN 3%nat pos (Vint n) (contents_init_data (pos + 1) id') | Init_float32 f :: id' => - store_contents Size32 (contents_init_data (pos + 4) id') pos (Vfloat f) + setN 3%nat pos (Vfloat f) (contents_init_data (pos + 1) id') | Init_float64 f :: id' => - store_contents Size64 (contents_init_data (pos + 8) id') pos (Vfloat f) + setN 7%nat pos (Vfloat f) (contents_init_data (pos + 1) id') | Init_space n :: id' => contents_init_data (pos + Zmax n 0) id' | Init_pointer x :: id' => @@ -664,32 +527,8 @@ Proof. generalize (Zmax2 z 0). omega. omega. Qed. -Remark contents_init_data_undef_outside: - forall id pos x, - x < pos \/ x >= pos + size_init_data_list id -> - contents_init_data pos id x = Undef. -Proof. - induction id; simpl; intros. - auto. - generalize (size_init_data_list_pos id); intro. - assert (forall n delta dt, - delta = 1 + Z_of_nat n -> - x < pos \/ x >= pos + (delta + size_init_data_list id) -> - setN n pos dt (contents_init_data (pos + delta) id) x = Undef). - intros. unfold setN. rewrite update_o. - transitivity (contents_init_data (pos + delta) id x). - apply set_cont_outside. omega. - apply IHid. omega. omega. - unfold size_init_data in H; destruct a; - try (apply H1; [reflexivity|assumption]). - apply IHid. generalize (Zmax2 z 0). omega. - apply IHid. omega. -Qed. - Definition block_init_data (id: list init_data) : block_contents := - mkblock 0 (size_init_data_list id) - (contents_init_data 0 id) - (contents_init_data_undef_outside id 0). + mkblock 0 (size_init_data_list id) (contents_init_data 0 id). Definition alloc_init_data (m: mem) (id: list init_data) : mem * block := (mkmem (update m.(nextblock) @@ -702,8 +541,7 @@ Definition alloc_init_data (m: mem) (id: list init_data) : mem * block := Remark block_init_data_empty: block_init_data nil = empty_block 0 0. Proof. - unfold block_init_data, empty_block. simpl. - decEq. apply proof_irrelevance. + auto. Qed. (** * Properties of the memory operations *) @@ -716,573 +554,961 @@ Proof. intros; red; intros. subst b'. contradiction. Qed. -Theorem fresh_block_alloc: - forall (m1 m2: mem) (lo hi: Z) (b: block), - alloc m1 lo hi = (m2, b) -> ~(valid_block m1 b). +Lemma valid_access_valid_block: + forall m chunk b ofs, + valid_access m chunk b ofs -> valid_block m b. Proof. - intros. injection H; intros; subst b. - unfold valid_block. omega. + intros. inv H; auto. Qed. -Theorem valid_new_block: - forall (m1 m2: mem) (lo hi: Z) (b: block), - alloc m1 lo hi = (m2, b) -> valid_block m2 b. +Hint Resolve valid_not_valid_diff valid_access_valid_block: mem. + +(** ** Properties related to [load] *) + +Theorem valid_access_load: + forall m chunk b ofs, + valid_access m chunk b ofs -> + exists v, load chunk m b ofs = Some v. Proof. - unfold alloc, valid_block; intros. - injection H; intros. subst b; subst m2; simpl. omega. + intros. econstructor. unfold load. rewrite in_bounds_true; auto. Qed. -Theorem valid_block_alloc: - forall (m1 m2: mem) (lo hi: Z) (b b': block), - alloc m1 lo hi = (m2, b') -> - valid_block m1 b -> valid_block m2 b. +Theorem load_valid_access: + forall m chunk b ofs v, + load chunk m b ofs = Some v -> + valid_access m chunk b ofs. Proof. - unfold alloc, valid_block; intros. - injection H; intros. subst m2; simpl. omega. + intros. generalize (load_inv _ _ _ _ _ H). tauto. Qed. -Theorem valid_block_store: - forall (chunk: memory_chunk) (m1 m2: mem) (b b': block) (ofs: Z) (v: val), - store chunk m1 b' ofs v = Some m2 -> - valid_block m1 b -> valid_block m2 b. +Hint Resolve load_valid_access valid_access_load. + +(** ** Properties related to [store] *) + +Lemma valid_access_store: + forall m1 chunk b ofs v, + valid_access m1 chunk b ofs -> + exists m2, store chunk m1 b ofs v = Some m2. Proof. - intros. generalize (store_inv _ _ _ _ _ _ H). - intros [A [B [C [D [P E]]]]]. - red. rewrite D. exact H0. + intros. econstructor. unfold store. rewrite in_bounds_true; auto. Qed. -Theorem valid_block_free: - forall (m: mem) (b b': block), - valid_block m b -> valid_block (free m b') b. +Hint Resolve valid_access_store: mem. + +Section STORE. +Variable chunk: memory_chunk. +Variable m1: mem. +Variable b: block. +Variable ofs: Z. +Variable v: val. +Variable m2: mem. +Hypothesis STORE: store chunk m1 b ofs v = Some m2. + +Lemma low_bound_store: + forall b', low_bound m2 b' = low_bound m1 b'. Proof. - unfold valid_block, free; intros. - simpl. auto. + intro. elim (store_inv _ _ _ _ _ _ STORE); intros. + subst m2. unfold low_bound, unchecked_store; simpl. + unfold update. destruct (zeq b' b); auto. subst b'; auto. +Qed. + +Lemma high_bound_store: + forall b', high_bound m2 b' = high_bound m1 b'. +Proof. + intro. elim (store_inv _ _ _ _ _ _ STORE); intros. + subst m2. unfold high_bound, unchecked_store; simpl. + unfold update. destruct (zeq b' b); auto. subst b'; auto. Qed. -(** ** Properties related to [alloc] *) +Lemma nextblock_store: + nextblock m2 = nextblock m1. +Proof. + intros. elim (store_inv _ _ _ _ _ _ STORE); intros. + subst m2; reflexivity. +Qed. -Theorem load_alloc_other: - forall (chunk: memory_chunk) (m1 m2: mem) - (b b': block) (ofs lo hi: Z) (v: val), - alloc m1 lo hi = (m2, b') -> - load chunk m1 b ofs = Some v -> - load chunk m2 b ofs = Some v. +Lemma store_valid_block_1: + forall b', valid_block m1 b' -> valid_block m2 b'. Proof. - unfold alloc; intros. - injection H; intros; subst m2; clear H. - generalize (load_inv _ _ _ _ _ H0). - intros (A, (B, (C, D))). - unfold load; simpl. - rewrite zlt_true. - repeat (rewrite update_o). - rewrite in_bounds_holds. congruence. auto. auto. - omega. omega. + unfold valid_block; intros. rewrite nextblock_store; auto. Qed. -Lemma load_contents_init: - forall (sz: memory_size) (ofs: Z), - load_contents sz (fun y => Undef) ofs = Vundef. +Lemma store_valid_block_2: + forall b', valid_block m2 b' -> valid_block m1 b'. Proof. - intros. destruct sz; reflexivity. + unfold valid_block; intros. rewrite nextblock_store in H; auto. Qed. -Theorem load_alloc_same: - forall (chunk: memory_chunk) (m1 m2: mem) - (b b': block) (ofs lo hi: Z) (v: val), - alloc m1 lo hi = (m2, b') -> - load chunk m2 b' ofs = Some v -> - v = Vundef. +Hint Resolve store_valid_block_1 store_valid_block_2: mem. + +Lemma store_valid_access_1: + forall chunk' b' ofs', + valid_access m1 chunk' b' ofs' -> valid_access m2 chunk' b' ofs'. Proof. - unfold alloc; intros. - injection H; intros; subst m2; clear H. - generalize (load_inv _ _ _ _ _ H0). - simpl. rewrite H1. rewrite update_s. simpl. intros (A, (B, (C, D))). - rewrite <- D. rewrite load_contents_init. - destruct chunk; reflexivity. -Qed. + intros. inv H. constructor. auto with mem. + rewrite low_bound_store; auto. + rewrite high_bound_store; auto. +Qed. -Theorem low_bound_alloc: - forall (m1 m2: mem) (b b': block) (lo hi: Z), - alloc m1 lo hi = (m2, b') -> - low_bound m2 b = if zeq b b' then lo else low_bound m1 b. +Lemma store_valid_access_2: + forall chunk' b' ofs', + valid_access m2 chunk' b' ofs' -> valid_access m1 chunk' b' ofs'. Proof. - unfold alloc; intros. - injection H; intros; subst m2; clear H. - unfold low_bound; simpl. - unfold update. - subst b'. - case (zeq b (nextblock m1)); reflexivity. + intros. inv H. constructor. auto with mem. + rewrite low_bound_store in H1; auto. + rewrite high_bound_store in H2; auto. Qed. -Theorem high_bound_alloc: - forall (m1 m2: mem) (b b': block) (lo hi: Z), - alloc m1 lo hi = (m2, b') -> - high_bound m2 b = if zeq b b' then hi else high_bound m1 b. +Lemma store_valid_access_3: + valid_access m1 chunk b ofs. Proof. - unfold alloc; intros. - injection H; intros; subst m2; clear H. - unfold high_bound; simpl. - unfold update. - subst b'. - case (zeq b (nextblock m1)); reflexivity. + elim (store_inv _ _ _ _ _ _ STORE); intros. auto. Qed. -Theorem store_alloc: - forall (chunk: memory_chunk) (m1 m2: mem) (b: block) (ofs lo hi: Z) (v: val), - alloc m1 lo hi = (m2, b) -> - lo <= ofs -> ofs + size_chunk chunk <= hi -> - exists m2', store chunk m2 b ofs v = Some m2'. +Hint Resolve store_valid_access_1 store_valid_access_2 + store_valid_access_3: mem. + +Theorem load_store_similar: + forall chunk', + size_chunk chunk' = size_chunk chunk -> + load chunk' m2 b ofs = Some (Val.load_result chunk' v). Proof. - unfold alloc; intros. - injection H; intros. - assert (A: b < m2.(nextblock)). - subst m2; subst b; simpl; omega. - assert (B: low_bound m2 b <= ofs). - subst m2; subst b. unfold low_bound; simpl. rewrite update_s. - simpl. assumption. - assert (C: ofs + size_chunk chunk <= high_bound m2 b). - subst m2; subst b. unfold high_bound; simpl. rewrite update_s. - simpl. assumption. - exact (store_in_bounds chunk m2 b ofs v A B C). + intros. destruct (store_inv _ _ _ _ _ _ STORE). + unfold load. rewrite in_bounds_true. + decEq. decEq. rewrite H1. unfold unchecked_store; simpl. + rewrite update_s. simpl. + replace (pred_size_chunk chunk) with (pred_size_chunk chunk'). + apply getN_setN_same. + repeat rewrite size_chunk_pred in H. omega. + apply store_valid_access_1. + inv H0. constructor; auto. congruence. Qed. -Hint Resolve store_alloc high_bound_alloc low_bound_alloc load_alloc_same -load_contents_init load_alloc_other. +Theorem load_store_same: + load chunk m2 b ofs = Some (Val.load_result chunk v). +Proof. + eapply load_store_similar; eauto. +Qed. + +Theorem load_store_other: + forall chunk' b' ofs', + b' <> b + \/ ofs' + size_chunk chunk' <= ofs + \/ ofs + size_chunk chunk <= ofs' -> + load chunk' m2 b' ofs' = load chunk' m1 b' ofs'. +Proof. + intros. destruct (store_inv _ _ _ _ _ _ STORE). + unfold load. destruct (in_bounds m1 chunk' b' ofs'). + rewrite in_bounds_true. decEq. decEq. + rewrite H1; unfold unchecked_store; simpl. + unfold update. destruct (zeq b' b). subst b'. + simpl. repeat rewrite size_chunk_pred in H. + apply getN_setN_other. elim H; intro. congruence. omega. + auto. + eauto with mem. + destruct (in_bounds m2 chunk' b' ofs'); auto. + elim n. eauto with mem. +Qed. + +Theorem load_store_overlap: + forall chunk' ofs' v', + load chunk' m2 b ofs' = Some v' -> + ofs' <> ofs -> + ofs' + size_chunk chunk' > ofs -> + ofs + size_chunk chunk > ofs' -> + v' = Vundef. +Proof. + intros. destruct (store_inv _ _ _ _ _ _ STORE). + destruct (load_inv _ _ _ _ _ H). rewrite H6. + rewrite H4. unfold unchecked_store. simpl. rewrite update_s. + simpl. rewrite getN_setN_overlap. + destruct chunk'; reflexivity. + auto. rewrite size_chunk_pred in H2. omega. + rewrite size_chunk_pred in H1. omega. +Qed. + +Theorem load_store_overlap': + forall chunk' ofs', + valid_access m1 chunk' b ofs' -> + ofs' <> ofs -> + ofs' + size_chunk chunk' > ofs -> + ofs + size_chunk chunk > ofs' -> + load chunk' m2 b ofs' = Some Vundef. +Proof. + intros. + assert (exists v', load chunk' m2 b ofs' = Some v'). + eauto with mem. + destruct H3 as [v' LOAD]. rewrite LOAD. decEq. + eapply load_store_overlap; eauto. +Qed. -(** ** Properties related to [free] *) +Theorem load_store_mismatch: + forall chunk' v', + load chunk' m2 b ofs = Some v' -> + size_chunk chunk' <> size_chunk chunk -> + v' = Vundef. +Proof. + intros. destruct (store_inv _ _ _ _ _ _ STORE). + destruct (load_inv _ _ _ _ _ H). rewrite H4. + rewrite H2. unfold unchecked_store. simpl. rewrite update_s. + simpl. rewrite getN_setN_mismatch. + destruct chunk'; reflexivity. + repeat rewrite size_chunk_pred in H0; omega. +Qed. -Theorem load_free: - forall (chunk: memory_chunk) (m: mem) (b bf: block) (ofs: Z), - b <> bf -> - load chunk (free m bf) b ofs = load chunk m b ofs. +Theorem load_store_mismatch': + forall chunk', + valid_access m1 chunk' b ofs -> + size_chunk chunk' <> size_chunk chunk -> + load chunk' m2 b ofs = Some Vundef. Proof. - intros. unfold free, load; simpl. - case (zlt b (nextblock m)). - repeat (rewrite update_o; auto). - reflexivity. + intros. + assert (exists v', load chunk' m2 b ofs = Some v'). + eauto with mem. + destruct H1 as [v' LOAD]. rewrite LOAD. decEq. + eapply load_store_mismatch; eauto. +Qed. + +Inductive load_store_cases + (chunk1: memory_chunk) (b1: block) (ofs1: Z) + (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Set := + | lsc_similar: + b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 = size_chunk chunk2 -> + load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 + | lsc_other: + b1 <> b2 \/ ofs2 + size_chunk chunk2 <= ofs1 \/ ofs1 + size_chunk chunk1 <= ofs2 -> + load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 + | lsc_overlap: + b1 = b2 -> ofs1 <> ofs2 -> ofs2 + size_chunk chunk2 > ofs1 -> ofs1 + size_chunk chunk1 > ofs2 -> + load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 + | lsc_mismatch: + b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 <> size_chunk chunk2 -> + load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2. + +Remark size_chunk_pos: + forall chunk1, size_chunk chunk1 > 0. +Proof. + destruct chunk1; simpl; omega. +Qed. + +Definition load_store_classification: + forall (chunk1: memory_chunk) (b1: block) (ofs1: Z) + (chunk2: memory_chunk) (b2: block) (ofs2: Z), + load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2. +Proof. + intros. destruct (eq_block b1 b2). + destruct (zeq ofs1 ofs2). + destruct (zeq (size_chunk chunk1) (size_chunk chunk2)). + apply lsc_similar; auto. + apply lsc_mismatch; auto. + destruct (zle (ofs2 + size_chunk chunk2) ofs1). + apply lsc_other. tauto. + destruct (zle (ofs1 + size_chunk chunk1) ofs2). + apply lsc_other. tauto. + apply lsc_overlap; auto. + apply lsc_other; tauto. +Qed. + +Theorem load_store_characterization: + forall chunk' b' ofs', + valid_access m1 chunk' b' ofs' -> + load chunk' m2 b' ofs' = + match load_store_classification chunk b ofs chunk' b' ofs' with + | lsc_similar _ _ _ => Some (Val.load_result chunk' v) + | lsc_other _ => load chunk' m1 b' ofs' + | lsc_overlap _ _ _ _ => Some Vundef + | lsc_mismatch _ _ _ => Some Vundef + end. +Proof. + intros. + assert (exists v', load chunk' m2 b' ofs' = Some v') by eauto with mem. + destruct H0 as [v' LOAD]. + destruct (load_store_classification chunk b ofs chunk' b' ofs'). + subst b' ofs'. apply load_store_similar; auto. + apply load_store_other; intuition. + subst b'. rewrite LOAD. decEq. + eapply load_store_overlap; eauto. + subst b' ofs'. rewrite LOAD. decEq. + eapply load_store_mismatch; eauto. Qed. -Theorem low_bound_free: - forall (m: mem) (b bf: block), - b <> bf -> - low_bound (free m bf) b = low_bound m b. +End STORE. + +Hint Resolve store_valid_block_1 store_valid_block_2: mem. +Hint Resolve store_valid_access_1 store_valid_access_2 + store_valid_access_3: mem. + +(** ** Properties related to [alloc]. *) + +Section ALLOC. + +Variable m1: mem. +Variables lo hi: Z. +Variable m2: mem. +Variable b: block. +Hypothesis ALLOC: alloc m1 lo hi = (m2, b). + +Lemma nextblock_alloc: + nextblock m2 = Zsucc (nextblock m1). Proof. - intros. unfold free, low_bound; simpl. - rewrite update_o; auto. + injection ALLOC; intros. rewrite <- H0; auto. Qed. -Theorem high_bound_free: - forall (m: mem) (b bf: block), - b <> bf -> - high_bound (free m bf) b = high_bound m b. +Lemma alloc_result: + b = nextblock m1. Proof. - intros. unfold free, high_bound; simpl. - rewrite update_o; auto. + injection ALLOC; auto. Qed. -Hint Resolve load_free low_bound_free high_bound_free. -(** ** Properties related to [store] *) +Lemma valid_block_alloc: + forall b', valid_block m1 b' -> valid_block m2 b'. +Proof. + unfold valid_block; intros. rewrite nextblock_alloc. omega. +Qed. -Lemma store_is_in_bounds: - forall chunk m1 b ofs v m2, - store chunk m1 b ofs v = Some m2 -> - low_bound m1 b <= ofs /\ ofs + size_chunk chunk <= high_bound m1 b. +Lemma fresh_block_alloc: + ~(valid_block m1 b). Proof. - intros. generalize (store_inv _ _ _ _ _ _ H). - intros [A [B [C [P D]]]]. - unfold low_bound, high_bound. tauto. + unfold valid_block. rewrite alloc_result. omega. Qed. -Lemma load_store_contents_same: - forall (sz: memory_size) (c: contentmap) (ofs: Z) (v: val), - load_contents sz (store_contents sz c ofs v) ofs = v. +Lemma valid_new_block: + valid_block m2 b. Proof. - intros until v. - unfold load_contents, store_contents in |- *; case sz; - rewrite getN_setN_same; reflexivity. + unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. omega. Qed. - -Theorem load_store_same: - forall (chunk: memory_chunk) (m1 m2: mem) (b: block) (ofs: Z) (v: val), - store chunk m1 b ofs v = Some m2 -> - load chunk m2 b ofs = Some (Val.load_result chunk v). + +Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. + +Lemma valid_block_alloc_inv: + forall b', valid_block m2 b' -> b' = b \/ valid_block m1 b'. Proof. - intros. - generalize (store_inv _ _ _ _ _ _ H). - intros (A, (B, (C, (D, (P, E))))). - unfold load. rewrite D. - rewrite zlt_true; auto. rewrite E. - repeat (rewrite update_s). simpl. - rewrite in_bounds_exten. rewrite in_bounds_holds; auto. - rewrite load_store_contents_same; auto. -Qed. - -Lemma load_store_contents_other: - forall (sz1 sz2: memory_size) (c: contentmap) - (ofs1 ofs2: Z) (v: val), - ofs2 + size_mem sz2 <= ofs1 \/ ofs1 + size_mem sz1 <= ofs2 -> - load_contents sz2 (store_contents sz1 c ofs1 v) ofs2 = - load_contents sz2 c ofs2. -Proof. - intros until v. - unfold size_mem, store_contents, load_contents; - case sz1; case sz2; intros; - (rewrite getN_setN_other; - [reflexivity | simpl Z_of_nat; omega]). + unfold valid_block; intros. + rewrite nextblock_alloc in H. rewrite alloc_result. + unfold block; omega. Qed. -Theorem load_store_other: - forall (chunk1 chunk2: memory_chunk) (m1 m2: mem) - (b1 b2: block) (ofs1 ofs2: Z) (v: val), - store chunk1 m1 b1 ofs1 v = Some m2 -> - b1 <> b2 - \/ ofs2 + size_chunk chunk2 <= ofs1 - \/ ofs1 + size_chunk chunk1 <= ofs2 -> - load chunk2 m2 b2 ofs2 = load chunk2 m1 b2 ofs2. +Lemma low_bound_alloc: + forall b', low_bound m2 b' = if zeq b' b then lo else low_bound m1 b'. Proof. - intros. - generalize (store_inv _ _ _ _ _ _ H). - intros (A, (B, (C, (D, (P, E))))). - unfold load. rewrite D. - case (zlt b2 (nextblock m1)); intro. - rewrite E; unfold update; case (zeq b2 b1); intro; simpl. - subst b2. rewrite in_bounds_exten. - rewrite load_store_contents_other. auto. - tauto. - reflexivity. - reflexivity. -Qed. - -Ltac LSCO := - match goal with - | |- (match getN ?sz2 ?ofs2 (setN ?sz1 ?ofs1 ?v ?c) with - | Undef => _ - | Datum8 _ => _ - | Datum16 _ => _ - | Datum32 _ => _ - | Datum64 _ => _ - | Cont => _ - end = _) => - elim (getN_setN_overlap sz1 sz2 ofs1 ofs2 v c); - [ let H := fresh in (intro H; rewrite H; reflexivity) - | let H := fresh in (intro H; rewrite H; reflexivity) - | assumption - | simpl Z_of_nat; omega - | simpl Z_of_nat; omega - | discriminate ] - end. + intros. injection ALLOC; intros. rewrite <- H0; unfold low_bound; simpl. + unfold update. rewrite H. destruct (zeq b' b); auto. +Qed. -Lemma load_store_contents_overlap: - forall (sz1 sz2: memory_size) (c: contentmap) - (ofs1 ofs2: Z) (v: val), - ofs1 <> ofs2 -> - ofs2 + size_mem sz2 > ofs1 -> ofs1 + size_mem sz1 > ofs2 -> - load_contents sz2 (store_contents sz1 c ofs1 v) ofs2 = Vundef. +Lemma low_bound_alloc_same: + low_bound m2 b = lo. Proof. - intros. - destruct sz1; destruct sz2; simpl in H0; simpl in H1; simpl; LSCO. -Qed. - -Ltac LSCM := - match goal with - | H:(?x <> ?x) |- _ => - elim H; reflexivity - | |- (match getN ?sz2 ?ofs (setN ?sz1 ?ofs ?v ?c) with - | Undef => _ - | Datum8 _ => _ - | Datum16 _ => _ - | Datum32 _ => _ - | Datum64 _ => _ - | Cont => _ - end = _) => - elim (getN_setN_mismatch sz1 sz2 ofs v c); - [ let H := fresh in (intro H; rewrite H; reflexivity) - | let H := fresh in (intro H; rewrite H; reflexivity) ] - end. + rewrite low_bound_alloc. apply zeq_true. +Qed. -Lemma load_store_contents_mismatch: - forall (sz1 sz2: memory_size) (c: contentmap) - (ofs: Z) (v: val), - sz1 <> sz2 -> - load_contents sz2 (store_contents sz1 c ofs v) ofs = Vundef. +Lemma low_bound_alloc_other: + forall b', valid_block m1 b' -> low_bound m2 b' = low_bound m1 b'. Proof. - intros. - destruct sz1; destruct sz2; simpl; LSCM. -Qed. + intros; rewrite low_bound_alloc. + apply zeq_false. eauto with mem. +Qed. -Theorem low_bound_store: - forall (chunk: memory_chunk) (m1 m2: mem) (b b': block) (ofs: Z) (v: val), - store chunk m1 b ofs v = Some m2 -> - low_bound m2 b' = low_bound m1 b'. +Lemma high_bound_alloc: + forall b', high_bound m2 b' = if zeq b' b then hi else high_bound m1 b'. Proof. - intros. - generalize (store_inv _ _ _ _ _ _ H). - intros (A, (B, (C, (D, (P, E))))). - unfold low_bound. rewrite E; unfold update. - case (zeq b' b); intro. - subst b'. reflexivity. - reflexivity. + intros. injection ALLOC; intros. rewrite <- H0; unfold high_bound; simpl. + unfold update. rewrite H. destruct (zeq b' b); auto. Qed. -Theorem high_bound_store: - forall (chunk: memory_chunk) (m1 m2: mem) (b b': block) (ofs: Z) (v: val), - store chunk m1 b ofs v = Some m2 -> - high_bound m2 b' = high_bound m1 b'. +Lemma high_bound_alloc_same: + high_bound m2 b = hi. Proof. - intros. - generalize (store_inv _ _ _ _ _ _ H). - intros (A, (B, (C, (D, (P, E))))). - unfold high_bound. rewrite E; unfold update. - case (zeq b' b); intro. - subst b'. reflexivity. - reflexivity. + rewrite high_bound_alloc. apply zeq_true. Qed. -Hint Resolve high_bound_store low_bound_store load_store_contents_mismatch - load_store_contents_overlap load_store_other store_is_in_bounds - load_store_contents_same load_store_same load_store_contents_other. +Lemma high_bound_alloc_other: + forall b', valid_block m1 b' -> high_bound m2 b' = high_bound m1 b'. +Proof. + intros; rewrite high_bound_alloc. + apply zeq_false. eauto with mem. +Qed. -(** * Agreement between memory blocks. *) +Lemma valid_access_alloc_other: + forall chunk b' ofs, + valid_access m1 chunk b' ofs -> + valid_access m2 chunk b' ofs. +Proof. + intros. inv H. constructor. auto with mem. + rewrite low_bound_alloc_other; auto. + rewrite high_bound_alloc_other; auto. +Qed. -(** Two memory blocks [c1] and [c2] agree on a range [lo] to [hi] - if they associate the same contents to byte offsets in the range - [lo] (included) to [hi] (excluded). *) +Lemma valid_access_alloc_same: + forall chunk ofs, + lo <= ofs -> ofs + size_chunk chunk <= hi -> + valid_access m2 chunk b ofs. +Proof. + intros. constructor. auto with mem. + rewrite low_bound_alloc_same; auto. + rewrite high_bound_alloc_same; auto. +Qed. + +Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem. + +Lemma valid_access_alloc_inv: + forall chunk b' ofs, + valid_access m2 chunk b' ofs -> + valid_access m1 chunk b' ofs \/ + (b' = b /\ lo <= ofs /\ ofs + size_chunk chunk <= hi). +Proof. + intros. inv H. + elim (valid_block_alloc_inv _ H0); intro. + subst b'. rewrite low_bound_alloc_same in H1. + rewrite high_bound_alloc_same in H2. + right. tauto. + left. constructor. auto. + rewrite low_bound_alloc_other in H1; auto. + rewrite high_bound_alloc_other in H2; auto. +Qed. + +Theorem load_alloc_unchanged: + forall chunk b' ofs, + valid_block m1 b' -> + load chunk m2 b' ofs = load chunk m1 b' ofs. +Proof. + intros. unfold load. + destruct (in_bounds m2 chunk b' ofs). + elim (valid_access_alloc_inv _ _ _ v). intro. + rewrite in_bounds_true; auto. + injection ALLOC; intros. rewrite <- H2; simpl. + rewrite update_o. auto. rewrite H1. apply sym_not_equal. eauto with mem. + intros [A [B C]]. subst b'. elimtype False. eauto with mem. + destruct (in_bounds m1 chunk b' ofs). + elim n; eauto with mem. + auto. +Qed. -Definition contentmap_agree (lo hi: Z) (c1 c2: contentmap) := - forall (ofs: Z), - lo <= ofs < hi -> c1 ofs = c2 ofs. +Theorem load_alloc_other: + forall chunk b' ofs v, + load chunk m1 b' ofs = Some v -> + load chunk m2 b' ofs = Some v. +Proof. + intros. rewrite <- H. apply load_alloc_unchanged. eauto with mem. +Qed. -Definition block_contents_agree (lo hi: Z) (c1 c2: block_contents) := - contentmap_agree lo hi c1.(contents) c2.(contents). +Theorem load_alloc_same: + forall chunk ofs v, + load chunk m2 b ofs = Some v -> + v = Vundef. +Proof. + intros. destruct (load_inv _ _ _ _ _ H). rewrite H1. + injection ALLOC; intros. rewrite <- H3; simpl. + rewrite <- H2. rewrite update_s. + simpl. rewrite getN_init. destruct chunk; auto. +Qed. + +Theorem load_alloc_same': + forall chunk ofs, + lo <= ofs -> ofs + size_chunk chunk <= hi -> + load chunk m2 b ofs = Some Vundef. +Proof. + intros. assert (exists v, load chunk m2 b ofs = Some v). + apply valid_access_load. constructor; eauto with mem. + rewrite low_bound_alloc_same. auto. + rewrite high_bound_alloc_same. auto. + destruct H1 as [v LOAD]. rewrite LOAD. decEq. + eapply load_alloc_same; eauto. +Qed. + +End ALLOC. + +Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. +Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem. +Hint Resolve load_alloc_unchanged: mem. + +(** ** Properties related to [free]. *) -Definition block_agree (b: block) (lo hi: Z) (m1 m2: mem) := - block_contents_agree lo hi - (m1.(blocks) b) (m2.(blocks) b). +Section FREE. -Theorem block_agree_refl: - forall (m: mem) (b: block) (lo hi: Z), - block_agree b lo hi m m. +Variable m: mem. +Variable bf: block. + +Lemma valid_block_free_1: + forall b, valid_block m b -> valid_block (free m bf) b. Proof. - intros. hnf. auto. + unfold valid_block, free; intros; simpl; auto. Qed. -Theorem block_agree_sym: - forall (m1 m2: mem) (b: block) (lo hi: Z), - block_agree b lo hi m1 m2 -> - block_agree b lo hi m2 m1. +Lemma valid_block_free_2: + forall b, valid_block (free m bf) b -> valid_block m b. Proof. - intros. hnf. intros. symmetry. apply H. auto. + unfold valid_block, free; intros; simpl in *; auto. Qed. -Theorem block_agree_trans: - forall (m1 m2 m3: mem) (b: block) (lo hi: Z), - block_agree b lo hi m1 m2 -> - block_agree b lo hi m2 m3 -> - block_agree b lo hi m1 m3. +Hint Resolve valid_block_free_1 valid_block_free_2: mem. + +Lemma low_bound_free: + forall b, b <> bf -> low_bound (free m bf) b = low_bound m b. Proof. - intros. hnf. intros. - transitivity (contents (blocks m2 b) ofs). - apply H; auto. apply H0; auto. + intros. unfold low_bound, free; simpl. + rewrite update_o; auto. Qed. -Lemma check_cont_agree: - forall (c1 c2: contentmap) (lo hi: Z), - contentmap_agree lo hi c1 c2 -> - forall (n: nat) (ofs: Z), - lo <= ofs -> ofs + Z_of_nat n <= hi -> - check_cont n ofs c2 = check_cont n ofs c1. +Lemma high_bound_free: + forall b, b <> bf -> high_bound (free m bf) b = high_bound m b. Proof. - induction n; intros; simpl. - auto. - rewrite inj_S in H1. - rewrite H. case (c2 ofs); intros; auto. - apply IHn; omega. - omega. + intros. unfold high_bound, free; simpl. + rewrite update_o; auto. Qed. -Lemma getN_agree: - forall (c1 c2: contentmap) (lo hi: Z), - contentmap_agree lo hi c1 c2 -> - forall (n: nat) (ofs: Z), - lo <= ofs -> ofs + Z_of_nat n < hi -> - getN n ofs c2 = getN n ofs c1. +Lemma low_bound_free_same: + forall m b, low_bound (free m b) b = 0. Proof. - intros. unfold getN. - rewrite (check_cont_agree c1 c2 lo hi H n (ofs + 1)). - case (check_cont n (ofs + 1) c1). - symmetry. apply H. omega. auto. - omega. omega. + intros. unfold low_bound; simpl. rewrite update_s. simpl; omega. Qed. -Lemma load_contentmap_agree: - forall (sz: memory_size) (c1 c2: contentmap) (lo hi ofs: Z), - contentmap_agree lo hi c1 c2 -> - lo <= ofs -> ofs + size_mem sz <= hi -> - load_contents sz c2 ofs = load_contents sz c1 ofs. +Lemma high_bound_free_same: + forall m b, high_bound (free m b) b = 0. Proof. - intros sz c1 c2 lo hi ofs EX LO. - unfold load_contents, size_mem; case sz; intro HI; - rewrite (getN_agree c1 c2 lo hi EX); auto; simpl Z_of_nat; omega. + intros. unfold high_bound; simpl. rewrite update_s. simpl; omega. Qed. -Lemma set_cont_agree: - forall (lo hi: Z) (n: nat) (c1 c2: contentmap) (ofs: Z), - contentmap_agree lo hi c1 c2 -> - contentmap_agree lo hi (set_cont n ofs c1) (set_cont n ofs c2). +Lemma valid_access_free_1: + forall chunk b ofs, + valid_access m chunk b ofs -> b <> bf -> + valid_access (free m bf) chunk b ofs. Proof. - induction n; simpl; intros. - auto. - red. intros p B. - case (zeq p ofs); intro. - subst p. repeat (rewrite update_s). reflexivity. - repeat (rewrite update_o). apply IHn. assumption. - assumption. auto. auto. + intros. inv H. constructor. auto with mem. + rewrite low_bound_free; auto. rewrite high_bound_free; auto. Qed. -Lemma setN_agree: - forall (lo hi: Z) (n: nat) (c1 c2: contentmap) (ofs: Z) (v: content), - contentmap_agree lo hi c1 c2 -> - contentmap_agree lo hi (setN n ofs v c1) (setN n ofs v c2). +Lemma valid_access_free_2: + forall chunk ofs, ~(valid_access (free m bf) chunk bf ofs). Proof. - intros. unfold setN. red; intros p B. - case (zeq p ofs); intro. - subst p. repeat (rewrite update_s). reflexivity. - repeat (rewrite update_o; auto). - exact (set_cont_agree lo hi n c1 c2 (ofs + 1) H p B). + intros; red; intros. inv H. + unfold free, low_bound in H1; simpl in H1. rewrite update_s in H1. simpl in H1. + unfold free, high_bound in H2; simpl in H2. rewrite update_s in H2. simpl in H2. + generalize (size_chunk_pos chunk). omega. Qed. -Lemma store_contentmap_agree: - forall (sz: memory_size) (c1 c2: contentmap) (lo hi ofs: Z) (v: val), - contentmap_agree lo hi c1 c2 -> - contentmap_agree lo hi - (store_contents sz c1 ofs v) (store_contents sz c2 ofs v). +Hint Resolve valid_access_free_1 valid_access_free_2: mem. + +Lemma valid_access_free_inv: + forall chunk b ofs, + valid_access (free m bf) chunk b ofs -> + valid_access m chunk b ofs /\ b <> bf. Proof. - intros. unfold store_contents; case sz; apply setN_agree; auto. + intros. destruct (eq_block b bf). subst b. + elim (valid_access_free_2 _ _ H). + inv H. rewrite low_bound_free in H1; auto. + rewrite high_bound_free in H2; auto. + split; auto. constructor; auto with mem. Qed. -Lemma set_cont_outside_agree: - forall (lo hi: Z) (n: nat) (c1 c2: contentmap) (ofs: Z), - contentmap_agree lo hi c1 c2 -> - ofs + Z_of_nat n <= lo \/ hi <= ofs -> - contentmap_agree lo hi c1 (set_cont n ofs c2). +Theorem load_free: + forall chunk b ofs, + b <> bf -> + load chunk (free m bf) b ofs = load chunk m b ofs. Proof. - induction n; intros; simpl. - auto. - red; intros p R. rewrite inj_S in H0. - unfold update. case (zeq p ofs); intro. - subst p. omegaContradiction. - apply IHn. auto. omega. auto. + intros. unfold load. + destruct (in_bounds m chunk b ofs). + rewrite in_bounds_true; auto with mem. + unfold free; simpl. rewrite update_o; auto. + destruct (in_bounds (free m bf) chunk b ofs); auto. + elim n. elim (valid_access_free_inv _ _ _ v); auto. +Qed. + +End FREE. + +(** ** Properties related to [free_list] *) + +Lemma valid_block_free_list_1: + forall bl m b, valid_block m b -> valid_block (free_list m bl) b. +Proof. + induction bl; simpl; intros. auto. + apply valid_block_free_1; auto. Qed. -Lemma setN_outside_agree: - forall (lo hi: Z) (n: nat) (c1 c2: contentmap) (ofs: Z) (v: content), - contentmap_agree lo hi c1 c2 -> - ofs + Z_of_nat n < lo \/ hi <= ofs -> - contentmap_agree lo hi c1 (setN n ofs v c2). +Lemma valid_block_free_list_2: + forall bl m b, valid_block (free_list m bl) b -> valid_block m b. Proof. - intros. unfold setN. red; intros p R. - unfold update. case (zeq p ofs); intro. - omegaContradiction. - apply (set_cont_outside_agree lo hi n c1 c2 (ofs + 1) H). - omega. auto. + induction bl; simpl; intros. auto. + apply IHbl. apply valid_block_free_2 with a; auto. Qed. -Lemma store_contentmap_outside_agree: - forall (sz: memory_size) (c1 c2: contentmap) (lo hi ofs: Z) (v: val), - contentmap_agree lo hi c1 c2 -> - ofs + size_mem sz <= lo \/ hi <= ofs -> - contentmap_agree lo hi c1 (store_contents sz c2 ofs v). +Lemma valid_access_free_list: + forall chunk b ofs m bl, + valid_access m chunk b ofs -> ~In b bl -> + valid_access (free_list m bl) chunk b ofs. Proof. - intros until v. - unfold store_contents; case sz; simpl; intros; - apply setN_outside_agree; auto; simpl Z_of_nat; omega. + induction bl; simpl; intros. auto. + apply valid_access_free_1. apply IHbl. auto. intuition. intuition congruence. Qed. -Theorem load_agree: - forall (chunk: memory_chunk) (m1 m2: mem) - (b: block) (lo hi: Z) (ofs: Z) (v1 v2: val), - block_agree b lo hi m1 m2 -> - lo <= ofs -> ofs + size_chunk chunk <= hi -> - load chunk m1 b ofs = Some v1 -> - load chunk m2 b ofs = Some v2 -> - v1 = v2. +Lemma valid_access_free_list_inv: + forall chunk b ofs m bl, + valid_access (free_list m bl) chunk b ofs -> + ~In b bl /\ valid_access m chunk b ofs. +Proof. + induction bl; simpl; intros. + tauto. + elim (valid_access_free_inv _ _ _ _ _ H); intros. + elim (IHbl H0); intros. + intuition congruence. +Qed. + +(** ** Properties related to pointer validity *) + +Lemma valid_pointer_valid_access: + forall m b ofs, + valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs. +Proof. + unfold valid_pointer; intros; split; intros. + destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). + constructor. red. eapply proj_sumbool_true; eauto. + eapply proj_sumbool_true; eauto. + change (size_chunk Mint8unsigned) with 1. + generalize (proj_sumbool_true _ H1). omega. + inv H. unfold proj_sumbool. + rewrite zlt_true; auto. rewrite zle_true; auto. + change (size_chunk Mint8unsigned) with 1 in H2. + rewrite zlt_true. auto. omega. +Qed. + +Theorem valid_pointer_alloc: + forall (m1 m2: mem) (lo hi: Z) (b b': block) (ofs: Z), + alloc m1 lo hi = (m2, b') -> + valid_pointer m1 b ofs = true -> + valid_pointer m2 b ofs = true. +Proof. + intros. rewrite valid_pointer_valid_access in H0. + rewrite valid_pointer_valid_access. + eauto with mem. +Qed. + +Theorem valid_pointer_store: + forall (chunk: memory_chunk) (m1 m2: mem) (b b': block) (ofs ofs': Z) (v: val), + store chunk m1 b' ofs' v = Some m2 -> + valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true. +Proof. + intros. rewrite valid_pointer_valid_access in H0. + rewrite valid_pointer_valid_access. + eauto with mem. +Qed. + +(** * Generic injections between memory states. *) + +Section GENERIC_INJECT. + +Definition meminj : Set := block -> option (block * Z). + +Variable val_inj: meminj -> val -> val -> Prop. + +(* +Hypothesis val_inj_ptr: + forall mi b1 ofs1 b2 ofs2, + val_inj mi (Vptr b1 ofs1) (Vptr b2 ofs2) <-> + exists delta, mi b1 = Some(b2, delta) /\ ofs2 = Int.repr (Int.signed ofs1 + delta). +*) + +Hypothesis val_inj_undef: + forall mi, val_inj mi Vundef Vundef. + +Definition mem_inj (mi: meminj) (m1 m2: mem) := + forall chunk b1 ofs v1 b2 delta, + mi b1 = Some(b2, delta) -> + load chunk m1 b1 ofs = Some v1 -> + exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inj mi v1 v2. + +Lemma valid_access_inj: + forall mi m1 m2 chunk b1 ofs b2 delta, + mi b1 = Some(b2, delta) -> + mem_inj mi m1 m2 -> + valid_access m1 chunk b1 ofs -> + valid_access m2 chunk b2 (ofs + delta). Proof. intros. - generalize (load_inv _ _ _ _ _ H2). intros [K [L [M N]]]. - generalize (load_inv _ _ _ _ _ H3). intros [P [Q [R S]]]. - subst v1; subst v2. symmetry. - decEq. eapply load_contentmap_agree. - apply H. auto. auto. -Qed. - -Theorem store_agree: - forall (chunk: memory_chunk) (m1 m2 m1' m2': mem) - (b: block) (lo hi: Z) - (b': block) (ofs: Z) (v: val), - block_agree b lo hi m1 m2 -> - store chunk m1 b' ofs v = Some m1' -> - store chunk m2 b' ofs v = Some m2' -> - block_agree b lo hi m1' m2'. + assert (exists v1, load chunk m1 b1 ofs = Some v1) by eauto with mem. + destruct H2 as [v1 LOAD1]. + destruct (H0 _ _ _ _ _ _ H LOAD1) as [v2 [LOAD2 VCP]]. + eauto with mem. +Qed. + +Hint Resolve valid_access_inj: mem. + +Lemma store_unmapped_inj: + forall mi m1 m2 b ofs v chunk m1', + mem_inj mi m1 m2 -> + mi b = None -> + store chunk m1 b ofs v = Some m1' -> + mem_inj mi m1' m2. +Proof. + intros; red; intros. + assert (load chunk0 m1 b1 ofs0 = Some v1). + rewrite <- H3; symmetry. eapply load_store_other; eauto. + left. congruence. + eapply H; eauto. +Qed. + +Lemma store_outside_inj: + forall mi m1 m2 chunk b ofs v m2', + mem_inj mi m1 m2 -> + (forall b' delta, + mi b' = Some(b, delta) -> + high_bound m1 b' + delta <= ofs + \/ ofs + size_chunk chunk <= low_bound m1 b' + delta) -> + store chunk m2 b ofs v = Some m2' -> + mem_inj mi m1 m2'. +Proof. + intros; red; intros. + exploit H; eauto. intros [v2 [LOAD2 VINJ]]. + exists v2; split; auto. + rewrite <- LOAD2. eapply load_store_other; eauto. + destruct (eq_block b2 b). subst b2. + right. generalize (H0 _ _ H2); intro. + assert (valid_access m1 chunk0 b1 ofs0) by eauto with mem. + inv H5. omega. auto. +Qed. + +Definition meminj_no_overlap (mi: meminj) (m: mem) : Prop := + forall b1 b1' delta1 b2 b2' delta2, + b1 <> b2 -> + mi b1 = Some (b1', delta1) -> + mi b2 = Some (b2', delta2) -> + b1' <> b2' + \/ low_bound m b1 >= high_bound m b1 + \/ low_bound m b2 >= high_bound m b2 + \/ high_bound m b1 + delta1 <= low_bound m b2 + delta2 + \/ high_bound m b2 + delta2 <= low_bound m b1 + delta1. + +Lemma store_mapped_inj: + forall mi m1 m2 b1 ofs b2 delta v1 v2 chunk m1', + mem_inj mi m1 m2 -> + meminj_no_overlap mi m1 -> + mi b1 = Some(b2, delta) -> + store chunk m1 b1 ofs v1 = Some m1' -> + (forall chunk', size_chunk chunk' = size_chunk chunk -> + val_inj mi (Val.load_result chunk' v1) (Val.load_result chunk' v2)) -> + exists m2', + store chunk m2 b2 (ofs + delta) v2 = Some m2' /\ mem_inj mi m1' m2'. Proof. - intros. - generalize (store_inv _ _ _ _ _ _ H0). - intros [I [J [K [L [x M]]]]]. - generalize (store_inv _ _ _ _ _ _ H1). - intros [P [Q [R [S [y T]]]]]. - red. red. - rewrite M; rewrite T; unfold update. - case (zeq b b'); intro; simpl. - subst b'. apply store_contentmap_agree. assumption. - apply H. -Qed. - -Theorem store_outside_agree: - forall (chunk: memory_chunk) (m1 m2 m2': mem) - (b: block) (lo hi: Z) - (b': block) (ofs: Z) (v: val), - block_agree b lo hi m1 m2 -> - b <> b' \/ ofs + size_chunk chunk <= lo \/ hi <= ofs -> - store chunk m2 b' ofs v = Some m2' -> - block_agree b lo hi m1 m2'. + intros. + assert (exists m2', store chunk m2 b2 (ofs + delta) v2 = Some m2') by eauto with mem. + destruct H4 as [m2' STORE2]. + exists m2'; split. auto. + red. intros chunk' b1' ofs' v b2' delta' CP LOAD1. + assert (valid_access m1 chunk' b1' ofs') by eauto with mem. + generalize (load_store_characterization _ _ _ _ _ _ H2 _ _ _ H4). + destruct (load_store_classification chunk b1 ofs chunk' b1' ofs'); + intro. + (* similar *) + subst b1' ofs'. + rewrite CP in H1. inv H1. + rewrite LOAD1 in H5. inv H5. + exists (Val.load_result chunk' v2). split. + eapply load_store_similar; eauto. + auto. + (* disjoint *) + rewrite LOAD1 in H5. + destruct (H _ _ _ _ _ _ CP (sym_equal H5)) as [v2' [LOAD2 VCP]]. + exists v2'. split; auto. + rewrite <- LOAD2. eapply load_store_other; eauto. + destruct (eq_block b1 b1'). subst b1'. + rewrite CP in H1; inv H1. + right. elim o; [congruence | omega]. + assert (valid_access m1 chunk b1 ofs) by eauto with mem. + generalize (H0 _ _ _ _ _ _ n H1 CP). intros [A | [A | [A | A]]]. + auto. + inv H6. generalize (size_chunk_pos chunk). intro. omegaContradiction. + inv H4. generalize (size_chunk_pos chunk'). intro. omegaContradiction. + right. inv H4. inv H6. omega. + (* overlapping *) + subst b1'. rewrite CP in H1; inv H1. + assert (exists v2', load chunk' m2' b2 (ofs' + delta) = Some v2') by eauto with mem. + destruct H1 as [v2' LOAD2']. + assert (v2' = Vundef). eapply load_store_overlap; eauto. + omega. omega. omega. + exists v2'; split. auto. + replace v with Vundef by congruence. subst v2'. apply val_inj_undef. + (* mismatch *) + subst b1' ofs'. rewrite CP in H1; inv H1. + assert (exists v2', load chunk' m2' b2 (ofs + delta) = Some v2') by eauto with mem. + destruct H1 as [v2' LOAD2']. + assert (v2' = Vundef). eapply load_store_mismatch; eauto. + exists v2'; split. auto. + replace v with Vundef by congruence. subst v2'. apply val_inj_undef. +Qed. + +Lemma alloc_parallel_inj: + forall mi m1 m2 lo1 hi1 m1' b1 lo2 hi2 m2' b2 delta, + mem_inj mi m1 m2 -> + alloc m1 lo1 hi1 = (m1', b1) -> + alloc m2 lo2 hi2 = (m2', b2) -> + mi b1 = Some(b2, delta) -> + lo2 <= lo1 + delta -> hi1 + delta <= hi2 -> + mem_inj mi m1' m2'. +Proof. + intros; red; intros. + exploit (valid_access_alloc_inv m1); eauto with mem. + intros [A | [A [B C]]]. + assert (load chunk m1 b0 ofs = Some v1). + rewrite <- H6. symmetry. eapply load_alloc_unchanged; eauto with mem. + exploit H; eauto. intros [v2 [LOAD2 VINJ]]. + exists v2; split. + rewrite <- LOAD2. eapply load_alloc_unchanged; eauto with mem. + auto. + subst b0. rewrite H2 in H5. inversion H5. subst b3 delta0. + assert (v1 = Vundef). eapply load_alloc_same with (m1 := m1); eauto. + subst v1. + assert (exists v2, load chunk m2' b2 (ofs + delta) = Some v2). + apply valid_access_load. + eapply valid_access_alloc_same; eauto. omega. omega. + destruct H7 as [v2 LOAD2]. + assert (v2 = Vundef). eapply load_alloc_same with (m1 := m2); eauto. + subst v2. + exists Vundef; split. auto. apply val_inj_undef. +Qed. + +Lemma alloc_right_inj: + forall mi m1 m2 lo hi b2 m2', + mem_inj mi m1 m2 -> + alloc m2 lo hi = (m2', b2) -> + mem_inj mi m1 m2'. Proof. - intros. - generalize (store_inv _ _ _ _ _ _ H1). - intros [I [J [K [L [x M]]]]]. - red. red. rewrite M; unfold update; - case (zeq b b'); intro; simpl. - subst b'. apply store_contentmap_outside_agree. - assumption. - elim H0; intro. tauto. exact H2. - apply H. + intros; red; intros. + exploit H; eauto. intros [v2 [LOAD2 VINJ]]. + exists v2; split; auto. + assert (valid_block m2 b0). + apply valid_access_valid_block with chunk (ofs + delta). + eauto with mem. + rewrite <- LOAD2. eapply load_alloc_unchanged; eauto. +Qed. + +Hypothesis val_inj_undef_any: + forall mi v, val_inj mi Vundef v. + +Lemma alloc_left_unmapped_inj: + forall mi m1 m2 lo hi b1 m1', + mem_inj mi m1 m2 -> + alloc m1 lo hi = (m1', b1) -> + mi b1 = None -> + mem_inj mi m1' m2. +Proof. + intros; red; intros. + exploit (valid_access_alloc_inv m1); eauto with mem. + intros [A | [A [B C]]]. + eapply H; eauto. + rewrite <- H3. symmetry. eapply load_alloc_unchanged; eauto with mem. + subst b0. congruence. +Qed. + +Lemma alloc_left_mapped_inj: + forall mi m1 m2 lo hi b1 m1' b2 delta, + mem_inj mi m1 m2 -> + alloc m1 lo hi = (m1', b1) -> + mi b1 = Some(b2, delta) -> + valid_block m2 b2 -> + low_bound m2 b2 <= lo + delta -> hi + delta <= high_bound m2 b2 -> + mem_inj mi m1' m2. +Proof. + intros; red; intros. + exploit (valid_access_alloc_inv m1); eauto with mem. + intros [A | [A [B C]]]. + eapply H; eauto. + rewrite <- H6. symmetry. eapply load_alloc_unchanged; eauto with mem. + subst b0. rewrite H1 in H5. inversion H5. subst b3 delta0. + assert (v1 = Vundef). eapply load_alloc_same with (m1 := m1); eauto. + subst v1. + assert (exists v2, load chunk m2 b2 (ofs + delta) = Some v2). + apply valid_access_load. constructor. auto. omega. omega. + destruct H7 as [v2 LOAD2]. exists v2; split. auto. + apply val_inj_undef_any. +Qed. + +Lemma free_parallel_inj: + forall mi m1 m2 b1 b2 delta, + mem_inj mi m1 m2 -> + mi b1 = Some(b2, delta) -> + (forall b delta', mi b = Some(b2, delta') -> b = b1) -> + mem_inj mi (free m1 b1) (free m2 b2). +Proof. + intros; red; intros. + exploit valid_access_free_inv; eauto with mem. intros [A B]. + assert (load chunk m1 b0 ofs = Some v1). + rewrite <- H3. symmetry. apply load_free. auto. + exploit H; eauto. intros [v2 [LOAD2 INJ]]. + exists v2; split. + rewrite <- LOAD2. apply load_free. + red; intro; subst b3. elim B. eauto. + auto. Qed. -(** * Store extensions *) +Lemma free_left_inj: + forall mi m1 m2 b1, + mem_inj mi m1 m2 -> + mem_inj mi (free m1 b1) m2. +Proof. + intros; red; intros. + exploit valid_access_free_inv; eauto with mem. intros [A B]. + eapply H; eauto with mem. + rewrite <- H1; symmetry; eapply load_free; eauto. +Qed. + +Lemma free_list_left_inj: + forall mi bl m1 m2, + mem_inj mi m1 m2 -> + mem_inj mi (free_list m1 bl) m2. +Proof. + induction bl; intros; simpl. + auto. + apply free_left_inj. auto. +Qed. + +Lemma free_right_inj: + forall mi m1 m2 b2, + mem_inj mi m1 m2 -> + (forall b1 delta chunk ofs, + mi b1 = Some(b2, delta) -> ~(valid_access m1 chunk b1 ofs)) -> + mem_inj mi m1 (free m2 b2). +Proof. + intros; red; intros. + assert (b0 <> b2). + red; intro; subst b0. elim (H0 b1 delta chunk ofs H1). + eauto with mem. + exploit H; eauto. intros [v2 [LOAD2 INJ]]. + exists v2; split; auto. + rewrite <- LOAD2. apply load_free. auto. +Qed. + +Lemma valid_pointer_inj: + forall mi m1 m2 b1 ofs b2 delta, + mi b1 = Some(b2, delta) -> + mem_inj mi m1 m2 -> + valid_pointer m1 b1 ofs = true -> + valid_pointer m2 b2 (ofs + delta) = true. +Proof. + intros. rewrite valid_pointer_valid_access in H1. + rewrite valid_pointer_valid_access. eauto with mem. +Qed. + +End GENERIC_INJECT. + +(** ** Store extensions *) (** A store [m2] extends a store [m1] if [m2] can be obtained from [m1] by increasing the sizes of the memory blocks of [m1] (decreasing the low bounds, increasing the high bounds), while still keeping the - same contents for block offsets that are valid in [m1]. - This notion is used in the proof of semantic equivalence in - module [Machenv]. *) + same contents for block offsets that are valid in [m1]. *) -Definition block_contents_extends (c1 c2: block_contents) := - c2.(low) <= c1.(low) /\ c1.(high) <= c2.(high) /\ - contentmap_agree c1.(low) c1.(high) c1.(contents) c2.(contents). +Definition inject_id : meminj := fun b => Some(b, 0). + +Definition val_inj_id (mi: meminj) (v1 v2: val) : Prop := v1 = v2. Definition extends (m1 m2: mem) := - m1.(nextblock) = m2.(nextblock) /\ - forall (b: block), - b < m1.(nextblock) -> - block_contents_extends (m1.(blocks) b) (m2.(blocks) b). + nextblock m1 = nextblock m2 /\ mem_inj val_inj_id inject_id m1 m2. Theorem extends_refl: forall (m: mem), extends m m. Proof. - intro. red. split. - reflexivity. - intros. red. - split. omega. split. omega. - red. intros. reflexivity. + intros; split. auto. + red; unfold inject_id; intros. inv H. + exists v1; split. replace (ofs + 0) with ofs by omega. auto. + unfold val_inj_id; auto. Qed. Theorem alloc_extends: @@ -1293,16 +1519,18 @@ Theorem alloc_extends: alloc m2 lo2 hi2 = (m2', b2) -> b1 = b2 /\ extends m1' m2'. Proof. - unfold extends, alloc; intros. - injection H2; intros; subst m1'; subst b1. - injection H3; intros; subst m2'; subst b2. - simpl. intuition. - rewrite <- H4. case (zeq b (nextblock m1)); intro. - subst b. repeat rewrite update_s. - red; simpl. intuition. - red; intros; reflexivity. - repeat rewrite update_o. apply H5. omega. - auto. auto. + intros. destruct H. + assert (b1 = b2). + transitivity (nextblock m1). eapply alloc_result; eauto. + symmetry. rewrite H. eapply alloc_result; eauto. + subst b2. split. auto. split. + rewrite (nextblock_alloc _ _ _ _ _ H2). + rewrite (nextblock_alloc _ _ _ _ _ H3). + congruence. + eapply alloc_parallel_inj; eauto. + unfold val_inj_id; auto. + unfold inject_id; eauto. + omega. omega. Qed. Theorem free_extends: @@ -1310,16 +1538,11 @@ Theorem free_extends: extends m1 m2 -> extends (free m1 b) (free m2 b). Proof. - unfold extends, free; intros. - simpl. intuition. - red; intros; simpl. - case (zeq b0 b); intro. - subst b0; repeat (rewrite update_s). - simpl. split. omega. split. omega. - red. intros. omegaContradiction. - repeat (rewrite update_o). - exact (H1 b0 H). - auto. auto. + intros. destruct H. split. + simpl; auto. + eapply free_parallel_inj; eauto. + unfold inject_id. eauto. + unfold inject_id; intros. congruence. Qed. Theorem load_extends: @@ -1328,18 +1551,10 @@ Theorem load_extends: load chunk m1 b ofs = Some v -> load chunk m2 b ofs = Some v. Proof. - intros sz m1 m2 b ofs v (X, Y) L. - generalize (load_inv _ _ _ _ _ L). - intros (A, (B, (C, D))). - unfold load. rewrite <- X. rewrite zlt_true; auto. - generalize (Y b A); intros [M [P Q]]. - rewrite in_bounds_holds. - rewrite <- D. - decEq. decEq. - apply load_contentmap_agree with - (lo := low((blocks m1) b)) - (hi := high((blocks m1) b)); auto. - omega. omega. + intros. destruct H. + exploit H1; eauto. unfold inject_id. eauto. + unfold val_inj_id. intros [v2 [LOAD EQ]]. + replace (ofs + 0) with ofs in LOAD by omega. congruence. Qed. Theorem store_within_extends: @@ -1348,24 +1563,21 @@ Theorem store_within_extends: store chunk m1 b ofs v = Some m1' -> exists m2', store chunk m2 b ofs v = Some m2' /\ extends m1' m2'. Proof. - intros sz m1 m2 m1' b ofs v (X, Y) STORE. - generalize (store_inv _ _ _ _ _ _ STORE). - intros (A, (B, (C, (D, (x, E))))). - generalize (Y b A); intros [M [P Q]]. - unfold store. rewrite <- X. rewrite zlt_true; auto. - case (in_bounds sz ofs (blocks m2 b)); intro. - exists (unchecked_store sz m2 b ofs v a). - split. auto. + intros. destruct H. + exploit store_mapped_inj; eauto. + unfold val_inj_id; eauto. + unfold meminj_no_overlap, inject_id; intros. + inv H3. inv H4. auto. + unfold inject_id; eauto. + unfold val_inj_id; intros. eauto. + intros [m2' [STORE MINJ]]. + exists m2'; split. + replace (ofs + 0) with ofs in STORE by omega. auto. split. - unfold unchecked_store; simpl. congruence. - intros b' LT. - unfold block_contents_extends, unchecked_store, block_contents_agree. - rewrite E; unfold update; simpl. - case (zeq b' b); intro; simpl. - subst b'. split. omega. split. omega. - apply store_contentmap_agree. auto. - apply Y. rewrite <- D. auto. - omegaContradiction. + rewrite (nextblock_store _ _ _ _ _ _ H0). + rewrite (nextblock_store _ _ _ _ _ _ STORE). + auto. + auto. Qed. Theorem store_outside_extends: @@ -1375,59 +1587,147 @@ Theorem store_outside_extends: store chunk m2 b ofs v = Some m2' -> extends m1 m2'. Proof. - intros sz m1 m2 m2' b ofs v (X, Y) BOUNDS STORE. - generalize (store_inv _ _ _ _ _ _ STORE). - intros (A, (B, (C, (D, (x, E))))). - split. - congruence. - intros b' LT. - rewrite E; unfold update; case (zeq b' b); intro. - subst b'. generalize (Y b LT). intros [M [P Q]]. - red; simpl. split. omega. split. omega. - apply store_contentmap_outside_agree. - assumption. exact BOUNDS. - auto. -Qed. - -(** * Memory extensionality properties *) - -Lemma block_contents_exten: - forall (c1 c2: block_contents), - c1.(low) = c2.(low) -> - c1.(high) = c2.(high) -> - block_contents_agree c1.(low) c1.(high) c1 c2 -> - c1 = c2. -Proof. - intros. caseEq c1; intros lo1 hi1 m1 UO1 EQ1. subst c1. - caseEq c2; intros lo2 hi2 m2 UO2 EQ2. subst c2. - simpl in *. subst lo2 hi2. - assert (m1 = m2). - unfold contentmap. apply extensionality. intro. - case (zlt x lo1); intro. - rewrite UO1. rewrite UO2. auto. tauto. tauto. - case (zlt x hi1); intro. - apply H1. omega. - rewrite UO1. rewrite UO2. auto. tauto. tauto. - subst m2. - assert (UO1 = UO2). - apply proof_irrelevance. - subst UO2. reflexivity. -Qed. - -Theorem mem_exten: - forall m1 m2, - m1.(nextblock) = m2.(nextblock) -> - (forall b, m1.(blocks) b = m2.(blocks) b) -> - m1 = m2. -Proof. - intros. destruct m1 as [map1 nb1 nextpos1]. destruct m2 as [map2 nb2 nextpos2]. - simpl in *. subst nb2. - assert (map1 = map2). apply extensionality. assumption. - assert (nextpos1 = nextpos2). apply proof_irrelevance. + intros. destruct H. split. + rewrite (nextblock_store _ _ _ _ _ _ H1). auto. + eapply store_outside_inj; eauto. + unfold inject_id; intros. inv H3. omega. +Qed. + +Theorem valid_pointer_extends: + forall m1 m2 b ofs, + extends m1 m2 -> valid_pointer m1 b ofs = true -> + valid_pointer m2 b ofs = true. +Proof. + intros. destruct H. + replace ofs with (ofs + 0) by omega. + apply valid_pointer_inj with val_inj_id inject_id m1 b; auto. +Qed. + +(** * The ``less defined than'' relation over memory states *) + +(** A memory state [m1] is less defined than [m2] if, for all addresses, + the value [v1] read in [m1] at this address is less defined than + the value [v2] read in [m2], that is, either [v1 = v2] or [v1 = Vundef]. *) + +Definition val_inj_lessdef (mi: meminj) (v1 v2: val) : Prop := + Val.lessdef v1 v2. + +Definition lessdef (m1 m2: mem) : Prop := + nextblock m1 = nextblock m2 /\ + mem_inj val_inj_lessdef inject_id m1 m2. + +Lemma lessdef_refl: + forall m, lessdef m m. +Proof. + intros; split. auto. + red; intros. unfold inject_id in H. inv H. + exists v1; split. replace (ofs + 0) with ofs by omega. auto. + red. constructor. +Qed. + +Lemma load_lessdef: + forall m1 m2 chunk b ofs v1, + lessdef m1 m2 -> load chunk m1 b ofs = Some v1 -> + exists v2, load chunk m2 b ofs = Some v2 /\ Val.lessdef v1 v2. +Proof. + intros. destruct H. + exploit H1; eauto. unfold inject_id. eauto. + intros [v2 [LOAD INJ]]. exists v2; split. + replace ofs with (ofs + 0) by omega. auto. + auto. +Qed. + +Lemma loadv_lessdef: + forall m1 m2 chunk addr1 addr2 v1, + lessdef m1 m2 -> Val.lessdef addr1 addr2 -> + loadv chunk m1 addr1 = Some v1 -> + exists v2, loadv chunk m2 addr2 = Some v2 /\ Val.lessdef v1 v2. +Proof. + intros. inv H0. + destruct addr2; simpl in *; try discriminate. + eapply load_lessdef; eauto. + simpl in H1; discriminate. +Qed. + +Lemma store_lessdef: + forall m1 m2 chunk b ofs v1 v2 m1', + lessdef m1 m2 -> Val.lessdef v1 v2 -> + store chunk m1 b ofs v1 = Some m1' -> + exists m2', store chunk m2 b ofs v2 = Some m2' /\ lessdef m1' m2'. +Proof. + intros. destruct H. + exploit store_mapped_inj; eauto. + unfold val_inj_lessdef; intros; constructor. + red; unfold inject_id; intros. inv H4. inv H5. auto. + unfold inject_id; eauto. + unfold val_inj_lessdef; intros. + apply Val.load_result_lessdef. eexact H0. + intros [m2' [STORE MINJ]]. + exists m2'; split. replace ofs with (ofs + 0) by omega. auto. + split. + rewrite (nextblock_store _ _ _ _ _ _ H1). + rewrite (nextblock_store _ _ _ _ _ _ STORE). + auto. + auto. +Qed. + +Lemma storev_lessdef: + forall m1 m2 chunk addr1 v1 addr2 v2 m1', + lessdef m1 m2 -> Val.lessdef addr1 addr2 -> Val.lessdef v1 v2 -> + storev chunk m1 addr1 v1 = Some m1' -> + exists m2', storev chunk m2 addr2 v2 = Some m2' /\ lessdef m1' m2'. +Proof. + intros. inv H0. + destruct addr2; simpl in H2; try discriminate. + simpl. eapply store_lessdef; eauto. + discriminate. +Qed. + +Lemma alloc_lessdef: + forall m1 m2 lo hi b1 m1' b2 m2', + lessdef m1 m2 -> alloc m1 lo hi = (m1', b1) -> alloc m2 lo hi = (m2', b2) -> + b1 = b2 /\ lessdef m1' m2'. +Proof. + intros. destruct H. + assert (b1 = b2). + transitivity (nextblock m1). eapply alloc_result; eauto. + symmetry. rewrite H. eapply alloc_result; eauto. + subst b2. split. auto. split. + rewrite (nextblock_alloc _ _ _ _ _ H0). + rewrite (nextblock_alloc _ _ _ _ _ H1). congruence. + eapply alloc_parallel_inj; eauto. + unfold val_inj_lessdef; auto. + unfold inject_id; eauto. + omega. omega. Qed. -(** * Store injections *) +Lemma free_lessdef: + forall m1 m2 b, lessdef m1 m2 -> lessdef (free m1 b) (free m2 b). +Proof. + intros. destruct H. split. + simpl; auto. + eapply free_parallel_inj; eauto. + unfold inject_id. eauto. + unfold inject_id; intros. congruence. +Qed. + +Lemma valid_block_lessdef: + forall m1 m2 b, lessdef m1 m2 -> valid_block m1 b -> valid_block m2 b. +Proof. + unfold valid_block. intros. destruct H. rewrite <- H; auto. +Qed. + +Lemma valid_pointer_lessdef: + forall m1 m2 b ofs, + lessdef m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true. +Proof. + intros. destruct H. + replace ofs with (ofs + 0) by omega. + apply valid_pointer_inj with val_inj_lessdef inject_id m1 b; auto. +Qed. + +(** ** Memory injections *) (** A memory injection [f] is a function from addresses to either [None] or [Some] of an address and an offset. It defines a correspondence @@ -1437,718 +1737,358 @@ Qed. a sub-block at offset [ofs] of the block [b'] in [m2]. *) -Definition meminj := (block -> option (block * Z))%type. - -Section MEM_INJECT. - -Variable f: meminj. - (** A memory injection defines a relation between values that is the identity relation, except for pointer values which are shifted as prescribed by the memory injection. *) -Inductive val_inject: val -> val -> Prop := +Inductive val_inject (mi: meminj): val -> val -> Prop := | val_inject_int: - forall i, val_inject (Vint i) (Vint i) + forall i, val_inject mi (Vint i) (Vint i) | val_inject_float: - forall f, val_inject (Vfloat f) (Vfloat f) + forall f, val_inject mi (Vfloat f) (Vfloat f) | val_inject_ptr: forall b1 ofs1 b2 ofs2 x, - f b1 = Some (b2, x) -> + mi b1 = Some (b2, x) -> ofs2 = Int.add ofs1 (Int.repr x) -> - val_inject (Vptr b1 ofs1) (Vptr b2 ofs2) + val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2) | val_inject_undef: forall v, - val_inject Vundef v. + val_inject mi Vundef v. Hint Resolve val_inject_int val_inject_float val_inject_ptr -val_inject_undef. + val_inject_undef. -Inductive val_list_inject: list val -> list val-> Prop:= +Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:= | val_nil_inject : - val_list_inject nil nil + val_list_inject mi nil nil | val_cons_inject : forall v v' vl vl' , - val_inject v v' -> val_list_inject vl vl'-> - val_list_inject (v::vl) (v':: vl'). - -Inductive val_content_inject: memory_size -> val -> val -> Prop := - | val_content_inject_base: - forall sz v1 v2, - val_inject v1 v2 -> - val_content_inject sz v1 v2 - | val_content_inject_8: - forall n1 n2, - Int.cast8unsigned n1 = Int.cast8unsigned n2 -> - val_content_inject Size8 (Vint n1) (Vint n2) - | val_content_inject_16: - forall n1 n2, - Int.cast16unsigned n1 = Int.cast16unsigned n2 -> - val_content_inject Size16 (Vint n1) (Vint n2) - | val_content_inject_32: - forall f1 f2, - Float.singleoffloat f1 = Float.singleoffloat f2 -> - val_content_inject Size32 (Vfloat f1) (Vfloat f2). + val_inject mi v v' -> val_list_inject mi vl vl'-> + val_list_inject mi (v :: vl) (v' :: vl'). -Hint Resolve val_content_inject_base. - -Inductive content_inject: content -> content -> Prop := - | content_inject_undef: - forall c, - content_inject Undef c - | content_inject_datum8: - forall v1 v2, - val_content_inject Size8 v1 v2 -> - content_inject (Datum8 v1) (Datum8 v2) - | content_inject_datum16: - forall v1 v2, - val_content_inject Size16 v1 v2 -> - content_inject (Datum16 v1) (Datum16 v2) - | content_inject_datum32: - forall v1 v2, - val_content_inject Size32 v1 v2 -> - content_inject (Datum32 v1) (Datum32 v2) - | content_inject_datum64: - forall v1 v2, - val_content_inject Size64 v1 v2 -> - content_inject (Datum64 v1) (Datum64 v2) - | content_inject_cont: - content_inject Cont Cont. - -Hint Resolve content_inject_undef content_inject_datum8 -content_inject_datum16 content_inject_datum32 content_inject_datum64 -content_inject_cont. - -Definition contentmap_inject (c1 c2: contentmap) (lo hi delta: Z) : Prop := - forall x, lo <= x < hi -> - content_inject (c1 x) (c2 (x + delta)). - -(** A block contents [c1] injects into another block content [c2] at - offset [delta] if the contents of [c1] at all valid offsets - correspond to the contents of [c2] at the same offsets shifted by [delta]. - Some additional conditions are imposed to guard against arithmetic - overflow in address computations. *) - -Record block_contents_inject (c1 c2: block_contents) (delta: Z) : Prop := - mk_block_contents_inject { - bci_range1: Int.min_signed <= delta <= Int.max_signed; - bci_range2: delta = 0 \/ - (Int.min_signed <= c2.(low) /\ c2.(high) <= Int.max_signed); - bci_lowhigh:forall x, c1.(low) <= x < c1.(high) -> - c2.(low) <= x+delta < c2.(high) ; - bci_contents: - contentmap_inject c1.(contents) c2.(contents) c1.(low) c1.(high) delta - }. +Hint Resolve val_nil_inject val_cons_inject. (** A memory state [m1] injects into another memory state [m2] via the memory injection [f] if the following conditions hold: +- loads in [m1] must have matching loads in [m2] in the sense + of the [mem_inj] predicate; - unallocated blocks in [m1] must be mapped to [None] by [f]; -- if [f b = Some(b', delta)], [b'] must be valid in [m2] and - the contents of [b] in [m1] must inject into the contents of [b'] in [m2] - with offset [delta]; -- distinct blocks in [m1] cannot be mapped to overlapping sub-blocks in [m2]. +- if [f b = Some(b', delta)], [b'] must be valid in [m2]; +- distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2]; +- the sizes of [m2]'s blocks are representable with signed machine integers; +- the offsets [delta] are representable with signed machine integers. *) -Record mem_inject (m1 m2: mem) : Prop := +Record mem_inject (f: meminj) (m1 m2: mem) : Prop := mk_mem_inject { + mi_inj: + mem_inj val_inject f m1 m2; mi_freeblocks: - forall b, b >= m1.(nextblock) -> f b = None; + forall b, ~(valid_block m1 b) -> f b = None; mi_mappedblocks: + forall b b' delta, f b = Some(b', delta) -> valid_block m2 b'; + mi_no_overlap: + meminj_no_overlap f m1; + mi_range_1: forall b b' delta, f b = Some(b', delta) -> - b' < m2.(nextblock) /\ - block_contents_inject (m1.(blocks) b) - (m2.(blocks) b') - delta; - mi_no_overlap: - forall b1 b2 b1' b2' delta1 delta2, - b1 <> b2 -> - f b1 = Some (b1', delta1) -> - f b2 = Some (b2', delta2) -> - b1' <> b2' - \/ (forall x1 x2, low_bound m1 b1 <= x1 < high_bound m1 b1 -> - low_bound m1 b2 <= x2 < high_bound m1 b2 -> - x1+delta1 <> x2+delta2) - }. + Int.min_signed <= delta <= Int.max_signed; + mi_range_2: + forall b b' delta, + f b = Some(b', delta) -> + delta = 0 \/ (Int.min_signed <= low_bound m2 b' /\ high_bound m2 b' <= Int.max_signed) + }. + (** The following lemmas establish the absence of machine integer overflow during address computations. *) -Lemma size_mem_pos: forall sz, size_mem sz > 0. -Proof. destruct sz; simpl; omega. Qed. - -Lemma size_chunk_pos: forall chunk, size_chunk chunk > 0. -Proof. intros. unfold size_chunk. apply size_mem_pos. Qed. - Lemma address_inject: - forall m1 m2 chunk b1 ofs1 b2 ofs2 x, - mem_inject m1 m2 -> - (m1.(blocks) b1).(low) <= Int.signed ofs1 -> - Int.signed ofs1 + size_chunk chunk <= (m1.(blocks) b1).(high) -> - f b1 = Some (b2, x) -> - ofs2 = Int.add ofs1 (Int.repr x) -> - Int.signed ofs2 = Int.signed ofs1 + x. + forall f m1 m2 chunk b1 ofs1 b2 delta, + mem_inject f m1 m2 -> + valid_access m1 chunk b1 (Int.signed ofs1) -> + f b1 = Some (b2, delta) -> + Int.signed (Int.add ofs1 (Int.repr delta)) = Int.signed ofs1 + delta. Proof. - intros. - generalize (size_chunk_pos chunk). intro. - generalize (mi_mappedblocks m1 m2 H _ _ _ H2). intros [C D]. - inversion D. - elim bci_range4 ; intro. - (**x=0**) - subst x . rewrite Zplus_0_r. rewrite Int.add_zero in H3. - subst ofs2 ; auto . - (**x<>0**) - rewrite H3. rewrite Int.add_signed. repeat rewrite Int.signed_repr. - auto. auto. - assert (low (blocks m1 b1) <= Int.signed ofs1 < high (blocks m1 b1)). - omega. - generalize (bci_lowhigh0 (Int.signed ofs1) H6). omega. - auto. + intros. inversion H. + elim (mi_range_4 _ _ _ H1); intro. + (* delta = 0 *) + subst delta. change (Int.repr 0) with Int.zero. + rewrite Int.add_zero. omega. + (* delta <> 0 *) + rewrite Int.add_signed. + repeat rewrite Int.signed_repr. auto. + eauto. + assert (valid_access m2 chunk b2 (Int.signed ofs1 + delta)). + eapply valid_access_inj; eauto. + inv H3. generalize (size_chunk_pos chunk); omega. + eauto. Qed. Lemma valid_pointer_inject_no_overflow: - forall m1 m2 b ofs b' x, - mem_inject m1 m2 -> + forall f m1 m2 b ofs b' x, + mem_inject f m1 m2 -> valid_pointer m1 b (Int.signed ofs) = true -> f b = Some(b', x) -> Int.min_signed <= Int.signed ofs + Int.signed (Int.repr x) <= Int.max_signed. Proof. - intros. unfold valid_pointer in H0. - destruct (zlt b (nextblock m1)); try discriminate. - destruct (zle (low (blocks m1 b)) (Int.signed ofs)); try discriminate. - destruct (zlt (Int.signed ofs) (high (blocks m1 b))); try discriminate. - inversion H. generalize (mi_mappedblocks0 _ _ _ H1). - intros [A B]. inversion B. - elim bci_range4 ; intro. - (**x=0**) - rewrite Int.signed_repr ; auto. - subst x . rewrite Zplus_0_r. apply Int.signed_range . - (**x<>0**) - generalize (bci_lowhigh0 _ (conj z0 z1)). intro. - rewrite Int.signed_repr. omega. auto. -Qed. - -(** Relation between injections and loads. *) - -Lemma check_cont_inject: - forall c1 c2 lo hi delta, - contentmap_inject c1 c2 lo hi delta -> - forall n p, - lo <= p -> p + Z_of_nat n <= hi -> - check_cont n p c1 = true -> - check_cont n (p + delta) c2 = true. -Proof. - induction n. - intros. simpl. reflexivity. - simpl check_cont. rewrite inj_S. intros p H0 H1. - assert (lo <= p < hi). omega. - generalize (H p H2). intro. inversion H3; intros; try discriminate. - replace (p + delta + 1) with ((p + 1) + delta). - apply IHn. omega. omega. auto. + intros. inv H. rewrite valid_pointer_valid_access in H0. + assert (valid_access m2 Mint8unsigned b' (Int.signed ofs + x)). + eapply valid_access_inj; eauto. + inv H. change (size_chunk Mint8unsigned) with 1 in H4. + rewrite Int.signed_repr; eauto. + exploit mi_range_4; eauto. intros [A | [A B]]. + subst x. rewrite Zplus_0_r. apply Int.signed_range. omega. Qed. -Hint Resolve check_cont_inject. - -Lemma getN_inject: - forall c1 c2 lo hi delta, - contentmap_inject c1 c2 lo hi delta -> - forall n p, - lo <= p -> p + Z_of_nat n < hi -> - content_inject (getN n p c1) (getN n (p + delta) c2). -Proof. - intros. simpl in H1. - assert (lo <= p < hi). omega. - unfold getN. - caseEq (check_cont n (p + 1) c1); intro. - replace (check_cont n (p + delta + 1) c2) with true. - apply H. assumption. - symmetry. replace (p + delta + 1) with ((p + 1) + delta). - eapply check_cont_inject; eauto. - omega. omega. omega. - constructor. -Qed. - -Hint Resolve getN_inject. - -Definition ztonat (z:Z): nat:= -match z with -| Z0 => O -| Zpos p => (nat_of_P p) -| Zneg p =>O -end. - -Lemma load_contents_inject: - forall sz c1 c2 lo hi delta p, - contentmap_inject c1 c2 lo hi delta -> - lo <= p -> p + size_mem sz <= hi -> - val_content_inject sz (load_contents sz c1 p) (load_contents sz c2 (p + delta)). -Proof. -intros. -assert (content_inject (getN (ztonat (size_mem sz)-1) p c1) -(getN (ztonat(size_mem sz)-1) (p + delta) c2)). -induction sz; assert (lo<= p< hi); simpl in H1; try omega; -apply getN_inject with lo hi; try assumption; simpl ; try omega. -induction sz ; simpl; inversion H2; auto. -Qed. - -Hint Resolve load_contents_inject. - -Lemma load_result_inject: - forall chunk v1 v2, - val_content_inject (mem_chunk chunk) v1 v2 -> - val_inject (Val.load_result chunk v1) (Val.load_result chunk v2). -Proof. -intros. -destruct chunk; simpl in H; inversion H; simpl; auto; -try (inversion H0; simpl; auto; fail). -replace (Int.cast8signed n2) with (Int.cast8signed n1). constructor. -apply Int.cast8_signed_equal_if_unsigned_equal; auto. -rewrite H0; constructor. -replace (Int.cast16signed n2) with (Int.cast16signed n1). constructor. -apply Int.cast16_signed_equal_if_unsigned_equal; auto. -rewrite H0; constructor. -inversion H0; simpl; auto. -apply val_inject_ptr with x; auto. -Qed. - -Lemma in_bounds_inject: - forall chunk c1 c2 delta p, - block_contents_inject c1 c2 delta -> - c1.(low) <= p /\ p + size_chunk chunk <= c1.(high) -> - c2.(low) <= p + delta /\ (p + delta) + size_chunk chunk <= c2.(high). +Lemma valid_pointer_inject: + forall f m1 m2 b ofs b' ofs', + mem_inject f m1 m2 -> + valid_pointer m1 b (Int.signed ofs) = true -> + val_inject f (Vptr b ofs) (Vptr b' ofs') -> + valid_pointer m2 b' (Int.signed ofs') = true. Proof. - intros. - inversion H. - generalize (size_chunk_pos chunk); intro. - assert (low c1 <= p + size_chunk chunk - 1 < high c1). - omega. - generalize (bci_lowhigh0 _ H2). intro. - assert (low c1 <= p < high c1). - omega. - generalize (bci_lowhigh0 _ H4). intro. - omega. + intros. inv H1. + exploit valid_pointer_inject_no_overflow; eauto. intro NOOV. + inv H. rewrite Int.add_signed. rewrite Int.signed_repr; auto. + rewrite Int.signed_repr; eauto. + eapply valid_pointer_inj; eauto. Qed. -Lemma block_cont_val: -forall c1 c2 delta p sz, -block_contents_inject c1 c2 delta -> -c1.(low) <= p -> p + size_mem sz <= c1.(high) -> - val_content_inject sz (load_contents sz c1.(contents) p) - (load_contents sz c2.(contents) (p + delta)). -Proof. -intros. -inversion H . -apply load_contents_inject with c1.(low) c1.(high) ;assumption. -Qed. +(** Relation between injections and loads. *) Lemma load_inject: - forall m1 m2 chunk b1 ofs b2 delta v1, - mem_inject m1 m2 -> + forall f m1 m2 chunk b1 ofs b2 delta v1, + mem_inject f m1 m2 -> load chunk m1 b1 ofs = Some v1 -> f b1 = Some (b2, delta) -> - exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject v1 v2. + exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2. Proof. - intros. - generalize (load_inv _ _ _ _ _ H0). intros [A [B [C D]]]. - inversion H. - generalize (mi_mappedblocks0 _ _ _ H1). intros [U V]. - inversion V. - exists (Val.load_result chunk (load_contents (mem_chunk chunk) - (m2.(blocks) b2).(contents) (ofs+delta))). - split. - unfold load. - generalize (size_chunk_pos chunk); intro. - rewrite zlt_true. rewrite in_bounds_holds. auto. - assert (low (blocks m1 b1) <= ofs < high (blocks m1 b1)). - omega. - generalize (bci_lowhigh0 _ H3). tauto. - assert (low (blocks m1 b1) <= ofs + size_chunk chunk - 1 < high(blocks m1 b1)). - omega. - generalize (bci_lowhigh0 _ H3). omega. - assumption. - rewrite <- D. apply load_result_inject. - eapply load_contents_inject; eauto. + intros. inversion H. + eapply mi_inj0; eauto. Qed. Lemma loadv_inject: - forall m1 m2 chunk a1 a2 v1, - mem_inject m1 m2 -> + forall f m1 m2 chunk a1 a2 v1, + mem_inject f m1 m2 -> loadv chunk m1 a1 = Some v1 -> - val_inject a1 a2 -> - exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject v1 v2. + val_inject f a1 a2 -> + exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. - induction H1 ; simpl in H0 ; try discriminate H0. - simpl. - replace (Int.signed ofs2) with (Int.signed ofs1 + x). - apply load_inject with m1 b1 ; assumption. - symmetry. generalize (load_inv _ _ _ _ _ H0). intros [A [B [C D]]]. - apply address_inject with m1 m2 chunk b1 b2; auto. + intros. inv H1; simpl in H0; try discriminate. + exploit load_inject; eauto. intros [v2 [LOAD INJ]]. + exists v2; split; auto. simpl. + replace (Int.signed (Int.add ofs1 (Int.repr x))) + with (Int.signed ofs1 + x). + auto. symmetry. eapply address_inject; eauto with mem. Qed. (** Relation between injections and stores. *) -Lemma set_cont_inject: - forall c1 c2 lo hi delta, - contentmap_inject c1 c2 lo hi delta -> - forall n p, - lo <= p -> p + Z_of_nat n <= hi -> - contentmap_inject (set_cont n p c1) (set_cont n (p + delta) c2) lo hi delta. -Proof. -induction n. intros. simpl. assumption. -intros. simpl. unfold contentmap_inject. -intros p2 Hp2. unfold update. -case (zeq p2 p); intro. -subst p2. rewrite zeq_true. constructor. -rewrite zeq_false. replace (p + delta + 1) with ((p + 1) + delta). -apply IHn. omega. rewrite inj_S in H1. omega. assumption. -omega. omega. -Qed. - -Lemma setN_inject: - forall c1 c2 lo hi delta n p v1 v2, - contentmap_inject c1 c2 lo hi delta -> - content_inject v1 v2 -> - lo <= p -> p + Z_of_nat n < hi -> - contentmap_inject (setN n p v1 c1) (setN n (p + delta) v2 c2) - lo hi delta. -Proof. - intros. unfold setN. red; intros. - unfold update. - case (zeq x p); intro. - subst p. rewrite zeq_true. assumption. - rewrite zeq_false. - replace (p + delta + 1) with ((p + 1) + delta). - apply set_cont_inject with lo hi. - assumption. omega. omega. assumption. omega. - omega. -Qed. - -Lemma store_contents_inject: - forall c1 c2 lo hi delta sz p v1 v2, - contentmap_inject c1 c2 lo hi delta -> - val_content_inject sz v1 v2 -> - lo <= p -> p + size_mem sz <= hi -> - contentmap_inject (store_contents sz c1 p v1) - (store_contents sz c2 (p + delta) v2) - lo hi delta. -Proof. - intros. - destruct sz; simpl in *; apply setN_inject; auto; simpl; omega. -Qed. - -Lemma set_cont_outside1 : - forall n p m q , - (forall x , p <= x < p + Z_of_nat n -> x <> q) -> - (set_cont n p m) q = m q. -Proof. - induction n; intros; simpl. - auto. - rewrite inj_S in H. rewrite update_o. apply IHn. - intros. apply H. omega. - apply H. omega. -Qed. - -Lemma set_cont_outside_inject: - forall c1 c2 lo hi delta, - contentmap_inject c1 c2 lo hi delta -> - forall n p, - (forall x1 x2, p <= x1 < p + Z_of_nat n -> - lo <= x2 < hi -> - x1 <> x2 + delta) -> - contentmap_inject c1 (set_cont n p c2) lo hi delta. -Proof. - unfold contentmap_inject. intros. - rewrite set_cont_outside1. apply H. assumption. - intros. apply H0. auto. auto. -Qed. - -Lemma setN_outside_inject: - forall n c1 c2 lo hi delta p v, - contentmap_inject c1 c2 lo hi delta -> - (forall x1 x2, p <= x1 < p + Z_of_nat (S n) -> - lo <= x2 < hi -> - x1 <> x2 + delta) -> - contentmap_inject c1 (setN n p v c2) lo hi delta. -Proof. - intros. unfold setN. red; intros. rewrite update_o. - apply set_cont_outside_inject with lo hi. auto. - intros. apply H0. rewrite inj_S. omega. auto. auto. - apply H0. rewrite inj_S. omega. auto. -Qed. +Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop := + | val_content_inject_base: + forall chunk v1 v2, + val_inject f v1 v2 -> + val_content_inject f chunk v1 v2 + | val_content_inject_8: + forall chunk n1 n2, + chunk = Mint8unsigned \/ chunk = Mint8signed -> + Int.cast8unsigned n1 = Int.cast8unsigned n2 -> + val_content_inject f chunk (Vint n1) (Vint n2) + | val_content_inject_16: + forall chunk n1 n2, + chunk = Mint16unsigned \/ chunk = Mint16signed -> + Int.cast16unsigned n1 = Int.cast16unsigned n2 -> + val_content_inject f chunk (Vint n1) (Vint n2) + | val_content_inject_32: + forall f1 f2, + Float.singleoffloat f1 = Float.singleoffloat f2 -> + val_content_inject f Mfloat32 (Vfloat f1) (Vfloat f2). -Lemma store_contents_outside_inject: - forall c1 c2 lo hi delta sz p v, - contentmap_inject c1 c2 lo hi delta -> - (forall x1 x2, p <= x1 < p + size_mem sz -> - lo <= x2 < hi -> - x1 <> x2 + delta)-> - contentmap_inject c1 (store_contents sz c2 p v) lo hi delta. -Proof. - intros c1 c2 lo hi delta sz. generalize (size_mem_pos sz) . intro . - induction sz ;intros ;simpl ; apply setN_outside_inject ; assumption . -Qed. +Hint Resolve val_content_inject_base. -Lemma store_mapped_inject_1: - forall chunk m1 b1 ofs v1 n1 m2 b2 delta v2, - mem_inject m1 m2 -> +Lemma load_result_inject: + forall f chunk v1 v2 chunk', + val_content_inject f chunk v1 v2 -> + size_chunk chunk = size_chunk chunk' -> + val_inject f (Val.load_result chunk' v1) (Val.load_result chunk' v2). +Proof. + intros. inv H; simpl. + inv H1; destruct chunk'; simpl; econstructor; eauto. + + elim H1; intro; subst chunk; + destruct chunk'; simpl in H0; try discriminate; simpl. + replace (Int.cast8signed n1) with (Int.cast8signed n2). + constructor. apply Int.cast8_signed_equal_if_unsigned_equal; auto. + rewrite H2. constructor. + replace (Int.cast8signed n1) with (Int.cast8signed n2). + constructor. apply Int.cast8_signed_equal_if_unsigned_equal; auto. + rewrite H2. constructor. + + elim H1; intro; subst chunk; + destruct chunk'; simpl in H0; try discriminate; simpl. + replace (Int.cast16signed n1) with (Int.cast16signed n2). + constructor. apply Int.cast16_signed_equal_if_unsigned_equal; auto. + rewrite H2. constructor. + replace (Int.cast16signed n1) with (Int.cast16signed n2). + constructor. apply Int.cast16_signed_equal_if_unsigned_equal; auto. + rewrite H2. constructor. + + destruct chunk'; simpl in H0; try discriminate; simpl. + constructor. rewrite H1; constructor. +Qed. + +Lemma store_mapped_inject_1 : + forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2, + mem_inject f m1 m2 -> store chunk m1 b1 ofs v1 = Some n1 -> f b1 = Some (b2, delta) -> - val_content_inject (mem_chunk chunk) v1 v2 -> + val_content_inject f chunk v1 v2 -> exists n2, store chunk m2 b2 (ofs + delta) v2 = Some n2 - /\ mem_inject n1 n2. -Proof. -intros. -generalize (size_chunk_pos chunk); intro SIZEPOS. -generalize (store_inv _ _ _ _ _ _ H0). -intros [A [B [C [D [P E]]]]]. -inversion H. -generalize (mi_mappedblocks0 _ _ _ H1). intros [U V]. -inversion V. -generalize (in_bounds_inject _ _ _ _ _ V (conj B C)). intro BND. -exists (unchecked_store chunk m2 b2 (ofs+delta) v2 BND). -split. unfold store. -rewrite zlt_true; auto. -case (in_bounds chunk (ofs + delta) (blocks m2 b2)); intro. -assert (a = BND). apply proof_irrelevance. congruence. -omegaContradiction. -constructor. -intros. apply mi_freeblocks0. rewrite <- D. assumption. -intros. generalize (mi_mappedblocks0 b b' delta0 H3). -intros [W Y]. split. simpl. auto. -rewrite E; simpl. unfold update. -(* Cas 1: memes blocs b = b1 b'= b2 *) -case (zeq b b1); intro. -subst b. assert (b'= b2). congruence. subst b'. -assert (delta0 = delta). congruence. subst delta0. -rewrite zeq_true. inversion Y. constructor; simpl; auto. -apply store_contents_inject; auto. -(* Cas 2: blocs differents dans m1 mais mappes sur le meme bloc de m2 *) -case (zeq b' b2); intro. -subst b'. -inversion Y. constructor; simpl; auto. -generalize (store_contents_outside_inject _ _ _ _ _ (mem_chunk chunk) - (ofs+delta) v2 bci_contents1). -intros. -apply H4. -elim (mi_no_overlap0 b b1 b2 b2 delta0 delta n H3 H1). -tauto. -unfold high_bound, low_bound. intros. -apply sym_not_equal. replace x1 with ((x1 - delta) + delta). -apply H5. assumption. unfold size_chunk in C. omega. omega. -(* Cas 3: blocs differents dans m1 et dans m2 *) -auto. - -unfold high_bound, low_bound. -rewrite E; simpl; intros. -unfold high_bound, low_bound in mi_no_overlap0. -unfold update. -case (zeq b0 b1). -intro. subst b1. simpl. -rewrite zeq_false; auto. -intro. case (zeq b3 b1); intro. -subst b3. simpl. auto. -auto. + /\ mem_inject f n1 n2. +Proof. + intros. inversion H. + exploit store_mapped_inj; eauto. + intros; constructor. + intros. apply load_result_inject with chunk; eauto. + intros [n2 [STORE MINJ]]. + exists n2; split. auto. constructor. + (* inj *) + auto. + (* freeblocks *) + intros. apply mi_freeblocks0. red; intro. elim H3. eauto with mem. + (* mappedblocks *) + intros. eauto with mem. + (* no_overlap *) + red; intros. + repeat rewrite (low_bound_store _ _ _ _ _ _ H0). + repeat rewrite (high_bound_store _ _ _ _ _ _ H0). + eapply mi_no_overlap0; eauto. + (* range *) + auto. + intros. + repeat rewrite (low_bound_store _ _ _ _ _ _ STORE). + repeat rewrite (high_bound_store _ _ _ _ _ _ STORE). + eapply mi_range_4; eauto. Qed. Lemma store_mapped_inject: - forall chunk m1 b1 ofs v1 n1 m2 b2 delta v2, - mem_inject m1 m2 -> + forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2, + mem_inject f m1 m2 -> store chunk m1 b1 ofs v1 = Some n1 -> f b1 = Some (b2, delta) -> - val_inject v1 v2 -> + val_inject f v1 v2 -> exists n2, store chunk m2 b2 (ofs + delta) v2 = Some n2 - /\ mem_inject n1 n2. + /\ mem_inject f n1 n2. Proof. intros. eapply store_mapped_inject_1; eauto. Qed. Lemma store_unmapped_inject: - forall chunk m1 b1 ofs v1 n1 m2, - mem_inject m1 m2 -> + forall f chunk m1 b1 ofs v1 n1 m2, + mem_inject f m1 m2 -> store chunk m1 b1 ofs v1 = Some n1 -> f b1 = None -> - mem_inject n1 m2. -Proof. -intros. -inversion H. -generalize (store_inv _ _ _ _ _ _ H0). -intros [A [B [C [D [P E]]]]]. -constructor. -rewrite D. assumption. -intros. elim (mi_mappedblocks0 _ _ _ H2); intros. -split. auto. -rewrite E; unfold update. -rewrite zeq_false. assumption. -congruence. -intros. -assert (forall b, low_bound n1 b = low_bound m1 b). - intros. unfold low_bound; rewrite E; unfold update. - case (zeq b b1); intros. subst b1; reflexivity. reflexivity. -assert (forall b, high_bound n1 b = high_bound m1 b). - intros. unfold high_bound; rewrite E; unfold update. - case (zeq b b1); intros. subst b1; reflexivity. reflexivity. -repeat rewrite H5. repeat rewrite H6. auto. + mem_inject f n1 m2. +Proof. + intros. inversion H. + constructor. + (* inj *) + eapply store_unmapped_inj; eauto. + (* freeblocks *) + intros. apply mi_freeblocks0. red; intros; elim H2; eauto with mem. + (* mappedblocks *) + intros. eapply mi_mappedblocks0; eauto with mem. + (* no_overlap *) + red; intros. + repeat rewrite (low_bound_store _ _ _ _ _ _ H0). + repeat rewrite (high_bound_store _ _ _ _ _ _ H0). + eapply mi_no_overlap0; eauto. + (* range *) + auto. auto. Qed. Lemma storev_mapped_inject_1: - forall chunk m1 a1 v1 n1 m2 a2 v2, - mem_inject m1 m2 -> + forall f chunk m1 a1 v1 n1 m2 a2 v2, + mem_inject f m1 m2 -> storev chunk m1 a1 v1 = Some n1 -> - val_inject a1 a2 -> - val_content_inject (mem_chunk chunk) v1 v2 -> + val_inject f a1 a2 -> + val_content_inject f chunk v1 v2 -> exists n2, - storev chunk m2 a2 v2 = Some n2 /\ mem_inject n1 n2. + storev chunk m2 a2 v2 = Some n2 /\ mem_inject f n1 n2. Proof. - intros. destruct a1; simpl in H0; try discriminate. - inversion H1. subst b. - simpl. replace (Int.signed ofs2) with (Int.signed i + x). + intros. inv H1; simpl in H0; try discriminate. + simpl. replace (Int.signed (Int.add ofs1 (Int.repr x))) + with (Int.signed ofs1 + x). eapply store_mapped_inject_1; eauto. - symmetry. generalize (store_inv _ _ _ _ _ _ H0). intros [A [B [C [D [P E]]]]]. - apply address_inject with m1 m2 chunk b1 b2; auto. + symmetry. eapply address_inject; eauto with mem. Qed. Lemma storev_mapped_inject: - forall chunk m1 a1 v1 n1 m2 a2 v2, - mem_inject m1 m2 -> + forall f chunk m1 a1 v1 n1 m2 a2 v2, + mem_inject f m1 m2 -> storev chunk m1 a1 v1 = Some n1 -> - val_inject a1 a2 -> - val_inject v1 v2 -> + val_inject f a1 a2 -> + val_inject f v1 v2 -> exists n2, - storev chunk m2 a2 v2 = Some n2 /\ mem_inject n1 n2. + storev chunk m2 a2 v2 = Some n2 /\ mem_inject f n1 n2. Proof. intros. eapply storev_mapped_inject_1; eauto. Qed. (** Relation between injections and [free] *) -Lemma free_first_inject : - forall m1 m2 b, - mem_inject m1 m2 -> - mem_inject (free m1 b) m2. -Proof. - intros. inversion H. constructor . auto. - simpl. intros. - generalize (mi_mappedblocks0 b0 b' delta H0). - intros [A B] . split. assumption . unfold update. - case (zeq b0 b); intro. inversion B. constructor; simpl; auto. - intros. omega. - unfold contentmap_inject. - intros. omegaContradiction. - auto. intros. - unfold free . unfold low_bound , high_bound. simpl. unfold update. - case (zeq b1 b);intro. simpl. - right. intros. omegaContradiction. - case (zeq b2 b);intro. simpl. - right . intros. omegaContradiction. - unfold low_bound, high_bound in mi_no_overlap0. auto. -Qed. - -Lemma free_first_list_inject : - forall l m1 m2, - mem_inject m1 m2 -> - mem_inject (free_list m1 l) m2. -Proof. - induction l; simpl; intros. - auto. - apply free_first_inject. auto. -Qed. - -Lemma free_snd_inject: - forall m1 m2 b, - (forall b1 delta, f b1 = Some(b, delta) -> - low_bound m1 b1 >= high_bound m1 b1) -> - mem_inject m1 m2 -> - mem_inject m1 (free m2 b). -Proof. - intros. inversion H0. constructor. auto. - simpl. intros. - generalize (mi_mappedblocks0 b0 b' delta H1). - intros [A B] . split. assumption . - inversion B. unfold update. - case (zeq b' b); intro. - subst b'. generalize (H _ _ H1). unfold low_bound, high_bound; intro. - constructor. auto. elim bci_range4 ; intro. - (**delta=0**) - left ; auto . - (** delta<>0**) - right . - simpl. compute. split; intro; congruence. - intros. omegaContradiction. - red; intros. omegaContradiction. - auto. - auto. -Qed. - -Lemma bounds_free_block: - forall m1 b m1' , free m1 b = m1' -> - low_bound m1' b >= high_bound m1' b. +Lemma meminj_no_overlap_free: + forall mi m b, + meminj_no_overlap mi m -> + meminj_no_overlap mi (free m b). Proof. - intros. unfold free in H. - rewrite<- H . unfold low_bound , high_bound . - simpl . rewrite update_s. simpl. omega. + intros; red; intros. + assert (low_bound (free m b) b >= high_bound (free m b) b). + rewrite low_bound_free_same; rewrite high_bound_free_same; auto. + omega. + destruct (eq_block b1 b); destruct (eq_block b2 b); subst; auto. + repeat (rewrite low_bound_free; auto). + repeat (rewrite high_bound_free; auto). Qed. -Lemma free_empty_bounds: - forall l m1 , - let m1' := free_list m1 l in - (forall b, In b l -> low_bound m1' b >= high_bound m1' b). +Lemma meminj_no_overlap_free_list: + forall mi m bl, + meminj_no_overlap mi m -> + meminj_no_overlap mi (free_list m bl). Proof. - induction l . intros . inversion H. - intros. - generalize (in_inv H). - intro . elim H0. intro . subst b. simpl in m1' . - generalize ( bounds_free_block - (fold_right (fun (b : block) (m : mem) => free m b) m1 l) a m1') . - intros. apply H1. auto . intros. simpl in m1'. unfold m1' . - unfold low_bound , high_bound . simpl . - unfold update; case (zeq b a); intro; simpl. - omega . - unfold low_bound , high_bound in IHl . auto. -Qed. + induction bl; simpl; intros. auto. + apply meminj_no_overlap_free. auto. +Qed. Lemma free_inject: - forall m1 m2 l b, + forall f m1 m2 l b, (forall b1 delta, f b1 = Some(b, delta) -> In b1 l) -> - mem_inject m1 m2 -> - mem_inject (free_list m1 l) (free m2 b). -Proof. - intros. apply free_snd_inject. - intros. apply free_empty_bounds. apply H with delta. auto. - apply free_first_list_inject. auto. -Qed. - -Lemma contents_init_data_inject: - forall id, contentmap_inject (contents_init_data 0 id) (contents_init_data 0 id) 0 (size_init_data_list id) 0. -Proof. - intro id0. - set (sz0 := size_init_data_list id0). - assert (forall id pos, - 0 <= pos -> pos + size_init_data_list id <= sz0 -> - contentmap_inject (contents_init_data pos id) (contents_init_data pos id) 0 sz0 0). - induction id; simpl; intros. - red; intros; constructor. - assert (forall n dt, - size_init_data a = 1 + Z_of_nat n -> - content_inject dt dt -> - contentmap_inject (setN n pos dt (contents_init_data (pos + size_init_data a) id)) - (setN n pos dt (contents_init_data (pos + size_init_data a) id)) - 0 sz0 0). - intros. set (pos' := pos) in |- * at 3. replace pos' with (pos + 0). - apply setN_inject. apply IHid. omega. omega. auto. auto. - generalize (size_init_data_list_pos id). omega. unfold pos'; omega. - destruct a; - try (apply H1; [reflexivity|repeat constructor]). - apply IHid. generalize (Zmax2 z 0). omega. simpl in H0; omega. - apply IHid. omega. simpl size_init_data in H0. omega. - apply H. omega. unfold sz0. omega. -Qed. - -End MEM_INJECT. - -Hint Resolve val_inject_int val_inject_float val_inject_ptr val_inject_undef. -Hint Resolve val_nil_inject val_cons_inject. + mem_inject f m1 m2 -> + mem_inject f (free_list m1 l) (free m2 b). +Proof. + intros. inversion H0. constructor. + (* inj *) + apply free_right_inj. apply free_list_left_inj. auto. + intros; red; intros. + elim (valid_access_free_list_inv _ _ _ _ _ H2); intros. + elim H3; eauto. + (* freeblocks *) + intros. apply mi_freeblocks0. red; intro; elim H1. + apply valid_block_free_list_1; auto. + (* mappedblocks *) + intros. apply valid_block_free_1. eauto. + (* overlap *) + apply meminj_no_overlap_free_list; auto. + (* range *) + auto. + intros. destruct (eq_block b' b). subst b'. + rewrite low_bound_free_same; rewrite high_bound_free_same. + right; compute; intuition congruence. + rewrite low_bound_free; auto. rewrite high_bound_free; auto. + eauto. +Qed. (** Monotonicity properties of memory injections. *) @@ -2160,16 +2100,11 @@ Lemma inject_incr_refl : Proof. unfold inject_incr . intros. left . auto . Qed. Lemma inject_incr_trans : - forall f1 f2 f3 , + forall f1 f2 f3, inject_incr f1 f2 -> inject_incr f2 f3 -> inject_incr f1 f3 . Proof . - unfold inject_incr . intros . - generalize (H b) . intro . generalize (H0 b) . intro . - elim H1 ; elim H2 ; intros. - rewrite H3 in H4 . left . auto . - rewrite H3 in H4 . right . auto . - right ; auto . - right ; auto . + unfold inject_incr; intros. + generalize (H b); generalize (H0 b); intuition congruence. Qed. Lemma val_inject_incr: @@ -2192,61 +2127,17 @@ Lemma val_list_inject_incr: inject_incr f1 f2 -> val_list_inject f1 vl vl' -> val_list_inject f2 vl vl'. Proof. - induction vl ; intros; inversion H0. auto . - subst a . generalize (val_inject_incr f1 f2 v v' H H3) . - intro . auto . -Qed. - -Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr. - -Section MEM_INJECT_INCR. - -Variable f1 f2: meminj. -Hypothesis INCR: inject_incr f1 f2. - -Lemma val_content_inject_incr: - forall chunk v v', - val_content_inject f1 chunk v v' -> - val_content_inject f2 chunk v v'. -Proof. - intros. inversion H. - apply val_content_inject_base. eapply val_inject_incr; eauto. - apply val_content_inject_8; auto. - apply val_content_inject_16; auto. - apply val_content_inject_32; auto. + induction vl; intros; inv H0. auto. + constructor. eapply val_inject_incr; eauto. auto. Qed. -Lemma content_inject_incr: - forall c c', content_inject f1 c c' -> content_inject f2 c c'. -Proof. - induction 1; constructor; eapply val_content_inject_incr; eauto. -Qed. - -Lemma contentmap_inject_incr: - forall c c' lo hi delta, - contentmap_inject f1 c c' lo hi delta -> - contentmap_inject f2 c c' lo hi delta. -Proof. - unfold contentmap_inject; intros. - apply content_inject_incr. auto. -Qed. - -Lemma block_contents_inject_incr: - forall c c' delta, - block_contents_inject f1 c c' delta -> - block_contents_inject f2 c c' delta. -Proof. - intros. inversion H. constructor; auto. - apply contentmap_inject_incr; auto. -Qed. - -End MEM_INJECT_INCR. +Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr. (** Properties of injections and allocations. *) Definition extend_inject (b: block) (x: option (block * Z)) (f: meminj) : meminj := - fun b' => if eq_block b' b then x else f b'. + fun (b': block) => if zeq b' b then x else f b'. Lemma extend_inject_incr: forall f b x, @@ -2254,7 +2145,7 @@ Lemma extend_inject_incr: inject_incr f (extend_inject b x f). Proof. intros; red; intros. unfold extend_inject. - case (eq_block b0 b); intro. subst b0. right; auto. left; auto. + destruct (zeq b0 b). subst b0; auto. auto. Qed. Lemma alloc_right_inject: @@ -2263,14 +2154,17 @@ Lemma alloc_right_inject: alloc m2 lo hi = (m2', b) -> mem_inject f m1 m2'. Proof. - intros. unfold alloc in H0. injection H0; intros A B; clear H0. - inversion H. - constructor. - assumption. - intros. generalize (mi_mappedblocks0 _ _ _ H0). intros [C D]. - rewrite <- B; simpl. split. omega. - rewrite update_o. auto. omega. - assumption. + intros. inversion H. constructor. + eapply alloc_right_inj; eauto. + auto. + intros. eauto with mem. + auto. + auto. + intros. replace (low_bound m2' b') with (low_bound m2 b'). + replace (high_bound m2' b') with (high_bound m2 b'). + eauto. + symmetry. eapply high_bound_alloc_other; eauto. + symmetry. eapply low_bound_alloc_other; eauto. Qed. Lemma alloc_unmapped_inject: @@ -2280,26 +2174,36 @@ Lemma alloc_unmapped_inject: mem_inject (extend_inject b None f) m1' m2 /\ inject_incr f (extend_inject b None f). Proof. - intros. unfold alloc in H0. injection H0; intros; clear H0. - inversion H. + intros. inversion H. assert (inject_incr f (extend_inject b None f)). - apply extend_inject_incr. apply mi_freeblocks0. rewrite H1. omega. - split; auto. - constructor. - rewrite <- H2; simpl; intros. unfold extend_inject. - case (eq_block b0 b); intro. auto. apply mi_freeblocks0. omega. - intros until delta. unfold extend_inject at 1. case (eq_block b0 b); intro. - intros; discriminate. - intros. rewrite <- H2; simpl. rewrite H1. - rewrite update_o; auto. - elim (mi_mappedblocks0 _ _ _ H3). intros A B. - split. auto. apply block_contents_inject_incr with f. auto. auto. - intros until delta2. unfold extend_inject. - case (eq_block b1 b); intro. congruence. - case (eq_block b2 b); intro. congruence. - rewrite <- H2. unfold low_bound, high_bound; simpl. rewrite H1. - repeat rewrite update_o; auto. - exact (mi_no_overlap0 b1 b2 b1' b2' delta1 delta2). + apply extend_inject_incr. apply mi_freeblocks0. eauto with mem. + split; auto. constructor. + (* inj *) + eapply alloc_left_unmapped_inj; eauto. + red; intros. unfold extend_inject in H2. + destruct (zeq b1 b). congruence. + exploit mi_inj0; eauto. intros [v2 [LOAD VINJ]]. + exists v2; split. auto. + apply val_inject_incr with f; auto. + unfold extend_inject. apply zeq_true. + (* freeblocks *) + intros. unfold extend_inject. destruct (zeq b0 b). auto. + apply mi_freeblocks0; red; intro. elim H2. eauto with mem. + (* mappedblocks *) + intros. unfold extend_inject in H2. destruct (zeq b0 b). + discriminate. eauto. + (* overlap *) + red; unfold extend_inject, update; intros. + repeat rewrite (low_bound_alloc _ _ _ _ _ H0). + repeat rewrite (high_bound_alloc _ _ _ _ _ H0). + destruct (zeq b1 b); try discriminate. + destruct (zeq b2 b); try discriminate. + eauto. + (* range *) + unfold extend_inject; intros. + destruct (zeq b0 b). discriminate. eauto. + unfold extend_inject; intros. + destruct (zeq b0 b). discriminate. eauto. Qed. Lemma alloc_mapped_inject: @@ -2319,50 +2223,41 @@ Lemma alloc_mapped_inject: mem_inject (extend_inject b (Some (b', ofs)) f) m1' m2 /\ inject_incr f (extend_inject b (Some (b', ofs)) f). Proof. - intros. - generalize (fun b' => low_bound_alloc _ _ b' _ _ _ H0). - intro LOW. - generalize (fun b' => high_bound_alloc _ _ b' _ _ _ H0). - intro HIGH. - unfold alloc in H0. injection H0; intros A B; clear H0. - inversion H. - (* inject_incr *) + intros. inversion H. assert (inject_incr f (extend_inject b (Some (b', ofs)) f)). - apply extend_inject_incr. apply mi_freeblocks0. rewrite A. omega. + apply extend_inject_incr. apply mi_freeblocks0. eauto with mem. split; auto. constructor. - (* mi_freeblocks *) - rewrite <- B; simpl; intros. unfold extend_inject. - case (eq_block b0 b); intro. unfold block in *. omegaContradiction. - apply mi_freeblocks0. omega. - (* mi_mappedblocks *) - intros until delta. unfold extend_inject at 1. - case (eq_block b0 b); intro. - intros. subst b0. inversion H8. subst b'0; subst delta. - split. assumption. - rewrite <- B; simpl. rewrite A. rewrite update_s. - constructor; auto. - unfold empty_block. simpl. intros. unfold low_bound in H5. unfold high_bound in H6. omega. - simpl. red; intros. constructor. - intros. - generalize (mi_mappedblocks0 _ _ _ H8). intros [C D]. - split. auto. - rewrite <- B; simpl; rewrite A; rewrite update_o; auto. - apply block_contents_inject_incr with f; auto. - (* no overlap *) - intros until delta2. unfold extend_inject. - repeat rewrite LOW. repeat rewrite HIGH. unfold eq_block. - case (zeq b1 b); case (zeq b2 b); intros. - congruence. - inversion H9. subst b1'; subst delta1. - case (eq_block b' b2'); intro. - subst b2'. generalize (H7 _ _ H10). intro. - right. intros. omega. left. auto. - inversion H10. subst b2'; subst delta2. - case (eq_block b' b1'); intro. - subst b1'. generalize (H7 _ _ H9). intro. - right. intros. omega. left. auto. - apply mi_no_overlap0; auto. + (* inj *) + eapply alloc_left_mapped_inj; eauto. + red; intros. unfold extend_inject in H9. + rewrite zeq_false in H9. + exploit mi_inj0; eauto. intros [v2 [LOAD VINJ]]. + exists v2; split. auto. eapply val_inject_incr; eauto. + eauto with mem. + unfold extend_inject. apply zeq_true. + (* freeblocks *) + intros. unfold extend_inject. rewrite zeq_false. + apply mi_freeblocks0. red; intro. elim H9; eauto with mem. + apply sym_not_equal; eauto with mem. + (* mappedblocks *) + unfold extend_inject; intros. + destruct (zeq b0 b). inv H9. auto. eauto. + (* overlap *) + red; unfold extend_inject, update; intros. + repeat rewrite (low_bound_alloc _ _ _ _ _ H0). + repeat rewrite (high_bound_alloc _ _ _ _ _ H0). + destruct (zeq b1 b); [inv H10|idtac]; + (destruct (zeq b2 b); [inv H11|idtac]). + congruence. + destruct (zeq b1' b2'). subst b2'. generalize (H7 _ _ H11). tauto. auto. + destruct (zeq b1' b2'). subst b2'. generalize (H7 _ _ H10). tauto. auto. + eauto. + (* range *) + unfold extend_inject; intros. + destruct (zeq b0 b). inv H9. auto. eauto. + unfold extend_inject; intros. + destruct (zeq b0 b). inv H9. auto. eauto. Qed. Lemma alloc_parallel_inject: @@ -2371,20 +2266,104 @@ Lemma alloc_parallel_inject: alloc m1 lo hi = (m1', b1) -> alloc m2 lo hi = (m2', b2) -> Int.min_signed <= lo -> hi <= Int.max_signed -> - mem_inject (extend_inject b1 (Some(b2,0)) f) m1' m2' /\ - inject_incr f (extend_inject b1 (Some(b2,0)) f). + mem_inject (extend_inject b1 (Some(b2, 0)) f) m1' m2' /\ + inject_incr f (extend_inject b1 (Some(b2, 0)) f). Proof. intros. - generalize (low_bound_alloc _ _ b2 _ _ _ H1). rewrite zeq_true; intro LOW. - generalize (high_bound_alloc _ _ b2 _ _ _ H1). rewrite zeq_true; intro HIGH. eapply alloc_mapped_inject; eauto. eapply alloc_right_inject; eauto. - eapply valid_new_block; eauto. - compute. intuition congruence. - rewrite LOW; auto. - rewrite HIGH; auto. - rewrite LOW; omega. - rewrite HIGH; omega. - intros. elim (mi_mappedblocks _ _ _ H _ _ _ H4); intros. - injection H1; intros. rewrite H7 in H5. omegaContradiction. + eauto with mem. + compute; intuition congruence. + rewrite (low_bound_alloc_same _ _ _ _ _ H1). auto. + rewrite (high_bound_alloc_same _ _ _ _ _ H1). auto. + rewrite (low_bound_alloc_same _ _ _ _ _ H1). omega. + rewrite (high_bound_alloc_same _ _ _ _ _ H1). omega. + intros. elimtype False. inv H. + exploit mi_mappedblocks0; eauto. + change (~ valid_block m2 b2). eauto with mem. +Qed. + +Definition meminj_init (m: mem) : meminj := + fun (b: block) => if zlt b m.(nextblock) then Some(b, 0) else None. + +Definition mem_inject_neutral (m: mem) : Prop := + forall f chunk b ofs v, + load chunk m b ofs = Some v -> val_inject f v v. + +Lemma init_inject: + forall m, + mem_inject_neutral m -> + mem_inject (meminj_init m) m m. +Proof. + intros; constructor. + (* inj *) + red; intros. unfold meminj_init in H0. + destruct (zlt b1 (nextblock m)); inversion H0. + subst b2 delta. exists v1; split. + rewrite Zplus_0_r. auto. eapply H; eauto. + (* free blocks *) + unfold valid_block, meminj_init; intros. + apply zlt_false. omega. + (* mapped blocks *) + unfold valid_block, meminj_init; intros. + destruct (zlt b (nextblock m)); inversion H0. subst b'; auto. + (* overlap *) + red; unfold meminj_init; intros. + destruct (zlt b1 (nextblock m)); inversion H1. + destruct (zlt b2 (nextblock m)); inversion H2. + left; congruence. + (* range *) + unfold meminj_init; intros. + destruct (zlt b (nextblock m)); inversion H0. subst delta. + compute; intuition congruence. + unfold meminj_init; intros. + destruct (zlt b (nextblock m)); inversion H0. subst delta. + auto. +Qed. + +Remark getN_setN_inject: + forall f m v n1 p1 n2 p2, + val_inject f (getN n2 p2 m) (getN n2 p2 m) -> + val_inject f v v -> + val_inject f (getN n2 p2 (setN n1 p1 v m)) + (getN n2 p2 (setN n1 p1 v m)). +Proof. + intros. + destruct (getN_setN_characterization m v n1 p1 n2 p2) + as [A | [A | A]]; rewrite A; auto. +Qed. + +Remark getN_contents_init_data_inject: + forall f n ofs id pos, + val_inject f (getN n ofs (contents_init_data pos id)) + (getN n ofs (contents_init_data pos id)). +Proof. + induction id; simpl; intros. + repeat rewrite getN_init. constructor. + destruct a; auto; apply getN_setN_inject; auto. +Qed. + +Lemma alloc_init_data_neutral: + forall m id m' b, + mem_inject_neutral m -> + alloc_init_data m id = (m', b) -> + mem_inject_neutral m'. +Proof. + intros. injection H0; intros A B. + red; intros. + exploit load_inv; eauto. intros [C D]. + rewrite <- B in D; simpl in D. rewrite A in D. + unfold update in D. destruct (zeq b0 b). + subst b0. rewrite D. simpl. + apply load_result_inject with chunk. constructor. + apply getN_contents_init_data_inject. auto. + apply H with chunk b0 ofs. unfold load. + rewrite in_bounds_true. congruence. + inversion C. constructor. + generalize H2. unfold valid_block. rewrite <- B; simpl. + rewrite A. unfold block in n; intros. omega. + replace (low_bound m b0) with (low_bound m' b0). auto. + unfold low_bound; rewrite <- B; simpl; rewrite A. rewrite update_o; auto. + replace (high_bound m b0) with (high_bound m' b0). auto. + unfold high_bound; rewrite <- B; simpl; rewrite A. rewrite update_o; auto. Qed. diff --git a/common/Smallstep.v b/common/Smallstep.v new file mode 100644 index 0000000..7f6c776 --- /dev/null +++ b/common/Smallstep.v @@ -0,0 +1,460 @@ +(** Tools for small-step operational semantics *) + +(** This module defines generic operations and theorems over + the one-step transition relations that are used to specify + operational semantics in small-step style. *) + +Require Import Coqlib. +Require Import AST. +Require Import Events. +Require Import Globalenvs. +Require Import Integers. + +Set Implicit Arguments. + +(** * Closures of transitions relations *) + +Section CLOSURES. + +Variable genv: Set. +Variable state: Set. + +(** A one-step transition relation has the following signature. + It is parameterized by a global environment, which does not + change during the transition. It relates the initial state + of the transition with its final state. The [trace] parameter + captures the observable events possibly generated during the + transition. *) + +Variable step: genv -> state -> trace -> state -> Prop. + +(** Zero, one or several transitions. Also known as Kleene closure, + or reflexive transitive closure. *) + +Inductive star (ge: genv): state -> trace -> state -> Prop := + | star_refl: forall s, + star ge s E0 s + | star_step: forall s1 t1 s2 t2 s3 t, + step ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 -> + star ge s1 t s3. + +Lemma star_one: + forall ge s1 t s2, step ge s1 t s2 -> star ge s1 t s2. +Proof. + intros. eapply star_step; eauto. apply star_refl. traceEq. +Qed. + +Lemma star_trans: + forall ge s1 t1 s2, star ge s1 t1 s2 -> + forall t2 s3 t, star ge s2 t2 s3 -> t = t1 ** t2 -> star ge s1 t s3. +Proof. + induction 1; intros. + rewrite H0. simpl. auto. + eapply star_step; eauto. traceEq. +Qed. + +Lemma star_left: + forall ge s1 t1 s2 t2 s3 t, + step ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 -> + star ge s1 t s3. +Proof star_step. + +Lemma star_right: + forall ge s1 t1 s2 t2 s3 t, + star ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 -> + star ge s1 t s3. +Proof. + intros. eapply star_trans. eauto. apply star_one. eauto. auto. +Qed. + +(** One or several transitions. Also known as the transitive closure. *) + +Inductive plus (ge: genv): state -> trace -> state -> Prop := + | plus_left: forall s1 t1 s2 t2 s3 t, + step ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 -> + plus ge s1 t s3. + +Lemma plus_one: + forall ge s1 t s2, + step ge s1 t s2 -> plus ge s1 t s2. +Proof. + intros. econstructor; eauto. apply star_refl. traceEq. +Qed. + +Lemma plus_star: + forall ge s1 t s2, plus ge s1 t s2 -> star ge s1 t s2. +Proof. + intros. inversion H; subst. + eapply star_step; eauto. +Qed. + +Lemma plus_right: + forall ge s1 t1 s2 t2 s3 t, + star ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 -> + plus ge s1 t s3. +Proof. + intros. inversion H; subst. simpl. apply plus_one. auto. + rewrite Eapp_assoc. eapply plus_left; eauto. + eapply star_right; eauto. +Qed. + +Lemma plus_left': + forall ge s1 t1 s2 t2 s3 t, + step ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> + plus ge s1 t s3. +Proof. + intros. eapply plus_left; eauto. apply plus_star; auto. +Qed. + +Lemma plus_right': + forall ge s1 t1 s2 t2 s3 t, + plus ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 -> + plus ge s1 t s3. +Proof. + intros. eapply plus_right; eauto. apply plus_star; auto. +Qed. + +Lemma plus_star_trans: + forall ge s1 t1 s2 t2 s3 t, + plus ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. +Proof. + intros. inversion H; subst. + econstructor; eauto. eapply star_trans; eauto. + traceEq. +Qed. + +Lemma star_plus_trans: + forall ge s1 t1 s2 t2 s3 t, + star ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. +Proof. + intros. inversion H; subst. + simpl; auto. + rewrite Eapp_assoc. + econstructor. eauto. eapply star_trans. eauto. + apply plus_star. eauto. eauto. auto. +Qed. + +Lemma plus_trans: + forall ge s1 t1 s2 t2 s3 t, + plus ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. +Proof. + intros. eapply plus_star_trans. eauto. apply plus_star. eauto. auto. +Qed. + +Lemma plus_inv: + forall ge s1 t s2, plus ge s1 t s2 -> + step ge s1 t s2 \/ exists s', exists t1, exists t2, step ge s1 t1 s' /\ plus ge s' t2 s2 /\ t = t1 ** t2. +Proof. + intros. inversion H; subst. inversion H1; subst. + left. rewrite E0_right. auto. + right. exists s3; exists t1; exists (t0 ** t3); split. auto. + split. econstructor; eauto. auto. +Qed. + +(** Infinitely many transitions *) + +CoInductive forever (ge: genv): state -> traceinf -> Prop := + | forever_intro: forall s1 t s2 T, + step ge s1 t s2 -> forever ge s2 T -> + forever ge s1 (t *** T). + +(** An alternate, equivalent definition of [forever] that is useful + for coinductive reasoning. *) + +CoInductive forever_N (ge: genv): nat -> state -> traceinf -> Prop := + | forever_N_star: forall s1 t s2 p q T, + star ge s1 t s2 -> (p < q)%nat -> forever_N ge p s2 T -> + forever_N ge q s1 (t *** T) + | forever_N_plus: forall s1 t s2 p q T, + plus ge s1 t s2 -> forever_N ge p s2 T -> + forever_N ge q s1 (t *** T). + +Remark Peano_induction: + forall (P: nat -> Prop), + (forall p, (forall q, (q < p)%nat -> P q) -> P p) -> + forall p, P p. +Proof. + intros P IH. + assert (forall p, forall q, (q < p)%nat -> P q). + induction p; intros. elimtype False; omega. + apply IH. intros. apply IHp. omega. + intro. apply H with (S p). omega. +Qed. + +Lemma forever_N_inv: + forall ge p s T, + forever_N ge p s T -> + exists t, exists s', exists q, exists T', + step ge s t s' /\ forever_N ge q s' T' /\ T = t *** T'. +Proof. + intros ge p. pattern p. apply Peano_induction; intros. + inv H0. + (* star case *) + inv H1. + (* no transition *) + change (E0 *** T0) with T0. apply H with p1. auto. auto. + (* at least one transition *) + exists t1; exists s0; exists p0; exists (t2 *** T0). + split. auto. split. eapply forever_N_star; eauto. + apply Eappinf_assoc. + (* plus case *) + inv H1. + exists t1; exists s0; exists (S p1); exists (t2 *** T0). + split. auto. split. eapply forever_N_star; eauto. + apply Eappinf_assoc. +Qed. + +Lemma forever_N_forever: + forall ge p s T, forever_N ge p s T -> forever ge s T. +Proof. + cofix COINDHYP; intros. + destruct (forever_N_inv H) as [t [s' [q [T' [A [B C]]]]]]. + rewrite C. apply forever_intro with s'. auto. + apply COINDHYP with q; auto. +Qed. + +(** * Outcomes for program executions *) + +(** The two valid outcomes for the execution of a program: +- Termination, with a finite trace of observable events + and an integer value that stands for the process exit code + (the return value of the main function). +- Divergence with an infinite trace of observable events. + (The actual events generated by the execution can be a + finite prefix of this trace, or the whole trace.) +*) + +Inductive program_behavior: Set := + | Terminates: trace -> int -> program_behavior + | Diverges: traceinf -> program_behavior. + +(** Given a characterization of initial states and final states, + [program_behaves] relates a program behaviour with the + sequences of transitions that can be taken from an initial state + to a final state. *) + +Variable initial_state: state -> Prop. +Variable final_state: state -> int -> Prop. + +Inductive program_behaves (ge: genv): program_behavior -> Prop := + | program_terminates: forall s t s' r, + initial_state s -> + star ge s t s' -> + final_state s' r -> + program_behaves ge (Terminates t r) + | program_diverges: forall s T, + initial_state s -> + forever ge s T -> + program_behaves ge (Diverges T). + +End CLOSURES. + +(** * Simulations between two small-step semantics. *) + +(** In this section, we show that if two transition relations + satisfy certain simulation diagrams, then every program behaviour + generated by the first transition relation can also occur + with the second transition relation. *) + +Section SIMULATION. + +(** The first small-step semantics is axiomatized as follows. *) + +Variable genv1: Set. +Variable state1: Set. +Variable step1: genv1 -> state1 -> trace -> state1 -> Prop. +Variable initial_state1: state1 -> Prop. +Variable final_state1: state1 -> int -> Prop. +Variable ge1: genv1. + +(** The second small-step semantics is also axiomatized. *) + +Variable genv2: Set. +Variable state2: Set. +Variable step2: genv2 -> state2 -> trace -> state2 -> Prop. +Variable initial_state2: state2 -> Prop. +Variable final_state2: state2 -> int -> Prop. +Variable ge2: genv2. + +(** We assume given a matching relation between states of both semantics. + This matching relation must be compatible with initial states + and with final states. *) + + +Variable match_states: state1 -> state2 -> Prop. + +Hypothesis match_initial_states: + forall st1, initial_state1 st1 -> + exists st2, initial_state2 st2 /\ match_states st1 st2. + +Hypothesis match_final_states: + forall st1 st2 r, + match_states st1 st2 -> + final_state1 st1 r -> + final_state2 st2 r. + +(** Simulation when one transition in the first program + corresponds to zero, one or several transitions in the second program. + However, there is no stuttering: infinitely many transitions + in the source program must correspond to infinitely many + transitions in the second program. *) + +Section SIMULATION_STAR. + +(** [measure] is a nonnegative integer associated with states + of the first semantics. It must decrease when we take + a stuttering step. *) + +Variable measure: state1 -> nat. + +Hypothesis simulation: + forall st1 t st1', step1 ge1 st1 t st1' -> + forall st2, match_states st1 st2 -> + (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') + \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat. + +Lemma simulation_star_star: + forall st1 t st1', star step1 ge1 st1 t st1' -> + forall st2, match_states st1 st2 -> + exists st2', star step2 ge2 st2 t st2' /\ match_states st1' st2'. +Proof. + induction 1; intros. + exists st2; split. apply star_refl. auto. + elim (simulation H H2). + intros [st2' [A B]]. + destruct (IHstar _ B) as [st3' [C D]]. + exists st3'; split. apply star_trans with t1 st2' t2. + apply plus_star; auto. auto. auto. auto. + intros [A [B C]]. rewrite H1. rewrite B. simpl. apply IHstar; auto. +Qed. + +Lemma simulation_star_forever: + forall st1 st2 T, + forever step1 ge1 st1 T -> match_states st1 st2 -> + forever step2 ge2 st2 T. +Proof. + assert (forall st1 st2 T, + forever step1 ge1 st1 T -> match_states st1 st2 -> + forever_N step2 ge2 (measure st1) st2 T). + cofix COINDHYP; intros. + inversion H; subst. elim (simulation H1 H0). + intros [st2' [A B]]. apply forever_N_plus with st2' (measure s2). + auto. apply COINDHYP. assumption. assumption. + intros [A [B C]]. + apply forever_N_star with st2 (measure s2). + rewrite B. apply star_refl. auto. + apply COINDHYP. assumption. auto. + intros. eapply forever_N_forever; eauto. +Qed. + +Lemma simulation_star_preservation: + forall beh, + program_behaves step1 initial_state1 final_state1 ge1 beh -> + program_behaves step2 initial_state2 final_state2 ge2 beh. +Proof. + intros. inversion H; subst. + destruct (match_initial_states H0) as [s2 [A B]]. + destruct (simulation_star_star H1 B) as [s2' [C D]]. + econstructor; eauto. + destruct (match_initial_states H0) as [s2 [A B]]. + econstructor; eauto. + eapply simulation_star_forever; eauto. +Qed. + +End SIMULATION_STAR. + +(** Lock-step simulation: each transition in the first semantics + corresponds to exactly one transition in the second semantics. *) + +Section SIMULATION_STEP. + +Hypothesis simulation: + forall st1 t st1', step1 ge1 st1 t st1' -> + forall st2, match_states st1 st2 -> + exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2'. + +Lemma simulation_step_preservation: + forall beh, + program_behaves step1 initial_state1 final_state1 ge1 beh -> + program_behaves step2 initial_state2 final_state2 ge2 beh. +Proof. + intros. + pose (measure := fun (st: state1) => 0%nat). + assert (simulation': + forall st1 t st1', step1 ge1 st1 t st1' -> + forall st2, match_states st1 st2 -> + (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') + \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). + intros. destruct (simulation H0 H1) as [st2' [A B]]. + left; exists st2'; split. apply plus_one; auto. auto. + eapply simulation_star_preservation; eauto. +Qed. + +End SIMULATION_STEP. + +(** Simulation when one transition in the first program corresponds + to one or several transitions in the second program. *) + +Section SIMULATION_PLUS. + +Hypothesis simulation: + forall st1 t st1', step1 ge1 st1 t st1' -> + forall st2, match_states st1 st2 -> + exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2'. + +Lemma simulation_plus_preservation: + forall beh, + program_behaves step1 initial_state1 final_state1 ge1 beh -> + program_behaves step2 initial_state2 final_state2 ge2 beh. +Proof. + intros. + pose (measure := fun (st: state1) => 0%nat). + assert (simulation': + forall st1 t st1', step1 ge1 st1 t st1' -> + forall st2, match_states st1 st2 -> + (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') + \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). + intros. destruct (simulation H0 H1) as [st2' [A B]]. + left; exists st2'; auto. + eapply simulation_star_preservation; eauto. +Qed. + +End SIMULATION_PLUS. + +(** Simulation when one transition in the first program + corresponds to zero or one transitions in the second program. + However, there is no stuttering: infinitely many transitions + in the source program must correspond to infinitely many + transitions in the second program. *) + +Section SIMULATION_OPT. + +Variable measure: state1 -> nat. + +Hypothesis simulation: + forall st1 t st1', step1 ge1 st1 t st1' -> + forall st2, match_states st1 st2 -> + (exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2') + \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat. + +Lemma simulation_opt_preservation: + forall beh, + program_behaves step1 initial_state1 final_state1 ge1 beh -> + program_behaves step2 initial_state2 final_state2 ge2 beh. +Proof. + assert (simulation': + forall st1 t st1', step1 ge1 st1 t st1' -> + forall st2, match_states st1 st2 -> + (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') + \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). + intros. elim (simulation H H0). + intros [st2' [A B]]. left. exists st2'; split. apply plus_one; auto. auto. + intros [A [B C]]. right. intuition. + intros. eapply simulation_star_preservation; eauto. +Qed. + +End SIMULATION_OPT. + +End SIMULATION. + + diff --git a/common/Switch.v b/common/Switch.v new file mode 100644 index 0000000..e8b3967 --- /dev/null +++ b/common/Switch.v @@ -0,0 +1,165 @@ +(** Multi-way branches (``[switch]'') and their compilation + to 2-way comparison trees. *) + +Require Import EqNat. +Require Import Coqlib. +Require Import Integers. + +(** A multi-way branch is composed of a list of (key, action) pairs, + plus a default action. *) + +Definition table : Set := list (int * nat). + +Fixpoint switch_target (n: int) (dfl: nat) (cases: table) + {struct cases} : nat := + match cases with + | nil => dfl + | (key, action) :: rem => + if Int.eq n key then action else switch_target n dfl rem + end. + +(** Multi-way branches are translated to a 2-way comparison tree. + Each node of the tree performs an equality test or a less-than + test against one of the keys. *) + +Inductive comptree : Set := + | CTaction: nat -> comptree + | CTifeq: int -> nat -> comptree -> comptree + | CTiflt: int -> comptree -> comptree -> comptree. + +Fixpoint comptree_match (n: int) (t: comptree) {struct t}: nat := + match t with + | CTaction act => act + | CTifeq key act t' => + if Int.eq n key then act else comptree_match n t' + | CTiflt key t1 t2 => + if Int.ltu n key then comptree_match n t1 else comptree_match n t2 + end. + +(** The translation from a table to a comparison tree is performed + by untrusted Caml code (function [compile_switch] in + file [RTLgenaux.ml]). In Coq, we validate a posteriori the + result of this function. In other terms, we now develop + and prove correct Coq functions that take a table and a comparison + tree, and check that their semantics are equivalent. *) + +Fixpoint split_lt (pivot: int) (cases: table) + {struct cases} : table * table := + match cases with + | nil => (nil, nil) + | (key, act) :: rem => + let (l, r) := split_lt pivot rem in + if Int.ltu key pivot + then ((key, act) :: l, r) + else (l, (key, act) :: r) + end. + +Fixpoint split_eq (pivot: int) (cases: table) + {struct cases} : option nat * table := + match cases with + | nil => (None, nil) + | (key, act) :: rem => + let (same, others) := split_eq pivot rem in + if Int.eq key pivot + then (Some act, others) + else (same, (key, act) :: others) + end. + +Fixpoint validate_switch (default: nat) (cases: table) (t: comptree) + {struct t} : bool := + match t with + | CTaction act => + match cases with + | nil => beq_nat act default + | _ => false + end + | CTifeq pivot act t' => + match split_eq pivot cases with + | (None, _) => false + | (Some act', others) => beq_nat act act' && validate_switch default others t' + end + | CTiflt pivot t1 t2 => + match split_lt pivot cases with + | (lcases, rcases) => + validate_switch default lcases t1 && validate_switch default rcases t2 + end + end. + +(** Correctness proof for validation. *) + +Lemma split_eq_prop: + forall v default n cases optact cases', + split_eq n cases = (optact, cases') -> + switch_target v default cases = + (if Int.eq v n + then match optact with Some act => act | None => default end + else switch_target v default cases'). +Proof. + induction cases; simpl; intros until cases'. + intros. inversion H; subst. simpl. + destruct (Int.eq v n); auto. + destruct a as [key act]. + case_eq (split_eq n cases). intros same other SEQ. + rewrite (IHcases _ _ SEQ). + predSpec Int.eq Int.eq_spec key n; intro EQ; inversion EQ; simpl. + subst n. destruct (Int.eq v key). auto. auto. + predSpec Int.eq Int.eq_spec v key. + subst v. predSpec Int.eq Int.eq_spec key n. congruence. auto. + auto. +Qed. + +Lemma split_lt_prop: + forall v default n cases lcases rcases, + split_lt n cases = (lcases, rcases) -> + switch_target v default cases = + (if Int.ltu v n + then switch_target v default lcases + else switch_target v default rcases). +Proof. + induction cases; intros until rcases; simpl. + intro. inversion H; subst. simpl. + destruct (Int.ltu v n); auto. + destruct a as [key act]. + case_eq (split_lt n cases). intros lc rc SEQ. + rewrite (IHcases _ _ SEQ). + case_eq (Int.ltu key n); intros; inv H0; simpl. + predSpec Int.eq Int.eq_spec v key. + subst v. rewrite H. auto. + auto. + predSpec Int.eq Int.eq_spec v key. + subst v. rewrite H. auto. + auto. +Qed. + +Definition table_tree_agree + (default: nat) (cases: table) (t: comptree) : Prop := + forall v, switch_target v default cases = comptree_match v t. + +Lemma validate_switch_correct: + forall default t cases, + validate_switch default cases t = true -> + table_tree_agree default cases t. +Proof. + induction t; simpl; intros until cases. + (* base case *) + destruct cases. 2: congruence. + intro. replace n with default. + red; intros; simpl; auto. + symmetry. apply beq_nat_eq. auto. + (* eq node *) + case_eq (split_eq i cases). intros optact cases' EQ. + destruct optact as [ act | ]. 2: congruence. + intros. destruct (andb_prop _ _ H). + replace n with act. + generalize (IHt _ H1); intro. + red; intros. simpl. rewrite <- H2. + change act with (match Some act with Some act => act | None => default end). + eapply split_eq_prop; eauto. + symmetry. apply beq_nat_eq. auto. + (* lt node *) + case_eq (split_lt i cases). intros lcases rcases EQ V. + destruct (andb_prop _ _ V). + red; intros. simpl. + rewrite <- (IHt1 _ H). rewrite <- (IHt2 _ H0). + eapply split_lt_prop; eauto. +Qed. diff --git a/common/Values.v b/common/Values.v index aa59e04..e5b4971 100644 --- a/common/Values.v +++ b/common/Values.v @@ -885,4 +885,68 @@ Proof. elim H0; intro; subst v; reflexivity. Qed. +(** The ``is less defined'' relation between values. + A value is less defined than itself, and [Vundef] is + less defined than any value. *) + +Inductive lessdef: val -> val -> Prop := + | lessdef_refl: forall v, lessdef v v + | lessdef_undef: forall v, lessdef Vundef v. + +Inductive lessdef_list: list val -> list val -> Prop := + | lessdef_list_nil: + lessdef_list nil nil + | lessdef_list_cons: + forall v1 v2 vl1 vl2, + lessdef v1 v2 -> lessdef_list vl1 vl2 -> + lessdef_list (v1 :: vl1) (v2 :: vl2). + +Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons. + +Lemma lessdef_list_inv: + forall vl1 vl2, lessdef_list vl1 vl2 -> vl1 = vl2 \/ In Vundef vl1. +Proof. + induction 1; simpl. + tauto. + inv H. destruct IHlessdef_list. + left; congruence. tauto. tauto. +Qed. + +Lemma load_result_lessdef: + forall chunk v1 v2, + lessdef v1 v2 -> lessdef (load_result chunk v1) (load_result chunk v2). +Proof. + intros. inv H. auto. destruct chunk; simpl; auto. +Qed. + +Lemma cast8signed_lessdef: + forall v1 v2, lessdef v1 v2 -> lessdef (cast8signed v1) (cast8signed v2). +Proof. + intros; inv H; simpl; auto. +Qed. + +Lemma cast8unsigned_lessdef: + forall v1 v2, lessdef v1 v2 -> lessdef (cast8unsigned v1) (cast8unsigned v2). +Proof. + intros; inv H; simpl; auto. +Qed. + +Lemma cast16signed_lessdef: + forall v1 v2, lessdef v1 v2 -> lessdef (cast16signed v1) (cast16signed v2). +Proof. + intros; inv H; simpl; auto. +Qed. + +Lemma cast16unsigned_lessdef: + forall v1 v2, lessdef v1 v2 -> lessdef (cast16unsigned v1) (cast16unsigned v2). +Proof. + intros; inv H; simpl; auto. +Qed. + +Lemma singleoffloat_lessdef: + forall v1 v2, lessdef v1 v2 -> lessdef (singleoffloat v1) (singleoffloat v2). +Proof. + intros; inv H; simpl; auto. +Qed. + End Val. |