diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/AST.v | 250 | ||||
-rw-r--r-- | common/Events.v | 103 | ||||
-rw-r--r-- | common/Globalenvs.v | 643 | ||||
-rw-r--r-- | common/Main.v | 311 | ||||
-rw-r--r-- | common/Mem.v | 2385 | ||||
-rw-r--r-- | common/Values.v | 888 |
6 files changed, 4580 insertions, 0 deletions
diff --git a/common/AST.v b/common/AST.v new file mode 100644 index 00000000..1342bef1 --- /dev/null +++ b/common/AST.v @@ -0,0 +1,250 @@ +(** This file defines a number of data types and operations used in + the abstract syntax trees of many of the intermediate languages. *) + +Require Import Coqlib. +Require Import Integers. +Require Import Floats. + +Set Implicit Arguments. + +(** Identifiers (names of local variables, of global symbols and functions, + etc) are represented by the type [positive] of positive integers. *) + +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. *) + +Inductive typ : Set := + | Tint : typ + | Tfloat : typ. + +Definition typesize (ty: typ) : Z := + match ty with Tint => 4 | Tfloat => 8 end. + +(** 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 + are used in particular to determine appropriate calling conventions + for the function. *) + +Record signature : Set := mksignature { + sig_args: list typ; + sig_res: option typ +}. + +Definition proj_sig_res (s: signature) : typ := + match s.(sig_res) with + | None => Tint + | Some t => t + end. + +(** Memory accesses (load and store instructions) are annotated by + a ``memory chunk'' indicating the type, size and signedness of the + chunk of memory being accessed. *) + +Inductive memory_chunk : Set := + | Mint8signed : memory_chunk (**r 8-bit signed integer *) + | Mint8unsigned : memory_chunk (**r 8-bit unsigned integer *) + | Mint16signed : memory_chunk (**r 16-bit signed integer *) + | Mint16unsigned : memory_chunk (**r 16-bit unsigned integer *) + | Mint32 : memory_chunk (**r 32-bit integer, or pointer *) + | Mfloat32 : memory_chunk (**r 32-bit single-precision float *) + | Mfloat64 : memory_chunk. (**r 64-bit double-precision float *) + +(** Initialization data for global variables. *) + +Inductive init_data: Set := + | Init_int8: int -> init_data + | Init_int16: int -> init_data + | Init_int32: int -> init_data + | Init_float32: float -> init_data + | Init_float64: float -> init_data + | Init_space: Z -> init_data. + +(** Whole programs consist of: +- a collection of function definitions (name and description); +- the name of the ``main'' function that serves as entry point in the program; +- a collection of global variable declarations (name and initializer). + +The type of function descriptions varies among the various intermediate +languages and is taken as parameter to the [program] type. The other parts +of whole programs are common to all languages. *) + +Record program (funct: Set) : Set := mkprogram { + prog_funct: list (ident * funct); + prog_main: ident; + prog_vars: list (ident * list init_data) +}. + +(** 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. *) + +Section TRANSF_PROGRAM. + +Variable A B: Set. +Variable transf: A -> B. + +Fixpoint transf_program (l: list (ident * A)) : list (ident * B) := + match l with + | nil => nil + | (id, fn) :: rem => (id, transf fn) :: transf_program rem + end. + +Definition transform_program (p: program A) : program B := + mkprogram + (transf_program p.(prog_funct)) + p.(prog_main) + p.(prog_vars). + +Remark transf_program_functions: + forall fl i tf, + In (i, tf) (transf_program fl) -> + exists f, In (i, f) fl /\ transf f = tf. +Proof. + induction fl; simpl. + tauto. + destruct a. simpl. intros. + elim H; intro. exists a. split. left. congruence. congruence. + generalize (IHfl _ _ H0). intros [f [IN TR]]. + exists f. split. right. auto. auto. +Qed. + +Lemma transform_program_function: + forall p i tf, + In (i, tf) (transform_program p).(prog_funct) -> + exists f, In (i, f) p.(prog_funct) /\ transf f = tf. +Proof. + simpl. intros. eapply transf_program_functions; eauto. +Qed. + +End TRANSF_PROGRAM. + +(** The following is a variant of [transform_program] where the + code transformation function can fail and therefore returns an + option type. *) + +Section TRANSF_PARTIAL_PROGRAM. + +Variable A B: Set. +Variable transf_partial: A -> option B. + +Fixpoint transf_partial_program + (l: list (ident * A)) : option (list (ident * B)) := + match l with + | nil => Some nil + | (id, fn) :: rem => + match transf_partial fn with + | None => None + | Some fn' => + match transf_partial_program rem with + | None => None + | Some res => Some ((id, fn') :: res) + end + end + end. + +Definition transform_partial_program (p: program A) : option (program B) := + match transf_partial_program p.(prog_funct) with + | None => None + | Some fl => Some (mkprogram fl p.(prog_main) p.(prog_vars)) + end. + +Remark transf_partial_program_functions: + forall fl tfl i tf, + transf_partial_program fl = Some tfl -> + In (i, tf) tfl -> + exists f, In (i, f) fl /\ transf_partial f = Some tf. +Proof. + induction fl; simpl. + intros; injection H; intro; subst tfl; contradiction. + case a; intros id fn. intros until tf. + caseEq (transf_partial fn). + intros tfn TFN. + caseEq (transf_partial_program fl). + intros tfl1 TFL1 EQ. injection EQ; intro; clear EQ; subst tfl. + simpl. intros [EQ1|IN1]. + exists fn. intuition congruence. + generalize (IHfl _ _ _ TFL1 IN1). + intros [f [X Y]]. + exists f. intuition congruence. + intros; discriminate. + intros; discriminate. +Qed. + +Lemma transform_partial_program_function: + forall p tp i tf, + transform_partial_program p = Some tp -> + In (i, tf) tp.(prog_funct) -> + exists f, In (i, f) p.(prog_funct) /\ transf_partial f = Some tf. +Proof. + intros until tf. + unfold transform_partial_program. + caseEq (transf_partial_program (prog_funct p)). + intros. apply transf_partial_program_functions with l; auto. + injection H0; intros; subst tp. exact H1. + intros; discriminate. +Qed. + +Lemma transform_partial_program_main: + forall p tp, + transform_partial_program p = Some tp -> + tp.(prog_main) = p.(prog_main). +Proof. + intros p tp. unfold transform_partial_program. + destruct (transf_partial_program (prog_funct p)). + intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; reflexivity. + intro; discriminate. +Qed. + +End TRANSF_PARTIAL_PROGRAM. + +(** 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 + a type for such functions and some generic transformation functions. *) + +Record external_function : Set := mkextfun { + ef_id: ident; + ef_sig: signature +}. + +Inductive fundef (F: Set): Set := + | Internal: F -> fundef F + | External: external_function -> fundef F. + +Implicit Arguments External [F]. + +Section TRANSF_FUNDEF. + +Variable A B: Set. +Variable transf: A -> B. + +Definition transf_fundef (fd: fundef A): fundef B := + match fd with + | Internal f => Internal (transf f) + | External ef => External ef + end. + +End TRANSF_FUNDEF. + +Section TRANSF_PARTIAL_FUNDEF. + +Variable A B: Set. +Variable transf_partial: A -> option B. + +Definition transf_partial_fundef (fd: fundef A): option (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) + end. + +End TRANSF_PARTIAL_FUNDEF. + diff --git a/common/Events.v b/common/Events.v new file mode 100644 index 00000000..a0559fd0 --- /dev/null +++ b/common/Events.v @@ -0,0 +1,103 @@ +(** Representation of (traces of) observable events. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. + +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. + +Infix "**" := Eapp (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). + +Hint Rewrite E0_left E0_right Eapp_assoc: trace_rewrite. + +Ltac substTraceHyp := + match goal with + | [ H: (@eq trace ?x ?y) |- _ ] => + subst x || clear H + end. + +Ltac decomposeTraceEq := + match goal with + | [ |- (_ ** _) = (_ ** _) ] => + apply (f_equal2 Eapp); auto; decomposeTraceEq + | _ => + auto + end. + +Ltac traceEq := + repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq. + +Inductive eventval_match: eventval -> typ -> val -> Prop := + | ev_match_int: + forall i, eventval_match (EVint i) Tint (Vint i) + | ev_match_float: + forall f, eventval_match (EVfloat f) Tfloat (Vfloat f). + +Inductive eventval_list_match: list eventval -> list typ -> list val -> Prop := + | evl_match_nil: + eventval_list_match nil nil nil + | evl_match_cons: + forall ev1 evl ty1 tyl v1 vl, + eventval_match ev1 ty1 v1 -> + eventval_list_match evl tyl vl -> + eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl). + +Inductive event_match: + external_function -> list val -> trace -> val -> Prop := + event_match_intro: + forall ef vargs vres eargs eres, + eventval_list_match eargs (sig_args ef.(ef_sig)) vargs -> + eventval_match eres (proj_sig_res ef.(ef_sig)) vres -> + event_match ef vargs (Eextcall ef.(ef_id) eargs eres) vres. + +Require Import Mem. + +Section EVENT_MATCH_INJECT. + +Variable f: meminj. + +Remark eventval_match_inject: + forall ev ty v1, eventval_match ev ty v1 -> + forall v2, val_inject f v1 v2 -> + eventval_match ev ty v2. +Proof. + induction 1; intros; inversion H; constructor. +Qed. + +Remark eventval_list_match_inject: + forall evl tyl vl1, eventval_list_match evl tyl vl1 -> + forall vl2, val_list_inject f vl1 vl2 -> + eventval_list_match evl tyl vl2. +Proof. + induction 1; intros. + inversion H; constructor. + inversion H1; constructor. + eapply eventval_match_inject; eauto. + eauto. +Qed. + +Lemma event_match_inject: + forall ef args1 t res args2, + event_match ef args1 t res -> + val_list_inject f args1 args2 -> + event_match ef args2 t res /\ val_inject f res res. +Proof. + intros. inversion H; subst. + split. constructor. eapply eventval_list_match_inject; eauto. auto. + inversion H2; constructor. +Qed. + +End EVENT_MATCH_INJECT. diff --git a/common/Globalenvs.v b/common/Globalenvs.v new file mode 100644 index 00000000..036fd8f6 --- /dev/null +++ b/common/Globalenvs.v @@ -0,0 +1,643 @@ +(** Global environments are a component of the dynamic semantics of + all languages involved in the compiler. A global environment + maps symbol names (names of functions and of global variables) + to the corresponding memory addresses. It also maps memory addresses + of functions to the corresponding function descriptions. + + Global environments, along with the initial memory state at the beginning + of program execution, are built from the program of interest, as follows: +- A distinct memory address is assigned to each function of the program. + These function addresses use negative numbers to distinguish them from + addresses of memory blocks. The associations of function name to function + address and function address to function description are recorded in + the global environment. +- For each global variable, a memory block is allocated and associated to + the name of the variable. + + These operations reflect (at a high level of abstraction) what takes + place during program linking and program loading in a real operating + system. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Mem. + +Set Implicit Arguments. + +Module Type GENV. + +(** ** Types and operations *) + + Variable t: Set -> Set. + (** The type of global environments. The parameter [F] is the type + of function descriptions. *) + + Variable globalenv: forall (F: Set), program F -> t F. + (** Return the global environment for the given program. *) + + Variable init_mem: forall (F: Set), program F -> mem. + (** Return the initial memory state for the given program. *) + + Variable find_funct_ptr: forall (F: Set), t F -> block -> option F. + (** Return the function description associated with the given address, + if any. *) + + Variable find_funct: forall (F: Set), t F -> val -> option F. + (** Same as [find_funct_ptr] but the function address is given as + a value, which must be a pointer with offset 0. *) + + Variable find_symbol: forall (F: Set), t F -> ident -> option block. + (** Return the address of the given global symbol, if any. *) + +(** ** Properties of the operations. *) + + Hypothesis find_funct_inv: + forall (F: Set) (ge: t F) (v: val) (f: F), + find_funct ge v = Some f -> exists b, v = Vptr b Int.zero. + 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_funct_ptr_prop: + forall (F: Set) (P: F -> Prop) (p: program F) (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. + Hypothesis find_funct_prop: + forall (F: Set) (P: F -> Prop) (p: program F) (v: val) (f: F), + (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: Set) (p: program F) (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: Set) (p: program F), + let m := init_mem p in + valid_block m nullptr /\ + m.(blocks) nullptr = empty_block 0 0. + Hypothesis initmem_block_init: + forall (F: Set) (p: program F) (b: block), + exists id, (init_mem p).(blocks) b = block_init_data id. + Hypothesis find_funct_ptr_inv: + forall (F: Set) (p: program F) (b: block) (f: F), + find_funct_ptr (globalenv p) b = Some f -> b < 0. + Hypothesis find_symbol_inv: + forall (F: Set) (p: program F) (id: ident) (b: block), + find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p). + +(** Commutation properties between program transformations + and operations over global environments. *) + + Hypothesis find_funct_ptr_transf: + forall (A B: Set) (transf: A -> B) (p: program A) (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: Set) (transf: A -> B) (p: program A) (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: Set) (transf: A -> B) (p: program A) (s: ident), + find_symbol (globalenv (transform_program transf p)) s = + find_symbol (globalenv p) s. + Hypothesis init_mem_transf: + forall (A B: Set) (transf: A -> B) (p: program A), + init_mem (transform_program transf p) = init_mem p. + +(** Commutation properties between partial program transformations + and operations over global environments. *) + + Hypothesis find_funct_ptr_transf_partial: + forall (A B: Set) (transf: A -> option B) + (p: program A) (p': program B), + transform_partial_program transf p = Some 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. + Hypothesis find_funct_transf_partial: + forall (A B: Set) (transf: A -> option B) + (p: program A) (p': program B), + transform_partial_program transf p = Some p' -> + forall (v: val) (f: A), + find_funct (globalenv p) v = Some f -> + find_funct (globalenv p') v = transf f /\ transf f <> None. + Hypothesis find_symbol_transf_partial: + forall (A B: Set) (transf: A -> option B) + (p: program A) (p': program B), + transform_partial_program transf p = Some p' -> + forall (s: ident), + find_symbol (globalenv p') s = find_symbol (globalenv p) s. + Hypothesis init_mem_transf_partial: + forall (A B: Set) (transf: A -> option B) + (p: program A) (p': program B), + transform_partial_program transf p = Some p' -> + init_mem p' = init_mem p. +End GENV. + +(** The rest of this library is a straightforward implementation of + the module signature above. *) + +Module Genv: GENV. + +Section GENV. + +Variable funct: Set. (* The type of functions *) + +Record genv : Set := mkgenv { + functions: ZMap.t (option funct); (* mapping function ptr -> function *) + nextfunction: Z; + symbols: PTree.t block (* mapping symbol -> block *) +}. + +Definition t := genv. + +Definition add_funct (name_fun: (ident * funct)) (g: genv) : genv := + let b := g.(nextfunction) in + mkgenv (ZMap.set b (Some (snd name_fun)) g.(functions)) + (Zpred b) + (PTree.set (fst name_fun) b g.(symbols)). + +Definition add_symbol (name: ident) (b: block) (g: genv) : genv := + mkgenv g.(functions) + g.(nextfunction) + (PTree.set name b g.(symbols)). + +Definition find_funct_ptr (g: genv) (b: block) : option funct := + ZMap.get b g.(functions). + +Definition find_funct (g: genv) (v: val) : option funct := + match v with + | Vptr b ofs => + if Int.eq ofs Int.zero then find_funct_ptr g b else None + | _ => + None + end. + +Definition find_symbol (g: genv) (symb: ident) : option block := + PTree.get symb g.(symbols). + +Lemma find_funct_inv: + forall (ge: t) (v: val) (f: funct), + find_funct ge v = Some f -> exists b, v = Vptr b Int.zero. +Proof. + intros until f. unfold find_funct. destruct v; try (intros; discriminate). + generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros. + exists b. congruence. + discriminate. +Qed. + +Lemma find_funct_find_funct_ptr: + forall (ge: t) (b: block), + find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b. +Proof. + intros. simpl. + generalize (Int.eq_spec Int.zero Int.zero). + case (Int.eq Int.zero Int.zero); intros. + auto. tauto. +Qed. + +(* Construct environment and initial memory store *) + +Definition empty : genv := + mkgenv (ZMap.init None) (-1) (PTree.empty block). + +Definition add_functs (init: genv) (fns: list (ident * funct)) : genv := + List.fold_right add_funct init fns. + +Definition add_globals + (init: genv * mem) (vars: list (ident * list init_data)) : genv * mem := + List.fold_right + (fun (id_init: ident * list init_data) (g_st: genv * mem) => + let (id, init) := id_init in + let (g, st) := g_st in + let (st', b) := Mem.alloc_init_data st init in + (add_symbol id b g, st')) + init vars. + +Definition globalenv_initmem (p: program funct) : (genv * mem) := + add_globals + (add_functs empty p.(prog_funct), Mem.empty) + p.(prog_vars). + +Definition globalenv (p: program funct) : genv := + fst (globalenv_initmem p). +Definition init_mem (p: program funct) : mem := + snd (globalenv_initmem p). + +Lemma functions_globalenv: + forall (p: program funct), + functions (globalenv p) = functions (add_functs empty p.(prog_funct)). +Proof. + assert (forall init vars, + functions (fst (add_globals init vars)) = functions (fst init)). + induction vars; simpl. + reflexivity. + destruct a. destruct (add_globals init vars). + simpl. exact IHvars. + + unfold add_globals; simpl. + intros. unfold globalenv; unfold globalenv_initmem. + rewrite H. reflexivity. +Qed. + +Lemma initmem_nullptr: + forall (p: program funct), + let m := init_mem p in + valid_block m nullptr /\ + m.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0). +Proof. + assert + (forall init, + let m1 := snd init in + 0 < m1.(nextblock) -> + m1.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0) -> + forall vars, + let m2 := snd (add_globals init vars) in + 0 < m2.(nextblock) /\ + m2.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0)). + induction vars; simpl; intros. + tauto. + destruct a. + caseEq (add_globals init vars). intros g m2 EQ. + rewrite EQ in IHvars. simpl in IHvars. elim IHvars; intros. + simpl. split. omega. + rewrite update_o. auto. apply sym_not_equal. apply Zlt_not_eq. exact H1. + + intro. unfold init_mem. unfold globalenv_initmem. + unfold valid_block. apply H. simpl. omega. reflexivity. +Qed. + +Lemma initmem_block_init: + forall (p: program funct) (b: block), + exists id, (init_mem p).(blocks) b = block_init_data id. +Proof. + assert (forall g0 vars g1 m b, + 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. + destruct a. 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 l; auto. + eauto. + intros. caseEq (globalenv_initmem p). + intros g m EQ. unfold init_mem; rewrite EQ; simpl. + unfold globalenv_initmem in EQ. eauto. +Qed. + +Remark nextfunction_add_functs_neg: + forall fns, nextfunction (add_functs empty fns) < 0. +Proof. + induction fns; simpl; intros. omega. unfold Zpred. omega. +Qed. + +Theorem find_funct_ptr_inv: + forall (p: program funct) (b: block) (f: funct), + find_funct_ptr (globalenv p) b = Some f -> b < 0. +Proof. + intros until f. + assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some f -> b < 0). + induction fns; simpl. + rewrite ZMap.gi. congruence. + rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro. + intro. rewrite e. apply nextfunction_add_functs_neg. + auto. + unfold find_funct_ptr. rewrite functions_globalenv. + intros. eauto. +Qed. + +Theorem find_symbol_inv: + forall (p: program funct) (id: ident) (b: block), + find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p). +Proof. + assert (forall fns s b, + (symbols (add_functs empty fns)) ! s = Some b -> b < 0). + induction fns; simpl; intros until b. + rewrite PTree.gempty. congruence. + rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro. + intro EQ; inversion EQ. apply nextfunction_add_functs_neg. + eauto. + assert (forall fns vars g m s b, + add_globals (add_functs empty fns, Mem.empty) vars = (g, m) -> + (symbols g)!s = Some b -> + b < nextblock m). + induction vars; simpl; intros until b. + intros. inversion H0. subst g m. simpl. + generalize (H fns s b H1). omega. + destruct a. caseEq (add_globals (add_functs empty fns, Mem.empty) vars). + intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ. + unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s i); intro. + intro EQ; inversion EQ. omega. + intro. generalize (IHvars _ _ _ _ ADG H0). omega. + intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl. + caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty) + (prog_vars p)); intros g m EQ. + simpl; intros. eauto. +Qed. + +End GENV. + +(* Invariants on functions *) +Lemma find_funct_ptr_prop: + forall (F: Set) (P: F -> Prop) (p: program F) (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. +Qed. + +Lemma find_funct_prop: + forall (F: Set) (P: F -> Prop) (p: program F) (v: val) (f: F), + (forall id f, In (id, f) (prog_funct p) -> P f) -> + 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. +Qed. + +Lemma find_funct_ptr_symbol_inversion: + forall (F: Set) (p: program F) (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). +Proof. + intros until f. + 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. + rewrite ZMap.gi. congruence. + set (g := add_functs (empty F) fns). + rewrite PTree.gsspec. rewrite ZMap.gsspec. + case (peq id (fst a)); intro. + 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. + assert (forall g0 m0, b < 0 -> + forall vars g m, + @add_globals F (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. + destruct a. 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 i); intros. + assert (b > 0). injection H2; intros. rewrite <- H3. apply nextblock_pos. + omegaContradiction. + eauto. + intros. + generalize (find_funct_ptr_inv _ _ H3). 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). + auto. unfold globalenv, init_mem. rewrite <- surjective_pairing. + reflexivity. assumption. rewrite <- functions_globalenv. assumption. +Qed. + +(* Global environments and program transformations. *) + +Section TRANSF_PROGRAM_PARTIAL. + +Variable A B: Set. +Variable transf: A -> option B. +Variable p: program A. +Variable p': program B. +Hypothesis transf_OK: transform_partial_program transf p = Some p'. + +Lemma add_functs_transf: + forall (fns: list (ident * A)) (tfns: list (ident * B)), + transf_partial_program transf fns = Some 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 f /\ transf f <> None. +Proof. + induction fns; simpl. + + intros; injection H; intro; subst tfns. + simpl. split. reflexivity. split. reflexivity. + intros b f; repeat (rewrite ZMap.gi). intros; discriminate. + + intro tfns. destruct a. caseEq (transf a). intros a' TA. + caseEq (transf_partial_program transf 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. + 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). + + intros; discriminate. + intros; discriminate. +Qed. + +Lemma mem_add_globals_transf: + forall (g1: genv A) (g2: genv B) (m: mem) (vars: list (ident * list init_data)), + snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) vars). +Proof. + induction vars; simpl. + reflexivity. + destruct a. destruct (add_globals (g1, m) vars). + destruct (add_globals (g2, m) vars). + simpl in IHvars. subst m1. reflexivity. +Qed. + +Lemma symbols_add_globals_transf: + forall (g1: genv A) (g2: genv B) (m: mem), + symbols g1 = symbols g2 -> + forall (vars: list (ident * list init_data)), + symbols (fst (add_globals (g1, m) vars)) = + symbols (fst (add_globals (g2, m) vars)). +Proof. + induction vars; simpl. + assumption. + generalize (mem_add_globals_transf g1 g2 m vars); intro. + destruct a. destruct (add_globals (g1, m) vars). + destruct (add_globals (g2, m) vars). + simpl. simpl in IHvars. simpl in H0. + rewrite H0; rewrite IHvars. reflexivity. +Qed. + +Lemma prog_funct_transf_OK: + transf_partial_program transf p.(prog_funct) = Some p'.(prog_funct). +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. +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. +Proof. + intros until f. + generalize (add_functs_transf p.(prog_funct) prog_funct_transf_OK). + intros [X [Y Z]]. + unfold find_funct_ptr. + repeat (rewrite functions_globalenv). + apply Z. +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. +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_partial. +Qed. + +Lemma symbols_init_transf: + symbols (globalenv p') = symbols (globalenv p). +Proof. + unfold globalenv. unfold globalenv_initmem. + generalize (add_functs_transf p.(prog_funct) prog_funct_transf_OK). + intros [X [Y Z]]. + generalize transf_OK. + unfold transform_partial_program. + case (transf_partial_program transf (prog_funct p)). + intros. injection transf_OK0; intro; subst p'; simpl. + symmetry. apply symbols_add_globals_transf. + symmetry. exact Y. + intros; discriminate. +Qed. + +Theorem find_symbol_transf_partial: + forall (s: ident), + find_symbol (globalenv p') s = find_symbol (globalenv p) s. +Proof. + intros. unfold find_symbol. + rewrite symbols_init_transf. auto. +Qed. + +Theorem init_mem_transf_partial: + init_mem p' = init_mem p. +Proof. + unfold init_mem. unfold globalenv_initmem. + generalize transf_OK. + unfold transform_partial_program. + case (transf_partial_program transf (prog_funct p)). + intros. injection transf_OK0; intro; subst p'; simpl. + symmetry. apply mem_add_globals_transf. + intros; discriminate. +Qed. + +End TRANSF_PROGRAM_PARTIAL. + +Section TRANSF_PROGRAM. + +Variable A B: Set. +Variable transf: A -> B. +Variable p: program A. +Let tp := transform_program transf p. + +Definition transf_partial (x: A) : option B := Some (transf x). + +Lemma transf_program_transf_partial_program: + forall (fns: list (ident * A)), + transf_partial_program transf_partial fns = + Some (transf_program transf fns). +Proof. + induction fns; simpl. + reflexivity. + destruct a. rewrite IHfns. reflexivity. +Qed. + +Lemma transform_program_transform_partial_program: + transform_partial_program transf_partial p = Some tp. +Proof. + unfold tp. unfold transform_partial_program, transform_program. + rewrite transf_program_transf_partial_program. + reflexivity. +Qed. + +Theorem find_funct_ptr_transf: + forall (b: block) (f: A), + find_funct_ptr (globalenv p) b = Some f -> + find_funct_ptr (globalenv tp) b = Some (transf f). +Proof. + intros. + generalize (find_funct_ptr_transf_partial transf_partial p + transform_program_transform_partial_program). + intros. elim (H0 b f H). intros. exact H1. +Qed. + +Theorem find_funct_transf: + forall (v: val) (f: A), + find_funct (globalenv p) v = Some f -> + find_funct (globalenv tp) v = Some (transf f). +Proof. + intros. + generalize (find_funct_transf_partial transf_partial p + transform_program_transform_partial_program). + intros. elim (H0 v f H). intros. exact H1. +Qed. + +Theorem find_symbol_transf: + forall (s: ident), + find_symbol (globalenv tp) s = find_symbol (globalenv p) s. +Proof. + intros. + apply find_symbol_transf_partial with transf_partial. + apply transform_program_transform_partial_program. +Qed. + +Theorem init_mem_transf: + init_mem tp = init_mem p. +Proof. + apply init_mem_transf_partial with transf_partial. + apply transform_program_transform_partial_program. +Qed. + +End TRANSF_PROGRAM. + +End Genv. diff --git a/common/Main.v b/common/Main.v new file mode 100644 index 00000000..95dc4e6c --- /dev/null +++ b/common/Main.v @@ -0,0 +1,311 @@ +(** The compiler back-end and its proof of semantic preservation *) + +(** Libraries. *) +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Values. +(** Languages (syntax and semantics). *) +Require Csharpminor. +Require Cminor. +Require RTL. +Require LTL. +Require Linear. +Require Mach. +Require PPC. +(** Translation passes. *) +Require Cminorgen. +Require RTLgen. +Require Constprop. +Require CSE. +Require Allocation. +Require Tunneling. +Require Linearize. +Require Stacking. +Require PPCgen. +(** Type systems. *) +Require RTLtyping. +Require LTLtyping. +Require Lineartyping. +Require Machtyping. +(** Proofs of semantic preservation and typing preservation. *) +Require Cminorgenproof. +Require RTLgenproof. +Require Constpropproof. +Require CSEproof. +Require Allocproof. +Require Alloctyping. +Require Tunnelingproof. +Require Tunnelingtyping. +Require Linearizeproof. +Require Linearizetyping. +Require Stackingproof. +Require Stackingtyping. +Require Machabstr2mach. +Require PPCgenproof. + +(** * 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_partial (A B: Set) + (x: option A) (f: A -> option B) : option B := + match x with None => None | Some 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 Csharpminor program, the other with a Cminor program. Both + translations produce PPC programs ready for pretty-printing and + assembling. Some front-ends will prefer to generate Csharpminor + (e.g. a C front-end) while some others (e.g. an ML compiler) might + find it more convenient to generate Cminor directly, bypassing + Csharpminor. + + 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. + + The translation of a Cminor function to a PPC function is as follows. *) + +Definition transf_cminor_fundef (f: Cminor.fundef) : option PPC.fundef := + Some f + @@@ RTLgen.transl_fundef + @@ Constprop.transf_fundef + @@ CSE.transf_fundef + @@@ Allocation.transf_fundef + @@ Tunneling.tunnel_fundef + @@ Linearize.transf_fundef + @@@ Stacking.transf_fundef + @@@ PPCgen.transf_fundef. + +(** And here is the translation for Csharpminor functions. *) + +Definition transf_csharpminor_fundef + (gce: Cminorgen.compilenv) (f: Csharpminor.fundef) : option PPC.fundef := + Some f + @@@ Cminorgen.transl_fundef gce + @@@ transf_cminor_fundef. + +(** The corresponding translations for whole program follow. *) + +Definition transf_cminor_program (p: Cminor.program) : option PPC.program := + transform_partial_program transf_cminor_fundef p. + +Definition transf_csharpminor_program (p: Csharpminor.program) : option PPC.program := + let gce := Cminorgen.build_global_compilenv p in + transform_partial_program + (transf_csharpminor_fundef gce) + (Csharpminor.program_of_program p). + +(** * 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. + +Definition transf_csharpminor_program2 (p: Csharpminor.program) : option PPC.program := + Some p + @@@ Cminorgen.transl_program + @@@ transf_cminor_program2. + +Lemma transf_partial_program_compose: + forall (A B C: Set) + (f1: A -> option B) (f2: B -> option C) + (p: list (ident * A)), + transf_partial_program f1 p @@@ transf_partial_program f2 = + transf_partial_program (fun f => f1 f @@@ f2) p. +Proof. + induction p. simpl. auto. + simpl. destruct a. destruct (f1 a). + simpl. simpl in IHp. destruct (transf_partial_program f1 p). + simpl. simpl in IHp. destruct (f2 b). + destruct (transf_partial_program f2 l). + rewrite <- IHp. auto. + rewrite <- IHp. auto. + auto. + simpl. rewrite <- IHp. simpl. destruct (f2 b); auto. + simpl. auto. +Qed. + +Lemma transform_partial_program_compose: + forall (A B C: Set) + (f1: A -> option B) (f2: B -> option C) + (p: program A), + transform_partial_program f1 p @@@ + (fun p' => transform_partial_program f2 p') = + transform_partial_program (fun f => f1 f @@@ f2) p. +Proof. + unfold transform_partial_program; intros. + rewrite <- transf_partial_program_compose. simpl. + destruct (transf_partial_program f1 (prog_funct p)); simpl. + auto. auto. +Qed. + +Lemma transf_program_partial_total: + forall (A B: Set) (f: A -> B) (l: list (ident * A)), + Some (AST.transf_program f l) = + AST.transf_partial_program (fun x => Some (f x)) l. +Proof. + induction l. simpl. auto. + simpl. destruct a. rewrite <- IHl. auto. +Qed. + +Lemma transform_program_partial_total: + forall (A B: Set) (f: A -> B) (p: program A), + Some (transform_program f p) = + transform_partial_program (fun x => Some (f x)) p. +Proof. + intros. unfold transform_program, transform_partial_program. + rewrite <- transf_program_partial_total. auto. +Qed. + +Lemma apply_total_transf_program: + forall (A B: Set) (f: A -> B) (x: option (program A)), + 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. + +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. + +Lemma transf_csharpminor_program_equiv: + forall p, transf_csharpminor_program2 p = transf_csharpminor_program p. +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. + apply transform_partial_program_compose. + symmetry. apply extensionality. exact transf_cminor_program_equiv. +Qed. + +(** * Semantic preservation *) + +(** We prove that the [transf_program2] translations preserve semantics. The proof + composes the semantic preservation results for each pass. *) + +Lemma transf_cminor_program2_correct: + forall p tp t n, + transf_cminor_program2 p = Some tp -> + Cminor.exec_program p t (Vint n) -> + PPC.exec_program tp t (Vint n). +Proof. + intros until n. + 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. +Qed. + +Lemma transf_csharpminor_program2_correct: + forall p tp t n, + transf_csharpminor_program2 p = Some tp -> + Csharpminor.exec_program p t (Vint n) -> + PPC.exec_program tp t (Vint n). +Proof. + intros until n; unfold transf_csharpminor_program2; simpl. + caseEq (Cminorgen.transl_program p). + simpl; intros p1 EQ1 EQ2 EXEC. + apply transf_cminor_program2_correct with p1. auto. + apply Cminorgenproof.transl_program_correct with p. auto. + assumption. + simpl; intros; discriminate. +Qed. + +(** It follows that the whole compiler is semantic-preserving. *) + +Theorem transf_cminor_program_correct: + forall p tp t n, + transf_cminor_program p = Some tp -> + Cminor.exec_program p t (Vint n) -> + PPC.exec_program tp t (Vint n). +Proof. + intros. apply transf_cminor_program2_correct with p. + rewrite transf_cminor_program_equiv. assumption. assumption. +Qed. + +Theorem transf_csharpminor_program_correct: + forall p tp t n, + transf_csharpminor_program p = Some tp -> + Csharpminor.exec_program p t (Vint n) -> + PPC.exec_program tp t (Vint n). +Proof. + intros. apply transf_csharpminor_program2_correct with p. + rewrite transf_csharpminor_program_equiv. assumption. assumption. +Qed. diff --git a/common/Mem.v b/common/Mem.v new file mode 100644 index 00000000..7af696e1 --- /dev/null +++ b/common/Mem.v @@ -0,0 +1,2385 @@ +(** This file develops the memory model that is used in the dynamic + semantics of all the languages of the compiler back-end. + 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. +*) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +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. + +Implicit Arguments update [A]. + +Lemma update_s: + forall (A: Set) (x: Z) (v: A) (f: Z -> A), + update x v f x = v. +Proof. + intros; unfold update. apply zeq_true. +Qed. + +Lemma update_o: + forall (A: Set) (x: Z) (v: A) (f: Z -> A) (y: Z), + x <> y -> update x v f y = f y. +Proof. + intros; unfold update. apply zeq_false; auto. +Qed. + +(** 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], + [d+2] and [d+3]. The [Cont] contents enable detecting future writes + that would overlap partially 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 *) + +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. *) + +Record block_contents : Set := mkblock { + low: Z; + high: Z; + contents: contentmap; + undef_outside: forall ofs, ofs < low \/ ofs >= high -> contents ofs = Undef +}. + +(** A memory state is a mapping from block addresses (represented by [Z] + integers) to blocks. We also maintain the address of the next + unallocated block, and a proof that this address is positive. *) + +Record mem : Set := mkmem { + blocks: Z -> block_contents; + nextblock: block; + nextblock_pos: nextblock > 0 +}. + +(** * Operations on memory stores *) + +(** 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 + end. + +Definition mem_chunk (chunk: memory_chunk) := + match chunk with + | Mint8signed => Size8 + | Mint8unsigned => Size8 + | Mint16signed => Size16 + | Mint16unsigned => Size16 + | Mint32 => Size32 + | Mfloat32 => Size32 + | Mfloat64 => Size64 + end. + +Definition size_chunk (chunk: memory_chunk) := size_mem (mem_chunk chunk). + +(** 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). + +Definition empty: mem := + mkmem (fun x => empty_block 0 0) 1 one_pos. + +Definition nullptr: block := 0. + +(** Allocation of a fresh block with the given bounds. Return an updated + memory state and the address of the fresh block, which initially contains + undefined cells. Note that allocation never fails: we model an + infinite memory. *) + +Remark succ_nextblock_pos: + forall m, Zsucc m.(nextblock) > 0. +Proof. intro. generalize (nextblock_pos m). omega. Qed. + +Definition alloc (m: mem) (lo hi: Z) := + (mkmem (update m.(nextblock) + (empty_block lo hi) + m.(blocks)) + (Zsucc m.(nextblock)) + (succ_nextblock_pos m), + m.(nextblock)). + +(** Freeing a block. Return the updated memory state where the given + block address has been invalidated: future reads and writes to this + address will fail. Note that we make no attempt to return the block + to an allocation pool: the given block address will never be allocated + later. *) + +Definition free (m: mem) (b: block) := + mkmem (update b + (empty_block 0 0) + m.(blocks)) + m.(nextblock) + m.(nextblock_pos). + +(** Freeing of a list of blocks. *) + +Definition free_list (m:mem) (l:list block) := + List.fold_right (fun b m => free m b) m l. + +(** Return the low and high bounds for the given block address. + Those bounds are 0 for freed or not yet allocated address. *) + +Definition low_bound (m: mem) (b: block) := + low (m.(blocks) b). +Definition high_bound (m: mem) (b: block) := + high (m.(blocks) b). + +(** A block address is valid if it was previously allocated. It remains valid + even after being freed. *) + +Definition valid_block (m: mem) (b: block) := + b < m.(nextblock). + +(** Reading and writing [N] adjacent locations in a [contentmap]. + + We define two functions and prove some of their properties: + - [getN n ofs m] returns the datum at offset [ofs] in block contents [m] + after checking that the contents of offsets [ofs+1] to [ofs+n+1] + are [Cont]. + - [setN n ofs v m] updates the block contents [m], storing the content [v] + at offset [ofs] and the content [Cont] at offsets [ofs+1] to [ofs+n+1]. + *) + +Fixpoint check_cont (n: nat) (p: Z) (m: contentmap) {struct n} : bool := + match n with + | O => true + | S n1 => + match m p with + | Cont => check_cont n1 (p + 1) m + | _ => false + end + end. + +Definition getN (n: nat) (p: Z) (m: contentmap) : content := + if check_cont n (p + 1) m then m p else Undef. + +Fixpoint set_cont (n: nat) (p: Z) (m: contentmap) {struct n} : contentmap := + match n with + | O => m + | 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). + +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. +Proof. + induction n; intros. + reflexivity. + simpl. rewrite H. apply IHn. + intros. apply H. rewrite inj_S. omega. + rewrite inj_S. omega. +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). +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. +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 -> + check_cont n p m = false. +Proof. + intros. caseEq (check_cont n p m); intro. + generalize (check_cont_inv _ _ _ H1 q H). intro. contradiction. + auto. +Qed. + +Hint Resolve check_cont_false. + +Lemma set_cont_inside: + forall n p m q, + p <= q < p + Z_of_nat n -> + (set_cont n p m) q = Cont. +Proof. + induction n; intros. + unfold Z_of_nat in H. omegaContradiction. + simpl. + assert (p = q \/ p + 1 <= q < (p + 1) + Z_of_nat n). + rewrite inj_S in H. omega. + elim H0; intro. + subst q. apply update_s. + rewrite update_o. apply IHn. auto. + 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 -> + (set_cont n p m) q = m q. +Proof. + induction n; intros. + simpl. auto. + simpl. rewrite inj_S in H. + 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. 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. + 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. + +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. + +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. +Proof. + intros. unfold getN. + caseEq (check_cont n2 (p + 1) (setN n1 p v m)); intro. + left. unfold setN. apply update_s. + right. auto. +Qed. + +Hint Resolve getN_setN_mismatch. + +Lemma getN_init: + forall n p, + getN n p (fun y => Undef) = Undef. +Proof. + intros. unfold getN. + case (check_cont n (p + 1) (fun y => Undef)); auto. +Qed. + +Hint Resolve getN_init. + +(** 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. +Proof. + intros. case (in_bounds chunk ofs c); intro. + auto. + omegaContradiction. +Qed. + +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. +Proof. + intros; reflexivity. +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. + +(** [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 + or the memory access is out of bounds. *) + +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) + else + None. + +(** [loadv chunk m addr] is similar, but the address and offset are given + as a single value [addr], which must be a pointer value. *) + +Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val := + match addr with + | Vptr b ofs => load chunk m b (Int.signed ofs) + | _ => 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. + +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 := + 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))) + m.(blocks)) + m.(nextblock) + m.(nextblock_pos). + +(** [store chunk m b ofs v] perform a write in memory state [m]. + Value [v] is stored at address [b] and offset [ofs]. + Return the updated memory store, or [None] if the address is invalid + or the memory access is out of bounds. *) + +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. + +(** [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. *) + +Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := + match addr with + | Vptr b ofs => store chunk m b (Int.signed ofs) v + | _ => 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) + | Init_int16 n :: id' => + store_contents Size16 (contents_init_data (pos + 2) id') pos (Vint n) + | Init_int32 n :: id' => + store_contents Size32 (contents_init_data (pos + 4) id') pos (Vint n) + | Init_float32 f :: id' => + store_contents Size32 (contents_init_data (pos + 4) id') pos (Vfloat f) + | Init_float64 f :: id' => + store_contents Size64 (contents_init_data (pos + 8) id') pos (Vfloat f) + | Init_space n :: id' => + contents_init_data (pos + Zmax n 0) id' + end. + +Definition size_init_data (id: init_data) : Z := + match id with + | Init_int8 _ => 1 + | Init_int16 _ => 2 + | Init_int32 _ => 4 + | Init_float32 _ => 4 + | Init_float64 _ => 8 + | Init_space n => Zmax n 0 + end. + +Definition size_init_data_list (id: list init_data): Z := + List.fold_right (fun id sz => size_init_data id + sz) 0 id. + +Remark size_init_data_list_pos: + forall id, size_init_data_list id >= 0. +Proof. + induction id; simpl. + omega. + assert (size_init_data a >= 0). destruct a; simpl; try omega. + 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. +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). + +Definition alloc_init_data (m: mem) (id: list init_data) : mem * block := + (mkmem (update m.(nextblock) + (block_init_data id) + m.(blocks)) + (Zsucc m.(nextblock)) + (succ_nextblock_pos m), + m.(nextblock)). + +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. +Qed. + +(** * Properties of the memory operations *) + +(** ** Properties related to block validity *) + +Lemma valid_not_valid_diff: + forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'. +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). +Proof. + intros. injection H; intros; subst b. + unfold valid_block. omega. +Qed. + +Theorem valid_new_block: + forall (m1 m2: mem) (lo hi: Z) (b: block), + alloc m1 lo hi = (m2, b) -> valid_block m2 b. +Proof. + unfold alloc, valid_block; intros. + injection H; intros. subst b; subst m2; simpl. omega. +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. +Proof. + unfold alloc, valid_block; intros. + injection H; intros. subst m2; simpl. omega. +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. +Proof. + intros. generalize (store_inv _ _ _ _ _ _ H). + intros [A [B [C [D [P E]]]]]. + red. rewrite D. exact H0. +Qed. + +Theorem valid_block_free: + forall (m: mem) (b b': block), + valid_block m b -> valid_block (free m b') b. +Proof. + unfold valid_block, free; intros. + simpl. auto. +Qed. + +(** ** Properties related to [alloc] *) + +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. +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. +Qed. + +Lemma load_contents_init: + forall (sz: memory_size) (ofs: Z), + load_contents sz (fun y => Undef) ofs = Vundef. +Proof. + intros. destruct sz; reflexivity. +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. +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. + +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. +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. +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. +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. +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'. +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). +Qed. + +Hint Resolve store_alloc high_bound_alloc low_bound_alloc load_alloc_same +load_contents_init load_alloc_other. + +(** ** Properties related to [free] *) + +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. +Proof. + intros. unfold free, load; simpl. + case (zlt b (nextblock m)). + repeat (rewrite update_o; auto). + reflexivity. +Qed. + +Theorem low_bound_free: + forall (m: mem) (b bf: block), + b <> bf -> + low_bound (free m bf) b = low_bound m b. +Proof. + intros. unfold free, low_bound; simpl. + rewrite update_o; auto. +Qed. + +Theorem high_bound_free: + forall (m: mem) (b bf: block), + b <> bf -> + high_bound (free m bf) b = high_bound m b. +Proof. + intros. unfold free, high_bound; simpl. + rewrite update_o; auto. +Qed. +Hint Resolve load_free low_bound_free high_bound_free. + +(** ** Properties related to [store] *) + +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. +Proof. + intros. generalize (store_inv _ _ _ _ _ _ H). + intros [A [B [C [P D]]]]. + unfold low_bound, high_bound. tauto. +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. +Proof. + intros until v. + unfold load_contents, store_contents in |- *; case sz; + rewrite getN_setN_same; reflexivity. +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). +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]). +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. +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. + +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. +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. + +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. +Proof. + intros. + destruct sz1; destruct sz2; simpl; LSCM. +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'. +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. +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'. +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. +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. + +(** * Agreement between memory blocks. *) + +(** 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). *) + +Definition contentmap_agree (lo hi: Z) (c1 c2: contentmap) := + forall (ofs: Z), + lo <= ofs < hi -> c1 ofs = c2 ofs. + +Definition block_contents_agree (lo hi: Z) (c1 c2: block_contents) := + contentmap_agree lo hi c1.(contents) c2.(contents). + +Definition block_agree (b: block) (lo hi: Z) (m1 m2: mem) := + block_contents_agree lo hi + (m1.(blocks) b) (m2.(blocks) b). + +Theorem block_agree_refl: + forall (m: mem) (b: block) (lo hi: Z), + block_agree b lo hi m m. +Proof. + intros. hnf. 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. +Proof. + intros. hnf. intros. symmetry. apply H. 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. +Proof. + intros. hnf. intros. + transitivity (contents (blocks m2 b) ofs). + apply H; auto. apply H0; 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. +Proof. + induction n; intros; simpl. + auto. + rewrite inj_S in H1. + rewrite H. case (c2 ofs); intros; auto. + apply IHn; omega. + omega. +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. +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. +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. +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. +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). +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. +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). +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). +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). +Proof. + intros. unfold store_contents; case sz; apply setN_agree; auto. +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). +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. +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). +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. +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). +Proof. + intros until v. + unfold store_contents; case sz; simpl; intros; + apply setN_outside_agree; auto; simpl Z_of_nat; omega. +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. +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'. +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'. +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. +Qed. + +(** * 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]. *) + +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 extends (m1 m2: mem) := + m1.(nextblock) = m2.(nextblock) /\ + forall (b: block), + b < m1.(nextblock) -> + block_contents_extends (m1.(blocks) b) (m2.(blocks) b). + +Theorem extends_refl: + forall (m: mem), extends m m. +Proof. + intro. red. split. + reflexivity. + intros. red. + split. omega. split. omega. + red. intros. reflexivity. +Qed. + +Theorem alloc_extends: + forall (m1 m2 m1' m2': mem) (lo1 hi1 lo2 hi2: Z) (b1 b2: block), + extends m1 m2 -> + lo2 <= lo1 -> hi1 <= hi2 -> + alloc m1 lo1 hi1 = (m1', b1) -> + 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. +Qed. + +Theorem free_extends: + forall (m1 m2: mem) (b: block), + 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. +Qed. + +Theorem load_extends: + forall (chunk: memory_chunk) (m1 m2: mem) (b: block) (ofs: Z) (v: val), + extends m1 m2 -> + 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. +Qed. + +Theorem store_within_extends: + forall (chunk: memory_chunk) (m1 m2 m1': mem) (b: block) (ofs: Z) (v: val), + extends m1 m2 -> + 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. + 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. +Qed. + +Theorem store_outside_extends: + forall (chunk: memory_chunk) (m1 m2 m2': mem) (b: block) (ofs: Z) (v: val), + extends m1 m2 -> + ofs + size_chunk chunk <= low_bound m1 b \/ high_bound m1 b <= ofs -> + 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. + congruence. +Qed. + +(** * Store 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 + between the blocks of two memory states [m1] and [m2]: +- if [f b = None], the block [b] of [m1] has no equivalent in [m2]; +- if [f b = Some(b', ofs)], the block [b] of [m2] corresponds to + 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 := + | val_inject_int: + forall i, val_inject (Vint i) (Vint i) + | val_inject_float: + forall f, val_inject (Vfloat f) (Vfloat f) + | val_inject_ptr: + forall b1 ofs1 b2 ofs2 x, + f b1 = Some (b2, x) -> + ofs2 = Int.add ofs1 (Int.repr x) -> + val_inject (Vptr b1 ofs1) (Vptr b2 ofs2) + | val_inject_undef: forall v, + val_inject Vundef v. + +Hint Resolve val_inject_int val_inject_float val_inject_ptr +val_inject_undef. + +Inductive val_list_inject: list val -> list val-> Prop:= + | val_nil_inject : + val_list_inject 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). + +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 + }. + +(** A memory state [m1] injects into another memory state [m2] via the + memory injection [f] if the following conditions hold: +- 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]. +*) + +Record mem_inject (m1 m2: mem) : Prop := + mk_mem_inject { + mi_freeblocks: + forall b, b >= m1.(nextblock) -> f b = None; + mi_mappedblocks: + 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) + }. + +(** 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. +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. +Qed. + +Lemma valid_pointer_inject_no_overflow: + forall m1 m2 b ofs b' x, + mem_inject 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. + 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). +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. +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. + +Lemma load_inject: + forall m1 m2 chunk b1 ofs b2 delta v1, + mem_inject 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. +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. +Qed. + +Lemma loadv_inject: + forall m1 m2 chunk a1 a2 v1, + mem_inject m1 m2 -> + loadv chunk m1 a1 = Some v1 -> + val_inject a1 a2 -> + exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject 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. +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. + +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. + +Lemma store_mapped_inject_1: + forall chunk m1 b1 ofs v1 n1 m2 b2 delta v2, + mem_inject m1 m2 -> + store chunk m1 b1 ofs v1 = Some n1 -> + f b1 = Some (b2, delta) -> + val_content_inject (mem_chunk 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. +Qed. + +Lemma store_mapped_inject: + forall chunk m1 b1 ofs v1 n1 m2 b2 delta v2, + mem_inject m1 m2 -> + store chunk m1 b1 ofs v1 = Some n1 -> + f b1 = Some (b2, delta) -> + val_inject v1 v2 -> + exists n2, + store chunk m2 b2 (ofs + delta) v2 = Some n2 + /\ mem_inject 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 -> + 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. +Qed. + +Lemma storev_mapped_inject_1: + forall chunk m1 a1 v1 n1 m2 a2 v2, + mem_inject m1 m2 -> + storev chunk m1 a1 v1 = Some n1 -> + val_inject a1 a2 -> + val_content_inject (mem_chunk chunk) v1 v2 -> + exists n2, + storev chunk m2 a2 v2 = Some n2 /\ mem_inject 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). + 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. +Qed. + +Lemma storev_mapped_inject: + forall chunk m1 a1 v1 n1 m2 a2 v2, + mem_inject m1 m2 -> + storev chunk m1 a1 v1 = Some n1 -> + val_inject a1 a2 -> + val_inject v1 v2 -> + exists n2, + storev chunk m2 a2 v2 = Some n2 /\ mem_inject 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. +Proof. + intros. unfold free in H. + rewrite<- H . unfold low_bound , high_bound . + simpl . rewrite update_s. simpl. omega. +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). +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. + +Lemma free_inject: + forall 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 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. + +(** Monotonicity properties of memory injections. *) + +Definition inject_incr (f1 f2: meminj) : Prop := + forall b, f1 b = f2 b \/ f1 b = None. + +Lemma inject_incr_refl : + forall f , inject_incr f f . +Proof. unfold inject_incr . intros. left . auto . Qed. + +Lemma inject_incr_trans : + 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 . +Qed. + +Lemma val_inject_incr: + forall f1 f2 v v', + inject_incr f1 f2 -> + val_inject f1 v v' -> + val_inject f2 v v'. +Proof. + intros. inversion H0. + constructor. + constructor. + elim (H b1); intro. + apply val_inject_ptr with x. congruence. auto. + congruence. + constructor. +Qed. + +Lemma val_list_inject_incr: + forall f1 f2 vl vl' , + 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. +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. + +(** 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'. + +Lemma extend_inject_incr: + forall f b x, + f b = None -> + 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. +Qed. + +Lemma alloc_right_inject: + forall f m1 m2 lo hi m2' b, + mem_inject f m1 m2 -> + 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. +Qed. + +Lemma alloc_unmapped_inject: + forall f m1 m2 lo hi m1' b, + mem_inject f m1 m2 -> + alloc m1 lo hi = (m1', b) -> + 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. + 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). +Qed. + +Lemma alloc_mapped_inject: + forall f m1 m2 lo hi m1' b b' ofs, + mem_inject f m1 m2 -> + alloc m1 lo hi = (m1', b) -> + valid_block m2 b' -> + Int.min_signed <= ofs <= Int.max_signed -> + Int.min_signed <= low_bound m2 b' -> + high_bound m2 b' <= Int.max_signed -> + low_bound m2 b' <= lo + ofs -> + hi + ofs <= high_bound m2 b' -> + (forall b0 ofs0, + f b0 = Some (b', ofs0) -> + high_bound m1 b0 + ofs0 <= lo + ofs \/ + hi + ofs <= low_bound m1 b0 + ofs0) -> + 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 *) + assert (inject_incr f (extend_inject b (Some (b', ofs)) f)). + apply extend_inject_incr. apply mi_freeblocks0. rewrite A. omega. + 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. +Qed. + +Lemma alloc_parallel_inject: + forall f m1 m2 lo hi m1' m2' b1 b2, + mem_inject f m1 m2 -> + 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). +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. +Qed. diff --git a/common/Values.v b/common/Values.v new file mode 100644 index 00000000..aa59e045 --- /dev/null +++ b/common/Values.v @@ -0,0 +1,888 @@ +(** This module defines the type of values that is used in the dynamic + semantics of all our intermediate languages. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. + +Definition block : Set := Z. +Definition eq_block := zeq. + +(** A value is either: +- a machine integer; +- a floating-point number; +- a pointer: a pair of a memory address and an integer offset with respect + to this address; +- the [Vundef] value denoting an arbitrary bit pattern, such as the + value of an uninitialized variable. +*) + +Inductive val: Set := + | Vundef: val + | Vint: int -> val + | Vfloat: float -> val + | Vptr: block -> int -> val. + +Definition Vzero: val := Vint Int.zero. +Definition Vone: val := Vint Int.one. +Definition Vmone: val := Vint Int.mone. + +Definition Vtrue: val := Vint Int.one. +Definition Vfalse: val := Vint Int.zero. + +(** The module [Val] defines a number of arithmetic and logical operations + over type [val]. Most of these operations are straightforward extensions + of the corresponding integer or floating-point operations. *) + +Module Val. + +Definition of_bool (b: bool): val := if b then Vtrue else Vfalse. + +Definition has_type (v: val) (t: typ) : Prop := + match v, t with + | Vundef, _ => True + | Vint _, Tint => True + | Vfloat _, Tfloat => True + | Vptr _ _, Tint => True + | _, _ => False + end. + +Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop := + match vl, tl with + | nil, nil => True + | v1 :: vs, t1 :: ts => has_type v1 t1 /\ has_type_list vs ts + | _, _ => False + end. + +(** Truth values. Pointers and non-zero integers are treated as [True]. + The integer 0 (also used to represent the null pointer) is [False]. + [Vundef] and floats are neither true nor false. *) + +Definition is_true (v: val) : Prop := + match v with + | Vint n => n <> Int.zero + | Vptr b ofs => True + | _ => False + end. + +Definition is_false (v: val) : Prop := + match v with + | Vint n => n = Int.zero + | _ => False + end. + +Inductive bool_of_val: val -> bool -> Prop := + | bool_of_val_int_true: + forall n, n <> Int.zero -> bool_of_val (Vint n) true + | bool_of_val_int_false: + bool_of_val (Vint Int.zero) false + | bool_of_val_ptr: + forall b ofs, bool_of_val (Vptr b ofs) true. + +Definition neg (v: val) : val := + match v with + | Vint n => Vint (Int.neg n) + | _ => Vundef + end. + +Definition negf (v: val) : val := + match v with + | Vfloat f => Vfloat (Float.neg f) + | _ => Vundef + end. + +Definition absf (v: val) : val := + match v with + | Vfloat f => Vfloat (Float.abs f) + | _ => Vundef + end. + +Definition intoffloat (v: val) : val := + match v with + | Vfloat f => Vint (Float.intoffloat f) + | _ => Vundef + end. + +Definition floatofint (v: val) : val := + match v with + | Vint n => Vfloat (Float.floatofint n) + | _ => Vundef + end. + +Definition floatofintu (v: val) : val := + match v with + | Vint n => Vfloat (Float.floatofintu n) + | _ => Vundef + end. + +Definition notint (v: val) : val := + match v with + | Vint n => Vint (Int.xor n Int.mone) + | _ => Vundef + end. + +Definition notbool (v: val) : val := + match v with + | Vint n => of_bool (Int.eq n Int.zero) + | Vptr b ofs => Vfalse + | _ => Vundef + end. + +Definition cast8signed (v: val) : val := + match v with + | Vint n => Vint(Int.cast8signed n) + | _ => Vundef + end. + +Definition cast8unsigned (v: val) : val := + match v with + | Vint n => Vint(Int.cast8unsigned n) + | _ => Vundef + end. + +Definition cast16signed (v: val) : val := + match v with + | Vint n => Vint(Int.cast16signed n) + | _ => Vundef + end. + +Definition cast16unsigned (v: val) : val := + match v with + | Vint n => Vint(Int.cast16unsigned n) + | _ => Vundef + end. + +Definition singleoffloat (v: val) : val := + match v with + | Vfloat f => Vfloat(Float.singleoffloat f) + | _ => Vundef + end. + +Definition add (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => Vint(Int.add n1 n2) + | Vptr b1 ofs1, Vint n2 => Vptr b1 (Int.add ofs1 n2) + | Vint n1, Vptr b2 ofs2 => Vptr b2 (Int.add ofs2 n1) + | _, _ => Vundef + end. + +Definition sub (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => Vint(Int.sub n1 n2) + | Vptr b1 ofs1, Vint n2 => Vptr b1 (Int.sub ofs1 n2) + | Vptr b1 ofs1, Vptr b2 ofs2 => + if zeq b1 b2 then Vint(Int.sub ofs1 ofs2) else Vundef + | _, _ => Vundef + end. + +Definition mul (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => Vint(Int.mul n1 n2) + | _, _ => Vundef + end. + +Definition divs (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero then Vundef else Vint(Int.divs n1 n2) + | _, _ => Vundef + end. + +Definition mods (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero then Vundef else Vint(Int.mods n1 n2) + | _, _ => Vundef + end. + +Definition divu (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero then Vundef else Vint(Int.divu n1 n2) + | _, _ => Vundef + end. + +Definition modu (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero then Vundef else Vint(Int.modu n1 n2) + | _, _ => Vundef + end. + +Definition and (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => Vint(Int.and n1 n2) + | _, _ => Vundef + end. + +Definition or (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => Vint(Int.or n1 n2) + | _, _ => Vundef + end. + +Definition xor (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => Vint(Int.xor n1 n2) + | _, _ => Vundef + end. + +Definition shl (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 32) + then Vint(Int.shl n1 n2) + else Vundef + | _, _ => Vundef + end. + +Definition shr (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 32) + then Vint(Int.shr n1 n2) + else Vundef + | _, _ => Vundef + end. + +Definition shr_carry (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 32) + then Vint(Int.shr_carry n1 n2) + else Vundef + | _, _ => Vundef + end. + +Definition shrx (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 32) + then Vint(Int.shrx n1 n2) + else Vundef + | _, _ => Vundef + end. + +Definition shru (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 32) + then Vint(Int.shru n1 n2) + else Vundef + | _, _ => Vundef + end. + +Definition rolm (v: val) (amount mask: int): val := + match v with + | Vint n => Vint(Int.rolm n amount mask) + | _ => Vundef + end. + +Definition addf (v1 v2: val): val := + match v1, v2 with + | Vfloat f1, Vfloat f2 => Vfloat(Float.add f1 f2) + | _, _ => Vundef + end. + +Definition subf (v1 v2: val): val := + match v1, v2 with + | Vfloat f1, Vfloat f2 => Vfloat(Float.sub f1 f2) + | _, _ => Vundef + end. + +Definition mulf (v1 v2: val): val := + match v1, v2 with + | Vfloat f1, Vfloat f2 => Vfloat(Float.mul f1 f2) + | _, _ => Vundef + end. + +Definition divf (v1 v2: val): val := + match v1, v2 with + | Vfloat f1, Vfloat f2 => Vfloat(Float.div f1 f2) + | _, _ => Vundef + end. + +Definition cmp_mismatch (c: comparison): val := + match c with + | Ceq => Vfalse + | Cne => Vtrue + | _ => Vundef + end. + +Definition cmp (c: comparison) (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => of_bool (Int.cmp c n1 n2) + | Vint n1, Vptr b2 ofs2 => + if Int.eq n1 Int.zero then cmp_mismatch c else Vundef + | Vptr b1 ofs1, Vptr b2 ofs2 => + if zeq b1 b2 + then of_bool (Int.cmp c ofs1 ofs2) + else cmp_mismatch c + | Vptr b1 ofs1, Vint n2 => + if Int.eq n2 Int.zero then cmp_mismatch c else Vundef + | _, _ => Vundef + end. + +Definition cmpu (c: comparison) (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + of_bool (Int.cmpu c n1 n2) + | Vint n1, Vptr b2 ofs2 => + if Int.eq n1 Int.zero then cmp_mismatch c else Vundef + | Vptr b1 ofs1, Vptr b2 ofs2 => + if zeq b1 b2 + then of_bool (Int.cmpu c ofs1 ofs2) + else cmp_mismatch c + | Vptr b1 ofs1, Vint n2 => + if Int.eq n2 Int.zero then cmp_mismatch c else Vundef + | _, _ => Vundef + end. + +Definition cmpf (c: comparison) (v1 v2: val): val := + match v1, v2 with + | Vfloat f1, Vfloat f2 => of_bool (Float.cmp c f1 f2) + | _, _ => Vundef + end. + +(** [load_result] is used in the memory model (library [Mem]) + to post-process the results of a memory read. For instance, + consider storing the integer value [0xFFF] on 1 byte at a + given address, and reading it back. If it is read back with + chunk [Mint8unsigned], zero-extension must be performed, resulting + in [0xFF]. If it is read back as a [Mint8signed], sign-extension + is performed and [0xFFFFFFFF] is returned. Type mismatches + (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *) + +Definition load_result (chunk: memory_chunk) (v: val) := + match chunk, v with + | Mint8signed, Vint n => Vint (Int.cast8signed n) + | Mint8unsigned, Vint n => Vint (Int.cast8unsigned n) + | Mint16signed, Vint n => Vint (Int.cast16signed n) + | Mint16unsigned, Vint n => Vint (Int.cast16unsigned n) + | Mint32, Vint n => Vint n + | Mint32, Vptr b ofs => Vptr b ofs + | Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f) + | Mfloat64, Vfloat f => Vfloat f + | _, _ => Vundef + end. + +(** Theorems on arithmetic operations. *) + +Theorem cast8unsigned_and: + forall x, cast8unsigned x = and x (Vint(Int.repr 255)). +Proof. + destruct x; simpl; auto. decEq. apply Int.cast8unsigned_and. +Qed. + +Theorem cast16unsigned_and: + forall x, cast16unsigned x = and x (Vint(Int.repr 65535)). +Proof. + destruct x; simpl; auto. decEq. apply Int.cast16unsigned_and. +Qed. + +Theorem istrue_not_isfalse: + forall v, is_false v -> is_true (notbool v). +Proof. + destruct v; simpl; try contradiction. + intros. subst i. simpl. discriminate. +Qed. + +Theorem isfalse_not_istrue: + forall v, is_true v -> is_false (notbool v). +Proof. + destruct v; simpl; try contradiction. + intros. generalize (Int.eq_spec i Int.zero). + case (Int.eq i Int.zero); intro. + contradiction. simpl. auto. + auto. +Qed. + +Theorem bool_of_true_val: + forall v, is_true v -> bool_of_val v true. +Proof. + intro. destruct v; simpl; intros; try contradiction. + constructor; auto. constructor. +Qed. + +Theorem bool_of_true_val2: + forall v, bool_of_val v true -> is_true v. +Proof. + intros. inversion H; simpl; auto. +Qed. + +Theorem bool_of_true_val_inv: + forall v b, is_true v -> bool_of_val v b -> b = true. +Proof. + intros. inversion H0; subst v b; simpl in H; auto. +Qed. + +Theorem bool_of_false_val: + forall v, is_false v -> bool_of_val v false. +Proof. + intro. destruct v; simpl; intros; try contradiction. + subst i; constructor. +Qed. + +Theorem bool_of_false_val2: + forall v, bool_of_val v false -> is_false v. +Proof. + intros. inversion H; simpl; auto. +Qed. + +Theorem bool_of_false_val_inv: + forall v b, is_false v -> bool_of_val v b -> b = false. +Proof. + intros. inversion H0; subst v b; simpl in H. + congruence. auto. contradiction. +Qed. + +Theorem notbool_negb_1: + forall b, of_bool (negb b) = notbool (of_bool b). +Proof. + destruct b; reflexivity. +Qed. + +Theorem notbool_negb_2: + forall b, of_bool b = notbool (of_bool (negb b)). +Proof. + destruct b; reflexivity. +Qed. + +Theorem notbool_idem2: + forall b, notbool(notbool(of_bool b)) = of_bool b. +Proof. + destruct b; reflexivity. +Qed. + +Theorem notbool_idem3: + forall x, notbool(notbool(notbool x)) = notbool x. +Proof. + destruct x; simpl; auto. + case (Int.eq i Int.zero); reflexivity. +Qed. + +Theorem add_commut: forall x y, add x y = add y x. +Proof. + destruct x; destruct y; simpl; auto. + decEq. apply Int.add_commut. +Qed. + +Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + rewrite Int.add_assoc; auto. + rewrite Int.add_assoc; auto. + decEq. decEq. apply Int.add_commut. + decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc. + decEq. apply Int.add_commut. + decEq. rewrite Int.add_assoc. auto. +Qed. + +Theorem add_permut: forall x y z, add x (add y z) = add y (add x z). +Proof. + intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut. +Qed. + +Theorem add_permut_4: + forall x y z t, add (add x y) (add z t) = add (add x z) (add y t). +Proof. + intros. rewrite add_permut. rewrite add_assoc. + rewrite add_permut. symmetry. apply add_assoc. +Qed. + +Theorem neg_zero: neg Vzero = Vzero. +Proof. + reflexivity. +Qed. + +Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y). +Proof. + destruct x; destruct y; simpl; auto. decEq. apply Int.neg_add_distr. +Qed. + +Theorem sub_zero_r: forall x, sub Vzero x = neg x. +Proof. + destruct x; simpl; auto. +Qed. + +Theorem sub_add_opp: forall x y, sub x (Vint y) = add x (Vint (Int.neg y)). +Proof. + destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto. +Qed. + +Theorem sub_add_l: + forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i). +Proof. + destruct v1; destruct v2; intros; simpl; auto. + rewrite Int.sub_add_l. auto. + rewrite Int.sub_add_l. auto. + case (zeq b b0); intro. rewrite Int.sub_add_l. auto. reflexivity. +Qed. + +Theorem sub_add_r: + forall v1 v2 i, sub v1 (add v2 (Vint i)) = add (sub v1 v2) (Vint (Int.neg i)). +Proof. + destruct v1; destruct v2; intros; simpl; auto. + rewrite Int.sub_add_r. auto. + repeat rewrite Int.sub_add_opp. decEq. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + decEq. repeat rewrite Int.sub_add_opp. + rewrite Int.add_assoc. decEq. apply Int.neg_add_distr. + case (zeq b b0); intro. simpl. decEq. + repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq. + apply Int.neg_add_distr. + reflexivity. +Qed. + +Theorem mul_commut: forall x y, mul x y = mul y x. +Proof. + destruct x; destruct y; simpl; auto. decEq. apply Int.mul_commut. +Qed. + +Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + decEq. apply Int.mul_assoc. +Qed. + +Theorem mul_add_distr_l: + forall x y z, mul (add x y) z = add (mul x z) (mul y z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + decEq. apply Int.mul_add_distr_l. +Qed. + + +Theorem mul_add_distr_r: + forall x y z, mul x (add y z) = add (mul x y) (mul x z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + decEq. apply Int.mul_add_distr_r. +Qed. + +Theorem mul_pow2: + forall x n logn, + Int.is_power2 n = Some logn -> + mul x (Vint n) = shl x (Vint logn). +Proof. + intros; destruct x; simpl; auto. + change 32 with (Z_of_nat wordsize). + rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto. +Qed. + +Theorem mods_divs: + forall x y, mods x y = sub x (mul (divs x y) y). +Proof. + destruct x; destruct y; simpl; auto. + case (Int.eq i0 Int.zero); simpl. auto. decEq. apply Int.mods_divs. +Qed. + +Theorem modu_divu: + forall x y, modu x y = sub x (mul (divu x y) y). +Proof. + destruct x; destruct y; simpl; auto. + generalize (Int.eq_spec i0 Int.zero); + case (Int.eq i0 Int.zero); simpl. auto. + intro. decEq. apply Int.modu_divu. auto. +Qed. + +Theorem divs_pow2: + forall x n logn, + Int.is_power2 n = Some logn -> + divs x (Vint n) = shrx x (Vint logn). +Proof. + intros; destruct x; simpl; auto. + change 32 with (Z_of_nat wordsize). + rewrite (Int.is_power2_range _ _ H). + generalize (Int.eq_spec n Int.zero); + case (Int.eq n Int.zero); intro. + subst n. compute in H. discriminate. + decEq. apply Int.divs_pow2. auto. +Qed. + +Theorem divu_pow2: + forall x n logn, + Int.is_power2 n = Some logn -> + divu x (Vint n) = shru x (Vint logn). +Proof. + intros; destruct x; simpl; auto. + change 32 with (Z_of_nat wordsize). + rewrite (Int.is_power2_range _ _ H). + generalize (Int.eq_spec n Int.zero); + case (Int.eq n Int.zero); intro. + subst n. compute in H. discriminate. + decEq. apply Int.divu_pow2. auto. +Qed. + +Theorem modu_pow2: + forall x n logn, + Int.is_power2 n = Some logn -> + modu x (Vint n) = and x (Vint (Int.sub n Int.one)). +Proof. + intros; destruct x; simpl; auto. + generalize (Int.eq_spec n Int.zero); + case (Int.eq n Int.zero); intro. + subst n. compute in H. discriminate. + decEq. eapply Int.modu_and; eauto. +Qed. + +Theorem and_commut: forall x y, and x y = and y x. +Proof. + destruct x; destruct y; simpl; auto. decEq. apply Int.and_commut. +Qed. + +Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + decEq. apply Int.and_assoc. +Qed. + +Theorem or_commut: forall x y, or x y = or y x. +Proof. + destruct x; destruct y; simpl; auto. decEq. apply Int.or_commut. +Qed. + +Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + decEq. apply Int.or_assoc. +Qed. + +Theorem xor_commut: forall x y, xor x y = xor y x. +Proof. + destruct x; destruct y; simpl; auto. decEq. apply Int.xor_commut. +Qed. + +Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + decEq. apply Int.xor_assoc. +Qed. + +Theorem shl_mul: forall x y, Val.mul x (Val.shl Vone y) = Val.shl x y. +Proof. + destruct x; destruct y; simpl; auto. + case (Int.ltu i0 (Int.repr 32)); auto. + decEq. symmetry. apply Int.shl_mul. +Qed. + +Theorem shl_rolm: + forall x n, + Int.ltu n (Int.repr 32) = true -> + shl x (Vint n) = rolm x n (Int.shl Int.mone n). +Proof. + intros; destruct x; simpl; auto. + rewrite H. decEq. apply Int.shl_rolm. exact H. +Qed. + +Theorem shru_rolm: + forall x n, + Int.ltu n (Int.repr 32) = true -> + shru x (Vint n) = rolm x (Int.sub (Int.repr 32) n) (Int.shru Int.mone n). +Proof. + intros; destruct x; simpl; auto. + rewrite H. decEq. apply Int.shru_rolm. exact H. +Qed. + +Theorem shrx_carry: + forall x y, + add (shr x y) (shr_carry x y) = shrx x y. +Proof. + destruct x; destruct y; simpl; auto. + case (Int.ltu i0 (Int.repr 32)); auto. + simpl. decEq. apply Int.shrx_carry. +Qed. + +Theorem or_rolm: + forall x n m1 m2, + or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2). +Proof. + intros; destruct x; simpl; auto. + decEq. apply Int.or_rolm. +Qed. + +Theorem rolm_rolm: + forall x n1 m1 n2 m2, + rolm (rolm x n1 m1) n2 m2 = + rolm x (Int.and (Int.add n1 n2) (Int.repr 31)) + (Int.and (Int.rol m1 n2) m2). +Proof. + intros; destruct x; simpl; auto. + decEq. + replace (Int.and (Int.add n1 n2) (Int.repr 31)) + with (Int.modu (Int.add n1 n2) (Int.repr 32)). + apply Int.rolm_rolm. + change (Int.repr 31) with (Int.sub (Int.repr 32) Int.one). + apply Int.modu_and with (Int.repr 5). reflexivity. +Qed. + +Theorem rolm_zero: + forall x m, + rolm x Int.zero m = and x (Vint m). +Proof. + intros; destruct x; simpl; auto. decEq. apply Int.rolm_zero. +Qed. + +Theorem addf_commut: forall x y, addf x y = addf y x. +Proof. + destruct x; destruct y; simpl; auto. decEq. apply Float.addf_commut. +Qed. + +Lemma negate_cmp_mismatch: + forall c, + cmp_mismatch (negate_comparison c) = notbool(cmp_mismatch c). +Proof. + destruct c; reflexivity. +Qed. + +Theorem negate_cmp: + forall c x y, + cmp (negate_comparison c) x y = notbool (cmp c x y). +Proof. + destruct x; destruct y; simpl; auto. + rewrite Int.negate_cmp. apply notbool_negb_1. + case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity. + case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity. + case (zeq b b0); intro. + rewrite Int.negate_cmp. apply notbool_negb_1. + apply negate_cmp_mismatch. +Qed. + +Theorem negate_cmpu: + forall c x y, + cmpu (negate_comparison c) x y = notbool (cmpu c x y). +Proof. + destruct x; destruct y; simpl; auto. + rewrite Int.negate_cmpu. apply notbool_negb_1. + case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity. + case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity. + case (zeq b b0); intro. + rewrite Int.negate_cmpu. apply notbool_negb_1. + apply negate_cmp_mismatch. +Qed. + +Lemma swap_cmp_mismatch: + forall c, cmp_mismatch (swap_comparison c) = cmp_mismatch c. +Proof. + destruct c; reflexivity. +Qed. + +Theorem swap_cmp: + forall c x y, + cmp (swap_comparison c) x y = cmp c y x. +Proof. + destruct x; destruct y; simpl; auto. + rewrite Int.swap_cmp. auto. + case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto. + case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto. + case (zeq b b0); intro. + subst b0. rewrite zeq_true. rewrite Int.swap_cmp. auto. + rewrite zeq_false. apply swap_cmp_mismatch. auto. +Qed. + +Theorem swap_cmpu: + forall c x y, + cmpu (swap_comparison c) x y = cmpu c y x. +Proof. + destruct x; destruct y; simpl; auto. + rewrite Int.swap_cmpu. auto. + case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto. + case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto. + case (zeq b b0); intro. + subst b0. rewrite zeq_true. rewrite Int.swap_cmpu. auto. + rewrite zeq_false. apply swap_cmp_mismatch. auto. +Qed. + +Theorem negate_cmpf_eq: + forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2. +Proof. + destruct v1; destruct v2; simpl; auto. + rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. + apply notbool_idem2. +Qed. + +Lemma or_of_bool: + forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2). +Proof. + destruct b1; destruct b2; reflexivity. +Qed. + +Theorem cmpf_le: + forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2). +Proof. + destruct v1; destruct v2; simpl; auto. + rewrite or_of_bool. decEq. apply Float.cmp_le_lt_eq. +Qed. + +Theorem cmpf_ge: + forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2). +Proof. + destruct v1; destruct v2; simpl; auto. + rewrite or_of_bool. decEq. apply Float.cmp_ge_gt_eq. +Qed. + +Definition is_bool (v: val) := + v = Vundef \/ v = Vtrue \/ v = Vfalse. + +Lemma of_bool_is_bool: + forall b, is_bool (of_bool b). +Proof. + destruct b; unfold is_bool; simpl; tauto. +Qed. + +Lemma undef_is_bool: is_bool Vundef. +Proof. + unfold is_bool; tauto. +Qed. + +Lemma cmp_mismatch_is_bool: + forall c, is_bool (cmp_mismatch c). +Proof. + destruct c; simpl; unfold is_bool; tauto. +Qed. + +Lemma cmp_is_bool: + forall c v1 v2, is_bool (cmp c v1 v2). +Proof. + destruct v1; destruct v2; simpl; try apply undef_is_bool. + apply of_bool_is_bool. + case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool. + case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool. + case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool. +Qed. + +Lemma cmpu_is_bool: + forall c v1 v2, is_bool (cmpu c v1 v2). +Proof. + destruct v1; destruct v2; simpl; try apply undef_is_bool. + apply of_bool_is_bool. + case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool. + case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool. + case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool. +Qed. + +Lemma cmpf_is_bool: + forall c v1 v2, is_bool (cmpf c v1 v2). +Proof. + destruct v1; destruct v2; simpl; + apply undef_is_bool || apply of_bool_is_bool. +Qed. + +Lemma notbool_is_bool: + forall v, is_bool (notbool v). +Proof. + destruct v; simpl. + apply undef_is_bool. apply of_bool_is_bool. + apply undef_is_bool. unfold is_bool; tauto. +Qed. + +Lemma notbool_xor: + forall v, is_bool v -> v = xor (notbool v) Vone. +Proof. + intros. elim H; intro. + subst v. reflexivity. + elim H0; intro; subst v; reflexivity. +Qed. + +End Val. |