summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Changelog6
-rw-r--r--arm/PrintAsm.ml17
-rw-r--r--backend/CMparser.mly37
-rw-r--r--backend/CMtypecheck.ml11
-rw-r--r--backend/Constprop.v20
-rw-r--r--backend/Constpropproof.v29
-rw-r--r--backend/Inlining.v18
-rw-r--r--backend/Inliningproof.v12
-rw-r--r--backend/Inliningspec.v51
-rw-r--r--backend/LTLintyping.v2
-rw-r--r--backend/LTLtyping.v2
-rw-r--r--backend/Lineartyping.v2
-rw-r--r--backend/Machtyping.v2
-rw-r--r--backend/PrintCminor.ml23
-rw-r--r--backend/PrintLTLin.ml10
-rw-r--r--backend/PrintMach.ml10
-rw-r--r--backend/PrintRTL.ml10
-rw-r--r--backend/RTLtyping.v2
-rw-r--r--backend/Stackingproof.v9
-rw-r--r--backend/Unusedglob.ml25
-rw-r--r--cfrontend/C2C.ml51
-rw-r--r--cfrontend/Cminorgen.v22
-rw-r--r--cfrontend/Cminorgenproof.v46
-rw-r--r--cfrontend/Cshmgen.v12
-rw-r--r--cfrontend/Cshmgenproof.v37
-rw-r--r--cfrontend/PrintClight.ml25
-rw-r--r--cfrontend/PrintCsyntax.ml27
-rw-r--r--common/AST.v422
-rw-r--r--common/Globalenvs.v1784
-rw-r--r--driver/Compiler.v97
-rw-r--r--driver/Interp.ml55
-rw-r--r--ia32/PrintAsm.ml16
-rw-r--r--powerpc/PrintAsm.ml23
-rw-r--r--test/regression/Makefile2
-rw-r--r--test/regression/Results/funptr23
-rw-r--r--test/regression/Results/initializers1
-rw-r--r--test/regression/funptr2.c14
-rw-r--r--test/regression/initializers.c3
38 files changed, 1301 insertions, 1637 deletions
diff --git a/Changelog b/Changelog
index af9ce00..e5cee60 100644
--- a/Changelog
+++ b/Changelog
@@ -7,6 +7,9 @@ Improvements in confidence:
top of the Flocq library.
Language semantics:
+- Comparison between function pointers is now correctly defined
+ in the semantics of CompCert C (it was previously undefined behavior,
+ by mistake).
- The "&&" and "||" operators are now primitive in CompCert C and are
given explicit semantic rules, instead of being expressed in terms
of "_ ? _ : _" as in previous CompCert releases.
@@ -28,6 +31,9 @@ Internal simplifications:
- Clight: removed dependencies on CompCert C syntax and semantics.
- Cminor: suppressed the "Oboolval" and "Onotbool" operators,
which can be expressed in terms of "Ocmpu" at no performance costs.
+- All languages: programs are now presented as a list of global definitions
+ (of functions or variables) instead of two lists, one for functions
+ and the other for variables.
Other changes:
- For compatibility with other C compilers, output files are now generated
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index ec1e836..60d0fa4 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -698,13 +698,6 @@ let print_function oc name fn =
fprintf oc " .type %a, %%function\n" print_symb name;
fprintf oc " .size %a, . - %a\n" print_symb name print_symb name
-let print_fundef oc (name, defn) =
- match defn with
- | Internal code ->
- print_function oc name code
- | External ef ->
- ()
-
(* Data *)
let print_init oc = function
@@ -734,7 +727,7 @@ let print_init_data oc name id =
else
List.iter (print_init oc) id
-let print_var oc (name, v) =
+let print_var oc name v =
match v.gvar_init with
| [] -> ()
| _ ->
@@ -756,8 +749,14 @@ let print_var oc (name, v) =
fprintf oc " .type %a, %%object\n" print_symb name;
fprintf oc " .size %a, . - %a\n" print_symb name print_symb name
+let print_globdef oc (name, gdef) =
+ | Gfun(Internal f) -> print_function oc name f
+ | Gfun(External ef) -> ()
+ | Gvar v -> print_var oc name v
+
let print_program oc p =
(* fprintf oc " .fpu vfp\n"; *)
List.iter (print_var oc) p.prog_vars;
- List.iter (print_fundef oc) p.prog_funct
+ List.iter (print_globdef oc) p.prog_defs
+
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index aec0a5e..a62bd74 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -307,10 +307,9 @@ let mkmatch expr cases =
/* Programs */
prog:
- global_declarations proc_list EOF
- { { prog_funct = List.rev $2;
- prog_main = intern_string "main";
- prog_vars = List.rev $1; } }
+ global_declarations EOF
+ { { prog_defs = List.rev $1;
+ prog_main = intern_string "main" } }
;
global_declarations:
@@ -319,12 +318,14 @@ global_declarations:
;
global_declaration:
- VAR STRINGLIT LBRACKET INTLIT RBRACKET /* old style */
- { ($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
- gvar_readonly = false; gvar_volatile = false}) }
+ proc
+ { $1 }
+ | VAR STRINGLIT LBRACKET INTLIT RBRACKET /* old style */
+ { ($2, Gvar{gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
+ gvar_readonly = false; gvar_volatile = false}) }
| VAR STRINGLIT is_readonly is_volatile LBRACE init_data_list RBRACE
- { ($2, {gvar_info = (); gvar_init = List.rev $6;
- gvar_readonly = $3; gvar_volatile = $4; } ) }
+ { ($2, Gvar{gvar_info = (); gvar_init = List.rev $6;
+ gvar_readonly = $3; gvar_volatile = $4; } ) }
;
is_readonly:
@@ -359,12 +360,6 @@ init_data:
| INTLIT LPAREN STRINGLIT RPAREN { Init_addrof ($3, coqint_of_camlint $1) }
;
-
-proc_list:
- /* empty */ { [] }
- | proc_list proc { $2 :: $1 }
-;
-
/* Procedures */
proc:
@@ -378,13 +373,13 @@ proc:
temporaries := [];
temp_counter := 0;
($1,
- Internal { fn_sig = $6;
- fn_params = List.rev $3;
- fn_vars = List.rev (tmp @ $9);
- fn_stackspace = $8;
- fn_body = $10 }) }
+ Gfun(Internal { fn_sig = $6;
+ fn_params = List.rev $3;
+ fn_vars = List.rev (tmp @ $9);
+ fn_stackspace = $8;
+ fn_body = $10 })) }
| EXTERN STRINGLIT COLON signature
- { ($2, External(EF_external($2,$4))) }
+ { ($2, Gfun(External(EF_external($2,$4)))) }
;
signature:
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 4070785..408e9ec 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -349,10 +349,11 @@ let type_function id f =
with Error s ->
raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s))
-let type_fundef (id, fd) =
- match fd with
- | Internal f -> type_function id f
- | External ef -> ()
+let type_globdef (id, gd) =
+ match gd with
+ | Gfun(Internal f) -> type_function id f
+ | Gfun(External ef) -> ()
+ | Gvar v -> ()
let type_program p =
- List.iter type_fundef p.prog_funct; p
+ List.iter type_globdef p.prog_defs; p
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 104aa3b..fc242e1 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -368,17 +368,21 @@ Definition transf_function (gapp: global_approx) (f: function) : function :=
Definition transf_fundef (gapp: global_approx) (fd: fundef) : fundef :=
AST.transf_fundef (transf_function gapp) fd.
-Fixpoint make_global_approx (gapp: global_approx) (vars: list (ident * globvar unit)) : global_approx :=
- match vars with
+Fixpoint make_global_approx (gapp: global_approx) (gdl: list (ident * globdef fundef unit)): global_approx :=
+ match gdl with
| nil => gapp
- | (id, gv) :: vars' =>
+ | (id, gl) :: gdl' =>
let gapp1 :=
- if gv.(gvar_readonly) && negb gv.(gvar_volatile)
- then PTree.set id gv.(gvar_init) gapp
- else PTree.remove id gapp in
- make_global_approx gapp1 vars'
+ match gl with
+ | Gfun f => PTree.remove id gapp
+ | Gvar gv =>
+ if gv.(gvar_readonly) && negb gv.(gvar_volatile)
+ then PTree.set id gv.(gvar_init) gapp
+ else PTree.remove id gapp
+ end in
+ make_global_approx gapp1 gdl'
end.
Definition transf_program (p: program) : program :=
- let gapp := make_global_approx (PTree.empty _) p.(prog_vars) in
+ let gapp := make_global_approx (PTree.empty _) p.(prog_defs) in
transform_program (transf_fundef gapp) p.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 8228493..f14e87a 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -37,7 +37,7 @@ Variable prog: program.
Let tprog := transf_program prog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
-Let gapp := make_global_approx (PTree.empty _) prog.(prog_vars).
+Let gapp := make_global_approx (PTree.empty _) prog.(prog_defs).
(** * Correctness of the static analysis *)
@@ -279,31 +279,34 @@ Definition global_approx_charact (g: genv) (ga: global_approx) : Prop :=
Genv.find_var_info g b = Some (mkglobvar tt il true false).
Lemma make_global_approx_correct:
- forall vl g ga,
+ forall gdl g ga,
global_approx_charact g ga ->
- global_approx_charact (Genv.add_variables g vl) (make_global_approx ga vl).
+ global_approx_charact (Genv.add_globals g gdl) (make_global_approx ga gdl).
Proof.
- induction vl; simpl; intros.
+ induction gdl; simpl; intros.
auto.
- destruct a as [id gv]. apply IHvl.
+ destruct a as [id gd]. apply IHgdl.
red; intros.
- assert (EITHER: id0 = id /\ gv = mkglobvar tt il true false
+ assert (EITHER: id0 = id /\ gd = Gvar(mkglobvar tt il true false)
\/ id0 <> id /\ ga!id0 = Some il).
- destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn.
+ destruct gd.
+ rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto].
+ destruct (gvar_readonly v && negb (gvar_volatile v)) as []_eqn.
rewrite PTree.gsspec in H0. destruct (peq id0 id).
inv H0. left. split; auto.
- destruct gv; simpl in *.
+ destruct v; simpl in *.
destruct gvar_readonly; try discriminate.
destruct gvar_volatile; try discriminate.
destruct gvar_info. auto.
- right; auto.
- rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); try discriminate.
- right; auto.
- unfold Genv.add_variable, Genv.find_symbol, Genv.find_var_info in *;
+ auto.
+ rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto].
+
+ unfold Genv.add_global, Genv.find_symbol, Genv.find_var_info in *;
simpl in *.
destruct EITHER as [[A B] | [A B]].
subst id0. rewrite PTree.gss in H1. inv H1. rewrite ZMap.gss. auto.
- rewrite PTree.gso in H1; auto. rewrite ZMap.gso. eapply H. eauto. auto.
+ rewrite PTree.gso in H1; auto. destruct gd. eapply H; eauto.
+ rewrite ZMap.gso. eapply H; eauto.
exploit Genv.genv_symb_range; eauto. unfold ZIndexed.t. omega.
Qed.
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 406447b..3ddfe9a 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -28,7 +28,7 @@ Ltac xomega := unfold Plt, Ple in *; zify; omega.
(** ** Environment of inlinable functions *)
(** We maintain a mapping from function names to their definitions.
- In this mapping, we only include functions that are eligible for
+ In this mapping, we only include internal functions that are eligible for
inlining, as determined by the external heuristic
[should_inline]. *)
@@ -38,22 +38,18 @@ Definition size_fenv (fenv: funenv) := PTree_Properties.cardinal fenv.
Parameter should_inline: ident -> function -> bool.
-Definition add_fundef (fenv: funenv) (idf: ident * fundef) : funenv :=
- match idf with
- | (id, External ef) =>
- PTree.remove id fenv
- | (id, Internal f) =>
+Definition add_globdef (fenv: funenv) (idg: ident * globdef fundef unit) : funenv :=
+ match idg with
+ | (id, Gfun (Internal f)) =>
if should_inline id f
then PTree.set id f fenv
else PTree.remove id fenv
+ | (id, _) =>
+ PTree.remove id fenv
end.
-Definition remove_vardef (fenv: funenv) (idv: ident * globvar unit) : funenv :=
- PTree.remove (fst idv) fenv.
-
Definition funenv_program (p: program) : funenv :=
- List.fold_left remove_vardef p.(prog_vars)
- (List.fold_left add_fundef p.(prog_funct) (PTree.empty function)).
+ List.fold_left add_globdef p.(prog_defs) (PTree.empty function).
(** Resources used by a function. *)
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 9ca351a..8de8487 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -358,7 +358,8 @@ Inductive match_globalenvs (F: meminj) (bound: Z): Prop :=
(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)
- (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
+ (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound)
+ (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
Lemma find_function_agree:
forall ros rs fd F ctx rs' bound,
@@ -374,9 +375,9 @@ Proof.
exploit Genv.find_funct_inv; eauto. intros [b EQ].
assert (A: val_inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto.
rewrite EQ in A; inv A.
- inv H1. rewrite DOMAIN in H5. inv H5. auto.
- rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H.
- exploit Genv.find_funct_ptr_negative. unfold ge in H; eexact H. omega.
+ inv H1. rewrite DOMAIN in H5. inv H5. auto.
+ apply FUNCTIONS with fd.
+ rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H. auto.
rewrite H2. eapply functions_translated; eauto.
(* symbol *)
rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try discriminate.
@@ -1219,7 +1220,8 @@ Proof.
apply Mem.nextblock_pos.
unfold Mem.flat_inj. apply zlt_true; auto.
unfold Mem.flat_inj in H. destruct (zlt b1 (Mem.nextblock m0)); congruence.
- eapply Genv.find_symbol_not_fresh; eauto.
+ eapply Genv.find_symbol_not_fresh; eauto.
+ eapply Genv.find_funct_ptr_not_fresh; eauto.
eapply Genv.find_var_info_not_fresh; eauto.
omega.
eapply Genv.initmem_inject; eauto.
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index ec72290..84bcdcd 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -35,43 +35,30 @@ Definition fenv_compat (ge: genv) (fenv: funenv) : Prop :=
fenv!id = Some f -> Genv.find_symbol ge id = Some b ->
Genv.find_funct_ptr ge b = Some (Internal f).
-Remark add_fundef_compat:
- forall ge fenv idf,
+Remark add_globdef_compat:
+ forall ge fenv idg,
fenv_compat ge fenv ->
- fenv_compat (Genv.add_function ge idf) (Inlining.add_fundef fenv idf).
+ fenv_compat (Genv.add_global ge idg) (Inlining.add_globdef fenv idg).
Proof.
- intros. destruct idf as [id fd]. red; simpl; intros.
+ intros. destruct idg as [id gd]. red; simpl; intros.
unfold Genv.find_symbol in H1; simpl in H1.
unfold Genv.find_funct_ptr; simpl.
rewrite PTree.gsspec in H1. destruct (peq id0 id).
(* same *)
- subst id0. inv H1. rewrite ZMap.gss.
- destruct fd. destruct (should_inline id f0).
- rewrite PTree.gss in H0. inv H0; auto.
+ subst id0. inv H1. destruct gd. destruct f0.
+ destruct (should_inline id f0).
+ rewrite PTree.gss in H0. rewrite ZMap.gss. inv H0; auto.
+ rewrite PTree.grs in H0; discriminate.
rewrite PTree.grs in H0; discriminate.
rewrite PTree.grs in H0; discriminate.
(* different *)
- rewrite ZMap.gso. eapply H; eauto.
- destruct fd. destruct (should_inline id f0).
+ destruct gd. rewrite ZMap.gso. eapply H; eauto.
+ destruct f0. destruct (should_inline id f0).
rewrite PTree.gso in H0; auto.
rewrite PTree.gro in H0; auto.
rewrite PTree.gro in H0; auto.
- exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega.
-Qed.
-
-Remark remove_vardef_compat:
- forall ge fenv idv,
- fenv_compat ge fenv ->
- fenv_compat (Genv.add_variable ge idv) (Inlining.remove_vardef fenv idv).
-Proof.
- intros. destruct idv as [id vi]. red; simpl; intros.
- unfold Genv.find_symbol in H1; simpl in H1.
- unfold Genv.find_funct_ptr; simpl.
- unfold remove_vardef in H0; simpl in H0.
- rewrite PTree.gsspec in H1. rewrite PTree.grspec in H0.
- unfold PTree.elt_eq in H0. destruct (peq id0 id).
- discriminate.
- eapply H; eauto.
+ exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega.
+ rewrite PTree.gro in H0; auto. eapply H; eauto.
Qed.
Lemma funenv_program_compat:
@@ -79,17 +66,11 @@ Lemma funenv_program_compat:
Proof.
intros.
unfold Genv.globalenv, funenv_program.
- assert (forall funs ge fenv,
- fenv_compat ge fenv ->
- fenv_compat (Genv.add_functions ge funs) (fold_left add_fundef funs fenv)).
- unfold Genv.add_functions. induction funs; simpl; intros.
- auto. apply IHfuns. apply add_fundef_compat; auto.
- assert (forall vars ge fenv,
+ assert (forall gl ge fenv,
fenv_compat ge fenv ->
- fenv_compat (Genv.add_variables ge vars) (fold_left remove_vardef vars fenv)).
- unfold Genv.add_variables. induction vars; simpl; intros.
- auto. apply IHvars. apply remove_vardef_compat; auto.
- apply H0. apply H. red; intros. rewrite PTree.gempty in H1; discriminate.
+ fenv_compat (Genv.add_globals ge gl) (fold_left add_globdef gl fenv)).
+ induction gl; simpl; intros. auto. apply IHgl. apply add_globdef_compat; auto.
+ apply H. red; intros. rewrite PTree.gempty in H0; discriminate.
Qed.
(** ** Soundness of the computed bounds over function resources *)
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 1a20f73..e9cc2df 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -122,4 +122,4 @@ Inductive wt_fundef: fundef -> Prop :=
wt_fundef (Internal f).
Definition wt_program (p: program): Prop :=
- forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+ forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 40a584f..2e627e9 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -142,4 +142,4 @@ Inductive wt_fundef: fundef -> Prop :=
wt_fundef (Internal f).
Definition wt_program (p: program): Prop :=
- forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+ forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 3930da3..da73b00 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -133,7 +133,7 @@ Inductive wt_fundef: fundef -> Prop :=
wt_fundef (Internal f).
Definition wt_program (p: program) : Prop :=
- forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+ forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
(** Typing the run-time state. These definitions are used in [Stackingproof]. *)
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index 2d8c83d..b9d8009 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -111,4 +111,4 @@ Inductive wt_fundef: fundef -> Prop :=
wt_fundef (Internal f).
Definition wt_program (p: program) : Prop :=
- forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+ forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 858ef21..8e49303 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -273,13 +273,6 @@ let print_extfun p id ef =
fprintf p "@[<v 0>extern @[<hov 2>\"%s\":@ %a@]@ "
(extern_atom id) print_sig (ef_sig ef)
-let print_fundef p (id, fd) =
- match fd with
- | External ef ->
- print_extfun p id ef
- | Internal f ->
- print_function p id f
-
let print_init_data p = function
| Init_int8 i -> fprintf p "int8 %ld" (camlint_of_coqint i)
| Init_int16 i -> fprintf p "int16 %ld" (camlint_of_coqint i)
@@ -306,14 +299,18 @@ let print_globvar p gv =
print_init_data_list p gv.gvar_init;
fprintf p "}"
-let print_var p (id, gv) =
- fprintf p "var \"%s\" %a\n" (extern_atom id) print_globvar gv
+let print_globdef p (id, gd) =
+ match gd with
+ | Gfun(External ef) ->
+ print_extfun p id ef
+ | Gfun(Internal f) ->
+ print_function p id f
+ | Gvar gv ->
+ fprintf p "var \"%s\" %a\n" (extern_atom id) print_globvar gv
let print_program p prog =
- fprintf p "@[<v>";
- List.iter (print_var p) prog.prog_vars;
- fprintf p "@]@[<v 0>";
- List.iter (print_fundef p) prog.prog_funct;
+ fprintf p "@[<v 0>";
+ List.iter (print_globdef p) prog.prog_defs;
fprintf p "@]@."
let destination : string option ref = ref None
diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
index bb360eb..4dc311c 100644
--- a/backend/PrintLTLin.ml
+++ b/backend/PrintLTLin.ml
@@ -95,13 +95,13 @@ let print_function pp id f =
List.iter (print_instruction pp) f.fn_code;
fprintf pp "@;<0 -2>}@]@."
-let print_fundef pp (id, fd) =
- match fd with
- | Internal f -> print_function pp id f
- | External _ -> ()
+let print_globdef pp (id, gd) =
+ match gd with
+ | Gfun(Internal f) -> print_function pp id f
+ | _ -> ()
let print_program pp prog =
- List.iter (print_fundef pp) prog.prog_funct
+ List.iter (print_globdef pp) prog.prog_defs
let destination : string option ref = ref None
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index 03977a6..dfbc66e 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -102,13 +102,13 @@ let print_function pp id f =
List.iter (print_instruction pp) f.fn_code;
fprintf pp "@;<0 -2>}@]@."
-let print_fundef pp (id, fd) =
- match fd with
- | Internal f -> print_function pp id f
- | External _ -> ()
+let print_globdef pp (id, gd) =
+ match gd with
+ | Gfun(Internal f) -> print_function pp id f
+ | _ -> ()
let print_program pp prog =
- List.iter (print_fundef pp) prog.prog_funct
+ List.iter (print_globdef pp) prog.prog_defs
let destination : string option ref = ref None
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 4fc8f56..4cd3871 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -103,13 +103,13 @@ let print_function pp id f =
List.iter (print_instruction pp) instrs;
fprintf pp "@;<0 -2>}@]@."
-let print_fundef pp (id, fd) =
- match fd with
- | Internal f -> print_function pp id f
- | External _ -> ()
+let print_globdef pp (id, gd) =
+ match gd with
+ | Gfun(Internal f) -> print_function pp id f
+ | _ -> ()
let print_program pp (prog: RTL.program) =
- List.iter (print_fundef pp) prog.prog_funct
+ List.iter (print_globdef pp) prog.prog_defs
let print_if optdest prog =
match !optdest with
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 65506c8..a14e944 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -158,7 +158,7 @@ Inductive wt_fundef: fundef -> Prop :=
wt_fundef (Internal f).
Definition wt_program (p: program): Prop :=
- forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+ forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
(** * Type inference *)
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 1cfb738..1d87ad3 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1734,7 +1734,8 @@ Inductive match_globalenvs (j: meminj) (bound: Z) : Prop :=
(DOMAIN: forall b, b < bound -> j b = Some(b, 0))
(IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
(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).
+ (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound)
+ (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
Inductive match_stacks (j: meminj) (m m': mem):
list Linear.stackframe -> list stackframe -> signature -> Z -> Z -> Prop :=
@@ -2170,9 +2171,8 @@ Proof.
exploit function_ptr_translated; eauto. intros [tf [A B]].
exists b; exists tf; split; auto. simpl.
generalize (AG m0). rewrite EQ. intro INJ. inv INJ.
- exploit Genv.find_funct_ptr_negative. unfold ge in FF; eexact FF. intros.
- inv MG. rewrite (DOMAIN b) in H2. inv H2. auto. omega.
- revert FF. case_eq (Genv.find_symbol ge i); intros; try discriminate.
+ inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto.
+ destruct (Genv.find_symbol ge i) as [b|]_eqn; try discriminate.
exploit function_ptr_translated; eauto. intros [tf [A B]].
exists b; exists tf; split; auto. simpl.
rewrite symbols_preserved. auto.
@@ -2742,6 +2742,7 @@ Proof.
intros. unfold Mem.flat_inj. apply zlt_true; auto.
unfold Mem.flat_inj; intros. destruct (zlt b1 (Mem.nextblock m0)); congruence.
intros. change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto.
+ intros. change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto.
intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto.
rewrite H3. red; intros. contradiction.
eapply Genv.find_funct_ptr_prop. eexact wt_prog.
diff --git a/backend/Unusedglob.ml b/backend/Unusedglob.ml
index 4139678..1a88ee9 100644
--- a/backend/Unusedglob.ml
+++ b/backend/Unusedglob.ml
@@ -28,10 +28,6 @@ let add_referenced_instr rf i =
let referenced_function f =
List.fold_left add_referenced_instr IdentSet.empty (code_of_function f)
-let referenced_fundef = function
- | Internal f -> referenced_function f
- | External ef -> IdentSet.empty
-
(* The set of globals referenced from a variable definition (initialization) *)
let add_referenced_init_data rf = function
@@ -43,10 +39,15 @@ let referenced_globvar gv =
(* The map global |-> set of globals it references *)
+let referenced_globdef gd =
+ match gd with
+ | Gfun(Internal f) -> referenced_function f
+ | Gfun(External ef) -> IdentSet.empty
+ | Gvar gv -> referenced_globvar gv
+
let use_map p =
- List.fold_left (fun m (id, gv) -> PTree.set id (referenced_globvar gv) m)
- (List.fold_left (fun m (id, fd) -> PTree.set id (referenced_fundef fd) m)
- PTree.empty p.prog_funct) p.prog_vars
+ List.fold_left (fun m (id, gd) -> PTree.set id (referenced_globdef gd) m)
+ PTree.empty p.prog_defs
(* Worklist algorithm computing the set of used globals *)
@@ -66,9 +67,8 @@ let add_nonstatic wrk id =
if C2C.atom_is_static id then wrk else id :: wrk
let initial_worklist p =
- List.fold_left (fun wrk (id, gv) -> add_nonstatic wrk id)
- (List.fold_left (fun wrk (id, fd) -> add_nonstatic wrk id)
- [] p.prog_funct) p.prog_vars
+ List.fold_left (fun wrk (id, gd) -> add_nonstatic wrk id)
+ [] p.prog_defs
(* Eliminate unused definitions *)
@@ -80,9 +80,8 @@ let rec filter used = function
else filter used rem
let filter_prog used p =
- { prog_funct = filter used p.prog_funct;
- prog_main = p.prog_main;
- prog_vars = filter used p.prog_vars }
+ { prog_defs = filter used p.prog_defs;
+ prog_main = p.prog_main }
(* Entry point *)
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index c659b86..2cdcc03 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -137,8 +137,8 @@ let global_for_string s id =
:: !init in
add_char '\000';
for i = String.length s - 1 downto 0 do add_char s.[i] done;
- (id, {gvar_info = typeStringLiteral s; gvar_init = !init;
- gvar_readonly = true; gvar_volatile = false})
+ (id, Gvar {gvar_info = typeStringLiteral s; gvar_init = !init;
+ gvar_readonly = true; gvar_volatile = false})
let globals_for_strings globs =
Hashtbl.fold
@@ -155,7 +155,7 @@ let register_special_external name ef targs tres =
let declare_special_externals k =
Hashtbl.fold
- (fun name fd k -> (intern_string name, fd) :: k)
+ (fun name fd k -> (intern_string name, Gfun fd) :: k)
special_externals_table k
(** ** Handling of stubs for variadic functions *)
@@ -709,8 +709,8 @@ let convertFundef env fd =
a_sections = Sections.for_function env id' fd.fd_ret;
a_small_data = false;
a_inline = fd.fd_inline };
- (id', Internal {fn_return = ret; fn_params = params;
- fn_vars = vars; fn_body = body'})
+ (id', Gfun(Internal {fn_return = ret; fn_params = params;
+ fn_vars = vars; fn_body = body'}))
(** External function declaration *)
@@ -727,7 +727,7 @@ let convertFundecl env (sto, id, ty, optinit) =
if List.mem_assoc id.name builtins.functions
then EF_builtin(id', sg)
else EF_external(id', sg) in
- (id', External(ef, args, res))
+ (id', Gfun(External(ef, args, res)))
(** Initializers *)
@@ -788,8 +788,8 @@ let convertGlobvar env (sto, id, ty, optinit) =
a_inline = false };
let volatile = List.mem C.AVolatile attr in
let readonly = List.mem C.AConst attr && not volatile in
- (id', {gvar_info = ty'; gvar_init = init';
- gvar_readonly = readonly; gvar_volatile = volatile})
+ (id', Gvar {gvar_info = ty'; gvar_init = init';
+ gvar_readonly = readonly; gvar_volatile = volatile})
(** Sanity checks on composite declarations. *)
@@ -803,13 +803,12 @@ let checkComposite env si id attr flds =
in List.iter checkField flds
(** Convert a list of global declarations.
- Result is a pair [(funs, vars)] where [funs] are
- the function definitions (internal and external)
- and [vars] the variable declarations. *)
+ Result is a list of CompCert C global declarations (functions +
+ variables). *)
-let rec convertGlobdecls env funs vars gl =
+let rec convertGlobdecls env res gl =
match gl with
- | [] -> (List.rev funs, List.rev vars)
+ | [] -> List.rev res
| g :: gl' ->
updateLoc g.gloc;
match g.gdesc with
@@ -819,29 +818,29 @@ let rec convertGlobdecls env funs vars gl =
Other types become variable declarations. *)
begin match Cutil.unroll env ty with
| TFun(_, Some _, false, _) ->
- convertGlobdecls env (convertFundecl env d :: funs) vars gl'
+ convertGlobdecls env (convertFundecl env d :: res) gl'
| TFun(_, None, false, _) ->
error "function declaration without prototype";
- convertGlobdecls env funs vars gl'
+ convertGlobdecls env res gl'
| TFun(_, _, true, _) ->
- convertGlobdecls env funs vars gl'
+ convertGlobdecls env res gl'
| _ ->
- convertGlobdecls env funs (convertGlobvar env d :: vars) gl'
+ convertGlobdecls env (convertGlobvar env d :: res) gl'
end
| C.Gfundef fd ->
- convertGlobdecls env (convertFundef env fd :: funs) vars gl'
+ convertGlobdecls env (convertFundef env fd :: res) gl'
| C.Gcompositedecl _ | C.Gtypedef _ | C.Genumdef _ ->
(* typedefs are unrolled, structs are expanded inline, and
enum tags are folded. So we just skip their declarations. *)
- convertGlobdecls env funs vars gl'
+ convertGlobdecls env res gl'
| C.Gcompositedef(su, id, attr, flds) ->
(* sanity checks on fields *)
checkComposite env su id attr flds;
- convertGlobdecls env funs vars gl'
+ convertGlobdecls env res gl'
| C.Gpragma s ->
if not (!process_pragma_hook s) then
warning ("'#pragma " ^ s ^ "' directive ignored");
- convertGlobdecls env funs vars gl'
+ convertGlobdecls env res gl'
(** Build environment of typedefs and structs *)
@@ -921,14 +920,12 @@ let convertProgram p =
Hashtbl.clear special_externals_table;
let p = Builtins.declarations() @ p in
try
- let (funs1, vars1) =
- convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in
- let funs2 = declare_special_externals funs1 in
- let vars2 = globals_for_strings vars1 in
+ let gl1 = convertGlobdecls (translEnv Env.empty p) [] (cleanupGlobals p) in
+ let gl2 = declare_special_externals gl1 in
+ let gl3 = globals_for_strings gl2 in
if !numErrors > 0
then None
- else Some { AST.prog_funct = funs2;
- AST.prog_vars = vars2;
+ else Some { AST.prog_defs = gl3;
AST.prog_main = intern_string "main" }
with Env.Error msg ->
error (Env.error_message msg); None
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 2c02813..a47efb2 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -565,19 +565,19 @@ Definition build_compilenv
(fn_variables f)
(globenv, 0).
-Definition assign_global_variable
- (ce: compilenv) (info: ident * globvar var_kind) : compilenv :=
- match info with
- | (id, mkglobvar vk _ _ _) =>
- PMap.set id (match vk with Vscalar chunk => Var_global_scalar chunk
- | Varray _ _ => Var_global_array
- end)
- ce
- end.
+Definition assign_global_def
+ (ce: compilenv) (gdef: ident * globdef Csharpminor.fundef var_kind) : compilenv :=
+ let (id, gd) := gdef in
+ let kind :=
+ match gd with
+ | Gvar (mkglobvar (Vscalar chunk) _ _ _) => Var_global_scalar chunk
+ | Gvar (mkglobvar (Varray _ _) _ _ _) => Var_global_array
+ | Gfun f => Var_global_array
+ end in
+ PMap.set id kind ce.
Definition build_global_compilenv (p: Csharpminor.program) : compilenv :=
- List.fold_left assign_global_variable
- p.(prog_vars) (PMap.init Var_global_array).
+ List.fold_left assign_global_def p.(prog_defs) (PMap.init Var_global_array).
(** * Translation of functions *)
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 0fa9ac0..42f54b3 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -109,23 +109,28 @@ Lemma global_compilenv_charact:
Proof.
assert (A: forall ge, global_compilenv_match (PMap.init Var_global_array) ge).
intros; red; intros. rewrite PMap.gi. auto.
- assert (B: forall ce ge v,
+ assert (B: forall ce ge idg,
global_compilenv_match ce ge ->
- global_compilenv_match (assign_global_variable ce v)
- (Genv.add_variable ge v)).
- intros; red; intros. destruct v as [id1 [info1 init1 ro1 vo1]].
- unfold assign_global_variable, Genv.find_symbol, Genv.find_var_info; simpl.
- rewrite PMap.gsspec. destruct (peq id id1). subst id.
+ global_compilenv_match (assign_global_def ce idg)
+ (Genv.add_global ge idg)).
+ intros; red; intros. unfold assign_global_def.
+ destruct idg as [id1 gd]. rewrite PMap.gsspec. destruct (peq id id1).
+ (* same var *)
+ subst id1. destruct gd as [f | [info1 init1 ro1 vo1]]. auto.
destruct info1; auto.
- rewrite PTree.gss. intros. inv H0. rewrite ZMap.gss in H1. inv H1. auto.
- generalize (H id). destruct (ce!!id); auto.
- rewrite PTree.gso; auto. intros. rewrite ZMap.gso in H2. eapply H0; eauto.
+ unfold Genv.find_symbol, Genv.find_var_info. simpl; intros.
+ rewrite PTree.gss in H0. inv H0. rewrite ZMap.gss in H1. inv H1; auto.
+ (* different var *)
+ generalize (H id). unfold Genv.find_symbol, Genv.find_var_info. simpl. intros.
+ destruct (ce!!id); auto. intros.
+ rewrite PTree.gso in H1; auto.
+ destruct gd as [f|v]. eauto. rewrite ZMap.gso in H2. eauto.
exploit Genv.genv_symb_range; eauto. unfold block, ZIndexed.t; omega.
- assert (C: forall vl ce ge,
+ assert (C: forall gl ce ge,
global_compilenv_match ce ge ->
- global_compilenv_match (fold_left assign_global_variable vl ce)
- (Genv.add_variables ge vl)).
- induction vl; simpl; intros. auto. apply IHvl. apply B. auto.
+ global_compilenv_match (fold_left assign_global_def gl ce)
+ (Genv.add_globals ge gl)).
+ induction gl; simpl; intros. auto. apply IHgl. apply B. auto.
unfold gce, build_global_compilenv, ge, Genv.globalenv.
apply C. apply A.
@@ -680,7 +685,8 @@ Inductive match_globalenvs (f: meminj) (bound: Z): Prop :=
(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)
- (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
+ (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound)
+ (VARINFOS: 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
@@ -1132,7 +1138,7 @@ Remark inj_preserves_globals:
Proof.
intros. inv H.
split. intros. apply DOMAIN. eapply SYMBOLS. eauto.
- split. intros. apply DOMAIN. eapply INFOS. eauto.
+ split. intros. apply DOMAIN. eapply VARINFOS. eauto.
intros. symmetry. eapply IMAGE; eauto.
Qed.
@@ -2822,16 +2828,15 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop :=
Remark val_inject_function_pointer:
forall bound v fd f tv,
- Genv.find_funct tge v = Some fd ->
+ Genv.find_funct ge v = Some fd ->
match_globalenvs f bound ->
val_inject f v tv ->
tv = v.
Proof.
intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v.
- rewrite Genv.find_funct_find_funct_ptr in H.
- assert (b < 0). unfold tge in H. eapply Genv.find_funct_ptr_negative; eauto.
- assert (f b = Some(b, 0)). inv H0. apply DOMAIN. omega.
- inv H1. rewrite H3 in H6; inv H6. reflexivity.
+ rewrite Genv.find_funct_find_funct_ptr in H.
+ assert (f b = Some(b, 0)). inv H0. apply DOMAIN. eapply FUNCTIONS; eauto.
+ inv H1. rewrite H2 in H5; inv H5. reflexivity.
Qed.
Lemma match_call_cont:
@@ -3426,6 +3431,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_funct_ptr_not_fresh; eauto.
intros. eapply Genv.find_var_info_not_fresh; eauto.
Qed.
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index c5e9b8d..a459297 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -546,8 +546,16 @@ with transl_lbl_stmt (tyret: type) (nbrk ncnt: nat)
Definition prefix_var_name (id: ident) : errmsg :=
MSG "In local variable " :: CTX id :: MSG ": " :: nil.
-Definition transl_vars (l: list (ident * type)) :=
- AST.map_partial prefix_var_name var_kind_of_type l.
+Fixpoint transl_vars (l: list (ident * type)) : res (list (ident * var_kind)) :=
+ match l with
+ | nil => OK nil
+ | (id, ty) :: l' =>
+ match var_kind_of_type ty with
+ | Error msg => Error (MSG "In local variable " :: CTX id :: MSG ": " :: msg)
+ | OK vk =>
+ do tl' <- transl_vars l'; OK ((id, vk) :: tl')
+ end
+ end.
Definition transl_function (f: Clight.function) : res function :=
do tparams <- transl_vars (Clight.fn_params f);
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 9f73467..2f319d0 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -214,39 +214,15 @@ Qed.
(** * Properties of the translation functions *)
-Lemma map_partial_names:
- forall (A B: Type) (f: A -> res B)
- (l: list (ident * A)) (tl: list (ident * B)),
- map_partial prefix_var_name f l = OK tl ->
- List.map (@fst ident B) tl = List.map (@fst ident A) l.
-Proof.
- induction l; simpl.
- intros. inversion H. reflexivity.
- intro tl. destruct a as [id x]. destruct (f x); try congruence.
- caseEq (map_partial prefix_var_name f l); simpl; intros; try congruence.
- inv H0. simpl. decEq. auto.
-Qed.
-
-Lemma map_partial_append:
- forall (A B: Type) (f: A -> res B)
- (l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)),
- map_partial prefix_var_name f l1 = OK tl1 ->
- map_partial prefix_var_name f l2 = OK tl2 ->
- map_partial prefix_var_name f (l1 ++ l2) = OK (tl1 ++ tl2).
-Proof.
- induction l1; intros until tl2; simpl.
- intros. inversion H. simpl; auto.
- destruct a as [id x]. destruct (f x); try congruence.
- caseEq (map_partial prefix_var_name f l1); simpl; intros; try congruence.
- inv H0. rewrite (IHl1 _ _ _ H H1). auto.
-Qed.
-
Lemma transl_vars_names:
forall vars tvars,
transl_vars vars = OK tvars ->
List.map variable_name tvars = var_names vars.
Proof.
- exact (map_partial_names _ _ var_kind_of_type).
+ induction vars; simpl; intros.
+ monadInv H. auto.
+ destruct a as [id ty]. destruct (var_kind_of_type ty); monadInv H.
+ simpl. decEq; auto.
Qed.
Lemma transl_names_norepet:
@@ -268,7 +244,10 @@ Lemma transl_vars_append:
transl_vars l1 = OK tl1 -> transl_vars l2 = OK tl2 ->
transl_vars (l1 ++ l2) = OK (tl1 ++ tl2).
Proof.
- exact (map_partial_append _ _ var_kind_of_type).
+ induction l1; simpl; intros.
+ inv H. auto.
+ destruct a as [id ty]. destruct (var_kind_of_type ty); monadInv H.
+ erewrite IHl1; eauto. simpl. auto.
Qed.
Lemma transl_fn_variables:
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 7b9f3d3..0e8b494 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -249,7 +249,7 @@ let print_function p id f =
print_stmt p f.fn_body;
fprintf p "@;<0 -2>}@]@ @ "
-let print_fundef p (id, fd) =
+let print_fundef p id fd =
match fd with
| External(EF_external(_,_), args, res) ->
fprintf p "extern %s;@ @ "
@@ -259,6 +259,11 @@ let print_fundef p (id, fd) =
| Internal f ->
print_function p id f
+let print_globdef p (id, gd) =
+ match gd with
+ | Gfun f -> print_fundef p id f
+ | Gvar v -> print_globvar p id v (* from PrintCsyntax *)
+
(* Collect struct and union types *)
let rec collect_expr e =
@@ -307,17 +312,14 @@ let collect_function f =
List.iter (fun (id, ty) -> collect_type ty) f.fn_temps;
collect_stmt f.fn_body
-let collect_fundef (id, fd) =
- match fd with
- | External(_, args, res) -> collect_type_list args; collect_type res
- | Internal f -> collect_function f
-
-let collect_globvar (id, v) =
- collect_type v.gvar_info
+let collect_globdef (id, gd) =
+ match gd with
+ | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res
+ | Gfun(Internal f) -> collect_function f
+ | Gvar v -> collect_type v.gvar_info
let collect_program p =
- List.iter collect_globvar p.prog_vars;
- List.iter collect_fundef p.prog_funct
+ List.iter collect_globdef p.prog_defs
let declare_struct_or_union p (name, fld) =
fprintf p "%s;@ @ " name
@@ -338,8 +340,7 @@ let print_program p prog =
fprintf p "@[<v 0>";
StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
StructUnionSet.iter (print_struct_or_union p) !struct_unions;
- List.iter (print_globvar p) prog.prog_vars;
- List.iter (print_fundef p) prog.prog_funct;
+ List.iter (print_globdef p) prog.prog_defs;
fprintf p "@]@."
let destination : string option ref = ref None
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 5490321..7858545 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -372,7 +372,7 @@ let print_function p id f =
print_stmt p f.fn_body;
fprintf p "@;<0 -2>}@]@ @ "
-let print_fundef p (id, fd) =
+let print_fundef p id fd =
match fd with
| External(EF_external(_,_), args, res) ->
fprintf p "extern %s;@ @ "
@@ -414,7 +414,7 @@ let print_init p = function
let re_string_literal = Str.regexp "__stringlit_[0-9]+"
-let print_globvar p (id, v) =
+let print_globvar p id v =
let name1 = extern_atom id in
let name2 = if v.gvar_readonly then "const " ^ name1 else name1 in
let name3 = if v.gvar_volatile then "volatile " ^ name2 else name2 in
@@ -439,6 +439,11 @@ let print_globvar p (id, v) =
end;
fprintf p ";@]@ @ "
+let print_globdef p (id, gd) =
+ match gd with
+ | Gfun f -> print_fundef p id f
+ | Gvar v -> print_globvar p id v
+
(* Collect struct and union types *)
let rec collect_type = function
@@ -519,17 +524,14 @@ let collect_function f =
List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
collect_stmt f.fn_body
-let collect_fundef (id, fd) =
- match fd with
- | External(_, args, res) -> collect_type_list args; collect_type res
- | Internal f -> collect_function f
-
-let collect_globvar (id, v) =
- collect_type v.gvar_info
+let collect_globdef (id, gd) =
+ match gd with
+ | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res
+ | Gfun(Internal f) -> collect_function f
+ | Gvar v -> collect_type v.gvar_info
let collect_program p =
- List.iter collect_globvar p.prog_vars;
- List.iter collect_fundef p.prog_funct
+ List.iter collect_globdef p.prog_defs
let declare_struct_or_union p (name, fld) =
fprintf p "%s;@ @ " name
@@ -550,8 +552,7 @@ let print_program p prog =
fprintf p "@[<v 0>";
StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
StructUnionSet.iter (print_struct_or_union p) !struct_unions;
- List.iter (print_globvar p) prog.prog_vars;
- List.iter (print_fundef p) prog.prog_funct;
+ List.iter (print_globdef p) prog.prog_defs;
fprintf p "@]@."
let destination : string option ref = ref None
diff --git a/common/AST.v b/common/AST.v
index 6425cb0..ccc9dbf 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -118,44 +118,29 @@ Record globvar (V: Type) : Type := mkglobvar {
}.
(** 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 information).
+- a collection of global definitions (name and description);
+- the name of the ``main'' function that serves as entry point in the program.
+A global definition is either a global function or a global variable.
The type of function descriptions and that of additional information
for variables vary among the various intermediate languages and are
taken as parameters to the [program] type. The other parts of whole
programs are common to all languages. *)
-Record program (F V: Type) : Type := mkprogram {
- prog_funct: list (ident * F);
- prog_main: ident;
- prog_vars: list (ident * globvar V)
-}.
+Inductive globdef (F V: Type) : Type :=
+ | Gfun (f: F)
+ | Gvar (v: globvar V).
-Definition funct_names (F: Type) (fl: list (ident * F)) : list ident :=
- map (@fst ident F) fl.
+Implicit Arguments Gfun [F V].
+Implicit Arguments Gvar [F V].
-Lemma funct_names_app : forall (F: Type) (fl1 fl2 : list (ident * F)),
- funct_names (fl1 ++ fl2) = funct_names fl1 ++ funct_names fl2.
-Proof.
- intros; unfold funct_names; apply list_append_map.
-Qed.
-
-Definition var_names (V: Type) (vl: list (ident * globvar V)) : list ident :=
- map (@fst ident (globvar V)) vl.
-
-Lemma var_names_app : forall (V: Type) (vl1 vl2 : list (ident * globvar V)),
- var_names (vl1 ++ vl2) = var_names vl1 ++ funct_names vl2.
-Proof.
- intros; unfold var_names; apply list_append_map.
-Qed.
-
-Definition prog_funct_names (F V: Type) (p: program F V) : list ident :=
- funct_names p.(prog_funct).
+Record program (F V: Type) : Type := mkprogram {
+ prog_defs: list (ident * globdef F V);
+ prog_main: ident
+}.
-Definition prog_var_names (F V: Type) (p: program F V) : list ident :=
- var_names p.(prog_vars).
+Definition prog_defs_names (F V: Type) (p: program F V) : list ident :=
+ List.map fst p.(prog_defs).
(** * Generic transformations over programs *)
@@ -168,253 +153,195 @@ Section TRANSF_PROGRAM.
Variable A B V: Type.
Variable transf: A -> B.
-Definition transf_program (l: list (ident * A)) : list (ident * B) :=
- List.map (fun id_fn => (fst id_fn, transf (snd id_fn))) l.
+Definition transform_program_globdef (idg: ident * globdef A V) : ident * globdef B V :=
+ match idg with
+ | (id, Gfun f) => (id, Gfun (transf f))
+ | (id, Gvar v) => (id, Gvar v)
+ end.
Definition transform_program (p: program A V) : program B V :=
mkprogram
- (transf_program p.(prog_funct))
- p.(prog_main)
- p.(prog_vars).
+ (List.map transform_program_globdef p.(prog_defs))
+ p.(prog_main).
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.
+ In (i, Gfun tf) (transform_program p).(prog_defs) ->
+ exists f, In (i, Gfun f) p.(prog_defs) /\ transf f = tf.
Proof.
- simpl. unfold transf_program. intros.
+ simpl. unfold transform_program. intros.
exploit list_in_map_inv; eauto.
- intros [[i' f] [EQ IN]]. simpl in EQ. inversion EQ; subst.
- exists f; split; auto.
+ intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ.
+ exists f; auto.
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. *)
+(** The following is a more general presentation of [transform_program] where
+ global variable information can be transformed, in addition to function
+ definitions. Moreover, the transformation functions can fail and
+ return an error message. *)
Open Local Scope error_monad_scope.
Open Local Scope string_scope.
-Section MAP_PARTIAL.
+Section TRANSF_PROGRAM_GEN.
-Variable A B C: Type.
-Variable prefix_errmsg: A -> errmsg.
-Variable f: B -> res C.
+Variables A B V W: Type.
+Variable transf_fun: A -> res B.
+Variable transf_var: V -> res W.
+
+Definition transf_globvar (g: globvar V) : res (globvar W) :=
+ do info' <- transf_var g.(gvar_info);
+ OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).
-Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
+Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) :=
match l with
| nil => OK nil
- | (a, b) :: rem =>
- match f b with
- | Error msg => Error (prefix_errmsg a ++ msg)%list
- | OK c =>
- do rem' <- map_partial rem;
- OK ((a, c) :: rem')
+ | (id, Gfun f) :: l' =>
+ match transf_fun f with
+ | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg)
+ | OK tf =>
+ do tl' <- transf_globdefs l'; OK ((id, Gfun tf) :: tl')
+ end
+ | (id, Gvar v) :: l' =>
+ match transf_globvar v with
+ | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg)
+ | OK tv =>
+ do tl' <- transf_globdefs l'; OK ((id, Gvar tv) :: tl')
end
end.
-Remark In_map_partial:
- forall l l' a c,
- map_partial l = OK l' ->
- In (a, c) l' ->
- exists b, In (a, b) l /\ f b = OK c.
-Proof.
- induction l; simpl.
- intros. inv H. elim H0.
- intros until c. destruct a as [a1 b1].
- caseEq (f b1); try congruence.
- intro c1; intros. monadInv H0.
- elim H1; intro. inv H0. exists b1; auto.
- exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
-Qed.
+Definition transform_partial_program2 (p: program A V) : res (program B W) :=
+ do gl' <- transf_globdefs p.(prog_defs); OK(mkprogram gl' p.(prog_main)).
-Remark map_partial_forall2:
- forall l l',
- map_partial l = OK l' ->
- list_forall2
- (fun (a_b: A * B) (a_c: A * C) =>
- fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
- l l'.
+Lemma transform_partial_program2_function:
+ forall p tp i tf,
+ transform_partial_program2 p = OK tp ->
+ In (i, Gfun tf) tp.(prog_defs) ->
+ exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun f = OK tf.
Proof.
- induction l; simpl.
- intros. inv H. constructor.
- intro l'. destruct a as [a b].
- caseEq (f b). 2: congruence. intro c; intros. monadInv H0.
- constructor. simpl. auto. auto.
+ intros. monadInv H. simpl in H0.
+ revert x EQ H0. induction (prog_defs p); simpl; intros.
+ inv EQ. contradiction.
+ destruct a as [id [f|v]].
+ destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ.
+ simpl in H0; destruct H0. inv H. exists f; auto.
+ exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
+ destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ.
+ simpl in H0; destruct H0. inv H.
+ exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
Qed.
-End MAP_PARTIAL.
-
-Remark map_partial_total:
- forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
- map_partial prefix (fun b => OK (f b)) l =
- OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
+Lemma transform_partial_program2_variable:
+ forall p tp i tv,
+ transform_partial_program2 p = OK tp ->
+ In (i, Gvar tv) tp.(prog_defs) ->
+ exists v,
+ In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs)
+ /\ transf_var v = OK tv.(gvar_info).
Proof.
- induction l; simpl.
- auto.
- destruct a as [a1 b1]. rewrite IHl. reflexivity.
+ intros. monadInv H. simpl in H0.
+ revert x EQ H0. induction (prog_defs p); simpl; intros.
+ inv EQ. contradiction.
+ destruct a as [id [f|v]].
+ destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ.
+ simpl in H0; destruct H0. inv H.
+ exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
+ destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ.
+ simpl in H0; destruct H0. inv H.
+ monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto.
+ exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
Qed.
-Remark map_partial_identity:
- forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
- map_partial prefix (fun b => OK b) l = OK l.
+Lemma transform_partial_program2_main:
+ forall p tp,
+ transform_partial_program2 p = OK tp ->
+ tp.(prog_main) = p.(prog_main).
Proof.
- induction l; simpl.
- auto.
- destruct a as [a1 b1]. rewrite IHl. reflexivity.
+ intros. monadInv H. reflexivity.
Qed.
-Section TRANSF_PARTIAL_PROGRAM.
+(** Additionally, we can also "augment" the program with new global definitions
+ and a different "main" function. *)
-Variable A B V: Type.
-Variable transf_partial: A -> res B.
-
-Definition prefix_name (id: ident) : errmsg :=
- MSG "In function " :: CTX id :: MSG ": " :: nil.
+Section AUGMENT.
-Definition transform_partial_program (p: program A V) : res (program B V) :=
- do fl <- map_partial prefix_name transf_partial p.(prog_funct);
- OK (mkprogram fl p.(prog_main) p.(prog_vars)).
+Variable new_globs: list(ident * globdef B W).
+Variable new_main: ident.
-Lemma transform_partial_program_function:
- forall p tp i tf,
- transform_partial_program p = OK tp ->
- In (i, tf) tp.(prog_funct) ->
- exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
-Proof.
- intros. monadInv H. simpl in H0.
- eapply In_map_partial; eauto.
-Qed.
+Definition transform_partial_augment_program (p: program A V) : res (program B W) :=
+ do gl' <- transf_globdefs p.(prog_defs);
+ OK(mkprogram (gl' ++ new_globs) new_main).
-Lemma transform_partial_program_main:
+Lemma transform_partial_augment_program_main:
forall p tp,
- transform_partial_program p = OK tp ->
- tp.(prog_main) = p.(prog_main).
+ transform_partial_augment_program p = OK tp ->
+ tp.(prog_main) = new_main.
Proof.
intros. monadInv H. reflexivity.
Qed.
-Lemma transform_partial_program_vars:
- forall p tp,
- transform_partial_program p = OK tp ->
- tp.(prog_vars) = p.(prog_vars).
+End AUGMENT.
+
+Remark transform_partial_program2_augment:
+ forall p,
+ transform_partial_program2 p =
+ transform_partial_augment_program nil p.(prog_main) p.
Proof.
- intros. monadInv H. reflexivity.
+ unfold transform_partial_program2, transform_partial_augment_program; intros.
+ destruct (transf_globdefs (prog_defs p)); auto.
+ simpl. f_equal. f_equal. rewrite <- app_nil_end. auto.
Qed.
-End TRANSF_PARTIAL_PROGRAM.
+End TRANSF_PROGRAM_GEN.
-(** The following is a variant of [transform_program_partial] where
- both the program functions and the additional variable information
- are transformed by functions that can fail. *)
+(** The following is a special case of [transform_partial_program2],
+ where only function definitions are transformed, but not variable definitions. *)
-Section TRANSF_PARTIAL_PROGRAM2.
-
-Variable A B V W: Type.
-Variable transf_partial_function: A -> res B.
-Variable transf_partial_variable: V -> res W.
-
-Definition transf_globvar (g: globvar V) : res (globvar W) :=
- do info' <- transf_partial_variable g.(gvar_info);
- OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).
-
-Definition transform_partial_program2 (p: program A V) : res (program B W) :=
- do fl <- map_partial prefix_name transf_partial_function p.(prog_funct);
- do vl <- map_partial prefix_name transf_globvar p.(prog_vars);
- OK (mkprogram fl p.(prog_main) vl).
+Section TRANSF_PARTIAL_PROGRAM.
-Lemma transform_partial_program2_function:
- forall p tp i tf,
- transform_partial_program2 p = OK tp ->
- In (i, tf) tp.(prog_funct) ->
- exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
-Proof.
- intros. monadInv H.
- eapply In_map_partial; eauto.
-Qed.
+Variable A B V: Type.
+Variable transf_partial: A -> res B.
-Lemma transform_partial_program2_variable:
- forall p tp i tg,
- transform_partial_program2 p = OK tp ->
- In (i, tg) tp.(prog_vars) ->
- exists v,
- In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars)
- /\ transf_partial_variable v = OK tg.(gvar_info).
-Proof.
- intros. monadInv H. exploit In_map_partial; eauto. intros [g [P Q]].
- monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto.
- Qed.
+Definition transform_partial_program (p: program A V) : res (program B V) :=
+ transform_partial_program2 transf_partial (fun v => OK v) p.
-Lemma transform_partial_program2_main:
+Lemma transform_partial_program_main:
forall p tp,
- transform_partial_program2 p = OK tp ->
+ transform_partial_program p = OK tp ->
tp.(prog_main) = p.(prog_main).
Proof.
- intros. monadInv H. reflexivity.
+ apply transform_partial_program2_main.
Qed.
-End TRANSF_PARTIAL_PROGRAM2.
-
-(** The following is a variant of [transform_partial_program2] where the
- where the set of functions and global data is augmented, and
- the main function is potentially changed. *)
-
-Section TRANSF_PARTIAL_AUGMENT_PROGRAM.
-
-Variable A B V W: Type.
-Variable transf_partial_function: A -> res B.
-Variable transf_partial_variable: V -> res W.
-
-Variable new_functs : list (ident * B).
-Variable new_vars : list (ident * globvar W).
-Variable new_main : ident.
-
-Definition transform_partial_augment_program (p: program A V) : res (program B W) :=
- do fl <- map_partial prefix_name transf_partial_function p.(prog_funct);
- do vl <- map_partial prefix_name (transf_globvar transf_partial_variable) p.(prog_vars);
- OK (mkprogram (fl ++ new_functs) new_main (vl ++ new_vars)).
-
-Lemma transform_partial_augment_program_function:
+Lemma transform_partial_program_function:
forall p tp i tf,
- transform_partial_augment_program p = OK tp ->
- In (i, tf) tp.(prog_funct) ->
- (exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf)
- \/ In (i,tf) new_functs.
-Proof.
- intros. monadInv H. simpl in H0.
- rewrite in_app in H0. destruct H0.
- left. eapply In_map_partial; eauto.
- right. auto.
-Qed.
-
-Lemma transform_partial_augment_program_main:
- forall p tp,
- transform_partial_augment_program p = OK tp ->
- tp.(prog_main) = new_main.
+ transform_partial_program p = OK tp ->
+ In (i, Gfun tf) tp.(prog_defs) ->
+ exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial f = OK tf.
Proof.
- intros. monadInv H. reflexivity.
+ apply transform_partial_program2_function.
Qed.
+End TRANSF_PARTIAL_PROGRAM.
-Lemma transform_partial_augment_program_variable:
- forall p tp i tg,
- transform_partial_augment_program p = OK tp ->
- In (i, tg) tp.(prog_vars) ->
- (exists v, In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars) /\ transf_partial_variable v = OK tg.(gvar_info))
- \/ In (i,tg) new_vars.
+Lemma transform_program_partial_program:
+ forall (A B V: Type) (transf: A -> B) (p: program A V),
+ transform_partial_program (fun f => OK(transf f)) p = OK(transform_program transf p).
Proof.
- intros. monadInv H.
- simpl in H0. rewrite in_app in H0. inversion H0.
- left. exploit In_map_partial; eauto. intros [g [P Q]].
- monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto.
- right. auto.
+ intros.
+ unfold transform_partial_program, transform_partial_program2, transform_program; intros.
+ replace (transf_globdefs (fun f => OK (transf f)) (fun v => OK v) p.(prog_defs))
+ with (OK (map (transform_program_globdef transf) p.(prog_defs))).
+ auto.
+ induction (prog_defs p); simpl.
+ auto.
+ destruct a as [id [f|v]]; rewrite <- IHl.
+ auto.
+ destruct v; auto.
Qed.
-End TRANSF_PARTIAL_AUGMENT_PROGRAM.
-
-
(** The following is a relational presentation of
[transform_partial_augment_preogram]. Given relations between function
definitions and between variable information, it defines a relation
@@ -429,61 +356,50 @@ Variable A B V W: Type.
Variable match_fundef: A -> B -> Prop.
Variable match_varinfo: V -> W -> Prop.
-Inductive match_funct_entry: ident * A -> ident * B -> Prop :=
- | match_funct_entry_intro: forall id fn1 fn2,
- match_fundef fn1 fn2 ->
- match_funct_entry (id, fn1) (id, fn2).
-
-Inductive match_var_entry: ident * globvar V -> ident * globvar W -> Prop :=
- | match_var_entry_intro: forall id info1 info2 init ro vo,
+Inductive match_globdef: ident * globdef A V -> ident * globdef B W -> Prop :=
+ | match_glob_fun: forall id f1 f2,
+ match_fundef f1 f2 ->
+ match_globdef (id, Gfun f1) (id, Gfun f2)
+ | match_glob_var: forall id init ro vo info1 info2,
match_varinfo info1 info2 ->
- match_var_entry (id, mkglobvar info1 init ro vo)
- (id, mkglobvar info2 init ro vo).
+ match_globdef (id, Gvar (mkglobvar info1 init ro vo)) (id, Gvar (mkglobvar info2 init ro vo)).
-Definition match_program (new_functs : list (ident * B))
- (new_vars : list (ident * globvar W))
+Definition match_program (new_globs : list (ident * globdef B W))
(new_main : ident)
(p1: program A V) (p2: program B W) : Prop :=
- (exists tfuncts, list_forall2 match_funct_entry p1.(prog_funct) tfuncts /\
- (p2.(prog_funct) = tfuncts ++ new_functs)) /\
- (exists tvars, list_forall2 match_var_entry p1.(prog_vars) tvars /\
- (p2.(prog_vars) = tvars ++ new_vars)) /\
+ (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\
+ p2.(prog_defs) = tglob ++ new_globs) /\
p2.(prog_main) = new_main.
End MATCH_PROGRAM.
-Remark transform_partial_augment_program_match:
+Lemma transform_partial_augment_program_match:
forall (A B V W: Type)
- (transf_partial_function: A -> res B)
- (transf_partial_variable : V -> res W)
+ (transf_fun: A -> res B)
+ (transf_var: V -> res W)
(p: program A V)
- (new_functs : list (ident * B))
- (new_vars : list (ident * globvar W))
+ (new_globs : list (ident * globdef B W))
(new_main : ident)
(tp: program B W),
- transform_partial_augment_program transf_partial_function transf_partial_variable new_functs new_vars new_main p = OK tp ->
+ transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK tp ->
match_program
- (fun fd tfd => transf_partial_function fd = OK tfd)
- (fun info tinfo => transf_partial_variable info = OK tinfo)
- new_functs new_vars new_main
+ (fun fd tfd => transf_fun fd = OK tfd)
+ (fun info tinfo => transf_var info = OK tinfo)
+ new_globs new_main
p tp.
Proof.
- intros. unfold transform_partial_augment_program in H. monadInv H. split.
- exists x. split.
- apply list_forall2_imply with
- (fun (ab: ident * A) (ac: ident * B) =>
- fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
- eapply map_partial_forall2. eauto.
- intros. destruct v1; destruct v2; simpl in *.
- destruct H1; subst. constructor. auto.
- auto.
- split. exists x0. split.
- apply list_forall2_imply with
- (fun (ab: ident * globvar V) (ac: ident * globvar W) =>
- fst ab = fst ac /\ transf_globvar transf_partial_variable (snd ab) = OK (snd ac)).
- eapply map_partial_forall2. eauto.
- intros. destruct v1; destruct v2; simpl in *. destruct H1; subst.
- monadInv H2. destruct g; simpl in *. constructor. auto. auto. auto.
+ unfold transform_partial_augment_program; intros. monadInv H.
+ red; simpl. split; auto. exists x; split; auto.
+ revert x EQ. generalize (prog_defs p). induction l; simpl; intros.
+ monadInv EQ. constructor.
+ destruct a as [id [f|v]].
+ (* function *)
+ destruct (transf_fun f) as [tf|?]_eqn; monadInv EQ.
+ constructor; auto. constructor; auto.
+ (* variable *)
+ unfold transf_globvar in EQ.
+ destruct (transf_var (gvar_info v)) as [tinfo|?]_eqn; simpl in EQ; monadInv EQ.
+ constructor; auto. destruct v; simpl in *. constructor; auto.
Qed.
(** * External functions *)
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index ba038f8..8565ae6 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -69,13 +69,13 @@ Record t: Type := mkgenv {
genv_symb: PTree.t block; (**r mapping symbol -> block *)
genv_funs: ZMap.t (option F); (**r mapping function pointer -> definition *)
genv_vars: ZMap.t (option (globvar V)); (**r mapping variable pointer -> info *)
- genv_nextfun: block; (**r next function pointer *)
- genv_nextvar: block; (**r next variable pointer *)
- genv_nextfun_neg: genv_nextfun < 0;
- genv_nextvar_pos: genv_nextvar > 0;
- genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> b <> 0 /\ genv_nextfun < b /\ b < genv_nextvar;
- genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> genv_nextfun < b < 0;
- genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_nextvar;
+ genv_next: block; (**r next symbol pointer *)
+ genv_next_pos: genv_next > 0;
+ genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> 0 < b < genv_next;
+ genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> 0 < b < genv_next;
+ genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_next;
+ genv_funs_vars: forall b1 b2 f v,
+ ZMap.get b1 genv_funs = Some f -> ZMap.get b2 genv_vars = Some v -> b1 <> b2;
genv_vars_inj: forall id1 id2 b,
PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2
}.
@@ -117,69 +117,53 @@ Definition find_var_info (ge: t) (b: block) : option (globvar V) :=
(** ** Constructing the global environment *)
-Program Definition add_function (ge: t) (idf: ident * F) : t :=
+Program Definition add_global (ge: t) (idg: ident * globdef F V) : t :=
@mkgenv
- (PTree.set idf#1 ge.(genv_nextfun) ge.(genv_symb))
- (ZMap.set ge.(genv_nextfun) (Some idf#2) ge.(genv_funs))
- ge.(genv_vars)
- (ge.(genv_nextfun) - 1)
- ge.(genv_nextvar)
+ (PTree.set idg#1 ge.(genv_next) ge.(genv_symb))
+ (match idg#2 with
+ | Gfun f => ZMap.set ge.(genv_next) (Some f) ge.(genv_funs)
+ | Gvar v => ge.(genv_funs)
+ end)
+ (match idg#2 with
+ | Gfun f => ge.(genv_vars)
+ | Gvar v => ZMap.set ge.(genv_next) (Some v) ge.(genv_vars)
+ end)
+ (ge.(genv_next) + 1)
_ _ _ _ _ _.
Next Obligation.
destruct ge; simpl; omega.
Qed.
Next Obligation.
- destruct ge; auto.
-Qed.
-Next Obligation.
destruct ge; simpl in *.
rewrite PTree.gsspec in H. destruct (peq id i). inv H. unfold block; omega.
exploit genv_symb_range0; eauto. unfold block; omega.
Qed.
Next Obligation.
- destruct ge; simpl in *. rewrite ZMap.gsspec in H.
- destruct (ZIndexed.eq b genv_nextfun0). subst; omega.
+ destruct ge; simpl in *.
+ destruct g.
+ rewrite ZMap.gsspec in H.
+ destruct (ZIndexed.eq b genv_next0). subst; omega.
+ exploit genv_funs_range0; eauto. omega.
exploit genv_funs_range0; eauto. omega.
-Qed.
-Next Obligation.
- destruct ge; eauto.
Qed.
Next Obligation.
destruct ge; simpl in *.
- rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0.
- destruct (peq id1 i); destruct (peq id2 i).
- congruence.
- exploit genv_symb_range0; eauto. intros [A B]. inv H. omegaContradiction.
- exploit genv_symb_range0; eauto. intros [A B]. inv H0. omegaContradiction.
- eauto.
-Qed.
-
-Program Definition add_variable (ge: t) (idv: ident * globvar V) : t :=
- @mkgenv
- (PTree.set idv#1 ge.(genv_nextvar) ge.(genv_symb))
- ge.(genv_funs)
- (ZMap.set ge.(genv_nextvar) (Some idv#2) ge.(genv_vars))
- ge.(genv_nextfun)
- (ge.(genv_nextvar) + 1)
- _ _ _ _ _ _.
-Next Obligation.
- destruct ge; auto.
-Qed.
-Next Obligation.
- destruct ge; simpl; omega.
-Qed.
-Next Obligation.
- destruct ge; simpl in *.
- rewrite PTree.gsspec in H. destruct (peq id i). inv H. unfold block; omega.
- exploit genv_symb_range0; eauto. unfold block; omega.
-Qed.
-Next Obligation.
- destruct ge; eauto.
+ destruct g.
+ exploit genv_vars_range0; eauto. omega.
+ rewrite ZMap.gsspec in H.
+ destruct (ZIndexed.eq b genv_next0). subst; omega.
+ exploit genv_vars_range0; eauto. omega.
Qed.
Next Obligation.
- destruct ge; simpl in *. rewrite ZMap.gsspec in H.
- destruct (ZIndexed.eq b genv_nextvar0). subst; omega.
- exploit genv_vars_range0; eauto. omega.
+ destruct ge; simpl in *. destruct g.
+ rewrite ZMap.gsspec in H.
+ destruct (ZIndexed.eq b1 genv_next0). inv H.
+ exploit genv_vars_range0; eauto. unfold ZIndexed.t; omega.
+ eauto.
+ rewrite ZMap.gsspec in H0.
+ destruct (ZIndexed.eq b2 genv_next0). inv H.
+ exploit genv_funs_range0; eauto. unfold ZIndexed.t; omega.
+ eauto.
Qed.
Next Obligation.
destruct ge; simpl in *.
@@ -191,16 +175,26 @@ Next Obligation.
eauto.
Qed.
+Definition add_globals (ge: t) (gl: list (ident * globdef F V)) : t :=
+ List.fold_left add_global gl ge.
+
+Lemma add_globals_app:
+ forall gl2 gl1 ge,
+ add_globals ge (gl1 ++ gl2) = add_globals (add_globals ge gl1) gl2.
+Proof.
+ induction gl1; simpl; intros. auto. rewrite IHgl1; auto.
+Qed.
+
Program Definition empty_genv : t :=
- @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) (-1) 1 _ _ _ _ _ _.
+ @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) 1 _ _ _ _ _ _.
Next Obligation.
omega.
Qed.
Next Obligation.
- omega.
+ rewrite PTree.gempty in H. discriminate.
Qed.
Next Obligation.
- rewrite PTree.gempty in H. discriminate.
+ rewrite ZMap.gi in H. discriminate.
Qed.
Next Obligation.
rewrite ZMap.gi in H. discriminate.
@@ -212,27 +206,54 @@ Next Obligation.
rewrite PTree.gempty in H. discriminate.
Qed.
-Definition add_functions (ge: t) (fl: list (ident * F)) : t :=
- List.fold_left add_function fl ge.
+Definition globalenv (p: program F V) :=
+ add_globals empty_genv p.(prog_defs).
-Lemma add_functions_app : forall ge fl1 fl2,
- add_functions ge (fl1 ++ fl2) = add_functions (add_functions ge fl1) fl2.
-Proof.
- intros. unfold add_functions. rewrite fold_left_app. auto.
-Qed.
+(** Proof principles *)
+Section GLOBALENV_PRINCIPLES.
-Definition add_variables (ge: t) (vl: list (ident * globvar V)) : t :=
- List.fold_left add_variable vl ge.
+Variable P: t -> Prop.
-Lemma add_variables_app : forall ge vl1 vl2 ,
- add_variables ge (vl1 ++ vl2) = add_variables (add_variables ge vl1) vl2.
-Proof.
- intros. unfold add_variables. rewrite fold_left_app. auto.
+Lemma add_globals_preserves:
+ forall gl ge,
+ (forall ge id g, P ge -> In (id, g) gl -> P (add_global ge (id, g))) ->
+ P ge -> P (add_globals ge gl).
+Proof.
+ induction gl; simpl; intros.
+ auto.
+ destruct a. apply IHgl; auto.
Qed.
-Definition globalenv (p: program F V) :=
- add_variables (add_functions empty_genv p.(prog_funct)) p.(prog_vars).
+Lemma add_globals_ensures:
+ forall id g gl ge,
+ (forall ge id g, P ge -> In (id, g) gl -> P (add_global ge (id, g))) ->
+ (forall ge, P (add_global ge (id, g))) ->
+ In (id, g) gl -> P (add_globals ge gl).
+Proof.
+ induction gl; simpl; intros.
+ contradiction.
+ destruct H1. subst a. apply add_globals_preserves; auto.
+ apply IHgl; auto.
+Qed.
+
+Lemma add_globals_norepet_ensures:
+ forall id g gl ge,
+ (forall ge id1 g1, P ge -> In (id1, g1) gl -> id1 <> id -> P (add_global ge (id1, g1))) ->
+ (forall ge, P (add_global ge (id, g))) ->
+ In (id, g) gl -> list_norepet (map fst gl) -> P (add_globals ge gl).
+Proof.
+ induction gl; simpl; intros.
+ contradiction.
+ inv H2.
+ destruct H1. subst a. simpl in H5.
+ apply add_globals_preserves; auto.
+ intros. apply H. auto. auto. red; intros; subst id0. elim H5.
+ change id with (fst (id, g0)). apply List.in_map; auto.
+ apply IHgl; auto.
+Qed.
+
+End GLOBALENV_PRINCIPLES.
(** ** Properties of the operations over global environments *)
@@ -254,298 +275,132 @@ Proof.
Qed.
Theorem find_symbol_exists:
- forall p id gv,
- In (id, gv) (prog_vars p) ->
+ forall p id g,
+ In (id, g) (prog_defs p) ->
exists b, find_symbol (globalenv p) id = Some b.
Proof.
- intros until gv.
- assert (forall vl ge,
- (exists b, find_symbol ge id = Some b) ->
- exists b, find_symbol (add_variables ge vl) id = Some b).
- unfold find_symbol; induction vl; simpl; intros. auto. apply IHvl.
- simpl. rewrite PTree.gsspec. fold ident. destruct (peq id a#1).
- exists (genv_nextvar ge); auto. auto.
-
- assert (forall vl ge, In (id, gv) vl ->
- exists b, find_symbol (add_variables ge vl) id = Some b).
- unfold find_symbol; induction vl; simpl; intros. contradiction.
- destruct H0. apply H. subst; unfold find_symbol; simpl.
- rewrite PTree.gss. exists (genv_nextvar ge); auto.
- eauto.
+ intros. unfold globalenv. eapply add_globals_ensures; eauto.
+(* preserves *)
+ intros. unfold find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id0).
+ econstructor; eauto.
+ auto.
+(* ensures *)
+ intros. unfold find_symbol; simpl. rewrite PTree.gss. econstructor; eauto.
+Qed.
- intros. unfold globalenv; eauto.
+Theorem find_funct_ptr_exists:
+ forall p id f,
+ list_norepet (prog_defs_names p) ->
+ In (id, Gfun f) (prog_defs p) ->
+ exists b,
+ find_symbol (globalenv p) id = Some b
+ /\ find_funct_ptr (globalenv p) b = Some f.
+Proof.
+ intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto.
+(* preserves *)
+ intros. unfold find_symbol, find_funct_ptr in *; simpl.
+ destruct H1 as [b [A B]]. exists b; split.
+ rewrite PTree.gso; auto.
+ destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto.
+ exploit genv_funs_range; eauto. unfold ZIndexed.t; omega.
+ auto.
+(* ensures *)
+ intros. unfold find_symbol, find_funct_ptr in *; simpl.
+ exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss.
Qed.
Theorem find_var_exists:
- forall p id gv,
- list_norepet (prog_var_names p) ->
- In (id, gv) (prog_vars p) ->
+ forall p id v,
+ list_norepet (prog_defs_names p) ->
+ In (id, Gvar v) (prog_defs p) ->
exists b,
find_symbol (globalenv p) id = Some b
- /\ find_var_info (globalenv p) b = Some gv.
-Proof.
- intros until gv.
- assert (forall vl ge,
- ~In id (var_names vl) ->
- (exists b, find_symbol ge id = Some b /\ find_var_info ge b = Some gv) ->
- (exists b, find_symbol (add_variables ge vl) id = Some b
- /\ find_var_info (add_variables ge vl) b = Some gv)).
- induction vl; simpl; intros.
- auto.
- apply IHvl. tauto. destruct a as [id1 gv1]. destruct H0 as [b [P Q]].
- unfold add_variable, find_symbol, find_var_info; simpl.
- exists b; split. rewrite PTree.gso. auto. intuition.
- rewrite ZMap.gso. auto. exploit genv_vars_range; eauto.
- unfold ZIndexed.t; omega.
-
- unfold globalenv, prog_var_names.
- generalize (prog_vars p) (add_functions empty_genv (prog_funct p)).
- induction l; simpl; intros.
- contradiction.
- destruct a as [id1 gv1]; simpl in *. inv H0.
- destruct H1. inv H0.
- apply H; auto.
- exists (genv_nextvar t0); split.
- unfold find_symbol, add_variable; simpl. apply PTree.gss.
- unfold find_var_info, add_variable; simpl. apply ZMap.gss.
- apply IHl; auto.
-Qed.
-
-Remark add_variables_inversion : forall vs e x b,
- find_symbol (add_variables e vs) x = Some b ->
- In x (var_names vs) \/ find_symbol e x = Some b.
-Proof.
- induction vs; intros.
- simpl in H. intuition.
- simpl in H. destruct (IHvs _ _ _ H).
- left. simpl. intuition.
- destruct a as [y ?].
- unfold add_variable, find_symbol in H0. simpl in H0.
- rewrite PTree.gsspec in H0. destruct (peq x y); subst; simpl; intuition.
-Qed.
-
-Remark add_functions_inversion : forall fs e x b,
- find_symbol (add_functions e fs) x = Some b ->
- In x (funct_names fs) \/ find_symbol e x = Some b.
-Proof.
- induction fs; intros.
- simpl in H. intuition.
- simpl in H. destruct (IHfs _ _ _ H).
- left. simpl. intuition.
- destruct a as [y ?].
- unfold add_variable, find_symbol in H0. simpl in H0.
- rewrite PTree.gsspec in H0. destruct (peq x y); subst; simpl; intuition.
+ /\ find_var_info (globalenv p) b = Some v.
+Proof.
+ intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto.
+(* preserves *)
+ intros. unfold find_symbol, find_var_info in *; simpl.
+ destruct H1 as [b [A B]]. exists b; split.
+ rewrite PTree.gso; auto.
+ destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto.
+ exploit genv_vars_range; eauto. unfold ZIndexed.t; omega.
+(* ensures *)
+ intros. unfold find_symbol, find_var_info in *; simpl.
+ exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss.
Qed.
Lemma find_symbol_inversion : forall p x b,
find_symbol (globalenv p) x = Some b ->
- In x (prog_var_names p ++ prog_funct_names p).
-Proof.
- unfold prog_var_names, prog_funct_names, globalenv.
- intros.
- apply in_app.
- apply add_variables_inversion in H. intuition.
- apply add_functions_inversion in H0. inversion H0. intuition.
- unfold find_symbol in H.
- rewrite PTree.gempty in H. inversion H.
-Qed.
-
-
-Remark add_functions_same_symb:
- forall id fl ge,
- ~In id (funct_names fl) ->
- find_symbol (add_functions ge fl) id = find_symbol ge id.
-Proof.
- induction fl; simpl; intros. auto.
- rewrite IHfl. unfold find_symbol; simpl. apply PTree.gso. intuition. intuition.
-Qed.
-
-Remark add_functions_same_address:
- forall b fl ge,
- b > ge.(genv_nextfun) ->
- find_funct_ptr (add_functions ge fl) b = find_funct_ptr ge b.
-Proof.
- induction fl; simpl; intros. auto.
- rewrite IHfl. unfold find_funct_ptr; simpl. apply ZMap.gso.
- red; intros; subst b; omegaContradiction.
- simpl. omega.
-Qed.
-
-Remark add_variables_same_symb:
- forall id vl ge,
- ~In id (var_names vl) ->
- find_symbol (add_variables ge vl) id = find_symbol ge id.
+ In x (prog_defs_names p).
Proof.
- induction vl; simpl; intros. auto.
- rewrite IHvl. unfold find_symbol; simpl. apply PTree.gso. intuition. intuition.
-Qed.
-
-Remark add_variables_same_address:
- forall b vl ge,
- b < ge.(genv_nextvar) ->
- find_var_info (add_variables ge vl) b = find_var_info ge b.
-Proof.
- induction vl; simpl; intros. auto.
- rewrite IHvl. unfold find_var_info; simpl. apply ZMap.gso.
- red; intros; subst b; omegaContradiction.
- simpl. omega.
-Qed.
-
-Remark add_variables_same_funs:
- forall b vl ge, find_funct_ptr (add_variables ge vl) b = find_funct_ptr ge b.
-Proof.
- induction vl; simpl; intros. auto. rewrite IHvl. auto.
+ intros until b; unfold globalenv. eapply add_globals_preserves.
+(* preserves *)
+ unfold find_symbol; simpl; intros. rewrite PTree.gsspec in H1.
+ destruct (peq x id). subst x. change id with (fst (id, g)). apply List.in_map; auto.
+ auto.
+(* base *)
+ unfold find_symbol; simpl; intros. rewrite PTree.gempty in H. discriminate.
Qed.
-Remark add_functions_nextvar:
- forall fl ge, genv_nextvar (add_functions ge fl) = genv_nextvar ge.
+Theorem find_funct_ptr_inversion:
+ forall p b f,
+ find_funct_ptr (globalenv p) b = Some f ->
+ exists id, In (id, Gfun f) (prog_defs p).
Proof.
- induction fl; simpl; intros. auto. rewrite IHfl. auto.
+ intros until f. unfold globalenv. apply add_globals_preserves.
+(* preserves *)
+ unfold find_funct_ptr; simpl; intros. destruct g; auto.
+ rewrite ZMap.gsspec in H1. destruct (ZIndexed.eq b (genv_next ge)).
+ inv H1. exists id; auto.
+ auto.
+(* base *)
+ unfold find_funct_ptr; simpl; intros. rewrite ZMap.gi in H. discriminate.
Qed.
-Remark add_variables_nextvar:
- forall vl ge, genv_nextvar (add_variables ge vl) = genv_nextvar ge + Z_of_nat(List.length vl).
+Theorem find_funct_inversion:
+ forall p v f,
+ find_funct (globalenv p) v = Some f ->
+ exists id, In (id, Gfun f) (prog_defs p).
Proof.
- induction vl; intros.
- simpl. unfold block; omega.
- simpl length; rewrite inj_S; simpl. rewrite IHvl. simpl. unfold block; omega.
-Qed.
-
-Theorem find_funct_ptr_exists:
- forall p id f,
- list_norepet (prog_funct_names p) ->
- list_disjoint (prog_funct_names p) (prog_var_names p) ->
- In (id, f) (prog_funct p) ->
- exists b, find_symbol (globalenv p) id = Some b
- /\ find_funct_ptr (globalenv p) b = Some f.
-Proof.
- intros until f.
-
- assert (forall fl ge, In (id, f) fl -> list_norepet (funct_names fl) ->
- exists b, find_symbol (add_functions ge fl) id = Some b
- /\ find_funct_ptr (add_functions ge fl) b = Some f).
- induction fl; simpl; intros. contradiction. inv H0.
- destruct H. subst a. exists (genv_nextfun ge); split.
- rewrite add_functions_same_symb; auto. unfold find_symbol; simpl. apply PTree.gss.
- rewrite add_functions_same_address. unfold find_funct_ptr; simpl. apply ZMap.gss.
- simpl; omega.
- apply IHfl; auto.
-
- intros. exploit (H p.(prog_funct) empty_genv); eauto. intros [b [A B]].
- unfold globalenv; exists b; split.
- rewrite add_variables_same_symb. auto. eapply list_disjoint_notin; eauto.
- unfold prog_funct_names. change id with (fst (id, f)). apply in_map; auto.
- rewrite add_variables_same_funs. auto.
+ intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v.
+ rewrite find_funct_find_funct_ptr in H.
+ eapply find_funct_ptr_inversion; eauto.
Qed.
Theorem find_funct_ptr_prop:
forall (P: F -> Prop) p b f,
- (forall id f, In (id, f) (prog_funct p) -> P f) ->
+ (forall id f, In (id, Gfun f) (prog_defs p) -> P f) ->
find_funct_ptr (globalenv p) b = Some f ->
P f.
Proof.
- intros until f. intros PROP.
- assert (forall fl ge,
- List.incl fl (prog_funct p) ->
- match find_funct_ptr ge b with None => True | Some f => P f end ->
- match find_funct_ptr (add_functions ge fl) b with None => True | Some f => P f end).
- induction fl; simpl; intros. auto.
- apply IHfl. eauto with coqlib. unfold find_funct_ptr; simpl.
- destruct a as [id' f']; simpl.
- rewrite ZMap.gsspec. destruct (ZIndexed.eq b (genv_nextfun ge)).
- apply PROP with id'. apply H. auto with coqlib.
- assumption.
-
- unfold globalenv. rewrite add_variables_same_funs. intro.
- exploit (H p.(prog_funct) empty_genv). auto with coqlib.
- unfold find_funct_ptr; simpl. rewrite ZMap.gi. auto.
- rewrite H0. auto.
+ intros. exploit find_funct_ptr_inversion; eauto. intros [id IN]. eauto.
Qed.
Theorem find_funct_prop:
forall (P: F -> Prop) p v f,
- (forall id f, In (id, f) (prog_funct p) -> P f) ->
+ (forall id f, In (id, Gfun f) (prog_defs p) -> P f) ->
find_funct (globalenv p) v = Some f ->
P f.
Proof.
- intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v.
- rewrite find_funct_find_funct_ptr in H0.
- eapply find_funct_ptr_prop; eauto.
-Qed.
-
-Theorem find_funct_ptr_inversion:
- forall p b f,
- find_funct_ptr (globalenv p) b = Some f ->
- exists id, In (id, f) (prog_funct p).
-Proof.
- intros. pattern f. apply find_funct_ptr_prop with p b; auto.
- intros. exists id; auto.
-Qed.
-
-Theorem find_funct_inversion:
- forall p v f,
- find_funct (globalenv p) v = Some f ->
- exists id, In (id, f) (prog_funct p).
-Proof.
- intros. pattern f. apply find_funct_prop with p v; auto.
- intros. exists id; auto.
-Qed.
-
-Theorem find_funct_ptr_negative:
- forall p b f,
- find_funct_ptr (globalenv p) b = Some f -> b < 0.
-Proof.
- unfold find_funct_ptr. intros. destruct (globalenv p). simpl in H.
- exploit genv_funs_range0; eauto. omega.
-Qed.
-
-Theorem find_var_info_positive:
- forall p b v,
- find_var_info (globalenv p) b = Some v -> b > 0.
-Proof.
- unfold find_var_info. intros. destruct (globalenv p). simpl in H.
- exploit genv_vars_range0; eauto. omega.
-Qed.
-
-Remark add_variables_symb_neg:
- forall id b vl ge,
- find_symbol (add_variables ge vl) id = Some b -> b < 0 ->
- find_symbol ge id = Some b.
-Proof.
- induction vl; simpl; intros. auto.
- exploit IHvl; eauto. unfold find_symbol; simpl. rewrite PTree.gsspec.
- fold ident. destruct (peq id (a#1)); auto. intros. inv H1.
- generalize (genv_nextvar_pos ge). intros. omegaContradiction.
+ intros. exploit find_funct_inversion; eauto. intros [id IN]. eauto.
Qed.
Theorem find_funct_ptr_symbol_inversion:
forall p id b 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 fl ge,
- find_symbol (add_functions ge fl) id = Some b ->
- find_funct_ptr (add_functions ge fl) b = Some f ->
- In (id, f) fl \/ (find_symbol ge id = Some b /\ find_funct_ptr ge b = Some f)).
- induction fl; simpl; intros.
+ In (id, Gfun f) p.(prog_defs).
+Proof.
+ intros until f. unfold globalenv, find_symbol, find_funct_ptr. apply add_globals_preserves.
+(* preserves *)
+ intros. simpl in *. rewrite PTree.gsspec in H1. destruct (peq id id0).
+ inv H1. destruct g as [f1|v1]. rewrite ZMap.gss in H2. inv H2. auto.
+ exploit genv_funs_range; eauto. intros. omegaContradiction.
+ destruct g as [f1|v1]. rewrite ZMap.gso in H2. auto.
+ exploit genv_symb_range; eauto. unfold ZIndexed.t; omega.
auto.
- exploit IHfl; eauto. intros [A | [A B]]. auto.
- destruct a as [id' f'].
- unfold find_symbol in A; simpl in A.
- unfold find_funct_ptr in B; simpl in B.
- rewrite PTree.gsspec in A. destruct (peq id id'). inv A.
- rewrite ZMap.gss in B. inv B. auto.
- rewrite ZMap.gso in B. right; auto.
- exploit genv_symb_range; eauto. unfold block, ZIndexed.t; omega.
-
- intros. assert (b < 0) by (eapply find_funct_ptr_negative; eauto).
- unfold globalenv in *. rewrite add_variables_same_funs in H1.
- exploit (H (prog_funct p) empty_genv).
- eapply add_variables_symb_neg; eauto. auto.
- intuition. unfold find_symbol in H3; simpl in H3. rewrite PTree.gempty in H3. discriminate.
+(* initial *)
+ intros. simpl in *. rewrite PTree.gempty in H. discriminate.
Qed.
Theorem find_symbol_not_nullptr:
@@ -553,7 +408,7 @@ Theorem find_symbol_not_nullptr:
find_symbol (globalenv p) id = Some b -> b <> Mem.nullptr.
Proof.
intros until b. unfold find_symbol. destruct (globalenv p); simpl.
- intros. exploit genv_symb_range0; eauto. intuition.
+ intros. exploit genv_symb_range0; eauto. unfold Mem.nullptr, block. omega.
Qed.
Theorem global_addresses_distinct:
@@ -599,6 +454,16 @@ Proof.
congruence.
Qed.
+Remark genv_next_add_globals:
+ forall gl ge,
+ genv_next (add_globals ge gl) = genv_next ge + Z_of_nat (length gl).
+Proof.
+ induction gl; intros.
+ simpl. unfold block; omega.
+ simpl add_globals; simpl length; rewrite inj_S.
+ rewrite IHgl. simpl. unfold block; omega.
+Qed.
+
(** * Construction of the initial memory state *)
Section INITMEM.
@@ -622,6 +487,18 @@ Proof.
destruct i; simpl; try omega. generalize (Zle_max_r z 0). omega.
Qed.
+Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem :=
+ if zle n 0 then Some m else
+ let n' := n - 1 in
+ match Mem.store Mint8unsigned m b p Vzero with
+ | Some m' => store_zeros m' b (p + 1) n'
+ | None => None
+ end.
+Proof.
+ intros. red. omega.
+ apply Zwf_well_founded.
+Qed.
+
Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option mem :=
match id with
| Init_int8 n => Mem.store Mint8unsigned m b p (Vint n)
@@ -648,18 +525,6 @@ Fixpoint store_init_data_list (m: mem) (b: block) (p: Z) (idl: list init_data)
end
end.
-Function store_zeros (m: mem) (b: block) (n: Z) {wf (Zwf 0) n}: option mem :=
- if zle n 0 then Some m else
- let n' := n - 1 in
- match Mem.store Mint8unsigned m b n' Vzero with
- | Some m' => store_zeros m' b n'
- | None => None
- end.
-Proof.
- intros. red. omega.
- apply Zwf_well_founded.
-Qed.
-
Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
match il with
| nil => 0
@@ -671,37 +536,54 @@ Definition perm_globvar (gv: globvar V) : permission :=
else if gv.(gvar_readonly) then Readable
else Writable.
-Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem :=
- let init := idv#2.(gvar_init) in
- let sz := init_data_list_size init in
- let (m1, b) := Mem.alloc m 0 sz in
- match store_zeros m1 b sz with
- | None => None
- | Some m2 =>
- match store_init_data_list m2 b 0 init with
+Definition alloc_global (m: mem) (idg: ident * globdef F V): option mem :=
+ match idg with
+ | (id, Gfun f) =>
+ let (m1, b) := Mem.alloc m 0 1 in
+ Mem.drop_perm m1 b 0 1 Nonempty
+ | (id, Gvar v) =>
+ let init := v.(gvar_init) in
+ let sz := init_data_list_size init in
+ let (m1, b) := Mem.alloc m 0 sz in
+ match store_zeros m1 b 0 sz with
| None => None
- | Some m3 => Mem.drop_perm m3 b 0 sz (perm_globvar idv#2)
+ | Some m2 =>
+ match store_init_data_list m2 b 0 init with
+ | None => None
+ | Some m3 => Mem.drop_perm m3 b 0 sz (perm_globvar v)
+ end
end
end.
-Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V))
- {struct vl} : option mem :=
- match vl with
+Fixpoint alloc_globals (m: mem) (gl: list (ident * globdef F V))
+ {struct gl} : option mem :=
+ match gl with
| nil => Some m
- | v :: vl' =>
- match alloc_variable m v with
+ | g :: gl' =>
+ match alloc_global m g with
| None => None
- | Some m' => alloc_variables m' vl'
+ | Some m' => alloc_globals m' gl'
end
end.
-Lemma alloc_variables_app : forall vl1 vl2 m m1,
- alloc_variables m vl1 = Some m1 ->
- alloc_variables m1 vl2 = alloc_variables m (vl1 ++ vl2).
+Lemma alloc_globals_app : forall gl1 gl2 m m1,
+ alloc_globals m gl1 = Some m1 ->
+ alloc_globals m1 gl2 = alloc_globals m (gl1 ++ gl2).
+Proof.
+ induction gl1.
+ simpl. intros. inversion H; subst. auto.
+ simpl. intros. destruct (alloc_global m a); eauto. inversion H.
+Qed.
+
+(** Next-block properties *)
+
+Remark store_zeros_nextblock:
+ forall m b p n m', store_zeros m b p n = Some m' -> Mem.nextblock m' = Mem.nextblock m.
Proof.
- induction vl1.
- simpl. intros. inversion H; subst. auto.
- simpl. intros. destruct (alloc_variable m a); eauto. inversion H.
+ intros until n. functional induction (store_zeros m b p n); intros.
+ inv H; auto.
+ rewrite IHo; eauto with mem.
+ congruence.
Qed.
Remark store_init_data_list_nextblock:
@@ -714,71 +596,52 @@ Proof.
caseEq (store_init_data m b p a); try congruence. intros.
transitivity (Mem.nextblock m0). eauto.
destruct a; simpl in H; try (eapply Mem.nextblock_store; eauto; fail).
- congruence.
- destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto.
-Qed.
-
-Remark store_zeros_nextblock:
- forall m b n m', store_zeros m b n = Some m' -> Mem.nextblock m' = Mem.nextblock m.
-Proof.
- intros until n. functional induction (store_zeros m b n); intros.
- inv H; auto.
- rewrite IHo; eauto with mem.
congruence.
+ destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto.
Qed.
-Remark alloc_variable_nextblock:
- forall v m m',
- alloc_variable m v = Some m' ->
+Remark alloc_global_nextblock:
+ forall g m m',
+ alloc_global m g = Some m' ->
Mem.nextblock m' = Zsucc(Mem.nextblock m).
Proof.
- unfold alloc_variable.
- intros until m'.
- set (init := gvar_init v#2).
- set (sz := init_data_list_size init).
- caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
- caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
- caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
- caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar v#2)); try congruence. intros m4 DROP REC.
- inv REC; subst.
- rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
- rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
- rewrite (store_zeros_nextblock _ _ _ STZ).
- rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC).
- auto.
-Qed.
-
-
-Remark alloc_variables_nextblock:
- forall vl m m',
- alloc_variables m vl = Some m' ->
- Mem.nextblock m' = Mem.nextblock m + Z_of_nat(List.length vl).
-Proof.
- induction vl.
+ unfold alloc_global. intros.
+ destruct g as [id [f|v]].
+ (* function *)
+ destruct (Mem.alloc m 0 1) as [m1 b]_eqn.
+ erewrite Mem.nextblock_drop; eauto. erewrite Mem.nextblock_alloc; eauto.
+ (* variable *)
+ set (init := gvar_init v) in *.
+ set (sz := init_data_list_size init) in *.
+ destruct (Mem.alloc m 0 sz) as [m1 b]_eqn.
+ destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate.
+ destruct (store_init_data_list m2 b 0 init) as [m3|]_eqn; try discriminate.
+ erewrite Mem.nextblock_drop; eauto.
+ erewrite store_init_data_list_nextblock; eauto.
+ erewrite store_zeros_nextblock; eauto.
+ erewrite Mem.nextblock_alloc; eauto.
+Qed.
+
+Remark alloc_globals_nextblock:
+ forall gl m m',
+ alloc_globals m gl = Some m' ->
+ Mem.nextblock m' = Mem.nextblock m + Z_of_nat(List.length gl).
+Proof.
+ induction gl.
simpl; intros. inv H; unfold block; omega.
- simpl length; rewrite inj_S; simpl. intros m m'.
- unfold alloc_variable.
- set (init := gvar_init a#2).
- set (sz := init_data_list_size init).
- caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
- caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
- caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
- caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC.
- rewrite (IHvl _ _ REC).
- rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
- rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
- rewrite (store_zeros_nextblock _ _ _ STZ).
- rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC).
- unfold block in *; omega.
+ simpl length; rewrite inj_S; simpl; intros.
+ destruct (alloc_global m a) as [m1|]_eqn; try discriminate.
+ erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto. unfold block; omega.
Qed.
+(** Permissions *)
Remark store_zeros_perm:
- forall k prm b' q m b n m',
- store_zeros m b n = Some m' ->
+ forall k prm b' q m b p n m',
+ store_zeros m b p n = Some m' ->
(Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
Proof.
- intros until n. functional induction (store_zeros m b n); intros.
+ intros until n. functional induction (store_zeros m b p n); intros.
inv H; tauto.
destruct (IHo _ H); intros. split; eauto with mem.
congruence.
@@ -793,56 +656,74 @@ Proof.
intros. inv H. tauto.
caseEq (store_init_data m b p a); try congruence. intros.
rewrite <- (IHidl _ _ _ _ H0).
- destruct a; simpl in H; split; eauto with mem.
- inv H; auto. inv H; auto.
- destruct (find_symbol ge i); try congruence. eauto with mem.
- destruct (find_symbol ge i); try congruence. eauto with mem.
+ assert (forall chunk v,
+ Mem.store chunk m b p v = Some m0 ->
+ (Mem.perm m b' q k prm <-> Mem.perm m0 b' q k prm)).
+ intros; split; eauto with mem.
+ destruct a; simpl in H; eauto.
+ inv H; tauto.
+ destruct (find_symbol ge i). eauto. discriminate.
Qed.
-Remark alloc_variables_perm:
- forall k prm b' q vl m m',
- alloc_variables m vl = Some m' ->
+Remark alloc_global_perm:
+ forall k prm b' q idg m m',
+ alloc_global m idg = Some m' ->
Mem.valid_block m b' ->
(Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
Proof.
- induction vl.
- simpl; intros. inv H. tauto.
- intros until m'. simpl. unfold alloc_variable.
- set (init := gvar_init a#2).
- set (sz := init_data_list_size init).
- caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
- caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
- caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
- caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID.
+ intros. destruct idg as [id [f|v]]; simpl in H.
+ (* function *)
+ destruct (Mem.alloc m 0 1) as [m1 b]_eqn.
+ assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
+ split; intros.
+ eapply Mem.perm_drop_3; eauto. eapply Mem.perm_alloc_1; eauto.
+ eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_drop_4; eauto.
+ (* variable *)
+ set (init := gvar_init v) in *.
+ set (sz := init_data_list_size init) in *.
+ destruct (Mem.alloc m 0 sz) as [m1 b]_eqn.
+ destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate.
+ destruct (store_init_data_list m2 b 0 init) as [m3|]_eqn; try discriminate.
assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
- assert (VALID': Mem.valid_block m4 b').
- unfold Mem.valid_block. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
- rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
- rewrite (store_zeros_nextblock _ _ _ STZ).
- change (Mem.valid_block m1 b'). eauto with mem.
- rewrite <- (IHvl _ _ REC VALID').
split; intros.
eapply Mem.perm_drop_3; eauto.
- rewrite <- store_init_data_list_perm; [idtac|eauto].
- rewrite <- store_zeros_perm; [idtac|eauto].
- eauto with mem.
- assert (Mem.perm m1 b' q k prm).
- rewrite store_zeros_perm; [idtac|eauto].
- rewrite store_init_data_list_perm; [idtac|eauto].
- eapply Mem.perm_drop_4; eauto.
- exploit Mem.perm_alloc_inv; eauto. rewrite zeq_false; auto.
+ erewrite <- store_init_data_list_perm; [idtac|eauto].
+ erewrite <- store_zeros_perm; [idtac|eauto].
+ eapply Mem.perm_alloc_1; eauto.
+ eapply Mem.perm_alloc_4; eauto.
+ erewrite store_zeros_perm; [idtac|eauto].
+ erewrite store_init_data_list_perm; [idtac|eauto].
+ eapply Mem.perm_drop_4; eauto.
+Qed.
+
+Remark alloc_globals_perm:
+ forall k prm b' q gl m m',
+ alloc_globals m gl = Some m' ->
+ Mem.valid_block m b' ->
+ (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
+Proof.
+ induction gl.
+ simpl; intros. inv H. tauto.
+ simpl; intros. destruct (alloc_global m a) as [m1|]_eqn; try discriminate.
+ erewrite alloc_global_perm; eauto. eapply IHgl; eauto.
+ unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. omega.
Qed.
+(** Data preservation properties *)
+
Remark store_zeros_outside:
- forall m b n m',
- store_zeros m b n = Some m' ->
- forall chunk b' p,
- b' <> b -> Mem.load chunk m' b' p = Mem.load chunk m b' p.
+ forall m b p n m',
+ store_zeros m b p n = Some m' ->
+ forall chunk b' p',
+ b' <> b \/ p' + size_chunk chunk <= p \/ p + n <= p' ->
+ Mem.load chunk m' b' p' = Mem.load chunk m b' p'.
Proof.
- intros until n. functional induction (store_zeros m b n); intros.
+ intros until n. functional induction (store_zeros m b p n); intros.
inv H; auto.
- rewrite IHo; auto. eapply Mem.load_store_other; eauto.
- inv H.
+ transitivity (Mem.load chunk m' b' p').
+ apply IHo. auto. unfold block in *; omega.
+ eapply Mem.load_store_other; eauto. simpl. unfold block in *; omega.
+ discriminate.
Qed.
Remark store_init_data_list_outside:
@@ -854,12 +735,12 @@ Remark store_init_data_list_outside:
Proof.
induction il; simpl.
intros; congruence.
- intros until m'. caseEq (store_init_data m b p a); try congruence.
- intros m1 A B chunk b' q C. transitivity (Mem.load chunk m1 b' q).
+ intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence.
+ transitivity (Mem.load chunk m1 b' q).
eapply IHil; eauto. generalize (init_data_size_pos a). intuition omega.
- destruct a; simpl in A;
+ destruct a; simpl in Heqo;
try (eapply Mem.load_store_other; eauto; intuition; fail).
- congruence.
+ inv Heqo. auto.
destruct (find_symbol ge i); try congruence.
eapply Mem.load_store_other; eauto; intuition.
Qed.
@@ -904,10 +785,9 @@ Proof.
induction il; simpl.
auto.
- intros until m'. caseEq (store_init_data m b p a); try congruence.
- intros m1 B C.
+ intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence.
exploit IHil; eauto. intro D.
- destruct a; simpl in B; intuition.
+ destruct a; simpl in Heqo; intuition.
eapply (A Mint8unsigned (Vint i)); eauto.
eapply (A Mint16unsigned (Vint i)); eauto.
eapply (A Mint32 (Vint i)); eauto.
@@ -917,36 +797,49 @@ Proof.
eapply (A Mint32 (Vptr b0 i0)); eauto.
Qed.
-Remark load_alloc_variables:
- forall chunk b p vl m m',
- alloc_variables m vl = Some m' ->
+Remark load_alloc_global:
+ forall chunk b p id g m m',
+ alloc_global m (id, g) = Some m' ->
Mem.valid_block m b ->
Mem.load chunk m' b p = Mem.load chunk m b p.
Proof.
- induction vl; simpl; intros until m'.
- congruence.
- unfold alloc_variable.
- set (init := gvar_init a#2).
- set (sz := init_data_list_size init).
- caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC.
- caseEq (store_zeros m1 b1 sz); try congruence. intros m2 STZ.
- caseEq (store_init_data_list m2 b1 0 init); try congruence. intros m3 STORE.
- caseEq (Mem.drop_perm m3 b1 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID.
- assert (b <> b1). apply Mem.valid_not_valid_diff with m; eauto with mem.
- transitivity (Mem.load chunk m4 b p).
- apply IHvl; auto. red.
- rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
- rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
- rewrite (store_zeros_nextblock _ _ _ STZ).
- change (Mem.valid_block m1 b). eauto with mem.
- transitivity (Mem.load chunk m3 b p).
+ intros. destruct g as [f|v]; simpl in H.
+ (* function *)
+ destruct (Mem.alloc m 0 1) as [m1 b']_eqn.
+ assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem.
+ transitivity (Mem.load chunk m1 b p).
eapply Mem.load_drop; eauto.
+ eapply Mem.load_alloc_unchanged; eauto.
+ (* variable *)
+ set (init := gvar_init v) in *.
+ set (sz := init_data_list_size init) in *.
+ destruct (Mem.alloc m 0 sz) as [m1 b']_eqn.
+ destruct (store_zeros m1 b' 0 sz) as [m2|]_eqn; try discriminate.
+ destruct (store_init_data_list m2 b' 0 init) as [m3|]_eqn; try discriminate.
+ assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem.
+ transitivity (Mem.load chunk m3 b p).
+ eapply Mem.load_drop; eauto.
transitivity (Mem.load chunk m2 b p).
- eapply store_init_data_list_outside; eauto.
+ eapply store_init_data_list_outside; eauto.
transitivity (Mem.load chunk m1 b p).
eapply store_zeros_outside; eauto.
eapply Mem.load_alloc_unchanged; eauto.
-Qed.
+Qed.
+
+Remark load_alloc_globals:
+ forall chunk b p gl m m',
+ alloc_globals m gl = Some m' ->
+ Mem.valid_block m b ->
+ Mem.load chunk m' b p = Mem.load chunk m b p.
+Proof.
+ induction gl; simpl; intros.
+ congruence.
+ destruct (alloc_global m a) as [m''|]_eqn; try discriminate.
+ transitivity (Mem.load chunk m'' b p).
+ apply IHgl; auto. unfold Mem.valid_block in *.
+ erewrite alloc_global_nextblock; eauto. omega.
+ destruct a as [id g]. eapply load_alloc_global; eauto.
+Qed.
Remark load_store_init_data_invariant:
forall m m' b,
@@ -967,114 +860,147 @@ Definition variables_initialized (g: t) (m: mem) :=
0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p)
/\ (gv.(gvar_volatile) = false -> load_store_init_data m b 0 gv.(gvar_init)).
-Lemma alloc_variable_initialized:
- forall g m id v m',
- genv_nextvar g = Mem.nextblock m ->
- alloc_variable m (id, v) = Some m' ->
- variables_initialized g m ->
- variables_initialized (add_variable g (id, v)) m'
- /\ genv_nextvar (add_variable g (id,v)) = Mem.nextblock m'.
-Proof.
- intros. revert H0. unfold alloc_variable. simpl.
- set (il := gvar_init v).
- set (sz := init_data_list_size il).
- caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC.
- caseEq (store_zeros m1 b1 sz); try congruence. intros m2 ZEROS.
- caseEq (store_init_data_list m2 b1 0 il); try congruence. intros m3 INIT DROP.
- exploit Mem.nextblock_alloc; eauto. intros NB1.
- assert (Mem.nextblock m' = Mem.nextblock m1).
- rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
- rewrite (store_init_data_list_nextblock _ _ _ _ INIT).
- eapply store_zeros_nextblock; eauto.
- exploit Mem.alloc_result; eauto. intro RES.
- split.
- (* var-init *)
- red; intros. revert H2.
- unfold add_variable, find_var_info; simpl.
- rewrite H; rewrite <- RES.
- rewrite ZMap.gsspec. destruct (ZIndexed.eq b b1); intros VI.
- (* new var *)
- injection VI; intro EQ. subst b gv. clear VI.
- fold il. fold sz.
- split. red; intros. eapply Mem.perm_drop_1; eauto.
- split. intros.
- assert (0 <= ofs < sz).
- eapply Mem.perm_alloc_3; eauto.
- rewrite store_zeros_perm; [idtac|eauto].
- rewrite store_init_data_list_perm; [idtac|eauto].
- eapply Mem.perm_drop_4; eauto.
- split; auto. eapply Mem.perm_drop_2; eauto.
+Definition functions_initialized (g: t) (m: mem) :=
+ forall b fd,
+ find_funct_ptr g b = Some fd ->
+ Mem.perm m b 0 Cur Nonempty
+ /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p).
+
+Lemma alloc_global_initialized:
+ forall ge m id g m',
+ genv_next ge = Mem.nextblock m ->
+ alloc_global m (id, g) = Some m' ->
+ variables_initialized ge m ->
+ functions_initialized ge m ->
+ variables_initialized (add_global ge (id, g)) m'
+ /\ functions_initialized (add_global ge (id, g)) m'
+ /\ genv_next (add_global ge (id, g)) = Mem.nextblock m'.
+Proof.
intros.
- apply load_store_init_data_invariant with m3.
- intros. eapply Mem.load_drop; eauto. right; right; right.
- unfold perm_globvar. destruct (gvar_volatile v); try discriminate.
- destruct (gvar_readonly v); auto with mem.
+ exploit alloc_global_nextblock; eauto. intros NB. split.
+(* variables-initialized *)
+ destruct g as [f|v].
+(* function *)
+ red; intros. unfold find_var_info in H3. simpl in H3.
+ exploit H1; eauto. intros [A [B C]].
+ assert (D: Mem.valid_block m b).
+ red. exploit genv_vars_range; eauto. rewrite H; omega.
+ split. red; intros. erewrite <- alloc_global_perm; eauto.
+ split. intros. eapply B. erewrite alloc_global_perm; eauto.
+ intros. apply load_store_init_data_invariant with m; auto.
+ intros. eapply load_alloc_global; eauto.
+(* variable *)
+ red; intros. unfold find_var_info in H3. simpl in H3. rewrite ZMap.gsspec in H3.
+ destruct (ZIndexed.eq b (genv_next ge0)).
+ (* same *)
+ inv H3. simpl in H0.
+ set (init := gvar_init gv) in *.
+ set (sz := init_data_list_size init) in *.
+ destruct (Mem.alloc m 0 sz) as [m1 b']_eqn.
+ destruct (store_zeros m1 b' 0 sz) as [m2|]_eqn; try discriminate.
+ destruct (store_init_data_list m2 b' 0 init) as [m3|]_eqn; try discriminate.
+ exploit Mem.alloc_result; eauto. intro RES.
+ replace (genv_next ge0) with b' by congruence.
+ split. red; intros. eapply Mem.perm_drop_1; eauto.
+ split. intros.
+ assert (0 <= ofs < sz).
+ eapply Mem.perm_alloc_3; eauto.
+ erewrite store_zeros_perm; [idtac|eauto].
+ erewrite store_init_data_list_perm; [idtac|eauto].
+ eapply Mem.perm_drop_4; eauto.
+ split. auto. eapply Mem.perm_drop_2; eauto.
+ intros. apply load_store_init_data_invariant with m3.
+ intros. eapply Mem.load_drop; eauto.
+ right; right; right. unfold perm_globvar. rewrite H3.
+ destruct (gvar_readonly gv); auto with mem.
eapply store_init_data_list_charact; eauto.
- (* older vars *)
+ (* older var *)
exploit H1; eauto. intros [A [B C]].
- split. red; intros. eapply Mem.perm_drop_3; eauto.
- rewrite <- store_init_data_list_perm; [idtac|eauto].
- rewrite <- store_zeros_perm; [idtac|eauto].
- eapply Mem.perm_alloc_1; eauto.
- split. intros. eapply B.
- eapply Mem.perm_alloc_4; eauto.
- rewrite store_zeros_perm; [idtac|eauto].
- rewrite store_init_data_list_perm; [idtac|eauto].
- eapply Mem.perm_drop_4; eauto.
- intros. apply load_store_init_data_invariant with m; auto.
- intros. transitivity (Mem.load chunk m3 b ofs).
- eapply Mem.load_drop; eauto.
- transitivity (Mem.load chunk m2 b ofs).
- eapply store_init_data_list_outside; eauto.
- transitivity (Mem.load chunk m1 b ofs).
- eapply store_zeros_outside; eauto.
- eapply Mem.load_alloc_unchanged; eauto.
- red. exploit genv_vars_range; eauto. rewrite <- H. omega.
- rewrite H0; rewrite NB1; rewrite H; auto.
-Qed.
-
-Lemma alloc_variables_initialized:
- forall vl g m m',
- genv_nextvar g = Mem.nextblock m ->
- alloc_variables m vl = Some m' ->
- variables_initialized g m ->
- variables_initialized (add_variables g vl) m'.
-Proof.
- induction vl; simpl; intros.
+ assert (D: Mem.valid_block m b).
+ red. exploit genv_vars_range; eauto. rewrite H; omega.
+ split. red; intros. erewrite <- alloc_global_perm; eauto.
+ split. intros. eapply B. erewrite alloc_global_perm; eauto.
+ intros. apply load_store_init_data_invariant with m; auto.
+ intros. eapply load_alloc_global; eauto.
+(* functions-initialized *)
+ split. destruct g as [f|v].
+(* function *)
+ red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite ZMap.gsspec in H3.
+ destruct (ZIndexed.eq b (genv_next ge0)).
+ (* same *)
+ inv H3. simpl in H0.
+ destruct (Mem.alloc m 0 1) as [m1 b']_eqn.
+ exploit Mem.alloc_result; eauto. intro RES.
+ replace (genv_next ge0) with b' by congruence.
+ split. eapply Mem.perm_drop_1; eauto. omega.
+ intros.
+ assert (0 <= ofs < 1).
+ eapply Mem.perm_alloc_3; eauto.
+ eapply Mem.perm_drop_4; eauto.
+ split. omega. eapply Mem.perm_drop_2; eauto.
+ (* older function *)
+ exploit H2; eauto. intros [A B].
+ assert (D: Mem.valid_block m b).
+ red. exploit genv_funs_range; eauto. rewrite H; omega.
+ split. erewrite <- alloc_global_perm; eauto.
+ intros. eapply B. erewrite alloc_global_perm; eauto.
+(* variables *)
+ red; intros. unfold find_funct_ptr in H3. simpl in H3.
+ exploit H2; eauto. intros [A B].
+ assert (D: Mem.valid_block m b).
+ red. exploit genv_funs_range; eauto. rewrite H; omega.
+ split. erewrite <- alloc_global_perm; eauto.
+ intros. eapply B. erewrite alloc_global_perm; eauto.
+(* nextblock *)
+ rewrite NB. simpl. rewrite H. unfold block; omega.
+Qed.
+
+Lemma alloc_globals_initialized:
+ forall gl ge m m',
+ genv_next ge = Mem.nextblock m ->
+ alloc_globals m gl = Some m' ->
+ variables_initialized ge m ->
+ functions_initialized ge m ->
+ variables_initialized (add_globals ge gl) m' /\ functions_initialized (add_globals ge gl) m'.
+Proof.
+ induction gl; simpl; intros.
inv H0; auto.
- destruct (alloc_variable m a) as [m1|]_eqn; try discriminate.
- destruct a as [id gv].
- exploit alloc_variable_initialized; eauto. intros [P Q].
- eapply IHvl; eauto.
+ destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|]_eqn; try discriminate.
+ exploit alloc_global_initialized; eauto. intros [P [Q R]].
+ eapply IHgl; eauto.
Qed.
End INITMEM.
Definition init_mem (p: program F V) :=
- alloc_variables (globalenv p) Mem.empty p.(prog_vars).
+ alloc_globals (globalenv p) Mem.empty p.(prog_defs).
+
+Lemma init_mem_genv_next: forall p m,
+ init_mem p = Some m ->
+ genv_next (globalenv p) = Mem.nextblock m.
+Proof.
+ unfold init_mem; intros.
+ exploit alloc_globals_nextblock; eauto. rewrite Mem.nextblock_empty. intro.
+ generalize (genv_next_add_globals (prog_defs p) empty_genv).
+ fold (globalenv p). simpl genv_next. intros. congruence.
+Qed.
Theorem find_symbol_not_fresh:
forall p id b m,
init_mem p = Some m ->
find_symbol (globalenv p) id = Some b -> Mem.valid_block m b.
Proof.
- unfold init_mem; intros.
- exploit alloc_variables_nextblock; eauto. rewrite Mem.nextblock_empty. intro.
- exploit genv_symb_range; eauto. intros.
- generalize (add_variables_nextvar (prog_vars p) (add_functions empty_genv (prog_funct p))).
- rewrite add_functions_nextvar. simpl genv_nextvar. intro.
- red. rewrite H1. rewrite <- H3. intuition.
+ intros. red. erewrite <- init_mem_genv_next; eauto.
+ exploit genv_symb_range; eauto. omega.
Qed.
-Lemma init_mem_genv_vars : forall p m,
- init_mem p = Some m ->
- genv_nextvar (globalenv p) = Mem.nextblock m.
+Theorem find_funct_ptr_not_fresh:
+ forall p b f m,
+ init_mem p = Some m ->
+ find_funct_ptr (globalenv p) b = Some f -> Mem.valid_block m b.
Proof.
- clear. unfold globalenv, init_mem. intros.
- exploit alloc_variables_nextblock; eauto.
- simpl (Mem.nextblock Mem.empty).
- rewrite add_variables_nextvar. rewrite add_functions_nextvar.
- simpl (genv_nextvar empty_genv). auto.
+ intros. red. erewrite <- init_mem_genv_next; eauto.
+ exploit genv_funs_range; eauto. omega.
Qed.
Theorem find_var_info_not_fresh:
@@ -1082,12 +1008,8 @@ Theorem find_var_info_not_fresh:
init_mem p = Some m ->
find_var_info (globalenv p) b = Some gv -> Mem.valid_block m b.
Proof.
- unfold init_mem; intros.
- exploit alloc_variables_nextblock; eauto. rewrite Mem.nextblock_empty. intro.
- exploit genv_vars_range; eauto. intros.
- generalize (add_variables_nextvar (prog_vars p) (add_functions empty_genv (prog_funct p))).
- rewrite add_functions_nextvar. simpl genv_nextvar. intro.
- red. rewrite H1. rewrite <- H3. intuition.
+ intros. red. erewrite <- init_mem_genv_next; eauto.
+ exploit genv_vars_range; eauto. omega.
Qed.
Theorem init_mem_characterization:
@@ -1099,10 +1021,23 @@ Theorem init_mem_characterization:
0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p)
/\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)).
Proof.
- intros. eapply alloc_variables_initialized; eauto.
- rewrite add_functions_nextvar; auto.
- red; intros. exploit genv_vars_range; eauto. rewrite add_functions_nextvar.
- simpl. intros. omegaContradiction.
+ intros. eapply alloc_globals_initialized; eauto.
+ rewrite Mem.nextblock_empty. auto.
+ red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction.
+ red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction.
+Qed.
+
+Theorem init_mem_characterization_2:
+ forall p b fd m,
+ find_funct_ptr (globalenv p) b = Some fd ->
+ init_mem p = Some m ->
+ Mem.perm m b 0 Cur Nonempty
+ /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p).
+Proof.
+ intros. unfold init_mem in H0. eapply alloc_globals_initialized; eauto.
+ rewrite Mem.nextblock_empty. auto.
+ red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction.
+ red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction.
Qed.
(** ** Compatibility with memory injections *)
@@ -1113,6 +1048,19 @@ Variable ge: t.
Variable thr: block.
Hypothesis symb_inject: forall id b, find_symbol ge id = Some b -> b < thr.
+Lemma store_zeros_neutral:
+ forall m b p n m',
+ Mem.inject_neutral thr m ->
+ b < thr ->
+ store_zeros m b p n = Some m' ->
+ Mem.inject_neutral thr m'.
+Proof.
+ intros until n. functional induction (store_zeros m b p n); intros.
+ inv H1; auto.
+ apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor.
+ inv H1.
+Qed.
+
Lemma store_init_data_neutral:
forall m b p id m',
Mem.inject_neutral thr m ->
@@ -1122,7 +1070,7 @@ Lemma store_init_data_neutral:
Proof.
intros.
destruct id; simpl in H1; try (eapply Mem.store_inject_neutral; eauto; fail).
- inv H1; auto.
+ congruence.
revert H1. caseEq (find_symbol ge i); try congruence. intros b' FS ST.
eapply Mem.store_inject_neutral; eauto.
econstructor. unfold Mem.flat_inj. apply zlt_true; eauto.
@@ -1143,54 +1091,46 @@ Proof.
eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto.
Qed.
-Lemma store_zeros_neutral:
- forall m b n m',
- Mem.inject_neutral thr m ->
- b < thr ->
- store_zeros m b n = Some m' ->
- Mem.inject_neutral thr m'.
-Proof.
- intros until n. functional induction (store_zeros m b n); intros.
- inv H1; auto.
- apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor.
- inv H1.
-Qed.
-
-Lemma alloc_variable_neutral:
- forall id m m',
- alloc_variable ge m id = Some m' ->
+Lemma alloc_global_neutral:
+ forall idg m m',
+ alloc_global ge m idg = Some m' ->
Mem.inject_neutral thr m ->
Mem.nextblock m < thr ->
Mem.inject_neutral thr m'.
Proof.
- intros until m'. unfold alloc_variable.
- set (init := gvar_init id#2).
- set (sz := init_data_list_size init).
- caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC.
- caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
- caseEq (store_init_data_list ge m2 b 0 init); try congruence.
- intros m3 STORE DROP NEUTRAL NEXT.
- assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto.
+ intros. destruct idg as [id [f|v]]; simpl in H.
+ (* function *)
+ destruct (Mem.alloc m 0 1) as [m1 b]_eqn.
+ assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+ eapply Mem.drop_inject_neutral; eauto.
+ eapply Mem.alloc_inject_neutral; eauto.
+ (* variable *)
+ set (init := gvar_init v) in *.
+ set (sz := init_data_list_size init) in *.
+ destruct (Mem.alloc m 0 sz) as [m1 b]_eqn.
+ destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate.
+ destruct (store_init_data_list ge m2 b 0 init) as [m3|]_eqn; try discriminate.
+ assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
eapply Mem.drop_inject_neutral; eauto.
eapply store_init_data_list_neutral with (m := m2) (b := b); eauto.
eapply store_zeros_neutral with (m := m1); eauto.
eapply Mem.alloc_inject_neutral; eauto.
Qed.
-Lemma alloc_variables_neutral:
- forall idl m m',
- alloc_variables ge m idl = Some m' ->
+Lemma alloc_globals_neutral:
+ forall gl m m',
+ alloc_globals ge m gl = Some m' ->
Mem.inject_neutral thr m ->
Mem.nextblock m' <= thr ->
Mem.inject_neutral thr m'.
Proof.
- induction idl; simpl.
+ induction gl; simpl.
intros. congruence.
- intros until m'. caseEq (alloc_variable ge m a); try congruence. intros.
- assert (Mem.nextblock m' = Mem.nextblock m + Z_of_nat(length (a :: idl))).
- eapply alloc_variables_nextblock with ge. simpl. rewrite H. auto.
+ intros until m'. caseEq (alloc_global ge m a); try congruence. intros.
+ assert (Mem.nextblock m' = Mem.nextblock m + Z_of_nat(length (a :: gl))).
+ eapply alloc_globals_nextblock with ge. simpl. rewrite H. auto.
simpl length in H3. rewrite inj_S in H3.
- exploit alloc_variable_neutral; eauto. unfold block in *; omega.
+ exploit alloc_global_neutral; eauto. unfold block in *; omega.
Qed.
End INITMEM_INJ.
@@ -1202,7 +1142,7 @@ Theorem initmem_inject:
Proof.
unfold init_mem; intros.
apply Mem.neutral_inject.
- eapply alloc_variables_neutral; eauto.
+ eapply alloc_globals_neutral; eauto.
intros. exploit find_symbol_not_fresh; eauto.
apply Mem.empty_inject_neutral.
omega.
@@ -1213,6 +1153,22 @@ Section INITMEM_AUGMENT_INJ.
Variable ge: t.
Variable thr: block.
+Lemma store_zeros_augment:
+ forall m1 m2 b p n m2',
+ Mem.inject (Mem.flat_inj thr) m1 m2 ->
+ b >= thr ->
+ store_zeros m2 b p n = Some m2' ->
+ Mem.inject (Mem.flat_inj thr) m1 m2'.
+Proof.
+ intros until n. functional induction (store_zeros m2 b p n); intros.
+ inv H1; auto.
+ apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl.
+ intros. exfalso. unfold Mem.flat_inj in H2. destruct (zlt b' thr).
+ inversion H2; subst; omega.
+ discriminate.
+ inv H1.
+Qed.
+
Lemma store_init_data_augment:
forall m1 m2 b p id m2',
Mem.inject (Mem.flat_inj thr) m1 m2 ->
@@ -1228,7 +1184,7 @@ Proof.
intros. unfold Mem.flat_inj in H0.
destruct (zlt b' thr); inversion H0; subst. omega.
destruct id; simpl in ST; try (eapply P; eauto; fail).
- inv ST; auto.
+ congruence.
revert ST. caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto.
Qed.
@@ -1246,59 +1202,49 @@ Proof.
eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto.
Qed.
-Lemma store_zeros_augment:
- forall m1 m2 b n m2',
- Mem.inject (Mem.flat_inj thr) m1 m2 ->
- b >= thr ->
- store_zeros m2 b n = Some m2' ->
- Mem.inject (Mem.flat_inj thr) m1 m2'.
-Proof.
- intros until n. functional induction (store_zeros m2 b n); intros.
- inv H1; auto.
- apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl.
- intros. exfalso. unfold Mem.flat_inj in H2. destruct (zlt b' thr).
- inversion H2; subst; omega.
- discriminate.
- inv H1.
-Qed.
-
-Lemma alloc_variable_augment:
- forall id m1 m2 m2',
- alloc_variable ge m2 id = Some m2' ->
+Lemma alloc_global_augment:
+ forall idg m1 m2 m2',
+ alloc_global ge m2 idg = Some m2' ->
Mem.inject (Mem.flat_inj thr) m1 m2 ->
Mem.nextblock m2 >= thr ->
Mem.inject (Mem.flat_inj thr) m1 m2'.
Proof.
- intros until m2'. unfold alloc_variable.
- set (sz := init_data_list_size (gvar_init id#2)).
- caseEq (Mem.alloc m2 0 sz); try congruence. intros m3 b ALLOC.
- caseEq (store_zeros m3 b sz); try congruence. intros m4 STZ.
- caseEq (store_init_data_list ge m4 b 0 (gvar_init id#2)); try congruence.
- intros m5 STORE DROP INJ NEXT.
- assert (b >= thr).
- pose proof (Mem.fresh_block_alloc _ _ _ _ _ ALLOC).
- unfold Mem.valid_block in H. unfold block in *; omega.
- eapply Mem.drop_outside_inject. 2: eauto.
- eapply store_init_data_list_augment. 2: eauto. 2: eauto.
- eapply store_zeros_augment. 2: eauto. 2: eauto.
- eapply Mem.alloc_right_inject; eauto.
- intros. unfold Mem.flat_inj in H0. destruct (zlt b' thr); inversion H0.
+ intros. destruct idg as [id [f|v]]; simpl in H.
+ (* function *)
+ destruct (Mem.alloc m2 0 1) as [m3 b]_eqn.
+ assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+ eapply Mem.drop_outside_inject. 2: eauto.
+ eapply Mem.alloc_right_inject; eauto.
+ intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3.
+ subst; exfalso; omega.
+ (* variable *)
+ set (init := gvar_init v) in *.
+ set (sz := init_data_list_size init) in *.
+ destruct (Mem.alloc m2 0 sz) as [m3 b]_eqn.
+ destruct (store_zeros m3 b 0 sz) as [m4|]_eqn; try discriminate.
+ destruct (store_init_data_list ge m4 b 0 init) as [m5|]_eqn; try discriminate.
+ assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+ eapply Mem.drop_outside_inject. 2: eauto.
+ eapply store_init_data_list_augment. 3: eauto. 2: eauto.
+ eapply store_zeros_augment. 3: eauto. 2: eauto.
+ eapply Mem.alloc_right_inject; eauto.
+ intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3.
subst; exfalso; omega.
Qed.
-Lemma alloc_variables_augment:
- forall idl m1 m2 m2',
- alloc_variables ge m2 idl = Some m2' ->
+Lemma alloc_globals_augment:
+ forall gl m1 m2 m2',
+ alloc_globals ge m2 gl = Some m2' ->
Mem.inject (Mem.flat_inj thr) m1 m2 ->
Mem.nextblock m2 >= thr ->
Mem.inject (Mem.flat_inj thr) m1 m2'.
Proof.
- induction idl; simpl.
+ induction gl; simpl.
intros. congruence.
- intros until m2'. caseEq (alloc_variable ge m2 a); try congruence. intros.
- eapply IHidl with (m2 := m); eauto.
- eapply alloc_variable_augment; eauto.
- rewrite (alloc_variable_nextblock _ _ _ H).
+ intros until m2'. caseEq (alloc_global ge m2 a); try congruence. intros.
+ eapply IHgl with (m2 := m); eauto.
+ eapply alloc_global_augment; eauto.
+ rewrite (alloc_global_nextblock _ _ _ H).
unfold block in *; omega.
Qed.
@@ -1321,216 +1267,156 @@ Inductive match_globvar: globvar V -> globvar W -> Prop :=
match_varinfo info1 info2 ->
match_globvar (mkglobvar info1 init ro vo) (mkglobvar info2 init ro vo).
-Record match_genvs (new_functs : list (ident * B)) (new_vars : list (ident * globvar W))
+Record match_genvs (new_globs : list (ident * globdef B W))
(ge1: t A V) (ge2: t B W): Prop := {
- mge_nextfun: genv_nextfun ge2 = genv_nextfun ge1 - Z_of_nat(length new_functs);
- mge_nextvar: genv_nextvar ge2 = genv_nextvar ge1 + Z_of_nat(length new_vars);
- mge_symb: forall id, ~ In id ((funct_names new_functs) ++ (var_names new_vars)) ->
+ mge_next:
+ genv_next ge2 = genv_next ge1 + Z_of_nat(length new_globs);
+ mge_symb:
+ forall id, ~ In id (map fst new_globs) ->
PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1);
mge_funs:
forall b f, ZMap.get b (genv_funs ge1) = Some f ->
exists tf, ZMap.get b (genv_funs ge2) = Some tf /\ match_fun f tf;
mge_rev_funs:
forall b tf, ZMap.get b (genv_funs ge2) = Some tf ->
- if zlt (genv_nextfun ge1) b then
+ if zlt b (genv_next ge1) then
exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf
else
- In tf (map (@snd ident B) new_functs);
+ In (Gfun tf) (map snd new_globs);
mge_vars:
forall b v, ZMap.get b (genv_vars ge1) = Some v ->
exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_globvar v tv;
mge_rev_vars:
forall b tv, ZMap.get b (genv_vars ge2) = Some tv ->
- if zlt b (genv_nextvar ge1) then
+ if zlt b (genv_next ge1) then
exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv
else
- In tv (map (@snd ident (globvar W)) new_vars)
+ In (Gvar tv) (map snd new_globs)
}.
-Lemma add_function_match:
- forall ge1 ge2 id f1 f2,
- match_genvs nil nil ge1 ge2 ->
- match_fun f1 f2 ->
- match_genvs nil nil (add_function ge1 (id, f1)) (add_function ge2 (id, f2)).
+Lemma add_global_match:
+ forall ge1 ge2 idg1 idg2,
+ match_genvs nil ge1 ge2 ->
+ match_globdef match_fun match_varinfo idg1 idg2 ->
+ match_genvs nil (add_global ge1 idg1) (add_global ge2 idg2).
Proof.
intros. destruct H.
- simpl in mge_nextfun0. rewrite Zminus_0_r in mge_nextfun0.
- simpl in mge_nextvar0. rewrite Zplus_0_r in mge_nextvar0.
- constructor; simpl.
- rewrite Zminus_0_r. congruence.
+ simpl in mge_next0. rewrite Zplus_0_r in mge_next0.
+ inv H0.
+(* two functions *)
+ constructor; simpl.
rewrite Zplus_0_r. congruence.
- intros. rewrite mge_nextfun0.
- repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
- rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec.
- destruct (ZIndexed.eq b (genv_nextfun ge1)).
+ intros. rewrite mge_next0.
+ repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
+ rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec.
+ destruct (ZIndexed.eq b (genv_next ge1)).
exists f2; split; congruence.
eauto.
- rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec.
- destruct (ZIndexed.eq b (genv_nextfun ge1)).
- subst b. destruct (zlt (genv_nextfun ge1 - 1) (genv_nextfun ge1)).
- exists f1; split; congruence. omega.
- pose proof (mge_rev_funs0 b tf H).
- destruct (zlt (genv_nextfun ge1) b);
- destruct (zlt (genv_nextfun ge1 - 1) b). auto. omega. exfalso; omega. intuition.
- auto.
- auto.
-Qed.
-
-Lemma add_functions_match:
- forall fl1 fl2, list_forall2 (match_funct_entry match_fun) fl1 fl2 ->
- forall ge1 ge2, match_genvs nil nil ge1 ge2 ->
- match_genvs nil nil (add_functions ge1 fl1) (add_functions ge2 fl2).
-Proof.
- induction 1; intros; simpl.
- auto.
- destruct a1 as [id1 f1]; destruct b1 as [id2 f2].
- destruct H. subst. apply IHlist_forall2. apply add_function_match; auto.
-Qed.
-
-Lemma add_function_augment_match:
- forall new_functs new_vars ge1 ge2 id f2,
- match_genvs new_functs new_vars ge1 ge2 ->
- match_genvs (new_functs++((id,f2)::nil)) new_vars ge1 (add_function ge2 (id, f2)).
-Proof.
- intros. destruct H. constructor; simpl.
- rewrite mge_nextfun0. rewrite app_length.
- simpl. rewrite inj_plus. rewrite inj_S. rewrite inj_0. unfold block; omega. (* painful! *)
- auto.
- intros. unfold funct_names in H. rewrite map_app in H. rewrite in_app in H. rewrite in_app in H. simpl in H.
- destruct (peq id id0). subst. intuition. rewrite PTree.gso.
- apply mge_symb0. intro. apply H. rewrite in_app in H0. inversion H0; intuition. intuition.
- intros. rewrite ZMap.gso. auto.
- rewrite mge_nextfun0. pose proof (genv_funs_range ge1 b H). intro; subst; omega.
- intros. rewrite ZMap.gsspec in H.
- destruct (ZIndexed.eq b (genv_nextfun ge2)).
- destruct (zlt (genv_nextfun ge1) b).
- exfalso. rewrite mge_nextfun0 in e. unfold block; omega.
- rewrite map_app. rewrite in_app. simpl. inversion H; intuition.
- pose proof (mge_rev_funs0 b tf H).
- destruct (zlt (genv_nextfun ge1) b).
- auto.
- rewrite map_app. rewrite in_app. intuition.
- auto.
- auto.
-Qed.
-
-
-Lemma add_functions_augment_match:
- forall fl new_functs new_vars ge1 ge2,
- match_genvs new_functs new_vars ge1 ge2 ->
- match_genvs (new_functs++fl) new_vars ge1 (add_functions ge2 fl).
-Proof.
- induction fl; simpl.
- intros. rewrite app_nil_r. auto.
- intros. replace (new_functs ++ a :: fl) with ((new_functs ++ (a::nil)) ++ fl)
- by (rewrite app_ass; auto).
- apply IHfl. destruct a. apply add_function_augment_match. auto.
-Qed.
-
-
-Lemma add_variable_match:
- forall new_functs ge1 ge2 id v1 v2,
- match_genvs new_functs nil ge1 ge2 ->
- match_globvar v1 v2 ->
- match_genvs new_functs nil (add_variable ge1 (id, v1)) (add_variable ge2 (id, v2)).
-Proof.
- intros. destruct H.
- simpl in mge_nextvar0. rewrite Zplus_0_r in mge_nextvar0.
- constructor; simpl.
- auto.
- rewrite Zplus_0_r. rewrite mge_nextvar0. auto.
- intros. rewrite mge_nextvar0.
- repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
- auto.
- auto.
- rewrite mge_nextvar0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec.
- destruct (ZIndexed.eq b (genv_nextvar ge1)).
- exists v2; split; congruence.
- eauto.
- rewrite mge_nextvar0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec.
- destruct (ZIndexed.eq b (genv_nextvar ge1)).
- subst b. inversion H; subst.
- destruct (zlt (genv_nextvar ge1) (genv_nextvar ge1 + 1)).
- exists v1; split; congruence. omega.
- pose proof (mge_rev_vars0 _ _ H).
- destruct (zlt b (genv_nextvar ge1));
- destruct (zlt b (genv_nextvar ge1 + 1)). auto. omega. exfalso; omega. intuition.
+ rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec.
+ destruct (ZIndexed.eq b (genv_next ge1)).
+ subst b. rewrite zlt_true. exists f1; split; congruence. omega.
+ pose proof (mge_rev_funs0 b tf H0).
+ destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega.
+ contradiction.
+ eauto.
+ intros.
+ pose proof (mge_rev_vars0 b tv H0).
+ destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega.
+ contradiction.
+(* two variables *)
+ constructor; simpl.
+ rewrite Zplus_0_r. congruence.
+ intros. rewrite mge_next0.
+ repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
+ eauto.
+ intros.
+ pose proof (mge_rev_funs0 b tf H0).
+ destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega.
+ contradiction.
+ rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec.
+ destruct (ZIndexed.eq b (genv_next ge1)).
+ econstructor; split. eauto. inv H0. constructor; auto.
+ eauto.
+ rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec.
+ destruct (ZIndexed.eq b (genv_next ge1)).
+ subst b. rewrite zlt_true.
+ econstructor; split. eauto. inv H0. constructor; auto.
+ omega.
+ pose proof (mge_rev_vars0 b tv H0).
+ destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega.
+ contradiction.
Qed.
-Lemma add_variables_match:
- forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 ->
- forall new_functs ge1 ge2, match_genvs new_functs nil ge1 ge2 ->
- match_genvs new_functs nil (add_variables ge1 vl1) (add_variables ge2 vl2).
+Lemma add_globals_match:
+ forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 ->
+ forall ge1 ge2, match_genvs nil ge1 ge2 ->
+ match_genvs nil (add_globals ge1 gl1) (add_globals ge2 gl2).
Proof.
induction 1; intros; simpl.
auto.
- inv H. apply IHlist_forall2. apply add_variable_match; auto. constructor; auto.
+ apply IHlist_forall2. apply add_global_match; auto.
Qed.
-
-Lemma add_variable_augment_match:
- forall ge1 new_functs new_vars ge2 id v2,
- match_genvs new_functs new_vars ge1 ge2 ->
- match_genvs new_functs (new_vars++((id,v2)::nil)) ge1 (add_variable ge2 (id, v2)).
+Lemma add_global_augment_match:
+ forall new_globs ge1 ge2 idg,
+ match_genvs new_globs ge1 ge2 ->
+ match_genvs (new_globs ++ (idg :: nil)) ge1 (add_global ge2 idg).
Proof.
intros. destruct H. constructor; simpl.
- auto.
- rewrite mge_nextvar0. rewrite app_length.
- simpl. rewrite inj_plus. rewrite inj_S. rewrite inj_0. unfold block; omega. (* painful! *)
- intros. unfold funct_names, var_names in H. rewrite map_app in H. rewrite in_app in H. rewrite in_app in H. simpl in H.
- destruct (peq id id0). subst. intuition. rewrite PTree.gso.
- apply mge_symb0. intro. apply H. rewrite in_app in H0. inversion H0; intuition. intuition.
- auto.
- auto.
- intros. rewrite ZMap.gso. auto.
- rewrite mge_nextvar0. pose proof (genv_vars_range ge1 b H). intro; subst; omega.
- intros. rewrite ZMap.gsspec in H.
- destruct (ZIndexed.eq b (genv_nextvar ge2)).
- destruct (zlt b (genv_nextvar ge1)).
- exfalso. rewrite mge_nextvar0 in e. unfold block; omega.
- rewrite map_app. rewrite in_app. simpl. inversion H; intuition.
- pose proof (mge_rev_vars0 b tv H).
- destruct (zlt b (genv_nextvar ge1)).
- auto.
- rewrite map_app. rewrite in_app. intuition.
-
-Qed.
-
-Lemma add_variables_augment_match:
- forall vl ge1 new_functs new_vars ge2,
- match_genvs new_functs new_vars ge1 ge2 ->
- match_genvs new_functs (new_vars++vl) ge1 (add_variables ge2 vl).
-Proof.
- induction vl; simpl.
+ rewrite mge_next0. rewrite app_length.
+ simpl. rewrite inj_plus. change (Z_of_nat 1) with 1. unfold block; omega.
+ intros. rewrite map_app in H. rewrite in_app in H. simpl in H.
+ destruct (peq id idg#1). subst. intuition. rewrite PTree.gso.
+ apply mge_symb0. intuition. auto.
+ intros. destruct idg as [id1 [f1|v1]]; simpl; eauto.
+ rewrite ZMap.gso. eauto. exploit genv_funs_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega.
+ intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H.
+ rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)).
+ rewrite zlt_false. rewrite in_app. simpl; right; left. congruence.
+ subst b. rewrite mge_next0. omega.
+ exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto.
+ rewrite in_app. tauto.
+ exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto.
+ rewrite in_app. tauto.
+ intros. destruct idg as [id1 [f1|v1]]; simpl; eauto.
+ rewrite ZMap.gso. eauto. exploit genv_vars_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega.
+ intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H.
+ exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto.
+ rewrite in_app. tauto.
+ rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)).
+ rewrite zlt_false. rewrite in_app. simpl; right; left. congruence.
+ subst b. rewrite mge_next0. omega.
+ exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto.
+ rewrite in_app. tauto.
+Qed.
+
+Lemma add_globals_augment_match:
+ forall gl new_globs ge1 ge2,
+ match_genvs new_globs ge1 ge2 ->
+ match_genvs (new_globs ++ gl) ge1 (add_globals ge2 gl).
+Proof.
+ induction gl; simpl.
intros. rewrite app_nil_r. auto.
- intros. replace (new_vars ++ a :: vl) with ((new_vars ++ (a::nil)) ++ vl)
- by (rewrite app_ass; auto).
- apply IHvl. destruct a. apply add_variable_augment_match. auto.
+ intros. change (a :: gl) with ((a :: nil) ++ gl). rewrite <- app_ass.
+ apply IHgl. apply add_global_augment_match. auto.
Qed.
-Variable new_functs : list (ident * B).
-Variable new_vars : list (ident * globvar W).
+Variable new_globs : list (ident * globdef B W).
Variable new_main : ident.
Variable p: program A V.
Variable p': program B W.
Hypothesis progmatch:
- match_program match_fun match_varinfo new_functs new_vars new_main p p'.
+ match_program match_fun match_varinfo new_globs new_main p p'.
Lemma globalenvs_match:
- match_genvs new_functs new_vars (globalenv p) (globalenv p').
-Proof.
- unfold globalenv. destruct progmatch. clear progmatch.
- destruct H as [tfuncts [P1 P2]]. destruct H0. clear H0. destruct H as [tvars [Q1 Q2]].
- rewrite P2. rewrite Q2. clear P2 Q2.
- rewrite add_variables_app.
- rewrite add_functions_app.
- pattern new_vars at 1. replace new_vars with (nil++new_vars) by auto.
- apply add_variables_augment_match.
- apply add_variables_match; auto.
- pattern new_functs at 1. replace new_functs with (nil++new_functs) by auto.
- apply add_functions_augment_match.
- apply add_functions_match; auto.
+ match_genvs new_globs (globalenv p) (globalenv p').
+Proof.
+ unfold globalenv. destruct progmatch as [[tglob [P Q]] R].
+ rewrite Q. rewrite add_globals_app.
+ change new_globs with (nil ++ new_globs) at 1.
+ apply add_globals_augment_match.
+ apply add_globals_match; auto.
constructor; simpl; auto; intros; rewrite ZMap.gi in H; congruence.
Qed.
@@ -1544,10 +1430,10 @@ Proof (mge_funs globalenvs_match).
Theorem find_funct_ptr_rev_match:
forall (b : block) (tf : B),
find_funct_ptr (globalenv p') b = Some tf ->
- if zlt (genv_nextfun (globalenv p)) b then
+ if zlt b (genv_next (globalenv p)) then
exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf
else
- In tf (map (@snd ident B) new_functs).
+ In (Gfun tf) (map snd new_globs).
Proof (mge_rev_funs globalenvs_match).
Theorem find_funct_match:
@@ -1565,13 +1451,13 @@ Theorem find_funct_rev_match:
forall (v : val) (tf : B),
find_funct (globalenv p') v = Some tf ->
(exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf)
- \/ (In tf (map (@snd ident B) new_functs)).
+ \/ (In (Gfun tf) (map snd new_globs)).
Proof.
intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v.
rewrite find_funct_find_funct_ptr in H.
rewrite find_funct_find_funct_ptr.
apply find_funct_ptr_rev_match in H.
- destruct (zlt (genv_nextfun (globalenv p)) b); intuition.
+ destruct (zlt b (genv_next (globalenv p))); auto.
Qed.
Theorem find_var_info_match:
@@ -1584,23 +1470,23 @@ Proof (mge_vars globalenvs_match).
Theorem find_var_info_rev_match:
forall (b : block) (tv : globvar W),
find_var_info (globalenv p') b = Some tv ->
- if zlt b (genv_nextvar (globalenv p)) then
+ if zlt b (genv_next (globalenv p)) then
exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv
else
- In tv (map (@snd ident (globvar W)) new_vars).
+ In (Gvar tv) (map snd new_globs).
Proof (mge_rev_vars globalenvs_match).
Theorem find_symbol_match:
forall (s : ident),
- ~In s (funct_names new_functs ++ var_names new_vars) ->
+ ~In s (map fst new_globs) ->
find_symbol (globalenv p') s = find_symbol (globalenv p) s.
Proof.
intros. destruct globalenvs_match. unfold find_symbol. auto.
Qed.
Hypothesis new_ids_fresh :
- (forall s', find_symbol (globalenv p) s' <> None ->
- ~In s' (funct_names new_functs ++ var_names new_vars)).
+ forall s', find_symbol (globalenv p) s' <> None ->
+ ~In s' (map fst new_globs).
Lemma store_init_data_list_match:
forall idl m b ofs m',
@@ -1611,46 +1497,43 @@ Proof.
auto.
assert (forall m', store_init_data (globalenv p) m b ofs a = Some m' ->
store_init_data (globalenv p') m b ofs a = Some m').
- destruct a; simpl; auto. rewrite find_symbol_match. auto.
- inversion H. case_eq (find_symbol (globalenv p) i).
- intros. apply new_ids_fresh. intro. rewrite H0 in H2; inversion H2.
- intro. rewrite H0 in H1. inversion H1.
+ destruct a; simpl; auto. rewrite find_symbol_match. auto.
+ simpl in H. destruct (find_symbol (globalenv p) i) as [b'|]_eqn; try discriminate.
+ apply new_ids_fresh. congruence.
case_eq (store_init_data (globalenv p) m b ofs a); intros.
rewrite H1 in H.
pose proof (H0 _ H1). rewrite H2. auto.
rewrite H1 in H. inversion H.
Qed.
-Lemma alloc_variables_match:
- forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 ->
+Lemma alloc_globals_match:
+ forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 ->
forall m m',
- alloc_variables (globalenv p) m vl1 = Some m' ->
- alloc_variables (globalenv p') m vl2 = Some m'.
+ alloc_globals (globalenv p) m gl1 = Some m' ->
+ alloc_globals (globalenv p') m gl2 = Some m'.
Proof.
- induction 1; intros until m'; simpl.
+ induction 1; simpl; intros.
auto.
- inv H.
- unfold alloc_variable; simpl.
- destruct (Mem.alloc m 0 (init_data_list_size init)).
- destruct (store_zeros m0 b (init_data_list_size init)); auto.
- case_eq (store_init_data_list (globalenv p) m1 b 0 init); intros m2 P.
- rewrite (store_init_data_list_match _ _ _ _ P).
- change (perm_globvar (mkglobvar info2 init ro vo))
- with (perm_globvar (mkglobvar info1 init ro vo)).
- destruct (Mem.drop_perm m2 b 0 (init_data_list_size init)
- (perm_globvar (mkglobvar info1 init ro vo))); auto.
- inversion P.
+ destruct (alloc_global (globalenv p) m a1) as [m1|]_eqn; try discriminate.
+ assert (alloc_global (globalenv p') m b1 = Some m1).
+ inv H; simpl in *.
+ auto.
+ set (sz := init_data_list_size init) in *.
+ destruct (Mem.alloc m 0 sz) as [m2 b]_eqn.
+ destruct (store_zeros m2 b 0 sz) as [m3|]_eqn; try discriminate.
+ destruct (store_init_data_list (globalenv p) m3 b 0 init) as [m4|]_eqn; try discriminate.
+ erewrite store_init_data_list_match; eauto.
+ rewrite H2. eauto.
Qed.
Theorem init_mem_match:
forall m, init_mem p = Some m ->
- init_mem p' = alloc_variables (globalenv p') m new_vars.
+ init_mem p' = alloc_globals (globalenv p') m new_globs.
Proof.
- unfold init_mem. destruct progmatch. destruct H0. destruct H0 as [tvars [P1 P2]].
- rewrite P2.
- intros.
- erewrite <- alloc_variables_app; eauto.
- eapply alloc_variables_match; eauto.
+ unfold init_mem; intros.
+ destruct progmatch as [[tglob [P Q]] R].
+ rewrite Q. erewrite <- alloc_globals_app; eauto.
+ eapply alloc_globals_match; eauto.
Qed.
End MATCH_PROGRAMS.
@@ -1661,21 +1544,20 @@ Variable A B V W: Type.
Variable transf_fun: A -> res B.
Variable transf_var: V -> res W.
-Variable new_functs : list (ident * B).
-Variable new_vars : list (ident * globvar W).
+Variable new_globs : list (ident * globdef B W).
Variable new_main : ident.
Variable p: program A V.
Variable p': program B W.
Hypothesis transf_OK:
- transform_partial_augment_program transf_fun transf_var new_functs new_vars new_main p = OK p'.
+ transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK p'.
Remark prog_match:
match_program
(fun fd tfd => transf_fun fd = OK tfd)
(fun info tinfo => transf_var info = OK tinfo)
- new_functs new_vars new_main
+ new_globs new_main
p p'.
Proof.
apply transform_partial_augment_program_match; auto.
@@ -1692,51 +1574,39 @@ Proof.
intros [tf [X Y]]. exists tf; auto.
Qed.
-
-
-(* This may not yet be in the ideal form for easy use .*)
Theorem find_new_funct_ptr_exists:
- list_norepet (prog_funct_names p ++ funct_names new_functs) ->
- list_disjoint (prog_funct_names p ++ funct_names new_functs) (prog_var_names p ++ var_names new_vars) ->
- forall id f, In (id, f) new_functs ->
+ list_norepet (List.map fst new_globs) ->
+ forall id f, In (id, Gfun f) new_globs ->
exists b, find_symbol (globalenv p') id = Some b
/\ find_funct_ptr (globalenv p') b = Some f.
Proof.
- intros.
- destruct p.
- unfold transform_partial_augment_program in transf_OK.
- monadInv transf_OK. rename x into prog_funct'. rename x0 into prog_vars'. simpl in *.
- assert (funct_names prog_funct = funct_names prog_funct').
- clear - EQ. generalize dependent prog_funct'. induction prog_funct; intros.
- simpl in EQ. inversion EQ; subst; auto.
- simpl in EQ. destruct a. destruct (transf_fun a); try discriminate. monadInv EQ.
- simpl; f_equal; auto.
- assert (var_names prog_vars = var_names prog_vars').
- clear - EQ1. generalize dependent prog_vars'. induction prog_vars; intros.
- simpl in EQ1. inversion EQ1; subst; auto.
- simpl in EQ1. destruct a. destruct (transf_globvar transf_var g); try discriminate. monadInv EQ1.
- simpl; f_equal; auto.
- apply find_funct_ptr_exists.
- unfold prog_funct_names in *; simpl in *.
- rewrite funct_names_app. rewrite <- H2. auto.
- unfold prog_funct_names, prog_var_names in *; simpl in *.
- rewrite funct_names_app. rewrite var_names_app. rewrite <- H2. rewrite <- H3. auto.
- simpl. intuition.
+ intros. destruct prog_match as [[tglob [P Q]] R].
+ unfold globalenv. rewrite Q. rewrite add_globals_app.
+ eapply add_globals_norepet_ensures; eauto.
+(* preserves *)
+ intros. unfold find_symbol, find_funct_ptr in *; simpl.
+ destruct H1 as [b [X Y]]. exists b; split.
+ rewrite PTree.gso; auto.
+ destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto.
+ exploit genv_funs_range; eauto. unfold ZIndexed.t; omega.
+ auto.
+(* ensures *)
+ intros. unfold find_symbol, find_funct_ptr in *; simpl.
+ exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss.
Qed.
Theorem find_funct_ptr_rev_transf_augment:
forall (b: block) (tf: B),
find_funct_ptr (globalenv p') b = Some tf ->
- if (zlt (genv_nextfun (globalenv p)) b) then
+ if zlt b (genv_next (globalenv p)) then
(exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf)
else
- In tf (map (@snd ident B) new_functs).
+ In (Gfun tf) (map snd new_globs).
Proof.
intros.
- exploit find_funct_ptr_rev_match;eauto. eexact prog_match; eauto. auto.
+ exploit find_funct_ptr_rev_match; eauto. eexact prog_match; eauto. auto.
Qed.
-
Theorem find_funct_transf_augment:
forall (v: val) (f: A),
find_funct (globalenv p) v = Some f ->
@@ -1744,15 +1614,14 @@ Theorem find_funct_transf_augment:
find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
Proof.
intros.
- exploit find_funct_match. eexact prog_match. eauto.
- intros [tf [X Y]]. exists tf; auto.
+ exploit find_funct_match. eexact prog_match. eauto. auto.
Qed.
Theorem find_funct_rev_transf_augment:
forall (v: val) (tf: B),
find_funct (globalenv p') v = Some tf ->
(exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf) \/
- In tf (map (@snd ident B) new_functs).
+ In (Gfun tf) (map snd new_globs).
Proof.
intros.
exploit find_funct_rev_match. eexact prog_match. eauto. auto.
@@ -1765,65 +1634,49 @@ Theorem find_var_info_transf_augment:
find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'.
Proof.
intros.
- exploit find_var_info_match. eexact prog_match. eauto.
- intros [tv [X Y]]. exists tv; split; auto. inv Y. unfold transf_globvar; simpl.
+ exploit find_var_info_match. eexact prog_match. eauto. intros [tv [X Y]].
+ exists tv; split; auto. inv Y. unfold transf_globvar; simpl.
rewrite H0; simpl. auto.
Qed.
Theorem find_new_var_exists:
- forall id gv,
- list_norepet (var_names new_vars) ->
- In (id, gv) new_vars ->
- exists b, find_symbol (globalenv p') id = Some b /\ find_var_info (globalenv p') b = Some gv.
-Proof.
- intros.
- assert (P: forall b vars (ge: t B W),
- ~In id (var_names vars) ->
- find_symbol ge id = Some b
- /\ find_var_info ge b = Some gv ->
- find_symbol (add_variables ge vars) id = Some b
- /\ find_var_info (add_variables ge vars) b = Some gv).
- induction vars; simpl; intros. auto. apply IHvars. tauto.
- destruct a as [id1 gv1]; unfold add_variable, find_symbol, find_var_info; simpl in *.
- destruct H2; split. rewrite PTree.gso. auto. intuition.
- rewrite ZMap.gso. auto. exploit genv_vars_range; eauto. unfold ZIndexed.t; omega.
-
- assert (Q: forall vars (ge: t B W),
- list_norepet (var_names vars) ->
- In (id, gv) vars ->
- exists b, find_symbol (add_variables ge vars) id = Some b
- /\ find_var_info (add_variables ge vars) b = Some gv).
- induction vars; simpl; intros.
- contradiction.
- destruct a as [id1 gv1]; simpl in *. inv H1. destruct H2. inv H1.
- exists (genv_nextvar ge). apply P; auto.
- unfold add_variable, find_symbol, find_var_info; simpl in *.
- split. apply PTree.gss. apply ZMap.gss.
- apply IHvars; auto.
-
- unfold transform_partial_augment_program in transf_OK.
- monadInv transf_OK. rename x into prog_funct'. rename x0 into prog_vars'. simpl in *.
- unfold globalenv; simpl. repeat rewrite add_variables_app. apply Q; auto.
+ list_norepet (List.map fst new_globs) ->
+ forall id gv, In (id, Gvar gv) new_globs ->
+ exists b, find_symbol (globalenv p') id = Some b
+ /\ find_var_info (globalenv p') b = Some gv.
+Proof.
+ intros. destruct prog_match as [[tglob [P Q]] R].
+ unfold globalenv. rewrite Q. rewrite add_globals_app.
+ eapply add_globals_norepet_ensures; eauto.
+(* preserves *)
+ intros. unfold find_symbol, find_var_info in *; simpl.
+ destruct H1 as [b [X Y]]. exists b; split.
+ rewrite PTree.gso; auto.
+ destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto.
+ exploit genv_vars_range; eauto. unfold ZIndexed.t; omega.
+(* ensures *)
+ intros. unfold find_symbol, find_var_info in *; simpl.
+ exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss.
Qed.
Theorem find_var_info_rev_transf_augment:
forall (b: block) (v': globvar W),
find_var_info (globalenv p') b = Some v' ->
- if zlt b (genv_nextvar (globalenv p)) then
+ if zlt b (genv_next (globalenv p)) then
(exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v')
else
- (In v' (map (@snd ident (globvar W)) new_vars)).
+ (In (Gvar v') (map snd new_globs)).
Proof.
intros.
exploit find_var_info_rev_match. eexact prog_match. eauto.
- destruct (zlt b (genv_nextvar (globalenv p))); auto.
+ destruct (zlt b (genv_next (globalenv p))); auto.
intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl.
rewrite H0; simpl. auto.
Qed.
Theorem find_symbol_transf_augment:
forall (s: ident),
- ~ In s (funct_names new_functs ++ var_names new_vars) ->
+ ~ In s (map fst new_globs) ->
find_symbol (globalenv p') s = find_symbol (globalenv p) s.
Proof.
intros. eapply find_symbol_match. eexact prog_match. auto.
@@ -1831,16 +1684,16 @@ Qed.
Theorem init_mem_transf_augment:
(forall s', find_symbol (globalenv p) s' <> None ->
- ~ In s' (funct_names new_functs ++ var_names new_vars)) ->
+ ~ In s' (map fst new_globs)) ->
forall m, init_mem p = Some m ->
- init_mem p' = alloc_variables (globalenv p') m new_vars.
+ init_mem p' = alloc_globals (globalenv p') m new_globs.
Proof.
intros. eapply init_mem_match. eexact prog_match. auto. auto.
Qed.
Theorem init_mem_inject_transf_augment:
(forall s', find_symbol (globalenv p) s' <> None ->
- ~ In s' (funct_names new_functs ++ var_names new_vars)) ->
+ ~ In s' (map fst new_globs)) ->
forall m, init_mem p = Some m ->
forall m', init_mem p' = Some m' ->
Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m'.
@@ -1848,10 +1701,9 @@ Proof.
intros.
pose proof (initmem_inject p H0).
erewrite init_mem_transf_augment in H1; eauto.
- eapply alloc_variables_augment; eauto. omega.
+ eapply alloc_globals_augment; eauto. omega.
Qed.
-
End TRANSF_PROGRAM_AUGMENT.
Section TRANSF_PROGRAM_PARTIAL2.
@@ -1865,13 +1717,9 @@ Hypothesis transf_OK:
transform_partial_program2 transf_fun transf_var p = OK p'.
Remark transf_augment_OK:
- transform_partial_augment_program transf_fun transf_var nil nil p.(prog_main) p = OK p'.
+ transform_partial_augment_program transf_fun transf_var nil p.(prog_main) p = OK p'.
Proof.
- rewrite <- transf_OK.
- unfold transform_partial_augment_program, transform_partial_program2.
- destruct (map_partial prefix_name transf_fun (prog_funct p)); auto. simpl.
- destruct (map_partial prefix_name (transf_globvar transf_var) (prog_vars p)); simpl.
- repeat rewrite app_nil_r. auto. auto.
+ rewrite <- transf_OK. apply symmetry. apply transform_partial_program2_augment.
Qed.
Theorem find_funct_ptr_transf_partial2:
@@ -1880,7 +1728,7 @@ Theorem find_funct_ptr_transf_partial2:
exists f',
find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.
Proof.
- exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+ exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
Qed.
Theorem find_funct_ptr_rev_transf_partial2:
@@ -1888,9 +1736,9 @@ Theorem find_funct_ptr_rev_transf_partial2:
find_funct_ptr (globalenv p') b = Some tf ->
exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf.
Proof.
- pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+ pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
intros. pose proof (H b tf H0).
- destruct (zlt (genv_nextfun (globalenv p)) b). auto. inversion H1.
+ destruct (zlt b (genv_next (globalenv p))). auto. contradiction.
Qed.
Theorem find_funct_transf_partial2:
@@ -1899,7 +1747,7 @@ Theorem find_funct_transf_partial2:
exists f',
find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
Proof.
- exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+ exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
Qed.
Theorem find_funct_rev_transf_partial2:
@@ -1907,9 +1755,9 @@ Theorem find_funct_rev_transf_partial2:
find_funct (globalenv p') v = Some tf ->
exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf.
Proof.
- pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+ pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
intros. pose proof (H v tf H0).
- destruct H1. auto. inversion H1.
+ destruct H1. auto. contradiction.
Qed.
Theorem find_var_info_transf_partial2:
@@ -1918,7 +1766,7 @@ Theorem find_var_info_transf_partial2:
exists v',
find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'.
Proof.
- exact (@find_var_info_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+ exact (@find_var_info_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
Qed.
Theorem find_var_info_rev_transf_partial2:
@@ -1927,23 +1775,23 @@ Theorem find_var_info_rev_transf_partial2:
exists v,
find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v'.
Proof.
- pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+ pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
intros. pose proof (H b v' H0).
- destruct (zlt b (genv_nextvar (globalenv p))). auto. inversion H1.
+ destruct (zlt b (genv_next (globalenv p))). auto. contradiction.
Qed.
Theorem find_symbol_transf_partial2:
forall (s: ident),
find_symbol (globalenv p') s = find_symbol (globalenv p) s.
Proof.
- pose proof (@find_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+ pose proof (@find_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
auto.
Qed.
Theorem init_mem_transf_partial2:
forall m, init_mem p = Some m -> init_mem p' = Some m.
Proof.
- pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+ pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
intros. simpl in H. apply H; auto.
Qed.
@@ -1957,24 +1805,13 @@ Variable p: program A V.
Variable p': program B V.
Hypothesis transf_OK: transform_partial_program transf p = OK p'.
-Remark transf2_OK:
- transform_partial_program2 transf (fun x => OK x) p = OK p'.
-Proof.
- rewrite <- transf_OK.
- unfold transform_partial_program2, transform_partial_program.
- destruct (map_partial prefix_name transf (prog_funct p)); auto.
- simpl. replace (transf_globvar (fun (x : V) => OK x)) with (fun (v: globvar V) => OK v).
- rewrite map_partial_identity; auto.
- apply extensionality; intros. destruct x; auto.
-Qed.
-
Theorem find_funct_ptr_transf_partial:
forall (b: block) (f: A),
find_funct_ptr (globalenv p) b = Some f ->
exists f',
find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'.
Proof.
- exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+ exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
Qed.
Theorem find_funct_ptr_rev_transf_partial:
@@ -1982,7 +1819,7 @@ Theorem find_funct_ptr_rev_transf_partial:
find_funct_ptr (globalenv p') b = Some tf ->
exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf.
Proof.
- exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+ exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
Qed.
Theorem find_funct_transf_partial:
@@ -1991,7 +1828,7 @@ Theorem find_funct_transf_partial:
exists f',
find_funct (globalenv p') v = Some f' /\ transf f = OK f'.
Proof.
- exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+ exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
Qed.
Theorem find_funct_rev_transf_partial:
@@ -1999,14 +1836,14 @@ Theorem find_funct_rev_transf_partial:
find_funct (globalenv p') v = Some tf ->
exists f, find_funct (globalenv p) v = Some f /\ transf f = OK tf.
Proof.
- exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+ exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
Qed.
Theorem find_symbol_transf_partial:
forall (s: ident),
find_symbol (globalenv p') s = find_symbol (globalenv p) s.
Proof.
- exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+ exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
Qed.
Theorem find_var_info_transf_partial:
@@ -2014,10 +1851,10 @@ Theorem find_var_info_transf_partial:
find_var_info (globalenv p') b = find_var_info (globalenv p) b.
Proof.
intros. case_eq (find_var_info (globalenv p) b); intros.
- exploit find_var_info_transf_partial2. eexact transf2_OK. eauto.
+ exploit find_var_info_transf_partial2. eexact transf_OK. eauto.
intros [v' [P Q]]. monadInv Q. rewrite P. inv EQ. destruct g; auto.
case_eq (find_var_info (globalenv p') b); intros.
- exploit find_var_info_rev_transf_partial2. eexact transf2_OK. eauto.
+ exploit find_var_info_rev_transf_partial2. eexact transf_OK. eauto.
intros [v' [P Q]]. monadInv Q. inv EQ. congruence.
auto.
Qed.
@@ -2025,7 +1862,7 @@ Qed.
Theorem init_mem_transf_partial:
forall m, init_mem p = Some m -> init_mem p' = Some m.
Proof.
- exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+ exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
Qed.
End TRANSF_PROGRAM_PARTIAL.
@@ -2040,8 +1877,7 @@ Let tp := transform_program transf p.
Remark transf_OK:
transform_partial_program (fun x => OK (transf x)) p = OK tp.
Proof.
- unfold tp, transform_program, transform_partial_program.
- rewrite map_partial_total. reflexivity.
+ unfold tp. apply transform_program_partial_program.
Qed.
Theorem find_funct_ptr_transf:
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 6fbfacd..e6e8cc2 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -184,91 +184,6 @@ Proof.
intros; unfold print. destruct (printer prog); auto.
Qed.
-Lemma map_partial_compose:
- forall (X A B C: Type)
- (ctx: X -> errmsg)
- (f1: A -> res B) (f2: B -> res C)
- (pa: list (X * A)) (pc: list (X * C)),
- map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc ->
- { pb | map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc }.
-Proof.
- induction pa; simpl.
- intros. inv H. econstructor; eauto.
- intro pc. destruct a as [x a].
- destruct (f1 a) as [] _eqn; simpl; try congruence.
- destruct (f2 b) as [] _eqn; simpl; try congruence.
- destruct (map_partial ctx (fun f => f1 f @@@ f2) pa) as [] _eqn; simpl; try congruence.
- intros. inv H.
- destruct (IHpa l) as [pb [P Q]]; auto.
- rewrite P; simpl.
- econstructor; split. eauto. simpl. rewrite Heqr0. rewrite Q. auto.
-Qed.
-
-Lemma transform_partial_program_compose:
- forall (A B C V: Type)
- (f1: A -> res B) (f2: B -> res C)
- (pa: program A V) (pc: program C V),
- transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc ->
- { pb | transform_partial_program f1 pa = OK pb /\
- transform_partial_program f2 pb = OK pc }.
-Proof.
- intros. unfold transform_partial_program in H.
- destruct (map_partial prefix_name (fun f : A => f1 f @@@ f2) (prog_funct pa)) as [] _eqn;
- simpl in H; inv H.
- destruct (map_partial_compose _ _ _ _ _ _ _ _ _ Heqr) as [xb [P Q]].
- exists (mkprogram xb (prog_main pa) (prog_vars pa)); split.
- unfold transform_partial_program. rewrite P; auto.
- unfold transform_partial_program. simpl. rewrite Q; auto.
-Qed.
-
-Lemma transform_program_partial_program:
- forall (A B V: Type) (f: A -> B) (p: program A V) (tp: program B V),
- transform_partial_program (fun x => OK (f x)) p = OK tp ->
- transform_program f p = tp.
-Proof.
- intros until tp. unfold transform_partial_program.
- rewrite map_partial_total. simpl. intros. inv H. auto.
-Qed.
-
-Lemma transform_program_compose:
- forall (A B C V: Type)
- (f1: A -> res B) (f2: B -> C)
- (pa: program A V) (pc: program C V),
- transform_partial_program (fun f => f1 f @@ f2) pa = OK pc ->
- { pb | transform_partial_program f1 pa = OK pb /\
- transform_program f2 pb = pc }.
-Proof.
- intros.
- replace (fun f : A => f1 f @@ f2)
- with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H.
- destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [pb [X Y]].
- exists pb; split. auto.
- apply transform_program_partial_program. auto.
- apply extensionality; intro. destruct(f1 x); auto.
-Qed.
-
-Lemma transform_partial_program_identity:
- forall (A V: Type) (pa pb: program A V),
- transform_partial_program (@OK A) pa = OK pb ->
- pa = pb.
-Proof.
- intros until pb. unfold transform_partial_program.
- replace (@OK A) with (fun b => @OK A b).
- rewrite map_partial_identity. simpl. destruct pa; simpl; congruence.
- apply extensionality; auto.
-Qed.
-
-Lemma transform_program_print_identity:
- forall (A V: Type) (p: program A V) (f: A -> unit),
- transform_program (print f) p = p.
-Proof.
- intros until f. unfold transform_program, transf_program.
- destruct p; simpl; f_equal.
- transitivity (map (fun x => x) prog_funct).
- apply list_map_exten; intros. destruct x; simpl. rewrite print_identity. auto.
- apply list_map_identity.
-Qed.
-
Lemma compose_print_identity:
forall (A: Type) (x: res A) (f: A -> unit),
x @@ print f = x.
@@ -290,18 +205,6 @@ Qed.
These results establish the correctness of the whole compiler! *)
-Ltac TransfProgInv :=
- match goal with
- | [ H: transform_partial_program (fun f => _ @@@ _) _ = OK _ |- _ ] =>
- let p := fresh "p" in let X := fresh "X" in let P := fresh "P" in
- destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p [X P]];
- clear H
- | [ H: transform_partial_program (fun f => _ @@ _) _ = OK _ |- _ ] =>
- let p := fresh "p" in let X := fresh "X" in let P := fresh "P" in
- destruct (transform_program_compose _ _ _ _ _ _ _ _ H) as [p [X P]];
- clear H
- end.
-
Theorem transf_rtl_program_correct:
forall p tp,
transf_rtl_program p = OK tp ->
diff --git a/driver/Interp.ml b/driver/Interp.ml
index fc0526a..9031042 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -87,9 +87,11 @@ let print_event p = function
let name_of_fundef prog fd =
let rec find_name = function
| [] -> "<unknown function>"
- | (id, fd') :: rem ->
+ | (id, Gfun fd') :: rem ->
if fd = fd' then extern_atom id else find_name rem
- in find_name prog.prog_funct
+ | (id, Gvar v) :: rem ->
+ find_name rem
+ in find_name prog.prog_defs
let name_of_function prog fn =
name_of_fundef prog (Internal fn)
@@ -468,11 +470,13 @@ let rec explore p prog ge time ss =
(* Massaging the source program *)
let unvolatile prog =
- let unvolatile_globvar (id, gv) =
- (id, if gv.gvar_volatile
- then {gv with gvar_readonly = false; gvar_volatile = false}
- else gv) in
- {prog with prog_vars = List.map unvolatile_globvar prog.prog_vars}
+ let unvolatile_globdef = function
+ | (id, Gvar gv) ->
+ (id, Gvar(if gv.gvar_volatile
+ then {gv with gvar_readonly = false; gvar_volatile = false}
+ else gv))
+ | idfd -> idfd in
+ {prog with prog_defs = List.map unvolatile_globdef prog.prog_defs}
let change_main_function p old_main old_main_ty =
let old_main = Evalof(Evar(old_main, old_main_ty), old_main_ty) in
@@ -483,24 +487,29 @@ let change_main_function p old_main old_main_ty =
let new_main_fn =
{ fn_return = type_int32s; fn_params = []; fn_vars = []; fn_body = body } in
let new_main_id = intern_string "___main" in
- { p with
- prog_main = new_main_id;
- prog_funct = (new_main_id, Internal new_main_fn) :: p.prog_funct }
+ { prog_main = new_main_id;
+ prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs }
+
+let rec find_main_function name = function
+ | [] -> None
+ | (id, Gfun fd) :: gdl -> if id = name then Some fd else find_main_function name gdl
+ | (id, Gvar v) :: gdl -> find_main_function name gdl
let fixup_main p =
- try
- match type_of_fundef (List.assoc p.prog_main p.prog_funct) with
- | Tfunction(Tnil, Tint(I32, Signed, _)) ->
- Some p
- | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)),
- Tint _) as ty ->
- Some (change_main_function p p.prog_main ty)
- | _ ->
- fprintf err_formatter "ERROR: wrong type for main() function";
- None
- with Not_found ->
- fprintf err_formatter "ERROR: no main() function";
- None
+ match find_main_function p.prog_main p.prog_defs with
+ | None ->
+ fprintf err_formatter "ERROR: no main() function";
+ None
+ | Some main_fd ->
+ match type_of_fundef main_fd with
+ | Tfunction(Tnil, Tint(I32, Signed, _)) ->
+ Some p
+ | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)),
+ Tint _) as ty ->
+ Some (change_main_function p p.prog_main ty)
+ | _ ->
+ fprintf err_formatter "ERROR: wrong type for main() function";
+ None
(* Execution of a whole program *)
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index a36adb1..08bd2f5 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -767,11 +767,6 @@ let print_function oc name code =
jumptables := []
end
-let print_fundef oc (name, defn) =
- match defn with
- | Internal code -> print_function oc name code
- | External ef -> ()
-
let print_init oc = function
| Init_int8 n ->
fprintf oc " .byte %ld\n" (camlint_of_coqint n)
@@ -802,7 +797,7 @@ let print_init_data oc name id =
else
List.iter (print_init oc) id
-let print_var oc (name, v) =
+let print_var oc name v =
match v.gvar_init with
| [] -> ()
| _ ->
@@ -826,11 +821,16 @@ let print_var oc (name, v) =
fprintf oc " .size %a, . - %a\n" symbol name symbol name
end
+let print_globdef oc (name, gdef) =
+ match gdef with
+ | Gfun(Internal code) -> print_function oc name code
+ | Gfun(External ef) -> ()
+ | Gvar v -> print_var oc name v
+
let print_program oc p =
need_masks := false;
indirect_symbols := StringSet.empty;
- List.iter (print_var oc) p.prog_vars;
- List.iter (print_fundef oc) p.prog_funct;
+ List.iter (print_globdef oc) p.prog_defs;
if !need_masks then begin
section oc Section_const; (* not Section_literal because not 8-bytes *)
print_align oc 16;
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index ac9a5da..5bfd3ee 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -881,7 +881,7 @@ let function_needs_stub name =
(* Generation of whole programs *)
-let print_fundef oc (name, defn) =
+let print_fundef oc name defn =
match defn with
| Internal code ->
print_function oc name code
@@ -890,13 +890,12 @@ let print_fundef oc (name, defn) =
| External _ ->
()
-let record_extfun (name, defn) =
- match defn with
- | Internal _ -> ()
- | External (EF_external _ | EF_malloc | EF_free) ->
+let record_extfun (name, gd) =
+ match gd with
+ | Gfun(External (EF_external _ | EF_malloc | EF_free)) ->
if function_needs_stub name then
stubbed_functions := IdentSet.add name !stubbed_functions
- | External _ -> ()
+ | _ -> ()
let print_init oc = function
| Init_int8 n ->
@@ -930,7 +929,7 @@ let print_init_data oc name id =
else
List.iter (print_init oc) id
-let print_var oc (name, v) =
+let print_var oc name v =
match v.gvar_init with
| [] -> ()
| _ ->
@@ -963,9 +962,13 @@ let print_var oc (name, v) =
(1 lsl align)
end
+let print_globdef oc (name, gdef) =
+ match gdef with
+ | Gfun f -> print_fundef oc name f
+ | Gvar v -> print_var oc name v
+
let print_program oc p =
stubbed_functions := IdentSet.empty;
- List.iter record_extfun p.prog_funct;
- List.iter (print_var oc) p.prog_vars;
- List.iter (print_fundef oc) p.prog_funct
+ List.iter record_extfun p.prog_defs;
+ List.iter (print_globdef oc) p.prog_defs
diff --git a/test/regression/Makefile b/test/regression/Makefile
index a649f88..e8fb236 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -9,7 +9,7 @@ LIBS=$(LIBMATH)
TESTS=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
bitfields5 bitfields6 bitfields7 \
- expr1 expr6 initializers volatile1 volatile2 volatile3 \
+ expr1 expr6 funptr2 initializers volatile1 volatile2 volatile3 \
funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \
sizeof1 sizeof2 packedstruct1 packedstruct2 \
instrsel bool compar
diff --git a/test/regression/Results/funptr2 b/test/regression/Results/funptr2
new file mode 100644
index 0000000..f364c59
--- /dev/null
+++ b/test/regression/Results/funptr2
@@ -0,0 +1,3 @@
+f == f is 1
+f == g is 0
+f + 1 == f is 0
diff --git a/test/regression/Results/initializers b/test/regression/Results/initializers
index d3fc91a..7474148 100644
--- a/test/regression/Results/initializers
+++ b/test/regression/Results/initializers
@@ -1,3 +1,4 @@
+x0 = 0
x1 = 'x'
x2 = 12345
x3 = 3.14159
diff --git a/test/regression/funptr2.c b/test/regression/funptr2.c
new file mode 100644
index 0000000..5c31dd2
--- /dev/null
+++ b/test/regression/funptr2.c
@@ -0,0 +1,14 @@
+/* Comparisons of pointers to functions */
+
+#include <stdio.h>
+
+int f(void) { return 0; }
+int g(void) { return 1; }
+
+int main(void) {
+ printf ("f == f is %d\n", &f == &f);
+ printf ("f == g is %d\n", &f == &g);
+ /* The following is undefined behavior */
+ printf ("f + 1 == f is %d\n", ((char *) &f) + 1 == (char *) &f);
+ return 0;
+}
diff --git a/test/regression/initializers.c b/test/regression/initializers.c
index f831c67..d0a35f3 100644
--- a/test/regression/initializers.c
+++ b/test/regression/initializers.c
@@ -1,5 +1,7 @@
#include <stdio.h>
+int x0;
+
char x1 = 'x';
int x2 = 12345;
@@ -67,6 +69,7 @@ int main()
{
int i;
+ printf("x0 = %d\n", x0);
printf("x1 = '%c'\n", x1);
printf("x2 = %d\n", x2);
printf("x3 = %.5f\n", x3);