From 3358c5ebecf24aec90df610b0cd46585d6af70ca Mon Sep 17 00:00:00 2001 From: Lélio Brun Date: Thu, 30 Jun 2016 17:05:58 +0200 Subject: Semantics parametrized by function entry --- cfrontend/ClightBigstep.v | 89 ++++++++++++++++++++++++++++------------------- 1 file changed, 53 insertions(+), 36 deletions(-) diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index 92457586..2bccf60a 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -74,6 +74,8 @@ Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem): Prop [t] is the trace of input/output events performed during this evaluation. *) +Variable function_entry: function -> list val -> mem -> env -> temp_env -> mem -> Prop. + Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> mem -> outcome -> Prop := | exec_Sskip: forall e le m, exec_stmt e le m Sskip @@ -163,14 +165,12 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> by the call. *) with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := - | eval_funcall_internal: forall le m f vargs t e m1 m2 m3 out vres m4, - alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> - list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> - bind_parameters ge e m1 f.(fn_params) vargs m2 -> - exec_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t le m3 out -> - outcome_result_value out f.(fn_return) vres m3 -> - Mem.free_list m3 (blocks_of_env ge e) = Some m4 -> - eval_funcall m (Internal f) vargs t m4 vres + | eval_funcall_internal: forall m f vargs t e le1 le2 m1 m2 out vres m3, + function_entry f vargs m e le1 m1 -> + exec_stmt e le1 m1 f.(fn_body) t le2 m2 out -> + outcome_result_value out f.(fn_return) vres m2 -> + Mem.free_list m2 (blocks_of_env ge e) = Some m3 -> + eval_funcall m (Internal f) vargs t m3 vres | eval_funcall_external: forall m ef targs tres cconv vargs t vres m', external_call ef ge vargs m t vres m' -> eval_funcall m (External ef targs tres cconv) vargs t m' vres. @@ -231,17 +231,19 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro [fd] on arguments [args] diverges, with observable trace [t]. *) with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop := - | evalinf_funcall_internal: forall m f vargs t e m1 m2, - alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> - list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> - bind_parameters ge e m1 f.(fn_params) vargs m2 -> - execinf_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t -> + | evalinf_funcall_internal: forall m f vargs t e m1 le1, + function_entry f vargs m e le1 m1 -> + execinf_stmt e le1 m1 f.(fn_body) t -> evalinf_funcall m (Internal f) vargs t. End BIGSTEP. (** Big-step execution of a whole program. *) +Section ENTRY. + +Variable function_entry: genv -> function -> list val -> mem -> env -> temp_env -> mem -> Prop. + Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := | bigstep_program_terminates_intro: forall b f m0 m1 t r, let ge := globalenv p in @@ -249,7 +251,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> type_of_fundef f = Tfunction Tnil type_int32s cc_default -> - eval_funcall ge m0 f nil t m1 (Vint r) -> + eval_funcall ge (function_entry ge) m0 f nil t m1 (Vint r) -> bigstep_program_terminates p t r. Inductive bigstep_program_diverges (p: program): traceinf -> Prop := @@ -259,12 +261,14 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> type_of_fundef f = Tfunction Tnil type_int32s cc_default -> - evalinf_funcall ge m0 f nil t -> + evalinf_funcall ge (function_entry ge) m0 f nil t -> bigstep_program_diverges p t. Definition bigstep_semantics (p: program) := Bigstep_semantics (bigstep_program_terminates p) (bigstep_program_diverges p). +End ENTRY. + (** * Implication from big-step semantics to transition semantics *) Section BIGSTEP_TO_TRANSITIONS. @@ -296,18 +300,31 @@ Proof. destruct k; simpl; intros; contradiction || auto. Qed. +Variable function_entry: genv -> function -> list val -> mem -> env -> temp_env -> mem -> Prop. + +Definition exec_stmt_fe (ge: genv) := exec_stmt ge (function_entry ge). +Definition eval_funcall_fe (ge: genv) := eval_funcall ge (function_entry ge). +Definition execinf_stmt_fe (ge: genv) := execinf_stmt ge (function_entry ge). +Definition evalinf_funcall_fe (ge: genv) := evalinf_funcall ge (function_entry ge). +Definition bigstep_semantics_fe := bigstep_semantics function_entry. + +Definition step_fe (ge: genv) := step ge (function_entry ge). +Definition semantics_fe (p: program) := + let ge := globalenv p in + Semantics_gen step_fe (initial_state p) final_state ge ge. + Lemma exec_stmt_eval_funcall_steps: (forall e le m s t le' m' out, - exec_stmt ge e le m s t le' m' out -> + exec_stmt_fe ge e le m s t le' m' out -> forall f k, exists S, - star step1 ge (State f s k e le m) t S + star step_fe ge (State f s k e le m) t S /\ outcome_state_match e le' m' f k out S) /\ (forall m fd args t m' res, - eval_funcall ge m fd args t m' res -> + eval_funcall_fe ge m fd args t m' res -> forall k, is_call_cont k -> - star step1 ge (Callstate fd args k m) t (Returnstate res k m')). + star step_fe ge (Callstate fd args k m) t (Returnstate res k m')). Proof. apply exec_stmt_funcall_ind; intros. @@ -450,23 +467,23 @@ Proof. unfold S2. inv B1; simpl; econstructor; eauto. (* call internal *) - destruct (H3 f k) as [S1 [A1 B1]]. - eapply star_left. eapply step_internal_function; eauto. econstructor; eauto. + destruct (H1 f k) as [S1 [A1 B1]]. + eapply star_left. eapply step_internal_function; eauto. eapply star_right. eexact A1. inv B1; simpl in H4; try contradiction. (* Out_normal *) assert (fn_return f = Tvoid /\ vres = Vundef). destruct (fn_return f); auto || contradiction. - destruct H7. subst vres. apply step_skip_call; auto. + destruct H5. subst vres. apply step_skip_call; auto. (* Out_return None *) assert (fn_return f = Tvoid /\ vres = Vundef). destruct (fn_return f); auto || contradiction. - destruct H8. subst vres. - rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7. + destruct H6. subst vres. + rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. apply step_return_0; auto. (* Out_return Some *) - destruct H4. - rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7. + destruct H2. + rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. eapply step_return_1; eauto. reflexivity. traceEq. @@ -476,31 +493,31 @@ Qed. Lemma exec_stmt_steps: forall e le m s t le' m' out, - exec_stmt ge e le m s t le' m' out -> + exec_stmt_fe ge e le m s t le' m' out -> forall f k, exists S, - star step1 ge (State f s k e le m) t S + star step_fe ge (State f s k e le m) t S /\ outcome_state_match e le' m' f k out S. Proof (proj1 exec_stmt_eval_funcall_steps). Lemma eval_funcall_steps: forall m fd args t m' res, - eval_funcall ge m fd args t m' res -> + eval_funcall_fe ge m fd args t m' res -> forall k, is_call_cont k -> - star step1 ge (Callstate fd args k m) t (Returnstate res k m'). + star step_fe ge (Callstate fd args k m) t (Returnstate res k m'). Proof (proj2 exec_stmt_eval_funcall_steps). Definition order (x y: unit) := False. Lemma evalinf_funcall_forever: forall m fd args T k, - evalinf_funcall ge m fd args T -> - forever_N step1 order ge tt (Callstate fd args k m) T. + evalinf_funcall_fe ge m fd args T -> + forever_N step_fe order ge tt (Callstate fd args k m) T. Proof. cofix CIH_FUN. assert (forall e le m s T f k, - execinf_stmt ge e le m s T -> - forever_N step1 order ge tt (State f s k e le m) T). + execinf_stmt_fe ge e le m s T -> + forever_N step_fe order ge tt (State f s k e le m) T). cofix CIH_STMT. intros. inv H. @@ -559,13 +576,13 @@ Proof. (* call internal *) intros. inv H0. eapply forever_N_plus. - eapply plus_one. econstructor; eauto. econstructor; eauto. + eapply plus_one. econstructor; eauto. apply H; eauto. traceEq. Qed. Theorem bigstep_semantics_sound: - bigstep_sound (bigstep_semantics prog) (semantics1 prog). + bigstep_sound (bigstep_semantics_fe prog) (semantics_fe prog). Proof. constructor; simpl; intros. (* termination *) -- cgit From da7ba2d116ec11fc2071432305db8ad4fdf4c9c0 Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Thu, 7 Jul 2016 09:35:25 +0200 Subject: Remove unnecessary module paths --- common/Separation.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/common/Separation.v b/common/Separation.v index 27065d1f..a8de7390 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -502,6 +502,26 @@ Proof. - auto. Qed. +Lemma range_contains': + forall chunk b ofs, + (align_chunk chunk | ofs) -> + massert_imp (range b ofs (ofs + size_chunk chunk)) + (contains chunk b ofs (fun v => True)). +Proof. + intros. constructor. + intros. destruct H0 as (D & E & F). + assert (Mem.valid_access m chunk b ofs Freeable). + { split; auto. red; auto. } + split. +- generalize (Memdata.size_chunk_pos chunk). + unfold Ptrofs.max_unsigned. omega. +- split; [assumption|]. + destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. + eauto with mem. + exists v; auto. +- auto. +Qed. + Lemma contains_imp: forall (spec1 spec2: val -> Prop) chunk b ofs, (forall v, spec1 v -> spec2 v) -> -- cgit From 2eddad7791630a02769c5810babc3e612a605bee Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Wed, 3 Aug 2016 11:55:01 +0200 Subject: Strengthen contains massert The idea is to be able to exchange a "contains" for a "range" over the same footprint, i.e., m |= contains chunk b ofs spec ** P -> m |= range b ofs (ofs + size_chunk chunk) ** P This requires knowing that ofs + size_chunk chunk <= Int.modulus. --- common/Separation.v | 77 ++++++++++++++++++++++++++++++++++------------------- 1 file changed, 50 insertions(+), 27 deletions(-) diff --git a/common/Separation.v b/common/Separation.v index a8de7390..1f0d9f7f 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -413,15 +413,16 @@ Qed. Program Definition contains (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {| m_pred := fun m => - 0 <= ofs <= Ptrofs.max_unsigned + 0 <= ofs /\ ofs + size_chunk chunk <= Ptrofs.modulus /\ Mem.valid_access m chunk b ofs Freeable /\ exists v, Mem.load chunk m b ofs = Some v /\ spec v; m_footprint := fun b' ofs' => b' = b /\ ofs <= ofs' < ofs + size_chunk chunk |}. Next Obligation. - rename H2 into v. split;[|split]. + rename H3 into v. split;[|split;[|split]]. - auto. -- destruct H1; split; auto. red; intros; eapply Mem.perm_unchanged_on; eauto. simpl; auto. +- auto. +- destruct H2; split; auto. red; intros; eapply Mem.perm_unchanged_on; eauto. simpl; auto. - exists v. split; auto. eapply Mem.load_unchanged_on; eauto. simpl; auto. Qed. Next Obligation. @@ -433,7 +434,11 @@ Lemma contains_no_overflow: m |= contains chunk b ofs spec -> 0 <= ofs <= Ptrofs.max_unsigned. Proof. - intros. simpl in H. tauto. + intros. simpl in H. + destruct H as (H1 & H2 & H3). + split; [assumption|]. + generalize (size_chunk_pos chunk). + unfold Ptrofs.max_unsigned. omega. Qed. Lemma load_rule: @@ -441,7 +446,7 @@ Lemma load_rule: m |= contains chunk b ofs spec -> exists v, Mem.load chunk m b ofs = Some v /\ spec v. Proof. - intros. destruct H as (D & E & v & F & G). + intros. destruct H as (D & E & F & v & G & H). exists v; auto. Qed. @@ -483,25 +488,6 @@ Proof. simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto. Qed. -Lemma range_contains: - forall chunk b ofs P m, - m |= range b ofs (ofs + size_chunk chunk) ** P -> - (align_chunk chunk | ofs) -> - m |= contains chunk b ofs (fun v => True) ** P. -Proof. - intros. destruct H as (A & B & C). destruct A as (D & E & F). - split; [|split]. -- assert (Mem.valid_access m chunk b ofs Freeable). - { split; auto. red; auto. } - split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. omega. - split. auto. -+ destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. - eauto with mem. - exists v; auto. -- auto. -- auto. -Qed. - Lemma range_contains': forall chunk b ofs, (align_chunk chunk | ofs) -> @@ -512,9 +498,9 @@ Proof. intros. destruct H0 as (D & E & F). assert (Mem.valid_access m chunk b ofs Freeable). { split; auto. red; auto. } - split. -- generalize (Memdata.size_chunk_pos chunk). - unfold Ptrofs.max_unsigned. omega. + split; [|split]. +- generalize (size_chunk_pos chunk). omega. +- assumption. - split; [assumption|]. destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. eauto with mem. @@ -522,6 +508,43 @@ Proof. - auto. Qed. +Lemma range_contains: + forall chunk b ofs P m, + m |= range b ofs (ofs + size_chunk chunk) ** P -> + (align_chunk chunk | ofs) -> + m |= contains chunk b ofs (fun v => True) ** P. +Proof. + intros. + rewrite range_contains' in H; assumption. +Qed. + +Lemma contains_range': + forall chunk b ofs spec, + massert_imp (contains chunk b ofs spec) + (range b ofs (ofs + size_chunk chunk)). +Proof. + intros. + split. +- intros. destruct H as (A & B & C & D). + split; [|split]; try assumption. + destruct C as (C1 & C2). + intros i k p Hr. + specialize (C1 _ Hr). + eapply Mem.perm_cur in C1. + apply Mem.perm_implies with (1:=C1). + apply perm_F_any. +- trivial. +Qed. + +Lemma contains_range: + forall chunk b ofs spec P m, + m |= contains chunk b ofs spec ** P -> + m |= range b ofs (ofs + size_chunk chunk) ** P. +Proof. + intros. + rewrite contains_range' in H; assumption. +Qed. + Lemma contains_imp: forall (spec1 spec2: val -> Prop) chunk b ofs, (forall v, spec1 v -> spec2 v) -> -- cgit From 872236554ea25292f301a519767555200b48813a Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Mon, 8 Aug 2016 16:58:51 +0200 Subject: Some more separation lemmas --- common/Separation.v | 90 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 90 insertions(+) diff --git a/common/Separation.v b/common/Separation.v index 1f0d9f7f..52c089a7 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -115,6 +115,23 @@ Qed. Hint Resolve massert_imp_refl massert_eqv_refl : core. +Instance footprint_massert_imp_Proper: + Proper (massert_imp --> eq ==> eq ==> Basics.impl) m_footprint. +Proof. + destruct 1. repeat intro. subst. intuition. +Qed. + +Instance footprint_massert_eqv_Proper: + Proper (massert_eqv ==> eq ==> eq ==> iff) m_footprint. +Proof. + intros P Q HPQ b' b Hbeq ofs' ofs Hoeq. + subst. + destruct HPQ as [HPQ HQP]. + split; intro HH. + now rewrite HQP. + now rewrite HPQ. +Qed. + (** * Separating conjunction *) Definition disjoint_footprint (P Q: massert) : Prop := @@ -315,6 +332,12 @@ Proof. simpl; intros. intuition auto. red; simpl; tauto. Qed. +Lemma sep_pure': + forall P m, m |= pure P <-> P. +Proof. + simpl; intros. intuition auto. +Qed. + (** A range of bytes, with full permissions and unspecified contents. *) Program Definition range (b: block) (lo hi: Z) : massert := {| @@ -346,6 +369,59 @@ Proof. eelim Mem.fresh_block_alloc; eauto. eapply (m_valid P); eauto. Qed. +Lemma free_rule: +forall P m b lo hi, + m |= range b lo hi ** P -> + exists m', + Mem.free m b lo hi = Some m' /\ m' |= P. +Proof. + intros P m b lo hi Hr. + destruct Hr as ((Hlo & Hhi & Hperm) & HP & Hdj). + assert (Mem.range_perm m b lo hi Cur Freeable) as Hrp + by (intros ? ?; now apply Hperm). + apply Mem.range_perm_free in Hrp. + destruct Hrp as (m2 & Hfree). + exists m2. + split; [assumption|]. + apply Mem.free_unchanged_on with (P:=m_footprint P) in Hfree. + now apply m_invar with (1:=HP) (2:=Hfree). + intros i Hr HfP. + apply Hdj with (2:=HfP). + now split. +Qed. + +Lemma range_split': + forall b lo hi mid, + lo <= mid <= hi -> + massert_eqv (range b lo hi) + (range b lo mid ** range b mid hi). +Proof. + intros * HR. + constructor; constructor. + - intros m HH. + inversion HH as [Hlo [Hhi Hperm]]. + split; constructor; repeat split. + + assumption. + + omega. + + intros. apply Hperm. omega. + + omega. + + exact Hhi. + + intros. apply Hperm. omega. + + red; simpl; intros; omega. + - intros. simpl in *. intuition. + - intros m HH. + inversion_clear HH as [Hlm [Hmh Hdisj]]. + inversion_clear Hlm as [Hlo [Hmid Hperm]]. + inversion_clear Hmh as [Hmid' [Hhi Hperm']]. + constructor; repeat split. + + assumption. + + assumption. + + intros i k p Hi. + destruct (Z.lt_ge_cases i mid); intuition. + - intros * Hfoot. simpl in *. + destruct (Z.lt_ge_cases ofs mid); intuition. +Qed. + Lemma range_split: forall b lo hi P mid m, lo <= mid <= hi -> @@ -488,6 +564,20 @@ Proof. simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto. Qed. +Lemma storev_rule2: + forall chunk m m' b ofs v (spec1 spec: val -> Prop) P, + m |= contains chunk b ofs spec1 ** P -> + spec (Val.load_result chunk v) -> + Memory.Mem.storev chunk m (Vptr b (Int.repr ofs)) v = Some m' -> + m' |= contains chunk b ofs spec ** P. +Proof. + intros ** Hm Hspec Hstore. + apply storev_rule with (1:=Hm) in Hspec. + destruct Hspec as [m'' [Hmem Hspec]]. + rewrite Hmem in Hstore. injection Hstore. + intro; subst. assumption. +Qed. + Lemma range_contains': forall chunk b ofs, (align_chunk chunk | ofs) -> -- cgit From 03b07d3f69fda4c32864fba9ecfff66aa23a2e67 Mon Sep 17 00:00:00 2001 From: Lélio Brun Date: Wed, 26 Oct 2016 16:21:29 +0200 Subject: pretty printer for Clight --- cfrontend/PrintClight.ml | 6 +----- common/Separation.v | 4 ++-- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 0e735d2d..7d4c47e5 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -30,11 +30,7 @@ open Clight not in the table of atoms. We print them as "$NNN" (a unique integer). *) -let temp_name (id: AST.ident) = - try - "$" ^ Hashtbl.find string_of_atom id - with Not_found -> - Printf.sprintf "$%d" (P.to_int id) +let temp_name (id: AST.ident) = (* "$" ^ Z.to_string (Z.Zpos id) *)extern_atom id (* Declarator (identifier + type) -- reuse from PrintCsyntax *) diff --git a/common/Separation.v b/common/Separation.v index 52c089a7..c4a46b6a 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -568,10 +568,10 @@ Lemma storev_rule2: forall chunk m m' b ofs v (spec1 spec: val -> Prop) P, m |= contains chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> - Memory.Mem.storev chunk m (Vptr b (Int.repr ofs)) v = Some m' -> + Memory.Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' -> m' |= contains chunk b ofs spec ** P. Proof. - intros ** Hm Hspec Hstore. + intros * Hm Hspec Hstore. apply storev_rule with (1:=Hm) in Hspec. destruct Hspec as [m'' [Hmem Hspec]]. rewrite Hmem in Hstore. injection Hstore. -- cgit From 850a1c46070c089523fa2836a231f66d67cab076 Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Fri, 11 Nov 2016 10:43:54 +0100 Subject: Expose constant elaboration functions --- cparser/Elab.mli | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/cparser/Elab.mli b/cparser/Elab.mli index 59c5efc1..937e86bf 100644 --- a/cparser/Elab.mli +++ b/cparser/Elab.mli @@ -13,6 +13,10 @@ (* *) (* *********************************************************************) +val elab_int_constant : Cabs.cabsloc -> string -> int64 * C.ikind +val elab_float_constant : Cabs.floatInfo -> C.float_cst * C.fkind +val elab_char_constant : Cabs.cabsloc -> bool -> int64 list -> int64 + val elab_file : Cabs.definition list -> C.program (* This is the main entry point. It transforms a list of toplevel definitions as produced by the parser into a program in C abstract -- cgit From 365e4f999541d8c8796ccc7210ee8fbf279fb2f1 Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Fri, 11 Nov 2016 10:53:03 +0100 Subject: Expose the kind of elaborated char constants --- cparser/Elab.ml | 8 ++++---- cparser/Elab.mli | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 9e17cb7e..73a80c6f 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -420,11 +420,12 @@ let elab_char_constant loc wide chars = warning loc Unnamed "character constant too long for its type"; (* C99 6.4.4.4 item 10: single character -> represent at type char or wchar_t *) - Ceval.normalize_int v + let k = (if List.length chars = 1 then if wide then wchar_ikind() else IChar else - IInt) + IInt) in + (Ceval.normalize_int v k, k) let elab_string_literal loc wide chars = let nbits = if wide then 8 * !config.sizeof_wchar else 8 in @@ -452,8 +453,7 @@ let elab_constant loc = function let (v, fk) = elab_float_constant f in CFloat(v, fk) | CONST_CHAR(wide, s) -> - let ikind = if wide then wchar_ikind () else IInt in - CInt(elab_char_constant loc wide s, ikind, "") + CInt(fst (elab_char_constant loc wide s), IInt, "") | CONST_STRING(wide, s) -> elab_string_literal loc wide s diff --git a/cparser/Elab.mli b/cparser/Elab.mli index 937e86bf..31d9b281 100644 --- a/cparser/Elab.mli +++ b/cparser/Elab.mli @@ -15,7 +15,7 @@ val elab_int_constant : Cabs.cabsloc -> string -> int64 * C.ikind val elab_float_constant : Cabs.floatInfo -> C.float_cst * C.fkind -val elab_char_constant : Cabs.cabsloc -> bool -> int64 list -> int64 +val elab_char_constant : Cabs.cabsloc -> bool -> int64 list -> int64 * C.ikind val elab_file : Cabs.definition list -> C.program (* This is the main entry point. It transforms a list of toplevel -- cgit From 8963dc970bb0c2ce8d281508da5b28b9d9aef01d Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Sun, 13 Nov 2016 20:31:32 +0100 Subject: Minor typo in docs: RTLtyping -> Ctyping --- doc/index.html | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/index.html b/doc/index.html index 631c5d99..5f4ac5e1 100644 --- a/doc/index.html +++ b/doc/index.html @@ -341,7 +341,8 @@ See also: NeedOp: process The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.
    -
  • Ctyping: typing for CompCert C + type-checking functions. +
  • Ctyping: typing for + CompCert C + type-checking functions.
  • RTLtyping: typing for RTL + type reconstruction.
  • Lineartyping: typing for Linear. -- cgit From 34a35d283bf068016a7f309367e9d9c3da82f9fa Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Thu, 9 Feb 2017 17:34:16 +0100 Subject: Add range_w for writeable static variables --- common/Separation.v | 191 ++++++++++++++++++++++++++++++++-------------------- x86/Stacklayout.v | 2 +- 2 files changed, 119 insertions(+), 74 deletions(-) diff --git a/common/Separation.v b/common/Separation.v index c4a46b6a..1176edf5 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -338,21 +338,37 @@ Proof. simpl; intros. intuition auto. Qed. -(** A range of bytes, with full permissions and unspecified contents. *) +(** A range of bytes with unspecified contents, and either full permissions + (f = true) or only writable permissions (f = false). *) -Program Definition range (b: block) (lo hi: Z) : massert := {| +Program Definition range' (f: bool) (b: block) (lo hi: Z) : massert := {| m_pred := fun m => 0 <= lo /\ hi <= Ptrofs.modulus - /\ (forall i k p, lo <= i < hi -> Mem.perm m b i k p); + /\ (forall i k, lo <= i < hi -> Mem.perm m b i k + (if f then Freeable else Writable)); m_footprint := fun b' ofs' => b' = b /\ lo <= ofs' < hi |}. Next Obligation. split; auto. split; auto. intros. eapply Mem.perm_unchanged_on; eauto. simpl; auto. Qed. Next Obligation. - apply Mem.perm_valid_block with ofs Cur Freeable; auto. + eapply Mem.perm_valid_block with ofs Cur _; auto. Qed. +Notation range := (range' true). +Notation range_w := (range' false). + +Lemma range_range_w: + forall b lo hi, + massert_imp (range b lo hi) (range_w b lo hi). +Proof. + constructor; auto. + destruct 1 as (Hlo & Hhi & Hperm). + repeat split; auto. + intros i k Hoff. + eapply Mem.perm_implies; eauto using perm_F_any. +Qed. + Lemma alloc_rule: forall m lo hi b m' P, Mem.alloc m lo hi = (m', b) -> @@ -391,10 +407,10 @@ Proof. Qed. Lemma range_split': - forall b lo hi mid, + forall {f} b lo hi mid, lo <= mid <= hi -> - massert_eqv (range b lo hi) - (range b lo mid ** range b mid hi). + massert_eqv (range' f b lo hi) + (range' f b lo mid ** range' f b mid hi). Proof. intros * HR. constructor; constructor. @@ -416,17 +432,17 @@ Proof. constructor; repeat split. + assumption. + assumption. - + intros i k p Hi. + + intros i k Hi. destruct (Z.lt_ge_cases i mid); intuition. - intros * Hfoot. simpl in *. destruct (Z.lt_ge_cases ofs mid); intuition. Qed. Lemma range_split: - forall b lo hi P mid m, + forall {f} b lo hi P mid m, lo <= mid <= hi -> - m |= range b lo hi ** P -> - m |= range b lo mid ** range b mid hi ** P. + m |= range' f b lo hi ** P -> + m |= range' f b lo mid ** range' f b mid hi ** P. Proof. intros. rewrite <- sep_assoc. eapply sep_imp; eauto. split; simpl; intros. @@ -440,29 +456,29 @@ Proof. Qed. Lemma range_drop_left: - forall b lo hi P mid m, + forall {f} b lo hi P mid m, lo <= mid <= hi -> - m |= range b lo hi ** P -> - m |= range b mid hi ** P. + m |= range' f b lo hi ** P -> + m |= range' f b mid hi ** P. Proof. - intros. apply sep_drop with (range b lo mid). apply range_split; auto. + intros. apply sep_drop with (range' f b lo mid). apply range_split; auto. Qed. Lemma range_drop_right: - forall b lo hi P mid m, + forall {f} b lo hi P mid m, lo <= mid <= hi -> - m |= range b lo hi ** P -> - m |= range b lo mid ** P. + m |= range' f b lo hi ** P -> + m |= range' f b lo mid ** P. Proof. - intros. apply sep_drop2 with (range b mid hi). apply range_split; auto. + intros. apply sep_drop2 with (range' f b mid hi). apply range_split; auto. Qed. Lemma range_split_2: - forall b lo hi P mid al m, + forall {f} b lo hi P mid al m, lo <= align mid al <= hi -> al > 0 -> - m |= range b lo hi ** P -> - m |= range b lo mid ** range b (align mid al) hi ** P. + m |= range' f b lo hi ** P -> + m |= range' f b lo mid ** range' f b (align mid al) hi ** P. Proof. intros. rewrite <- sep_assoc. eapply sep_imp; eauto. assert (mid <= align mid al) by (apply align_le; auto). @@ -477,20 +493,22 @@ Proof. Qed. Lemma range_preserved: - forall m m' b lo hi, - m |= range b lo hi -> + forall {f} m m' b lo hi, + m |= range' f b lo hi -> (forall i k p, lo <= i < hi -> Mem.perm m b i k p -> Mem.perm m' b i k p) -> - m' |= range b lo hi. + m' |= range' f b lo hi. Proof. intros. destruct H as (A & B & C). simpl; intuition auto. Qed. -(** A memory area that contains a value sastifying a given predicate *) +(** A memory area that contains a value satisfying a given predicate. + The permissions on the memory are either full (f = true) or only + writable (f = false). *) -Program Definition contains (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {| +Program Definition contains' (f: bool) (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {| m_pred := fun m => 0 <= ofs /\ ofs + size_chunk chunk <= Ptrofs.modulus - /\ Mem.valid_access m chunk b ofs Freeable + /\ Mem.valid_access m chunk b ofs (if f then Freeable else Writable) /\ exists v, Mem.load chunk m b ofs = Some v /\ spec v; m_footprint := fun b' ofs' => b' = b /\ ofs <= ofs' < ofs + size_chunk chunk |}. @@ -505,9 +523,23 @@ Next Obligation. eauto with mem. Qed. +Notation contains := (contains' true). +Notation contains_w := (contains' false). + +Lemma contains_contains_w: + forall chunk b ofs spec, + massert_imp (contains chunk b ofs spec) (contains_w chunk b ofs spec). +Proof. + constructor; auto. + inversion 1 as (Hlo & Hhi & Hac & v & Hload & Hspec). + eapply Mem.valid_access_implies with (p2:=Writable) in Hac; + auto using perm_F_any. + repeat (split; eauto). +Qed. + Lemma contains_no_overflow: - forall spec m chunk b ofs, - m |= contains chunk b ofs spec -> + forall {f} spec m chunk b ofs, + m |= contains' f chunk b ofs spec -> 0 <= ofs <= Ptrofs.max_unsigned. Proof. intros. simpl in H. @@ -518,8 +550,8 @@ Proof. Qed. Lemma load_rule: - forall spec m chunk b ofs, - m |= contains chunk b ofs spec -> + forall {f} spec m chunk b ofs, + m |= contains' f chunk b ofs spec -> exists v, Mem.load chunk m b ofs = Some v /\ spec v. Proof. intros. destruct H as (D & E & F & v & G & H). @@ -527,23 +559,23 @@ Proof. Qed. Lemma loadv_rule: - forall spec m chunk b ofs, - m |= contains chunk b ofs spec -> + forall {f} spec m chunk b ofs, + m |= contains' f chunk b ofs spec -> exists v, Mem.loadv chunk m (Vptr b (Ptrofs.repr ofs)) = Some v /\ spec v. Proof. - intros. exploit load_rule; eauto. intros (v & A & B). exists v; split; auto. + intros. exploit (@load_rule f); eauto. intros (v & A & B). exists v; split; auto. simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow; eauto. Qed. Lemma store_rule: - forall chunk m b ofs v (spec1 spec: val -> Prop) P, - m |= contains chunk b ofs spec1 ** P -> + forall {f} chunk m b ofs v (spec1 spec: val -> Prop) P, + m |= contains' f chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> exists m', - Mem.store chunk m b ofs v = Some m' /\ m' |= contains chunk b ofs spec ** P. + Mem.store chunk m b ofs v = Some m' /\ m' |= contains' f chunk b ofs spec ** P. Proof. intros. destruct H as (A & B & C). destruct A as (D & E & v0 & F & G). - assert (H: Mem.valid_access m chunk b ofs Writable) by eauto with mem. + assert (H: Mem.valid_access m chunk b ofs Writable) by (destruct f; eauto with mem). destruct (Mem.valid_access_store _ _ _ _ v H) as [m' STORE]. exists m'; split; auto. simpl. intuition auto. - eapply Mem.store_valid_access_1; eauto. @@ -554,22 +586,22 @@ Proof. Qed. Lemma storev_rule: - forall chunk m b ofs v (spec1 spec: val -> Prop) P, - m |= contains chunk b ofs spec1 ** P -> + forall {f} chunk m b ofs v (spec1 spec: val -> Prop) P, + m |= contains' f chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> exists m', - Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains chunk b ofs spec ** P. + Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains' f chunk b ofs spec ** P. Proof. - intros. exploit store_rule; eauto. intros (m' & A & B). exists m'; split; auto. + intros. exploit (@store_rule f); eauto. intros (m' & A & B). exists m'; split; auto. simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto. Qed. Lemma storev_rule2: - forall chunk m m' b ofs v (spec1 spec: val -> Prop) P, - m |= contains chunk b ofs spec1 ** P -> + forall {f} chunk m m' b ofs v (spec1 spec: val -> Prop) P, + m |= contains' f chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> Memory.Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' -> - m' |= contains chunk b ofs spec ** P. + m' |= contains' f chunk b ofs spec ** P. Proof. intros * Hm Hspec Hstore. apply storev_rule with (1:=Hm) in Hspec. @@ -579,91 +611,104 @@ Proof. Qed. Lemma range_contains': - forall chunk b ofs, + forall {f} chunk b ofs, (align_chunk chunk | ofs) -> - massert_imp (range b ofs (ofs + size_chunk chunk)) - (contains chunk b ofs (fun v => True)). + massert_imp (range' f b ofs (ofs + size_chunk chunk)) + (contains' f chunk b ofs (fun v => True)). Proof. intros. constructor. intros. destruct H0 as (D & E & F). - assert (Mem.valid_access m chunk b ofs Freeable). + assert (Mem.valid_access m chunk b ofs (if f then Freeable else Writable)). { split; auto. red; auto. } split; [|split]. - generalize (size_chunk_pos chunk). omega. - assumption. - split; [assumption|]. destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. - eauto with mem. + destruct f; eauto with mem. exists v; auto. - auto. Qed. Lemma range_contains: - forall chunk b ofs P m, - m |= range b ofs (ofs + size_chunk chunk) ** P -> + forall {f} chunk b ofs P m, + m |= range' f b ofs (ofs + size_chunk chunk) ** P -> (align_chunk chunk | ofs) -> - m |= contains chunk b ofs (fun v => True) ** P. + m |= contains' f chunk b ofs (fun v => True) ** P. Proof. intros. rewrite range_contains' in H; assumption. Qed. Lemma contains_range': - forall chunk b ofs spec, - massert_imp (contains chunk b ofs spec) - (range b ofs (ofs + size_chunk chunk)). + forall {f} chunk b ofs spec, + massert_imp (contains' f chunk b ofs spec) + (range' f b ofs (ofs + size_chunk chunk)). Proof. intros. split. - intros. destruct H as (A & B & C & D). split; [|split]; try assumption. destruct C as (C1 & C2). - intros i k p Hr. + intros i k Hr. specialize (C1 _ Hr). eapply Mem.perm_cur in C1. apply Mem.perm_implies with (1:=C1). - apply perm_F_any. + destruct f; apply perm_refl. - trivial. Qed. Lemma contains_range: - forall chunk b ofs spec P m, - m |= contains chunk b ofs spec ** P -> - m |= range b ofs (ofs + size_chunk chunk) ** P. + forall {f} chunk b ofs spec P m, + m |= contains' f chunk b ofs spec ** P -> + m |= range' f b ofs (ofs + size_chunk chunk) ** P. Proof. intros. rewrite contains_range' in H; assumption. Qed. Lemma contains_imp: - forall (spec1 spec2: val -> Prop) chunk b ofs, + forall {f} (spec1 spec2: val -> Prop) chunk b ofs, (forall v, spec1 v -> spec2 v) -> - massert_imp (contains chunk b ofs spec1) (contains chunk b ofs spec2). + massert_imp (contains' f chunk b ofs spec1) (contains' f chunk b ofs spec2). Proof. intros; split; simpl; intros. - intuition auto. destruct H4 as (v & A & B). exists v; auto. - auto. Qed. -(** A memory area that contains a given value *) +(** A memory area that contains a given value. + The permissions on the underlying memory are either full (f = true) + or only writable (f = false). *) -Definition hasvalue (chunk: memory_chunk) (b: block) (ofs: Z) (v: val) : massert := - contains chunk b ofs (fun v' => v' = v). +Definition hasvalue' (f: bool) (chunk: memory_chunk) (b: block) (ofs: Z) (v: val) : massert := + contains' f chunk b ofs (fun v' => v' = v). + +Notation hasvalue := (hasvalue' true). +Notation hasvalue_w := (hasvalue' false). + +Lemma hasvalue_hasvalue_w: + forall chunk b ofs v, + massert_imp (hasvalue chunk b ofs v) (hasvalue_w chunk b ofs v). +Proof. + constructor; auto. + apply contains_contains_w. +Qed. Lemma store_rule': - forall chunk m b ofs v (spec1: val -> Prop) P, - m |= contains chunk b ofs spec1 ** P -> + forall {f} chunk m b ofs v (spec1: val -> Prop) P, + m |= contains' f chunk b ofs spec1 ** P -> exists m', - Mem.store chunk m b ofs v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P. + Mem.store chunk m b ofs v = Some m' /\ m' |= hasvalue' f chunk b ofs (Val.load_result chunk v) ** P. Proof. intros. eapply store_rule; eauto. Qed. Lemma storev_rule': - forall chunk m b ofs v (spec1: val -> Prop) P, - m |= contains chunk b ofs spec1 ** P -> + forall {f} chunk m b ofs v (spec1: val -> Prop) P, + m |= contains' f chunk b ofs spec1 ** P -> exists m', - Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P. + Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue' f chunk b ofs (Val.load_result chunk v) ** P. Proof. intros. eapply storev_rule; eauto. Qed. diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v index d375febf..96b0c8ef 100644 --- a/x86/Stacklayout.v +++ b/x86/Stacklayout.v @@ -58,7 +58,7 @@ Lemma frame_env_separated: ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. -Local Opaque Z.add Z.mul sepconj range. +Local Opaque Z.add Z.mul sepconj range'. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). -- cgit From 3c4877a41b9aca5e0dabfb308de56857f91a3e51 Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Thu, 9 Feb 2017 23:04:07 +0100 Subject: Streamline range weakening lemma --- common/Separation.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/common/Separation.v b/common/Separation.v index 1176edf5..288950f6 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -358,16 +358,16 @@ Qed. Notation range := (range' true). Notation range_w := (range' false). -Lemma range_range_w: - forall b lo hi, - massert_imp (range b lo hi) (range_w b lo hi). +Lemma range'_range_w: + forall {f} b lo hi, + massert_imp (range' f b lo hi) (range_w b lo hi). Proof. constructor; auto. destruct 1 as (Hlo & Hhi & Hperm). repeat split; auto. intros i k Hoff. - eapply Mem.perm_implies; eauto using perm_F_any. -Qed. + destruct f; eapply Mem.perm_implies; eauto using perm_F_any, perm_refl. +Qed. Lemma alloc_rule: forall m lo hi b m' P, @@ -526,14 +526,14 @@ Qed. Notation contains := (contains' true). Notation contains_w := (contains' false). -Lemma contains_contains_w: - forall chunk b ofs spec, - massert_imp (contains chunk b ofs spec) (contains_w chunk b ofs spec). +Lemma contains'_contains_w: + forall {f} chunk b ofs spec, + massert_imp (contains' f chunk b ofs spec) (contains_w chunk b ofs spec). Proof. constructor; auto. inversion 1 as (Hlo & Hhi & Hac & v & Hload & Hspec). eapply Mem.valid_access_implies with (p2:=Writable) in Hac; - auto using perm_F_any. + destruct f; auto using perm_F_any, perm_refl. repeat (split; eauto). Qed. @@ -687,12 +687,12 @@ Definition hasvalue' (f: bool) (chunk: memory_chunk) (b: block) (ofs: Z) (v: val Notation hasvalue := (hasvalue' true). Notation hasvalue_w := (hasvalue' false). -Lemma hasvalue_hasvalue_w: - forall chunk b ofs v, - massert_imp (hasvalue chunk b ofs v) (hasvalue_w chunk b ofs v). +Lemma hasvalue'_hasvalue_w: + forall {f} chunk b ofs v, + massert_imp (hasvalue' f chunk b ofs v) (hasvalue_w chunk b ofs v). Proof. constructor; auto. - apply contains_contains_w. + apply contains'_contains_w. Qed. Lemma store_rule': -- cgit From d6ec1e0242ce492d3aa564116d50241417086ce5 Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Fri, 10 Feb 2017 06:50:21 +0100 Subject: Generalize definition of range --- backend/Stackingproof.v | 2 +- common/Separation.v | 211 ++++++++++++++++++++++++------------------------ 2 files changed, 108 insertions(+), 105 deletions(-) diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index ffd9b227..79ef016a 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -936,7 +936,7 @@ Local Opaque mreg_type. apply range_drop_left with (mid := pos1) in SEP; [ | omega ]. apply range_split with (mid := pos1 + sz) in SEP; [ | omega ]. unfold sz at 1 in SEP. rewrite <- size_type_chunk in SEP. - apply range_contains in SEP; auto. + apply range_contains in SEP; auto with mem. exploit (contains_set_stack (fun v' => Val.inject j (ls (R r)) v') (rs r)). eexact SEP. apply load_result_inject; auto. apply wt_ls. diff --git a/common/Separation.v b/common/Separation.v index 288950f6..0f40e65b 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -338,14 +338,12 @@ Proof. simpl; intros. intuition auto. Qed. -(** A range of bytes with unspecified contents, and either full permissions - (f = true) or only writable permissions (f = false). *) +(** A range of bytes with given permissions unspecified contents *) -Program Definition range' (f: bool) (b: block) (lo hi: Z) : massert := {| +Program Definition range' (p: permission) (b: block) (lo hi: Z) : massert := {| m_pred := fun m => 0 <= lo /\ hi <= Ptrofs.modulus - /\ (forall i k, lo <= i < hi -> Mem.perm m b i k - (if f then Freeable else Writable)); + /\ (forall i k, lo <= i < hi -> Mem.perm m b i k p); m_footprint := fun b' ofs' => b' = b /\ lo <= ofs' < hi |}. Next Obligation. @@ -355,18 +353,19 @@ Next Obligation. eapply Mem.perm_valid_block with ofs Cur _; auto. Qed. -Notation range := (range' true). -Notation range_w := (range' false). +Notation range := (range' Freeable). +Notation range_w := (range' Writable). -Lemma range'_range_w: - forall {f} b lo hi, - massert_imp (range' f b lo hi) (range_w b lo hi). +Lemma range'_imp: + forall p p' b lo hi, + perm_order p p' -> + massert_imp (range' p b lo hi) (range' p' b lo hi). Proof. constructor; auto. destruct 1 as (Hlo & Hhi & Hperm). repeat split; auto. intros i k Hoff. - destruct f; eapply Mem.perm_implies; eauto using perm_F_any, perm_refl. + eapply Mem.perm_implies; eauto. Qed. Lemma alloc_rule: @@ -407,10 +406,10 @@ Proof. Qed. Lemma range_split': - forall {f} b lo hi mid, + forall p b lo hi mid, lo <= mid <= hi -> - massert_eqv (range' f b lo hi) - (range' f b lo mid ** range' f b mid hi). + massert_eqv (range' p b lo hi) + (range' p b lo mid ** range' p b mid hi). Proof. intros * HR. constructor; constructor. @@ -439,10 +438,10 @@ Proof. Qed. Lemma range_split: - forall {f} b lo hi P mid m, + forall p b lo hi P mid m, lo <= mid <= hi -> - m |= range' f b lo hi ** P -> - m |= range' f b lo mid ** range' f b mid hi ** P. + m |= range' p b lo hi ** P -> + m |= range' p b lo mid ** range' p b mid hi ** P. Proof. intros. rewrite <- sep_assoc. eapply sep_imp; eauto. split; simpl; intros. @@ -456,29 +455,29 @@ Proof. Qed. Lemma range_drop_left: - forall {f} b lo hi P mid m, + forall p b lo hi P mid m, lo <= mid <= hi -> - m |= range' f b lo hi ** P -> - m |= range' f b mid hi ** P. + m |= range' p b lo hi ** P -> + m |= range' p b mid hi ** P. Proof. - intros. apply sep_drop with (range' f b lo mid). apply range_split; auto. + intros. apply sep_drop with (range' p b lo mid). apply range_split; auto. Qed. Lemma range_drop_right: - forall {f} b lo hi P mid m, + forall p b lo hi P mid m, lo <= mid <= hi -> - m |= range' f b lo hi ** P -> - m |= range' f b lo mid ** P. + m |= range' p b lo hi ** P -> + m |= range' p b lo mid ** P. Proof. - intros. apply sep_drop2 with (range' f b mid hi). apply range_split; auto. + intros. apply sep_drop2 with (range' p b mid hi). apply range_split; auto. Qed. Lemma range_split_2: - forall {f} b lo hi P mid al m, + forall p b lo hi P mid al m, lo <= align mid al <= hi -> al > 0 -> - m |= range' f b lo hi ** P -> - m |= range' f b lo mid ** range' f b (align mid al) hi ** P. + m |= range' p b lo hi ** P -> + m |= range' p b lo mid ** range' p b (align mid al) hi ** P. Proof. intros. rewrite <- sep_assoc. eapply sep_imp; eauto. assert (mid <= align mid al) by (apply align_le; auto). @@ -493,22 +492,20 @@ Proof. Qed. Lemma range_preserved: - forall {f} m m' b lo hi, - m |= range' f b lo hi -> + forall p m m' b lo hi, + m |= range' p b lo hi -> (forall i k p, lo <= i < hi -> Mem.perm m b i k p -> Mem.perm m' b i k p) -> - m' |= range' f b lo hi. + m' |= range' p b lo hi. Proof. intros. destruct H as (A & B & C). simpl; intuition auto. Qed. -(** A memory area that contains a value satisfying a given predicate. - The permissions on the memory are either full (f = true) or only - writable (f = false). *) +(** A memory area that contains a value satisfying a given predicate. *) -Program Definition contains' (f: bool) (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {| +Program Definition contains' (p: permission) (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {| m_pred := fun m => 0 <= ofs /\ ofs + size_chunk chunk <= Ptrofs.modulus - /\ Mem.valid_access m chunk b ofs (if f then Freeable else Writable) + /\ Mem.valid_access m chunk b ofs p /\ exists v, Mem.load chunk m b ofs = Some v /\ spec v; m_footprint := fun b' ofs' => b' = b /\ ofs <= ofs' < ofs + size_chunk chunk |}. @@ -523,23 +520,23 @@ Next Obligation. eauto with mem. Qed. -Notation contains := (contains' true). -Notation contains_w := (contains' false). +Notation contains := (contains' Freeable). +Notation contains_w := (contains' Writable). -Lemma contains'_contains_w: - forall {f} chunk b ofs spec, - massert_imp (contains' f chunk b ofs spec) (contains_w chunk b ofs spec). +Lemma contains'_imp: + forall p p' chunk b ofs spec, + perm_order p p' -> + massert_imp (contains' p chunk b ofs spec) (contains' p' chunk b ofs spec). Proof. constructor; auto. inversion 1 as (Hlo & Hhi & Hac & v & Hload & Hspec). - eapply Mem.valid_access_implies with (p2:=Writable) in Hac; - destruct f; auto using perm_F_any, perm_refl. + eapply Mem.valid_access_implies in Hac; eauto. repeat (split; eauto). Qed. Lemma contains_no_overflow: - forall {f} spec m chunk b ofs, - m |= contains' f chunk b ofs spec -> + forall p spec m chunk b ofs, + m |= contains' p chunk b ofs spec -> 0 <= ofs <= Ptrofs.max_unsigned. Proof. intros. simpl in H. @@ -550,32 +547,35 @@ Proof. Qed. Lemma load_rule: - forall {f} spec m chunk b ofs, - m |= contains' f chunk b ofs spec -> + forall p spec m chunk b ofs, + perm_order p Readable -> + m |= contains' p chunk b ofs spec -> exists v, Mem.load chunk m b ofs = Some v /\ spec v. Proof. - intros. destruct H as (D & E & F & v & G & H). + intros * Hp Hc. destruct Hc as (D & E & F & v & G & H). exists v; auto. Qed. Lemma loadv_rule: - forall {f} spec m chunk b ofs, - m |= contains' f chunk b ofs spec -> + forall p spec m chunk b ofs, + perm_order p Readable -> + m |= contains' p chunk b ofs spec -> exists v, Mem.loadv chunk m (Vptr b (Ptrofs.repr ofs)) = Some v /\ spec v. Proof. - intros. exploit (@load_rule f); eauto. intros (v & A & B). exists v; split; auto. + intros. exploit load_rule; eauto with mem. intros (v & A & B). exists v; split; auto. simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow; eauto. Qed. Lemma store_rule: - forall {f} chunk m b ofs v (spec1 spec: val -> Prop) P, - m |= contains' f chunk b ofs spec1 ** P -> + forall p chunk m b ofs v (spec1 spec: val -> Prop) P, + perm_order p Writable -> + m |= contains' p chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> exists m', - Mem.store chunk m b ofs v = Some m' /\ m' |= contains' f chunk b ofs spec ** P. + Mem.store chunk m b ofs v = Some m' /\ m' |= contains' p chunk b ofs spec ** P. Proof. - intros. destruct H as (A & B & C). destruct A as (D & E & v0 & F & G). - assert (H: Mem.valid_access m chunk b ofs Writable) by (destruct f; eauto with mem). + intros * Hp Hc Hs. destruct Hc as (A & B & C). destruct A as (D & E & v0 & F & G). + assert (H: Mem.valid_access m chunk b ofs Writable) by eauto with mem. destruct (Mem.valid_access_store _ _ _ _ v H) as [m' STORE]. exists m'; split; auto. simpl. intuition auto. - eapply Mem.store_valid_access_1; eauto. @@ -586,64 +586,68 @@ Proof. Qed. Lemma storev_rule: - forall {f} chunk m b ofs v (spec1 spec: val -> Prop) P, - m |= contains' f chunk b ofs spec1 ** P -> + forall p chunk m b ofs v (spec1 spec: val -> Prop) P, + perm_order p Writable -> + m |= contains' p chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> exists m', - Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains' f chunk b ofs spec ** P. + Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains' p chunk b ofs spec ** P. Proof. - intros. exploit (@store_rule f); eauto. intros (m' & A & B). exists m'; split; auto. + intros. exploit store_rule; eauto. intros (m' & A & B). exists m'; split; auto. simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto. Qed. Lemma storev_rule2: - forall {f} chunk m m' b ofs v (spec1 spec: val -> Prop) P, - m |= contains' f chunk b ofs spec1 ** P -> + forall p chunk m m' b ofs v (spec1 spec: val -> Prop) P, + perm_order p Writable -> + m |= contains' p chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> Memory.Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' -> - m' |= contains' f chunk b ofs spec ** P. + m' |= contains' p chunk b ofs spec ** P. Proof. - intros * Hm Hspec Hstore. - apply storev_rule with (1:=Hm) in Hspec. + intros * Hp Hm Hspec Hstore. + eapply storev_rule with (2:=Hm) in Hspec; eauto. destruct Hspec as [m'' [Hmem Hspec]]. rewrite Hmem in Hstore. injection Hstore. intro; subst. assumption. Qed. Lemma range_contains': - forall {f} chunk b ofs, + forall p chunk b ofs, + perm_order p Readable -> (align_chunk chunk | ofs) -> - massert_imp (range' f b ofs (ofs + size_chunk chunk)) - (contains' f chunk b ofs (fun v => True)). + massert_imp (range' p b ofs (ofs + size_chunk chunk)) + (contains' p chunk b ofs (fun v => True)). Proof. intros. constructor. - intros. destruct H0 as (D & E & F). - assert (Mem.valid_access m chunk b ofs (if f then Freeable else Writable)). + intros * Hr. destruct Hr as (D & E & F). + assert (Mem.valid_access m chunk b ofs p). { split; auto. red; auto. } split; [|split]. - generalize (size_chunk_pos chunk). omega. - assumption. - split; [assumption|]. destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. - destruct f; eauto with mem. + eauto with mem. exists v; auto. - auto. Qed. Lemma range_contains: - forall {f} chunk b ofs P m, - m |= range' f b ofs (ofs + size_chunk chunk) ** P -> + forall p chunk b ofs P m, + perm_order p Readable -> + m |= range' p b ofs (ofs + size_chunk chunk) ** P -> (align_chunk chunk | ofs) -> - m |= contains' f chunk b ofs (fun v => True) ** P. + m |= contains' p chunk b ofs (fun v => True) ** P. Proof. - intros. - rewrite range_contains' in H; assumption. + intros * Hp Hr Hc. + rewrite range_contains' in Hr; assumption. Qed. Lemma contains_range': - forall {f} chunk b ofs spec, - massert_imp (contains' f chunk b ofs spec) - (range' f b ofs (ofs + size_chunk chunk)). + forall p chunk b ofs spec, + massert_imp (contains' p chunk b ofs spec) + (range' p b ofs (ofs + size_chunk chunk)). Proof. intros. split. @@ -652,63 +656,62 @@ Proof. destruct C as (C1 & C2). intros i k Hr. specialize (C1 _ Hr). - eapply Mem.perm_cur in C1. - apply Mem.perm_implies with (1:=C1). - destruct f; apply perm_refl. + eauto with mem. - trivial. Qed. Lemma contains_range: - forall {f} chunk b ofs spec P m, - m |= contains' f chunk b ofs spec ** P -> - m |= range' f b ofs (ofs + size_chunk chunk) ** P. + forall p chunk b ofs spec P m, + m |= contains' p chunk b ofs spec ** P -> + m |= range' p b ofs (ofs + size_chunk chunk) ** P. Proof. intros. rewrite contains_range' in H; assumption. Qed. Lemma contains_imp: - forall {f} (spec1 spec2: val -> Prop) chunk b ofs, + forall p (spec1 spec2: val -> Prop) chunk b ofs, (forall v, spec1 v -> spec2 v) -> - massert_imp (contains' f chunk b ofs spec1) (contains' f chunk b ofs spec2). + massert_imp (contains' p chunk b ofs spec1) (contains' p chunk b ofs spec2). Proof. intros; split; simpl; intros. - intuition auto. destruct H4 as (v & A & B). exists v; auto. - auto. Qed. -(** A memory area that contains a given value. - The permissions on the underlying memory are either full (f = true) - or only writable (f = false). *) +(** A memory area that contains a given value. *) -Definition hasvalue' (f: bool) (chunk: memory_chunk) (b: block) (ofs: Z) (v: val) : massert := - contains' f chunk b ofs (fun v' => v' = v). +Definition hasvalue' (p: permission) (chunk: memory_chunk) (b: block) (ofs: Z) (v: val) : massert := + contains' p chunk b ofs (fun v' => v' = v). -Notation hasvalue := (hasvalue' true). -Notation hasvalue_w := (hasvalue' false). +Notation hasvalue := (hasvalue' Freeable). +Notation hasvalue_w := (hasvalue' Writable). -Lemma hasvalue'_hasvalue_w: - forall {f} chunk b ofs v, - massert_imp (hasvalue' f chunk b ofs v) (hasvalue_w chunk b ofs v). +Lemma hasvalue'_imp: + forall p p' chunk b ofs v, + perm_order p p' -> + massert_imp (hasvalue' p chunk b ofs v) (hasvalue' p' chunk b ofs v). Proof. constructor; auto. - apply contains'_contains_w. + now apply contains'_imp. Qed. Lemma store_rule': - forall {f} chunk m b ofs v (spec1: val -> Prop) P, - m |= contains' f chunk b ofs spec1 ** P -> + forall p chunk m b ofs v (spec1: val -> Prop) P, + perm_order p Writable -> + m |= contains' p chunk b ofs spec1 ** P -> exists m', - Mem.store chunk m b ofs v = Some m' /\ m' |= hasvalue' f chunk b ofs (Val.load_result chunk v) ** P. + Mem.store chunk m b ofs v = Some m' /\ m' |= hasvalue' p chunk b ofs (Val.load_result chunk v) ** P. Proof. intros. eapply store_rule; eauto. Qed. Lemma storev_rule': - forall {f} chunk m b ofs v (spec1: val -> Prop) P, - m |= contains' f chunk b ofs spec1 ** P -> + forall p chunk m b ofs v (spec1: val -> Prop) P, + perm_order p Writable -> + m |= contains' p chunk b ofs spec1 ** P -> exists m', - Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue' f chunk b ofs (Val.load_result chunk v) ** P. + Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue' p chunk b ofs (Val.load_result chunk v) ** P. Proof. intros. eapply storev_rule; eauto. Qed. -- cgit From 4f6dcb643f804fb9736b65ce58b6e0ddc1a0ca1a Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Fri, 10 Feb 2017 21:24:48 +0100 Subject: Fix out-of-date comment about function allocs --- common/Globalenvs.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/common/Globalenvs.v b/common/Globalenvs.v index d37fbd46..462a4ec1 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -22,10 +22,8 @@ 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. + 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. -- cgit From d87ea150694745a1efee967285ee68845ac66f05 Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Sun, 12 Feb 2017 21:46:35 +0100 Subject: Rewrites in disjoint_footprint --- common/Separation.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/common/Separation.v b/common/Separation.v index 0f40e65b..0aebb3c7 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -160,6 +160,21 @@ Proof. - intuition auto. Qed. +Add Morphism disjoint_footprint + with signature massert_eqv ==> massert_eqv ==> iff + as disjoint_footprint_morph_1. +Proof. + intros p q Hpq r s Hrs. + unfold disjoint_footprint. + split; intro HH; intros b ofs Hf1 Hf2. + - rewrite <-Hpq in Hf1. + rewrite <-Hrs in Hf2. + now specialize (HH _ _ Hf1 Hf2). + - rewrite Hpq in Hf1. + rewrite Hrs in Hf2. + now specialize (HH _ _ Hf1 Hf2). +Qed. + Add Morphism sepconj with signature massert_eqv ==> massert_eqv ==> massert_eqv as sepconj_morph_2. -- cgit From a3cf22317821f9f32e632344d51834a9a1524701 Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Wed, 5 Apr 2017 15:02:50 +0200 Subject: Fix other stacking proofs for range' --- arm/Stacklayout.v | 2 +- powerpc/Stacklayout.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v index 462d83ad..8e91f14b 100644 --- a/arm/Stacklayout.v +++ b/arm/Stacklayout.v @@ -64,7 +64,7 @@ Lemma frame_env_separated: ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. -Local Opaque Z.add Z.mul sepconj range. +Local Opaque Z.add Z.mul sepconj range'. intros; simpl. set (olink := 4 * b.(bound_outgoing)); set (ora := olink + 4); diff --git a/powerpc/Stacklayout.v b/powerpc/Stacklayout.v index cb3806bd..d5539b70 100644 --- a/powerpc/Stacklayout.v +++ b/powerpc/Stacklayout.v @@ -68,7 +68,7 @@ Lemma frame_env_separated: ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. -Local Opaque Z.add Z.mul sepconj range. +Local Opaque Z.add Z.mul sepconj range'. intros; simpl. set (ol := align (8 + 4 * b.(bound_outgoing)) 8). set (ora := ol + 4 * b.(bound_local)). -- cgit From f8da0614e106a324fa6646213db68f2045070af4 Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Sat, 20 Apr 2019 19:27:50 +0200 Subject: Fix rebase of Stackingproof/elab_char_constant --- backend/Stackingproof.v | 8 ++++---- common/Separation.v | 2 +- cparser/Elab.mli | 6 +----- 3 files changed, 6 insertions(+), 10 deletions(-) diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 79ef016a..d8b81689 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -149,7 +149,7 @@ Lemma contains_get_stack: Proof. intros. unfold load_stack. replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)). - eapply loadv_rule; eauto. + eapply loadv_rule; eauto using perm_F_any. simpl. rewrite Ptrofs.add_zero_l; auto. Qed. @@ -171,7 +171,7 @@ Lemma contains_set_stack: Proof. intros. unfold store_stack. replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)). - eapply storev_rule; eauto. + eapply storev_rule; eauto using perm_F_any. simpl. rewrite Ptrofs.add_zero_l; auto. Qed. @@ -1087,14 +1087,14 @@ Local Opaque b fe. apply (frame_env_separated b) in SEP. replace (make_env b) with fe in SEP by auto. (* Store of parent *) rewrite sep_swap3 in SEP. - apply (range_contains Mptr) in SEP; [|tauto]. + apply range_contains in SEP;[|apply perm_F_any|tauto]. exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tptr). rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto. clear SEP; intros (m3' & STORE_PARENT & SEP). rewrite sep_swap3 in SEP. (* Store of return address *) rewrite sep_swap4 in SEP. - apply (range_contains Mptr) in SEP; [|tauto]. + apply range_contains in SEP; [|apply perm_F_any|tauto]. exploit (contains_set_stack (fun v' => v' = ra) ra (fun _ => True) m3' Tptr). rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto. clear SEP; intros (m4' & STORE_RETADDR & SEP). diff --git a/common/Separation.v b/common/Separation.v index 0aebb3c7..2804fd73 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -29,7 +29,7 @@ frame rule; instead, a weak form of the frame rule is provided by the lemmas that help us reason about the logical assertions. *) -Require Import Setoid Program.Basics. +Require Import Setoid Morphisms Program.Basics. Require Import Coqlib Decidableplus. Require Import AST Integers Values Memory Events Globalenvs. diff --git a/cparser/Elab.mli b/cparser/Elab.mli index 31d9b281..68e33d06 100644 --- a/cparser/Elab.mli +++ b/cparser/Elab.mli @@ -13,10 +13,6 @@ (* *) (* *********************************************************************) -val elab_int_constant : Cabs.cabsloc -> string -> int64 * C.ikind -val elab_float_constant : Cabs.floatInfo -> C.float_cst * C.fkind -val elab_char_constant : Cabs.cabsloc -> bool -> int64 list -> int64 * C.ikind - val elab_file : Cabs.definition list -> C.program (* This is the main entry point. It transforms a list of toplevel definitions as produced by the parser into a program in C abstract @@ -24,6 +20,6 @@ val elab_file : Cabs.definition list -> C.program val elab_int_constant : Cabs.loc -> string -> int64 * C.ikind val elab_float_constant : Cabs.floatInfo -> C.float_cst * C.fkind -val elab_char_constant : Cabs.loc -> bool -> int64 list -> int64 +val elab_char_constant : Cabs.loc -> bool -> int64 list -> int64 * C.ikind (* These auxiliary functions are exported so that they can be reused in other projects that deal with C-style source languages. *) -- cgit From 4bda31427187fce0468004738a214830191ccda5 Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Tue, 5 Jul 2016 13:26:42 +0200 Subject: More rewriting for Separation --- common/Separation.v | 48 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 34 insertions(+), 14 deletions(-) diff --git a/common/Separation.v b/common/Separation.v index 2804fd73..9aee633f 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -113,6 +113,18 @@ Proof. intros P Q [[A B] [C D]]. split; auto. Qed. +Instance massert_imp_eqv_Proper: + Proper (massert_eqv ==> massert_eqv ==> iff) massert_imp. +Proof. + intros p q Hpq r s Hrs. + split; destruct 1 as [HR1 HR2]; + constructor; intros; + apply Hrs || apply Hpq; + apply HR1 || apply HR2; + apply Hpq || apply Hrs; + assumption. +Qed. + Hint Resolve massert_imp_refl massert_eqv_refl : core. Instance footprint_massert_imp_Proper: @@ -193,6 +205,15 @@ Proof. intros. rewrite <- H0, <- H1; auto. Qed. +Lemma sep_imp': + forall P P' Q Q', + massert_imp P P' -> + massert_imp Q Q' -> + massert_imp (P ** Q) (P' ** Q'). +Proof. + intros * HP HQ. rewrite HP, HQ. reflexivity. +Qed. + Lemma sep_comm_1: forall P Q, massert_imp (P ** Q) (Q ** P). Proof. @@ -272,15 +293,17 @@ Proof. Qed. Lemma sep_drop: - forall P Q m, m |= P ** Q -> m |= Q. + forall P Q, massert_imp (P ** Q) Q. Proof. - simpl; intros. tauto. + constructor. + - simpl; intros. tauto. + - intros. now constructor 2. Qed. Lemma sep_drop2: - forall P Q R m, m |= P ** Q ** R -> m |= P ** R. + forall P Q R, massert_imp (P ** Q ** R) (P ** R). Proof. - intros. rewrite sep_swap in H. eapply sep_drop; eauto. + intros. rewrite sep_swap, sep_drop. reflexivity. Qed. Lemma sep_proj1: @@ -291,7 +314,9 @@ Qed. Lemma sep_proj2: forall P Q m, m |= P ** Q -> m |= Q. -Proof sep_drop. +Proof. + apply sep_drop. +Qed. Definition sep_pick1 := sep_proj1. @@ -458,15 +483,10 @@ Lemma range_split: m |= range' p b lo hi ** P -> m |= range' p b lo mid ** range' p b mid hi ** P. Proof. - intros. rewrite <- sep_assoc. eapply sep_imp; eauto. - split; simpl; intros. -- intuition auto. -+ omega. -+ apply H5; omega. -+ omega. -+ apply H5; omega. -+ red; simpl; intros; omega. -- intuition omega. + intros. + rewrite <-sep_assoc. + rewrite range_split' with (1:=H) in H0. + assumption. Qed. Lemma range_drop_left: -- cgit From c9e4b66c10f7abd432c47c3cb2a9579a814b4395 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jul 2020 20:44:24 +0200 Subject: applied the Velus patch --- backend/Stackingproof.v | 1 + kvx/Stacklayout.v | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1ede0194..49d2956e 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -139,6 +139,7 @@ Qed. (** * Memory assertions used to describe the contents of stack frames *) Local Opaque Z.add Z.mul Z.divide. +Local Hint Immediate perm_F_any : core. (** Accessing the stack frame using [load_stack] and [store_stack]. *) diff --git a/kvx/Stacklayout.v b/kvx/Stacklayout.v index 46202e03..740c0cf2 100644 --- a/kvx/Stacklayout.v +++ b/kvx/Stacklayout.v @@ -62,7 +62,7 @@ Lemma frame_env_separated: ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. -Local Opaque Z.add Z.mul sepconj range. +Local Opaque Z.add Z.mul sepconj range'. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). -- cgit From 44f346554115278ec9409bdcb9bc8ee32f4017db Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jul 2020 22:35:10 +0200 Subject: rm 'range' causing compilation to end --- aarch64/Stacklayout.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/aarch64/Stacklayout.v b/aarch64/Stacklayout.v index 86ba9f45..e23fc0da 100644 --- a/aarch64/Stacklayout.v +++ b/aarch64/Stacklayout.v @@ -58,7 +58,7 @@ Lemma frame_env_separated: ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. -Local Opaque Z.add Z.mul sepconj range. + Local Opaque Z.add Z.mul sepconj. intros; simpl. set (olink := align (4 * b.(bound_outgoing)) 8). set (oretaddr := olink + 8). -- cgit From f0de7ba427c47b8274d9b748a72c468ef32cec38 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jul 2020 22:52:13 +0200 Subject: fix stacklayout for velus --- riscV/Stacklayout.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/riscV/Stacklayout.v b/riscV/Stacklayout.v index d0c6a526..369cda2b 100644 --- a/riscV/Stacklayout.v +++ b/riscV/Stacklayout.v @@ -59,7 +59,7 @@ Lemma frame_env_separated: ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. -Local Opaque Z.add Z.mul sepconj range. +Local Opaque Z.add Z.mul sepconj. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). -- cgit From 0776c3f64d3751d64f41500c78b7a5142c068ce9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 29 Jul 2020 10:10:23 +0200 Subject: keep Velus happy --- aarch64/Machregsaux.mli | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 aarch64/Machregsaux.mli diff --git a/aarch64/Machregsaux.mli b/aarch64/Machregsaux.mli new file mode 100644 index 00000000..d7117c21 --- /dev/null +++ b/aarch64/Machregsaux.mli @@ -0,0 +1,20 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Auxiliary functions on machine registers *) + +val name_of_register: Machregs.mreg -> string option +val register_by_name: string -> Machregs.mreg option +val is_scratch_register: string -> bool +val can_reserve_register: Machregs.mreg -> bool + +val class_of_type: AST.typ -> int -- cgit From 10a4ea3a510a51ca815729110cce13a781e87d34 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 19 Apr 2021 19:28:39 +0200 Subject: disable builds that don't work --- .gitlab-ci.yml | 168 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 84 insertions(+), 84 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7f992502..e4a0c84f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -87,94 +87,94 @@ build_aarch64: when: always - when: manual -build_arm: - stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda - before_script: - - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - - sudo apt-get -y install gcc-arm-linux-gnueabi qemu-user - - eval `opam config env` - - opam update - - opam install -y menhir - script: - - ./config_arm.sh - - make -j "$NJOBS" - - make -C test CCOMPOPTS=-static SIMU='qemu-arm' EXECUTE='qemu-arm' all test - - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabi-gcc' EXECUTE='qemu-arm' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32 - rules: - - if: '$CI_COMMIT_BRANCH == "kvx-work"' - when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' - when: always - - if: '$CI_COMMIT_BRANCH == "master"' - when: always - - when: manual +# build_arm: +# stage: build +# image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda +# before_script: +# - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update +# - sudo apt-get -y install gcc-arm-linux-gnueabi qemu-user +# - eval `opam config env` +# - opam update +# - opam install -y menhir +# script: +# - ./config_arm.sh +# - make -j "$NJOBS" +# - make -C test CCOMPOPTS=-static SIMU='qemu-arm' EXECUTE='qemu-arm' all test +# - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabi-gcc' EXECUTE='qemu-arm' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32 +# rules: +# - if: '$CI_COMMIT_BRANCH == "kvx-work"' +# when: always +# - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' +# when: always +# - if: '$CI_COMMIT_BRANCH == "master"' +# when: always +# - when: manual -build_armhf: - stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda - before_script: - - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - - sudo apt-get -y install gcc-arm-linux-gnueabihf qemu-user - - eval `opam config env` - - opam update - - opam install -y menhir - script: - - ./config_armhf.sh - - make -j "$NJOBS" - - make -C test CCOMPOPTS=-static SIMU='qemu-arm' EXECUTE='qemu-arm' all test - - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabihf-gcc' EXECUTE='qemu-arm' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32 - rules: - - if: '$CI_COMMIT_BRANCH == "kvx-work"' - when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' - when: always - - if: '$CI_COMMIT_BRANCH == "master"' - when: always - - when: manual +# build_armhf: +# stage: build +# image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda +# before_script: +# - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update +# - sudo apt-get -y install gcc-arm-linux-gnueabihf qemu-user +# - eval `opam config env` +# - opam update +# - opam install -y menhir +# script: +# - ./config_armhf.sh +# - make -j "$NJOBS" +# - make -C test CCOMPOPTS=-static SIMU='qemu-arm' EXECUTE='qemu-arm' all test +# - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabihf-gcc' EXECUTE='qemu-arm' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32 +# rules: +# - if: '$CI_COMMIT_BRANCH == "kvx-work"' +# when: always +# - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' +# when: always +# - if: '$CI_COMMIT_BRANCH == "master"' +# when: always +# - when: manual -build_ppc: - stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda - before_script: - - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - - sudo apt-get -y install gcc-powerpc-linux-gnu qemu-user - - eval `opam config env` - - opam update - - opam install -y menhir - script: - - ./config_ppc.sh - - make -j "$NJOBS" - rules: - - if: '$CI_COMMIT_BRANCH == "kvx-work"' - when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' - when: always - - if: '$CI_COMMIT_BRANCH == "master"' - when: always - - when: manual +# build_ppc: +# stage: build +# image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda +# before_script: +# - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update +# - sudo apt-get -y install gcc-powerpc-linux-gnu qemu-user +# - eval `opam config env` +# - opam update +# - opam install -y menhir +# script: +# - ./config_ppc.sh +# - make -j "$NJOBS" +# rules: +# - if: '$CI_COMMIT_BRANCH == "kvx-work"' +# when: always +# - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' +# when: always +# - if: '$CI_COMMIT_BRANCH == "master"' +# when: always +# - when: manual -build_ppc64: - stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda - before_script: - - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - - sudo apt-get -y install gcc-powerpc64-linux-gnu - - eval `opam config env` - - opam update - - opam install -y menhir - script: - - ./config_ppc64.sh - - make -j "$NJOBS" - rules: - - if: '$CI_COMMIT_BRANCH == "kvx-work"' - when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' - when: always - - if: '$CI_COMMIT_BRANCH == "master"' - when: always - - when: manual +# build_ppc64: +# stage: build +# image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda +# before_script: +# - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update +# - sudo apt-get -y install gcc-powerpc64-linux-gnu +# - eval `opam config env` +# - opam update +# - opam install -y menhir +# script: +# - ./config_ppc64.sh +# - make -j "$NJOBS" +# rules: +# - if: '$CI_COMMIT_BRANCH == "kvx-work"' +# when: always +# - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' +# when: always +# - if: '$CI_COMMIT_BRANCH == "master"' +# when: always +# - when: manual build_rv64: stage: build -- cgit