diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cminorgen.v | 6 | ||||
-rw-r--r-- | cfrontend/Cminorgenproof.v | 28 | ||||
-rw-r--r-- | cfrontend/Csem.v | 4 | ||||
-rw-r--r-- | cfrontend/Csharpminor.v | 4 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof3.v | 24 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 6 |
6 files changed, 40 insertions, 32 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 4ed4bc8e..e60de3de 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -599,10 +599,10 @@ Definition build_compilenv (globenv, 0). Definition assign_global_variable - (ce: compilenv) (info: ident * list init_data * var_kind) : compilenv := + (ce: compilenv) (info: ident * globvar var_kind) : compilenv := match info with - | (id, _, Vscalar chunk) => PMap.set id (Var_global_scalar chunk) ce - | (id, _, Varray _) => PMap.set id Var_global_array ce + | (id, mkglobvar (Vscalar chunk) _ _ _ ) => PMap.set id (Var_global_scalar chunk) ce + | (id, mkglobvar (Varray _) _ _ _) => PMap.set id Var_global_array ce end. Definition build_global_compilenv (p: Csharpminor.program) : compilenv := diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 9f572edb..bb7d95a8 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -94,9 +94,9 @@ Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop := Lemma global_compilenv_charact: global_compilenv_match gce gvare. Proof. - set (mkgve := fun gv (vars: list (ident * list init_data * var_kind)) => + set (mkgve := fun gv (vars: list (ident * globvar var_kind)) => List.fold_left - (fun gve x => match x with (id, init, k) => PTree.set id k gve end) + (fun gve x => match x with (id, v) => PTree.set id v.(gvar_info) gve end) vars gv). assert (forall vars gv ce, global_compilenv_match ce gv -> @@ -105,7 +105,7 @@ Proof. induction vars; simpl; intros. auto. apply IHvars. intro id1. unfold assign_global_variable. - destruct a as [[id2 init2] lv2]. destruct lv2; simpl; rewrite PMap.gsspec; rewrite PTree.gsspec. + destruct a as [id2 lv2]. destruct lv2. destruct gvar_info; simpl; rewrite PMap.gsspec; rewrite PTree.gsspec. case (peq id1 id2); intro. auto. apply H. case (peq id1 id2); intro. auto. apply H. @@ -799,7 +799,8 @@ Inductive match_globalenvs (f: meminj) (bound: Z): Prop := (POS: bound > 0) (DOMAIN: forall b, b < bound -> f b = Some(b, 0)) (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) - (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound). + (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound) + (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). (** Matching of call stacks imply: - matching of environments for each of the frames @@ -1250,22 +1251,23 @@ Qed. Remark external_call_nextblock_incr: forall ef vargs m1 t vres m2, - external_call ef (Genv.find_symbol ge) vargs m1 t vres m2 -> + external_call ef ge vargs m1 t vres m2 -> Mem.nextblock m1 <= Mem.nextblock m2. Proof. intros. - generalize (external_call_valid_block _ _ _ _ _ _ _ (Mem.nextblock m1 - 1) H). + generalize (@external_call_valid_block _ _ _ _ _ _ _ _ _ (Mem.nextblock m1 - 1) H). unfold Mem.valid_block. omega. Qed. Remark inj_preserves_globals: forall f hi, match_globalenvs f hi -> - meminj_preserves_globals (Genv.find_symbol ge) f. + meminj_preserves_globals ge f. Proof. - intros. inv H. split; intros. - apply DOMAIN. eapply SYMBOLS. eauto. - symmetry. eapply IMAGE; eauto. + intros. inv H. + split. intros. apply DOMAIN. eapply SYMBOLS. eauto. + split. intros. apply DOMAIN. eapply INFOS. eauto. + intros. symmetry. eapply IMAGE; eauto. Qed. (** * Soundness of chunk and type inference. *) @@ -3176,7 +3178,10 @@ Proof. intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]]. left; econstructor; split. apply plus_one. econstructor. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + eapply external_call_symbols_preserved_2; eauto. + exact symbols_preserved. + eexact (Genv.find_var_info_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). + eexact (Genv.find_var_info_rev_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). econstructor; eauto. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. @@ -3216,6 +3221,7 @@ Proof. intros. unfold Mem.flat_inj in H0. destruct (zlt b1 (Mem.nextblock m)); congruence. intros. eapply Genv.find_symbol_not_fresh; eauto. + intros. eapply Genv.find_var_info_not_fresh; eauto. Qed. Lemma transl_initial_states: diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 4e4c3795..42884091 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -901,7 +901,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State f f.(fn_body) k e m2) | step_external_function: forall id targs tres vargs k m vres t m', - external_call (external_function id targs tres) (Genv.find_symbol ge) vargs m t vres m' -> + external_call (external_function id targs tres) ge vargs m t vres m' -> step (Callstate (External id targs tres) vargs k m) t (Returnstate vres k m') @@ -1106,7 +1106,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := Mem.free_list m3 (blocks_of_env e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres | eval_funcall_external: forall m id targs tres vargs t vres m', - external_call (external_function id targs tres) (Genv.find_symbol ge) vargs m t vres m' -> + external_call (external_function id targs tres) ge vargs m t vres m' -> eval_funcall m (External id targs tres) vargs t m' vres. Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 4c61918d..558ae1c9 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -516,7 +516,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State f f.(fn_body) k e m2) | step_external_function: forall ef vargs k m t vres m', - external_call ef (Genv.find_symbol ge) vargs m t vres m' -> + external_call ef ge vargs m t vres m' -> step (Callstate (External ef) vargs k m) t (Returnstate vres k m') @@ -554,7 +554,7 @@ Inductive final_state: state -> int -> Prop := Definition global_var_env (p: program): gvarenv := List.fold_left - (fun gve x => match x with (id, init, k) => PTree.set id k gve end) + (fun gve x => match x with (id, v) => PTree.set id (gvar_info v) gve end) p.(prog_vars) (PTree.empty var_kind). Definition exec_program (p: program) (beh: program_behavior) : Prop := diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 99450dee..fb1edbe3 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -279,9 +279,9 @@ Qed. Definition globvarenv (gv: gvarenv) - (vars: list (ident * list init_data * var_kind)) := + (vars: list (ident * globvar var_kind)) := List.fold_left - (fun gve x => match x with (id, init, k) => PTree.set id k gve end) + (fun gve x => match x with (id, v) => PTree.set id (gvar_info v) gve end) vars gv. Definition type_not_by_value (ty: type) : Prop := @@ -324,21 +324,20 @@ Qed. Lemma add_global_var_match_globalenv: forall vars tenv gv tvars, match_globalenv tenv gv -> - map_partial AST.prefix_var_name transl_globvar vars = OK tvars -> + map_partial AST.prefix_name (transf_globvar transl_globvar) vars = OK tvars -> match_globalenv (add_global_vars tenv vars) (globvarenv gv tvars). Proof. induction vars; simpl. intros. inversion H0. assumption. - destruct a as [[id init] ty]. intros until tvars; intro. - caseEq (transl_globvar ty); simpl; try congruence. intros vk VK. - caseEq (map_partial AST.prefix_var_name transl_globvar vars); simpl; try congruence. intros tvars' EQ1 EQ2. + destruct a as [id v]. intros until tvars; intro. + caseEq (transf_globvar transl_globvar v); simpl; try congruence. intros vk VK. + caseEq (map_partial AST.prefix_name (transf_globvar transl_globvar) vars); simpl; try congruence. intros tvars' EQ1 EQ2. inversion EQ2; clear EQ2. simpl. apply IHvars; auto. - red. intros until chunk. repeat rewrite PTree.gsspec. + red. intros until chunk. unfold add_global_var. repeat rewrite PTree.gsspec. simpl. destruct (peq id0 id); intros. - inversion H0; clear H0; subst id0 ty0. - generalize (var_kind_by_value _ _ H2). - unfold transl_globvar in VK. congruence. + inv H0. monadInv VK. unfold transl_globvar in EQ. + generalize (var_kind_by_value _ _ H2). simpl. congruence. red in H. eauto. Qed. @@ -1561,7 +1560,10 @@ Proof. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. apply plus_one. constructor. eauto. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + eapply external_call_symbols_preserved_2; eauto. + exact symbols_preserved. + eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). + eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). econstructor; eauto. (* returnstate 0 *) diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 2bb9a9d4..b147fbda 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -159,11 +159,11 @@ Inductive wt_fundef: typenv -> fundef -> Prop := wt_fundef env (External id args res). Definition add_global_var - (env: typenv) (id_ty_init: ident * list init_data * type) : typenv := - match id_ty_init with (id, init, ty) => PTree.set id ty env end. + (env: typenv) (id_v: ident * globvar type) : typenv := + PTree.set (fst id_v) (gvar_info (snd id_v)) env. Definition add_global_vars - (env: typenv) (vars: list(ident * list init_data * type)) : typenv := + (env: typenv) (vars: list(ident * globvar type)) : typenv := List.fold_left add_global_var vars env. Definition add_global_fun |