diff options
| -rw-r--r-- | Changelog | 1 | ||||
| -rw-r--r-- | backend/CMlexer.mll | 16 | ||||
| -rw-r--r-- | backend/CMparser.mly | 75 | ||||
| -rw-r--r-- | backend/PrintCminor.ml | 47 | ||||
| -rw-r--r-- | backend/RTLgen.v | 2 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 1 | ||||
| -rw-r--r-- | common/AST.v | 128 | ||||
| -rw-r--r-- | common/Errors.v | 3 | ||||
| -rw-r--r-- | common/Globalenvs.v | 694 | ||||
| -rw-r--r-- | common/Memory.v | 52 | ||||
| -rw-r--r-- | common/Memtype.v | 10 | ||||
| -rw-r--r-- | driver/Driver.ml | 9 |
12 files changed, 913 insertions, 125 deletions
@@ -40,6 +40,7 @@ Other improvements: - Reference interpreter: better printing of pointer values and locations. - Added command-line options -Wp,<opt> -Wa,<opt> -Wl,<opt> to pass specific options to the preprocessor, assembler, or linker, respectively. +- More complete Cminor parser and printer (contributed by Andrew Tolmach). Release 1.9.1, 2011-11-28 diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index 3506e50..780d812 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -24,7 +24,8 @@ let floatlit = ['0'-'9'] ['0'-'9' '_']* ('.' ['0'-'9' '_']* )? (['e' 'E'] ['+' '-']? ['0'-'9'] ['0'-'9' '_']*)? -let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '0'-'9']* +let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '$' '0'-'9']* +let temp = "$" ['0'-'9'] ['0'-'9']* let intlit = "-"? ( ['0'-'9']+ | "0x" ['0'-'9' 'a'-'f' 'A'-'F']+ | "0o" ['0'-'7']+ | "0b" ['0'-'1']+ ) let stringlit = "\"" [ ^ '"' ] * '"' @@ -46,7 +47,6 @@ rule token = parse | ":" { COLON } | "," { COMMA } | "default" { DEFAULT } - | "$" { DOLLAR } | "else" { ELSE } | "=" { EQUAL } | "==" { EQUALEQUAL } @@ -59,6 +59,7 @@ rule token = parse | "float64" { FLOAT64 } | "floatofint" { FLOATOFINT } | "floatofintu" { FLOATOFINTU } + | "goto" { GOTO } | ">" { GREATER } | ">f" { GREATERF } | ">u" { GREATERU } @@ -69,10 +70,13 @@ rule token = parse | ">>u" { GREATERGREATERU } | "if" { IF } | "in" { IN } + | "inline" { INLINE } | "int" { INT } + | "int16" { INT16 } | "int16s" { INT16S } | "int16u" { INT16U } | "int32" { INT32 } + | "int8" { INT8 } | "int8s" { INT8S } | "int8u" { INT8U } | "intoffloat" { INTOFFLOAT } @@ -102,6 +106,7 @@ rule token = parse | "}" { RBRACE } | "}}" { RBRACERBRACE } | "]" { RBRACKET } + | "readonly" { READONLY } | "return" { RETURN } | ")" { RPAREN } | ";" { SEMICOLON } @@ -116,12 +121,17 @@ rule token = parse | "~" { TILDE } | "var" { VAR } | "void" { VOID } + | "volatile" { VOLATILE } + | "while" { WHILE } | intlit { INTLIT(Int32.of_string(Lexing.lexeme lexbuf)) } | floatlit { FLOATLIT(float_of_string(Lexing.lexeme lexbuf)) } | stringlit { let s = Lexing.lexeme lexbuf in STRINGLIT(intern_string(String.sub s 1 (String.length s - 2))) } - | ident { IDENT(intern_string(Lexing.lexeme lexbuf)) } + | ident { IDENT(BinPos.Coq_xO (intern_string(Lexing.lexeme lexbuf))) } + | temp { let s = Lexing.lexeme lexbuf in + let n = Int32.of_string(String.sub s 1 (String.length s -1)) in + IDENT(if n = 0l then BinPos.Coq_xH else BinPos.Coq_xI (positive_of_camlint n)) } | eof { EOF } | _ { raise(Error("illegal character `" ^ Char.escaped (Lexing.lexeme_char lexbuf 0) ^ "'")) } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 3df3f54..c52261d 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -13,6 +13,10 @@ /* */ /* *********************************************************************/ +/* HASP: Modified to parse global data declarations, other small changes */ +/* Note that this compiles a superset of the language defined by the AST, + including function calls in expressions, matches, while statements, etc. */ + %{ open Datatypes open Camlcoq @@ -22,6 +26,7 @@ open Integers open AST open Cminor + (** Naming function calls in expressions *) type rexpr = @@ -40,7 +45,7 @@ let temporaries = ref [] let mktemp () = incr temp_counter; let n = Printf.sprintf "__t%d" !temp_counter in - let id = intern_string n in + let id = Coq_xO (intern_string n) in temporaries := id :: !temporaries; id @@ -123,6 +128,9 @@ let mktailcall sg e1 el = let cl = convert_rexpr_list el in prepend_seq !convert_accu (Stailcall(sg, c1, cl)) +let mkwhile expr body = + Sblock (Sloop (mkifthenelse expr body (Sexit O))) + (** Other constructors *) let intconst n = @@ -133,7 +141,7 @@ let andbool e1 e2 = let orbool e1 e2 = Rcondition(e1, intconst 1l, e2) -let exitnum n = nat_of_camlint(Int32.pred n) +let exitnum n = nat_of_camlint n let mkswitch expr (cases, dfl) = convert_accu := []; @@ -207,7 +215,6 @@ let mkmatch expr cases = %token COLON %token COMMA %token DEFAULT -%token DOLLAR %token ELSE %token EQUAL %token EQUALEQUAL @@ -222,6 +229,7 @@ let mkmatch expr cases = %token <float> FLOATLIT %token FLOATOFINT %token FLOATOFINTU +%token GOTO %token GREATER %token GREATERF %token GREATERU @@ -233,10 +241,13 @@ let mkmatch expr cases = %token <AST.ident> IDENT %token IF %token IN +%token INLINE %token INT +%token INT16 %token INT16S %token INT16U %token INT32 +%token INT8 %token INT8S %token INT8U %token <int32> INTLIT @@ -267,6 +278,7 @@ let mkmatch expr cases = %token RBRACE %token RBRACERBRACE %token RBRACKET +%token READONLY %token RETURN %token RPAREN %token SEMICOLON @@ -282,6 +294,8 @@ let mkmatch expr cases = %token TAILCALL %token VAR %token VOID +%token VOLATILE +%token WHILE /* Precedences from low to high */ @@ -323,11 +337,47 @@ global_declarations: ; global_declaration: - VAR STRINGLIT LBRACKET INTLIT RBRACKET + VAR STRINGLIT LBRACKET INTLIT RBRACKET /* old style */ { ($2, {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; } ) } ; +is_readonly: + /* empty */ { false } + | READONLY { true } + +is_volatile: + /* empty */ { false } + | VOLATILE { true } + +init_data_list: + /* empty */ { [] } + | init_data_list_1 { $1 } + ; + +init_data_list_1: + init_data { [$1] } + | init_data_list_1 COMMA init_data { $3 :: $1 } + ; + +init_data: + INT8 INTLIT { Init_int8 (coqint_of_camlint $2) } + | INT16 INTLIT { Init_int16 (coqint_of_camlint $2) } + | INT32 INTLIT { Init_int32 (coqint_of_camlint $2) } + | INT INTLIT { Init_int32 (coqint_of_camlint $2) } + | INTLIT { Init_int32 (coqint_of_camlint $1) } + | FLOAT32 FLOATLIT { Init_float32 ($2) } + | FLOAT64 FLOATLIT { Init_float64 ($2) } + | FLOAT FLOATLIT { Init_float64 ($2) } + | FLOATLIT { Init_float64 ($1) } + | LBRACKET INTLIT RBRACKET { Init_space (z_of_camlint $2) } + | INTLIT LPAREN STRINGLIT RPAREN { Init_addrof ($3, coqint_of_camlint $1) } + ; + + proc_list: /* empty */ { [] } | proc_list proc { $2 :: $1 } @@ -345,13 +395,14 @@ proc: { let tmp = !temporaries in 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 }) } + ($1, + 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, External(EF_external($2,$4))) } ; signature: @@ -408,6 +459,9 @@ stmt: { mkmatch $3 $6 } | TAILCALL expr LPAREN expr_list RPAREN COLON signature SEMICOLON { mktailcall $7 $2 $4 } + | WHILE LPAREN expr RPAREN stmts { mkwhile $3 $5 } + | IDENT COLON stmts { Slabel ($1,$3) } + | GOTO IDENT SEMICOLON { Sgoto $2 } ; stmts: @@ -525,3 +579,4 @@ type_: INT { Tint } | FLOAT { Tfloat } ; + diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 110e735..330c6c2 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -42,7 +42,7 @@ let rec precedence = function | Eload _ -> (15, RtoL) | Econdition _ -> (3, RtoL) -(* Naming idents. We assume we run after Cminorgen, which encoded idents. *) +(* Naming idents. We assume idents are encoded as in Cminorgen. *) let ident_name id = match id with @@ -185,7 +185,7 @@ let rec print_stmt p s = print_expr_list (true, el) print_sig sg | Scall(Some id, sg, e1, el) -> - fprintf p "@[<hv 2>%s =@ %a@,(@[<hov 0>%a@]);@] : @[<hov 0>%a@]" + fprintf p "@[<hv 2>%s =@ %a@,(@[<hov 0>%a@])@] : @[<hov 0>%a;@]" (ident_name id) print_expr e1 print_expr_list (true, el) @@ -245,9 +245,9 @@ let rec print_stmt p s = | Sreturn (Some e) -> fprintf p "return %a;" print_expr e | Slabel(lbl, s1) -> - fprintf p "%s:@ %a" (extern_atom lbl) print_stmt s1 + fprintf p "%s:@ %a" (ident_name lbl) print_stmt s1 (* wrong for Cminorgen output *) | Sgoto lbl -> - fprintf p "goto %s;" (extern_atom lbl) + fprintf p "goto %s;" (ident_name lbl) (* wrong for Cminorgen output *) (* Functions *) @@ -273,15 +273,50 @@ let print_function p id f = print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ " +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 -> - () (* Todo? *) + 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) + | Init_int32 i -> fprintf p "%ld" (camlint_of_coqint i) + | Init_float32 f -> fprintf p "float32 %F" f + | Init_float64 f -> fprintf p "%F" f + | Init_space i -> fprintf p "[%ld]" (camlint_of_coqint i) + | Init_addrof(id,off) -> fprintf p "%ld(\"%s\")" (camlint_of_coqint off) (extern_atom id) + +let rec print_init_data_list p = function + | [] -> () + | [item] -> print_init_data p item + | item::rest -> + (print_init_data p item; + fprintf p ","; + print_init_data_list p rest) + +let print_globvar p gv = + if (gv.gvar_readonly) then + fprintf p "readonly "; + if (gv.gvar_volatile) then + fprintf p "volatile "; + fprintf p "{"; + 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_program p prog = - fprintf p "@[<v 0>"; + 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 "@]@." diff --git a/backend/RTLgen.v b/backend/RTLgen.v index a9c8f97..28d2b06 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -319,7 +319,7 @@ Fixpoint add_vars (map: mapping) (names: list ident) Definition find_var (map: mapping) (name: ident) : mon reg := match PTree.get name map.(map_vars) with - | None => error (Errors.MSG "RTLgen: unbound variable " :: Errors.CTX name :: nil) + | None => error (Errors.MSG "RTLgen: unbound variable " :: Errors.CTXL name :: nil) | Some r => ret r end. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 14e345b..6386445 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -727,6 +727,7 @@ let string_of_errmsg msg = let string_of_err = function | CompcertErrors.MSG s -> camlstring_of_coqstring s | CompcertErrors.CTX i -> extern_atom i + | CompcertErrors.CTXL i -> "" (* should not happen *) in String.concat "" (List.map string_of_err msg) let rec convertInit env init = diff --git a/common/AST.v b/common/AST.v index becf4e4..bcd63a2 100644 --- a/common/AST.v +++ b/common/AST.v @@ -131,11 +131,29 @@ Record program (F V: Type) : Type := mkprogram { prog_vars: list (ident * globvar V) }. +Definition funct_names (F: Type) (fl: list (ident * F)) : list ident := + map (@fst ident F) fl. + +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 := - map (@fst ident F) p.(prog_funct). + funct_names p.(prog_funct). Definition prog_var_names (F V: Type) (p: program F V) : list ident := - map (@fst ident (globvar V)) p.(prog_vars). + var_names p.(prog_vars). (** * Generic transformations over programs *) @@ -337,12 +355,71 @@ 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: + 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. +Proof. + intros. monadInv H. reflexivity. +Qed. + + +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. +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. +Qed. + +End TRANSF_PARTIAL_AUGMENT_PROGRAM. + + (** The following is a relational presentation of - [transform_program_partial2]. Given relations between function + [transform_partial_augment_preogram]. Given relations between function definitions and between variable information, it defines a relation - between programs stating that the two programs have the same shape - (same global names, etc) and that identically-named function definitions - are variable information are related. *) + between programs stating that the two programs have appropriately related + shapes (global names are preserved and possibly augmented, etc) + and that identically-named function definitions + and variable information are related. *) Section MATCH_PROGRAM. @@ -361,37 +438,50 @@ Inductive match_var_entry: ident * globvar V -> ident * globvar W -> Prop := match_var_entry (id, mkglobvar info1 init ro vo) (id, mkglobvar info2 init ro vo). -Definition match_program (p1: program A V) (p2: program B W) : Prop := - list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct) - /\ p1.(prog_main) = p2.(prog_main) - /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars). +Definition match_program (new_functs : list (ident * B)) + (new_vars : list (ident * globvar 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)) /\ + p2.(prog_main) = new_main. End MATCH_PROGRAM. -Remark transform_partial_program2_match: +Remark transform_partial_augment_program_match: forall (A B V W: Type) (transf_partial_function: A -> res B) - (transf_partial_variable: V -> res W) - (p: program A V) (tp: program B W), - transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp -> + (transf_partial_variable : V -> res W) + (p: program A V) + (new_functs : list (ident * B)) + (new_vars : list (ident * globvar 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 -> 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 p tp. Proof. - intros. monadInv H. split. + 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. - split. auto. + 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. + eapply map_partial_forall2. eauto. intros. destruct v1; destruct v2; simpl in *. destruct H1; subst. - monadInv H2. destruct g; simpl in *. constructor. auto. + monadInv H2. destruct g; simpl in *. constructor. auto. auto. auto. Qed. (** * External functions *) diff --git a/common/Errors.v b/common/Errors.v index 36e70c5..a70ea6e 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -30,7 +30,8 @@ Set Implicit Arguments. Inductive errcode: Type := | MSG: string -> errcode - | CTX: positive -> errcode. + | CTX: positive -> errcode (* a top-level identifier *) + | CTXL: positive -> errcode. (* an encoded local identifier *) Definition errmsg: Type := list errcode. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index a9db51e..367f44a 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -3,6 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* with contributions from Andrew Tolmach (Portland State University) *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -214,9 +215,22 @@ Qed. Definition add_functions (ge: t) (fl: list (ident * F)) : t := List.fold_left add_function fl ge. +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. + + Definition add_variables (ge: t) (vl: list (ident * globvar V)) : t := List.fold_left add_variable vl ge. +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. +Qed. + Definition globalenv (p: program F V) := add_variables (add_functions empty_genv p.(prog_funct)) p.(prog_vars). @@ -262,9 +276,49 @@ Proof. intros. unfold globalenv; eauto. 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. + 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. +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 (map (@fst ident F) fl) -> + ~In id (funct_names fl) -> find_symbol (add_functions ge fl) id = find_symbol ge id. Proof. induction fl; simpl; intros. auto. @@ -284,7 +338,7 @@ Qed. Remark add_variables_same_symb: forall id vl ge, - ~In id (map (@fst ident (globvar V)) vl) -> + ~In id (var_names vl) -> find_symbol (add_variables ge vl) id = find_symbol ge id. Proof. induction vl; simpl; intros. auto. @@ -332,7 +386,7 @@ Theorem find_funct_ptr_exists: Proof. intros until f. - assert (forall fl ge, In (id, f) fl -> list_norepet (map (@fst ident F) fl) -> + 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. @@ -606,6 +660,15 @@ Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V)) 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). +Proof. + induction vl1. + simpl. intros. inversion H; subst. auto. + simpl. intros. destruct (alloc_variable m a); eauto. inversion H. +Qed. + Remark store_init_data_list_nextblock: forall idl b m p m', store_init_data_list m b p idl = Some m' -> @@ -629,6 +692,28 @@ Proof. congruence. Qed. +Remark alloc_variable_nextblock: + forall v m m', + alloc_variable m v = 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' -> @@ -897,6 +982,17 @@ Proof. red. rewrite H1. rewrite <- H3. intuition. Qed. +Lemma init_mem_genv_vars : forall p m, + init_mem p = Some m -> + genv_nextvar (globalenv p) = Mem.nextblock m. +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. +Qed. + Theorem find_var_info_not_fresh: forall p b gv m, init_mem p = Some m -> @@ -1028,6 +1124,102 @@ Proof. omega. Qed. +Section INITMEM_AUGMENT_INJ. + +Variable ge: t. +Variable thr: block. + +Lemma store_init_data_augment: + forall m1 m2 b p id m2', + Mem.inject (Mem.flat_inj thr) m1 m2 -> + b >= thr -> + store_init_data ge m2 b p id = Some m2' -> + Mem.inject (Mem.flat_inj thr) m1 m2'. +Proof. + intros until m2'. intros INJ BND ST. + assert (P: forall chunk ofs v m2', + Mem.store chunk m2 b ofs v = Some m2' -> + Mem.inject (Mem.flat_inj thr) m1 m2'). + intros. eapply Mem.store_outside_inject; eauto. + intros b' ? INJ'. unfold Mem.flat_inj in INJ'. + destruct (zlt b' thr); inversion INJ'; subst. omega. + destruct id; simpl in ST; try (eapply P; eauto; fail). + inv ST; auto. + revert ST. caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. +Qed. + +Lemma store_init_data_list_augment: + forall b idl m1 m2 p m2', + Mem.inject (Mem.flat_inj thr) m1 m2 -> + b >= thr -> + store_init_data_list ge m2 b p idl = Some m2' -> + Mem.inject (Mem.flat_inj thr) m1 m2'. +Proof. + induction idl; simpl. + intros; congruence. + intros until m2'; intros INJ FB. + caseEq (store_init_data ge m2 b p a); try congruence. intros. + 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' -> + 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. + subst; exfalso; omega. +Qed. + +Lemma alloc_variables_augment: + forall idl m1 m2 m2', + alloc_variables ge m2 idl = 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. + 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). + unfold block in *; omega. +Qed. + +End INITMEM_AUGMENT_INJ. + End GENV. (** * Commutation with program transformations *) @@ -1045,48 +1237,65 @@ 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 (ge1: t A V) (ge2: t B W): Prop := { - mge_nextfun: genv_nextfun ge1 = genv_nextfun ge2; - mge_nextvar: genv_nextvar ge1 = genv_nextvar ge2; - mge_symb: genv_symb ge1 = genv_symb ge2; +Record match_genvs (new_functs : list (ident * B)) (new_vars : list (ident * globvar 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)) -> + 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 -> - exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf; + if zlt (genv_nextfun ge1) b then + exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf + else + In tf (map (@snd ident B) new_functs); 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 -> - exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv + if zlt b (genv_nextvar 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) }. Lemma add_function_match: forall ge1 ge2 id f1 f2, - match_genvs ge1 ge2 -> + match_genvs nil nil ge1 ge2 -> match_fun f1 f2 -> - match_genvs (add_function ge1 (id, f1)) (add_function ge2 (id, f2)). -Proof. - intros. destruct H. constructor; simpl. - congruence. congruence. congruence. - rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_nextfun ge2)). - exists f2; split; congruence. - eauto. + match_genvs nil nil (add_function ge1 (id, f1)) (add_function ge2 (id, f2)). +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. + 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)). + exists f2; split; congruence. + eauto. rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_nextfun ge2)). - exists f1; split; congruence. - eauto. + 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 ge1 ge2 -> - match_genvs (add_functions ge1 fl1) (add_functions ge2 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. @@ -1094,46 +1303,151 @@ Proof. destruct H. subst. apply IHlist_forall2. apply add_function_match; auto. Qed. -Lemma add_variable_match: - forall ge1 ge2 id v1 v2, - match_genvs ge1 ge2 -> - match_globvar v1 v2 -> - match_genvs (add_variable ge1 (id, v1)) (add_variable ge2 (id, v2)). +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. - congruence. congruence. congruence. + 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 ge2)). - exists v2; split; congruence. - eauto. + 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 ge2)). - exists v1; split; congruence. - eauto. + 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. Qed. Lemma add_variables_match: forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 -> - forall ge1 ge2, match_genvs ge1 ge2 -> - match_genvs (add_variables ge1 vl1) (add_variables ge2 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). Proof. induction 1; intros; simpl. auto. inv H. apply IHlist_forall2. apply add_variable_match; auto. constructor; 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)). +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. + 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. +Qed. + +Variable new_functs : list (ident * B). +Variable new_vars : list (ident * globvar W). +Variable new_main : ident. + Variable p: program A V. Variable p': program B W. -Hypothesis progmatch: match_program match_fun match_varinfo p p'. +Hypothesis progmatch: + match_program match_fun match_varinfo new_functs new_vars new_main p p'. Lemma globalenvs_match: - match_genvs (globalenv p) (globalenv p'). -Proof. - unfold globalenv. destruct progmatch. destruct H0. - apply add_variables_match; auto. apply add_functions_match; auto. - constructor; simpl; auto; intros; rewrite ZMap.gi in H2; congruence. + 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. + constructor; simpl; auto; intros; rewrite ZMap.gi in H; congruence. Qed. Theorem find_funct_ptr_match: @@ -1146,8 +1460,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 -> - exists f : A, - find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf. + if zlt (genv_nextfun (globalenv p)) b then + exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf + else + In tf (map (@snd ident B) new_functs). Proof (mge_rev_funs globalenvs_match). Theorem find_funct_match: @@ -1161,15 +1477,17 @@ Proof. apply find_funct_ptr_match. auto. Qed. -Theorem find_funct_rev_match: +Theorem find_funct_rev_match: (* a little weak *) forall (v : val) (tf : B), find_funct (globalenv p') v = Some tf -> - exists f : A, find_funct (globalenv p) v = Some f /\ match_fun f tf. + (exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf) + \/ (In tf (map (@snd ident B) new_functs)). 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. auto. + apply find_funct_ptr_rev_match in H. + destruct (zlt (genv_nextfun (globalenv p)) b); intuition. Qed. Theorem find_var_info_match: @@ -1182,78 +1500,104 @@ 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 -> - exists v, - find_var_info (globalenv p) b = Some v /\ match_globvar v tv. + if zlt b (genv_nextvar (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). Proof (mge_rev_vars globalenvs_match). Theorem find_symbol_match: forall (s : ident), + ~In s (funct_names new_functs ++ var_names new_vars) -> find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. - intros. destruct globalenvs_match. unfold find_symbol. congruence. + 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)). + Lemma store_init_data_list_match: - forall idl m b ofs, - store_init_data_list (globalenv p') m b ofs idl = - store_init_data_list (globalenv p) m b ofs idl. + forall idl m b ofs m', + store_init_data_list (globalenv p) m b ofs idl = Some m' -> + store_init_data_list (globalenv p') m b ofs idl = Some m'. Proof. induction idl; simpl; intros. auto. - assert (store_init_data (globalenv p') m b ofs a = - store_init_data (globalenv p) m b ofs a). - destruct a; simpl; auto. rewrite find_symbol_match. auto. - rewrite H. destruct (store_init_data (globalenv p) m b ofs a); 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. + 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 -> - forall m, - alloc_variables (globalenv p') m vl2 = alloc_variables (globalenv p) m vl1. + forall m m', + alloc_variables (globalenv p) m vl1 = Some m' -> + alloc_variables (globalenv p') m vl2 = Some m'. Proof. - induction 1; intros; simpl. + induction 1; intros until m'; simpl. 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. - rewrite store_init_data_list_match. - destruct (store_init_data_list (globalenv p) m1 b 0 init); auto. + 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. + (perm_globvar (mkglobvar info1 init ro vo))); auto. + inversion P. Qed. Theorem init_mem_match: - forall m, init_mem p = Some m -> init_mem p' = Some m. + forall m, init_mem p = Some m -> + init_mem p' = alloc_variables (globalenv p') m new_vars. Proof. - intros. rewrite <- H. unfold init_mem. destruct progmatch. destruct H1. - apply alloc_variables_match; auto. + 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. Qed. End MATCH_PROGRAMS. -Section TRANSF_PROGRAM_PARTIAL2. +Section TRANSF_PROGRAM_AUGMENT. 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_main : ident. + Variable p: program A V. Variable p': program B W. + Hypothesis transf_OK: - transform_partial_program2 transf_fun transf_var p = OK p'. + transform_partial_augment_program transf_fun transf_var new_functs new_vars 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 p p'. Proof. - apply transform_partial_program2_match; auto. + apply transform_partial_augment_program_match; auto. Qed. -Theorem find_funct_ptr_transf_partial2: +Theorem find_funct_ptr_transf_augment: forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> exists f', @@ -1264,16 +1608,52 @@ Proof. intros [tf [X Y]]. exists tf; auto. Qed. -Theorem find_funct_ptr_rev_transf_partial2: + + +(* 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 -> + 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. +Qed. + +Theorem find_funct_ptr_rev_transf_augment: forall (b: block) (tf: B), find_funct_ptr (globalenv p') b = Some tf -> - exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf. + if (zlt (genv_nextfun (globalenv p)) b) 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). Proof. intros. - exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto. + exploit find_funct_ptr_rev_match;eauto. eexact prog_match; eauto. auto. Qed. -Theorem find_funct_transf_partial2: + +Theorem find_funct_transf_augment: forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> exists f', @@ -1284,16 +1664,17 @@ Proof. intros [tf [X Y]]. exists tf; auto. Qed. -Theorem find_funct_rev_transf_partial2: +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. + (exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf) \/ + In tf (map (@snd ident B) new_functs). Proof. intros. exploit find_funct_rev_match. eexact prog_match. eauto. auto. Qed. -Theorem find_var_info_transf_partial2: +Theorem find_var_info_transf_augment: forall (b: block) (v: globvar V), find_var_info (globalenv p) b = Some v -> exists v', @@ -1305,29 +1686,172 @@ Proof. rewrite H0; simpl. auto. Qed. + +(* This may not yet be in the ideal form for easy use .*) +Theorem find_new_var_exists: + list_norepet (prog_var_names p ++ var_names new_vars) -> + forall id gv m, In (id, gv) new_vars -> + init_mem p' = Some m -> + exists b, find_symbol (globalenv p') id = Some b + /\ find_var_info (globalenv p') b = Some gv + /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv) + /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p') m b 0 gv.(gvar_init)). +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 (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_var_exists. + unfold prog_var_names in *; simpl in *. + rewrite var_names_app. rewrite <- H2. auto. + simpl. intuition. + auto. +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 + (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)). +Proof. + intros. + exploit find_var_info_rev_match. eexact prog_match. eauto. + destruct (zlt b (genv_nextvar (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) -> + find_symbol (globalenv p') s = find_symbol (globalenv p) s. +Proof. + intros. eapply find_symbol_match. eexact prog_match. auto. +Qed. + +Theorem init_mem_transf_augment: + (forall s', find_symbol (globalenv p) s' <> None -> + ~ In s' (funct_names new_functs ++ var_names new_vars)) -> + forall m, init_mem p = Some m -> + init_mem p' = alloc_variables (globalenv p') m new_vars. +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)) -> + forall m, init_mem p = Some m -> + forall m', init_mem p' = Some m' -> + Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m'. +Proof. + intros. + pose proof (initmem_inject p H0). + erewrite init_mem_transf_augment in H1; eauto. + eapply alloc_variables_augment; eauto. omega. +Qed. + + +End TRANSF_PROGRAM_AUGMENT. + +Section TRANSF_PROGRAM_PARTIAL2. + +Variable A B V W: Type. +Variable transf_fun: A -> res B. +Variable transf_var: V -> res W. +Variable p: program A V. +Variable p': program B W. +Hypothesis transf_OK: + transform_partial_program2 transf_fun transf_var p = OK p'. + +Remark transf_augment_OK: + transform_partial_augment_program transf_fun transf_var nil 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. +Qed. + +Theorem find_funct_ptr_transf_partial2: + forall (b: block) (f: A), + find_funct_ptr (globalenv p) b = Some f -> + exists f', + find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'. +Proof. + exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). +Qed. + +Theorem find_funct_ptr_rev_transf_partial2: + forall (b: block) (tf: B), + find_funct_ptr (globalenv p') b = Some tf -> + exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf. +Proof. + 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. +Qed. + +Theorem find_funct_transf_partial2: + forall (v: val) (f: A), + find_funct (globalenv p) v = Some f -> + exists f', + find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. +Proof. + exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). +Qed. + +Theorem find_funct_rev_transf_partial2: + forall (v: val) (tf: B), + find_funct (globalenv p') v = Some tf -> + exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf. +Proof. + pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + intros. pose proof (H v tf H0). + destruct H1. auto. inversion H1. +Qed. + +Theorem find_var_info_transf_partial2: + forall (b: block) (v: globvar V), + find_var_info (globalenv p) b = Some v -> + 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). +Qed. + Theorem find_var_info_rev_transf_partial2: forall (b: block) (v': globvar W), find_var_info (globalenv p') b = Some v' -> exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v'. Proof. - intros. - exploit find_var_info_rev_match. eexact prog_match. eauto. - intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl. - rewrite H0; simpl. auto. + 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. Qed. Theorem find_symbol_transf_partial2: forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. - intros. eapply find_symbol_match. eexact prog_match. + 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. - intros. eapply init_mem_match. eexact prog_match. auto. + pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + intros. simpl in H. apply H; auto. Qed. End TRANSF_PROGRAM_PARTIAL2. diff --git a/common/Memory.v b/common/Memory.v index e1c68bd..059a27e 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -2817,6 +2817,41 @@ Proof. auto. Qed. +Lemma drop_outside_inj: forall f m1 m2 b lo hi p m2', + mem_inj f m1 m2 -> + drop_perm m2 b lo hi p = Some m2' -> + (forall b' delta, + f b' = Some(b, delta) -> + high_bound m1 b' + delta <= lo + \/ hi <= low_bound m1 b' + delta) -> + mem_inj f m1 m2'. +Proof. + intros. destruct H. constructor; intros. + + (* access *) + inversion H2. + destruct (range_perm_in_bounds _ _ _ _ _ H3). + pose proof (size_chunk_pos chunk). omega. + pose proof (mi_access0 b1 b2 delta chunk ofs p0 H H2). clear mi_access0 H2 H3. + unfold valid_access in *. intuition. clear H3. + unfold range_perm in *. intros. + eapply perm_drop_3; eauto. + destruct (eq_block b2 b); subst; try (intuition; fail). + destruct (H1 b1 delta H); intuition omega. + + (* memval *) + pose proof (mi_memval0 _ _ _ _ H H2). clear mi_memval0. + unfold Mem.drop_perm in H0. + destruct (Mem.range_perm_dec m2 b lo hi p); inversion H0; subst; clear H0. + simpl. unfold update. destruct (zeq b2 b); subst; auto. + pose proof (perm_in_bounds _ _ _ _ H2). + destruct (H1 b1 delta H). + destruct (zle lo (ofs + delta)); simpl; auto. exfalso; omega. + destruct (zle lo (ofs + delta)); destruct (zlt (ofs + delta) hi); simpl; auto. + exfalso; omega. +Qed. + + (** * Memory extensions *) (** A store [m2] extends a store [m1] if [m2] can be obtained from [m1] @@ -3868,6 +3903,23 @@ Proof. Qed. *) +Lemma drop_outside_inject: forall f m1 m2 b lo hi p m2', + inject f m1 m2 -> + drop_perm m2 b lo hi p = Some m2' -> + (forall b' delta, + f b' = Some(b, delta) -> + high_bound m1 b' + delta <= lo + \/ hi <= low_bound m1 b' + delta) -> + inject f m1 m2'. +Proof. + intros. destruct H. constructor; eauto. + eapply drop_outside_inj; eauto. + + intros. unfold valid_block in *. erewrite nextblock_drop; eauto. + + intros. erewrite bounds_drop; eauto. +Qed. + (** Injecting a memory into itself. *) Definition flat_inj (thr: block) : meminj := diff --git a/common/Memtype.v b/common/Memtype.v index f763581..2e44331 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -1159,6 +1159,16 @@ Axiom free_inject: exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) -> inject f m1' m2'. +Axiom drop_outside_inject: + forall f m1 m2 b lo hi p m2', + inject f m1 m2 -> + drop_perm m2 b lo hi p = Some m2' -> + (forall b' delta, + f b' = Some(b, delta) -> + high_bound m1 b' + delta <= lo + \/ hi <= low_bound m1 b' + delta) -> + inject f m1 m2'. + (** Memory states that inject into themselves. *) Definition flat_inj (thr: block) : meminj := diff --git a/driver/Driver.ml b/driver/Driver.ml index 1ca915c..0523feb 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -35,10 +35,19 @@ let safe_remove file = (* Printing of error messages *) +(* Locally named idents are encoded as in Cminorgen. + This function should live somewhere more central. *) +let ident_name id = + match id with + | BinPos.Coq_xO n -> Camlcoq.extern_atom n + | BinPos.Coq_xI n -> Printf.sprintf "$%ld" (Camlcoq.camlint_of_positive n) + | BinPos.Coq_xH -> "$0" + let print_error oc msg = let print_one_error = function | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s) | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i) + | Errors.CTXL i -> output_string oc (ident_name i) in List.iter print_one_error msg; output_char oc '\n' |