diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Bounds.v | 7 | ||||
| -rw-r--r-- | backend/Inliningproof.v | 30 | ||||
| -rw-r--r-- | backend/NeedDomain.v | 4 | ||||
| -rw-r--r-- | backend/PrintAnnot.ml | 182 | ||||
| -rw-r--r-- | backend/PrintAsm.ml | 8 | ||||
| -rw-r--r-- | backend/PrintAsmaux.ml | 160 | ||||
| -rw-r--r-- | backend/Regalloc.ml | 6 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 50 | ||||
| -rw-r--r-- | backend/Unusedglobproof.v | 34 | ||||
| -rw-r--r-- | backend/ValueAnalysis.v | 2 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 6 |
11 files changed, 230 insertions, 259 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v index 7528b66e..04c1328d 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -87,8 +87,6 @@ Section BOUNDS. Variable f: function. -Parameter mregs_of_clobber: list ident -> list mreg. - (** In the proof of the [Stacking] pass, we only need to bound the registers written by an instruction. Therefore, this function returns these registers, ignoring registers used only as @@ -103,7 +101,6 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil - | Lbuiltin (EF_inline_asm txt typs clob) args res => res ++ mregs_of_clobber clob | Lbuiltin ef args res => res ++ destroyed_by_builtin ef | Lannot ef args => nil | Llabel lbl => nil @@ -354,9 +351,7 @@ Proof. (* call *) eapply size_arguments_bound; eauto. (* builtin *) - apply H1. destruct e; apply in_or_app; auto. - change (destroyed_by_builtin (EF_inline_asm text sg clobbers)) with (@nil mreg) in H2. - simpl in H2; tauto. + apply H1. apply in_or_app; auto. (* annot *) apply H0. rewrite slots_of_locs_charact; auto. Qed. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index e3c5bf2a..993e0b34 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -109,11 +109,11 @@ Qed. (** ** Agreement between register sets before and after inlining. *) Definition agree_regs (F: meminj) (ctx: context) (rs rs': regset) := - (forall r, Ple r ctx.(mreg) -> val_inject F rs#r rs'#(sreg ctx r)) + (forall r, Ple r ctx.(mreg) -> Val.inject F rs#r rs'#(sreg ctx r)) /\(forall r, Plt ctx.(mreg) r -> rs#r = Vundef). Definition val_reg_charact (F: meminj) (ctx: context) (rs': regset) (v: val) (r: reg) := - (Plt ctx.(mreg) r /\ v = Vundef) \/ (Ple r ctx.(mreg) /\ val_inject F v rs'#(sreg ctx r)). + (Plt ctx.(mreg) r /\ v = Vundef) \/ (Ple r ctx.(mreg) /\ Val.inject F v rs'#(sreg ctx r)). Remark Plt_Ple_dec: forall p q, {Plt p q} + {Ple q p}. @@ -138,7 +138,7 @@ Proof. Qed. Lemma agree_val_reg: - forall F ctx rs rs' r, agree_regs F ctx rs rs' -> val_inject F rs#r rs'#(sreg ctx r). + forall F ctx rs rs' r, agree_regs F ctx rs rs' -> Val.inject F rs#r rs'#(sreg ctx r). Proof. intros. exploit agree_val_reg_gen; eauto. instantiate (1 := r). intros [[A B] | [A B]]. rewrite B; auto. @@ -146,7 +146,7 @@ Proof. Qed. Lemma agree_val_regs: - forall F ctx rs rs' rl, agree_regs F ctx rs rs' -> val_list_inject F rs##rl rs'##(sregs ctx rl). + forall F ctx rs rs' rl, agree_regs F ctx rs rs' -> Val.inject_list F rs##rl rs'##(sregs ctx rl). Proof. induction rl; intros; simpl. constructor. constructor; auto. apply agree_val_reg; auto. Qed. @@ -154,7 +154,7 @@ Qed. Lemma agree_set_reg: forall F ctx rs rs' r v v', agree_regs F ctx rs rs' -> - val_inject F v v' -> + Val.inject F v v' -> Ple r ctx.(mreg) -> agree_regs F ctx (rs#r <- v) (rs'#(sreg ctx r) <- v'). Proof. @@ -218,7 +218,7 @@ Qed. Lemma agree_regs_init_regs: forall F ctx rl vl vl', - val_list_inject F vl vl' -> + Val.inject_list F vl vl' -> (forall r, In r rl -> Ple r ctx.(mreg)) -> agree_regs F ctx (init_regs vl rl) (init_regs vl' (sregs ctx rl)). Proof. @@ -389,7 +389,7 @@ Proof. (* register *) assert (rs'#(sreg ctx r) = rs#r). 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. + 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. apply FUNCTIONS with fd. @@ -411,7 +411,7 @@ Lemma tr_annot_arg: forall a v, eval_annot_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v -> exists v', eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (sannotarg ctx a) v' - /\ val_inject F v v'. + /\ Val.inject F v v'. Proof. intros until m'; intros MG AG SP MI. induction 1; simpl. - exists rs'#(sreg ctx x); split. constructor. eapply agree_val_reg; eauto. @@ -424,7 +424,7 @@ Proof. simpl. econstructor; eauto. rewrite Int.add_zero_l; auto. intros (v' & A & B). exists v'; split; auto. constructor. simpl. rewrite Int.add_zero_l; auto. - econstructor; split. constructor. simpl. econstructor; eauto. rewrite ! Int.add_zero_l; auto. -- assert (val_inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). +- assert (Val.inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. inv MG. econstructor. eauto. rewrite Int.add_zero; auto. } @@ -436,7 +436,7 @@ Proof. inv MG. econstructor. eauto. rewrite Int.add_zero; auto. - destruct IHeval_annot_arg1 as (v1 & A1 & B1). destruct IHeval_annot_arg2 as (v2 & A2 & B2). - econstructor; split. eauto with aarg. apply val_longofwords_inject; auto. + econstructor; split. eauto with aarg. apply Val.longofwords_inject; auto. Qed. Lemma tr_annot_args: @@ -448,7 +448,7 @@ Lemma tr_annot_args: forall al vl, eval_annot_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl -> exists vl', eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (map (sannotarg ctx) al) vl' - /\ val_list_inject F vl vl'. + /\ Val.inject_list F vl vl'. Proof. induction 5; simpl. - exists (@nil val); split; constructor. @@ -856,7 +856,7 @@ Inductive match_states: state -> state -> Prop := | match_call_states: forall stk fd args m stk' fd' args' m' F (MS: match_stacks F m m' stk stk' (Mem.nextblock m')) (FD: transf_fundef fenv fd = OK fd') - (VINJ: val_list_inject F args args') + (VINJ: Val.inject_list F args args') (MINJ: Mem.inject F m m'), match_states (Callstate stk fd args m) (Callstate stk' fd' args' m') @@ -876,7 +876,7 @@ Inductive match_states: state -> state -> Prop := (State stk' f' (Vptr sp' Int.zero) pc' rs' m') | match_return_states: forall stk v m stk' v' m' F (MS: match_stacks F m m' stk stk' (Mem.nextblock m')) - (VINJ: val_inject F v v') + (VINJ: Val.inject F v v') (MINJ: Mem.inject F m m'), match_states (Returnstate stk v m) (Returnstate stk' v' m') @@ -884,7 +884,7 @@ Inductive match_states: state -> state -> Prop := (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs') (RET: ctx.(retinfo) = Some rinfo) (AT: f'.(fn_code)!pc' = Some(inline_return ctx or rinfo)) - (VINJ: match or with None => v = Vundef | Some r => val_inject F v rs'#(sreg ctx r) end) + (VINJ: match or with None => v = Vundef | Some r => Val.inject F v rs'#(sreg ctx r) end) (MINJ: Mem.inject F m m') (VB: Mem.valid_block m' sp') (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize)) @@ -1120,7 +1120,7 @@ Proof. (* jumptable *) exploit tr_funbody_inv; eauto. intros TR; inv TR. - assert (val_inject F rs#arg rs'#(sreg ctx arg)). eapply agree_val_reg; eauto. + assert (Val.inject F rs#arg rs'#(sreg ctx arg)). eapply agree_val_reg; eauto. rewrite H0 in H2; inv H2. left; econstructor; split. eapply plus_one. eapply exec_Ijumptable; eauto. diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 8beff265..770648b1 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -840,7 +840,7 @@ Lemma default_needs_of_condition_sound: eval_condition cond args2 m2 = Some b. Proof. intros. apply eval_condition_inj with (f := inject_id) (m1 := m1) (vl1 := args1); auto. - apply val_list_inject_lessdef. apply lessdef_vagree_list. auto. + apply val_inject_list_lessdef. apply lessdef_vagree_list. auto. Qed. Lemma default_needs_of_operation_sound: @@ -866,7 +866,7 @@ Proof. eassumption. auto. auto. auto. instantiate (1 := op). intros. apply val_inject_lessdef; auto. apply val_inject_lessdef. instantiate (1 := Vptr sp Int.zero). instantiate (1 := Vptr sp Int.zero). auto. - apply val_list_inject_lessdef; eauto. + apply val_inject_list_lessdef; eauto. eauto. intros (v2 & A & B). exists v2; split; auto. apply vagree_lessdef. apply val_inject_lessdef. auto. diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml deleted file mode 100644 index 88f5d8d6..00000000 --- a/backend/PrintAnnot.ml +++ /dev/null @@ -1,182 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Printing annotations in asm syntax *) - -open Printf -open Datatypes -open Integers -open Floats -open Camlcoq -open AST -open Memdata -open Asm - -(** All files used in the debug entries *) -module StringSet = Set.Make(String) -let all_files : StringSet.t ref = ref StringSet.empty -let add_file file = - all_files := StringSet.add file !all_files - - -(** Line number annotations *) - -let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t - = Hashtbl.create 7 - -let last_file = ref "" - -let reset_filenames () = - Hashtbl.clear filename_info; last_file := "" - -let close_filenames () = - Hashtbl.iter - (fun file (num, fb) -> - match fb with Some b -> Printlines.close b | None -> ()) - filename_info; - reset_filenames() - -let enter_filename f = - let num = Hashtbl.length filename_info + 1 in - let filebuf = - if !Clflags.option_S || !Clflags.option_dasm then begin - try Some (Printlines.openfile f) - with Sys_error _ -> None - end else None in - Hashtbl.add filename_info f (num, filebuf); - (num, filebuf) - -(* Add file and line debug location, using GNU assembler-style DWARF2 - directives *) - -let print_file_line oc pref file line = - if !Clflags.option_g && file <> "" then begin - let (filenum, filebuf) = - try - Hashtbl.find filename_info file - with Not_found -> - let (filenum, filebuf as res) = enter_filename file in - fprintf oc " .file %d %S\n" filenum file; - res in - fprintf oc " .loc %d %d\n" filenum line; - match filebuf with - | None -> () - | Some fb -> Printlines.copy oc pref fb line line - end - -(* Add file and line debug location, using DWARF2 directives in the style - of Diab C 5 *) - -let print_file_line_d2 oc pref file line = - if !Clflags.option_g && file <> "" then begin - let (_, filebuf) = - try - Hashtbl.find filename_info file - with Not_found -> - enter_filename file in - if file <> !last_file then begin - fprintf oc " .d2file %S\n" file; - last_file := file - end; - fprintf oc " .d2line %d\n" line; - match filebuf with - | None -> () - | Some fb -> Printlines.copy oc pref fb line line - end - -(** "True" annotations *) - -let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" - -let rec print_annot print_preg sp_reg_name oc = function - | AA_base x -> print_preg oc x - | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n) - | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) - | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) - | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) - | AA_loadstack(chunk, ofs) -> - fprintf oc "mem(%s + %ld, %ld)" - sp_reg_name - (camlint_of_coqint ofs) - (camlint_of_coqint (size_chunk chunk)) - | AA_addrstack ofs -> - fprintf oc "(%s + %ld)" - sp_reg_name - (camlint_of_coqint ofs) - | AA_loadglobal(chunk, id, ofs) -> - fprintf oc "mem(\"%s\" + %ld, %ld)" - (extern_atom id) - (camlint_of_coqint ofs) - (camlint_of_coqint (size_chunk chunk)) - | AA_addrglobal(id, ofs) -> - fprintf oc "(\"%s\" + %ld)" - (extern_atom id) - (camlint_of_coqint ofs) - | AA_longofwords(hi, lo) -> - fprintf oc "(%a * 0x100000000 + %a)" - (print_annot print_preg sp_reg_name) hi - (print_annot print_preg sp_reg_name) lo - -let print_annot_text print_preg sp_reg_name oc txt args = - let print_fragment = function - | Str.Text s -> - output_string oc s - | Str.Delim "%%" -> - output_char oc '%' - | Str.Delim s -> - let n = int_of_string (String.sub s 1 (String.length s - 1)) in - try - print_annot print_preg sp_reg_name oc (List.nth args (n-1)) - with Failure _ -> - fprintf oc "<bad parameter %s>" s in - List.iter print_fragment (Str.full_split re_annot_param txt); - fprintf oc "\n" - -let print_annot_stmt print_preg sp_reg_name oc txt tys args = - print_annot_text print_preg sp_reg_name oc txt args - -let print_annot_val print_preg oc txt args = - print_annot_text print_preg "<internal error>" oc txt - (List.map (fun r -> AA_base r) args) - -(** Inline assembly *) - -let re_asm_param = Str.regexp "%%\\|%[0-9]+" - -let print_inline_asm print_preg oc txt sg args res = - let operands = - if sg.sig_res = None then args else res @ args in - let print_fragment = function - | Str.Text s -> - output_string oc s - | Str.Delim "%%" -> - output_char oc '%' - | Str.Delim s -> - let n = int_of_string (String.sub s 1 (String.length s - 1)) in - try - print_preg oc (List.nth operands n) - with Failure _ -> - fprintf oc "<bad parameter %s>" s in - List.iter print_fragment (Str.full_split re_asm_param txt); - fprintf oc "\n" - - -(** Print CompCert version and command-line as asm comment *) - -let print_version_and_options oc comment = - fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version; - fprintf oc "%s Command line:" comment; - for i = 1 to Array.length Sys.argv - 1 do - fprintf oc " %s" Sys.argv.(i) - done; - fprintf oc "\n" - diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 11854ace..e91b4e03 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -94,7 +94,7 @@ module Printer(Target:TARGET) = fprintf oc " %s\n" name_sec; Target.print_align oc align; if not (C2C.atom_is_static name) then - fprintf oc " .global %a\n" Target.symbol name; + fprintf oc " .globl %a\n" Target.symbol name; fprintf oc "%a:\n" Target.symbol name; print_init_data oc name v.gvar_init; Target.print_var_info oc name; @@ -130,12 +130,12 @@ module Printer(Target:TARGET) = let print_program oc p db = let module Target = (val (sel_target ()):TARGET) in let module Printer = Printer(Target) in - PrintAnnot.reset_filenames (); - PrintAnnot.print_version_and_options oc Target.comment; + reset_filenames (); + print_version_and_options oc Target.comment; Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; Target.print_epilogue oc; - PrintAnnot.close_filenames (); + close_filenames (); if !Clflags.option_g && Configuration.advanced_debug then begin match db with diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 8bc961ef..497760c1 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -16,6 +16,7 @@ open Asm open Camlcoq open DwarfTypes open Datatypes +open Memdata open Printf open Sections @@ -140,3 +141,162 @@ let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" (* Basic printing functions *) let coqint oc n = fprintf oc "%ld" (camlint_of_coqint n) + +(* Printing annotations in asm syntax *) +(** All files used in the debug entries *) +module StringSet = Set.Make(String) +let all_files : StringSet.t ref = ref StringSet.empty +let add_file file = + all_files := StringSet.add file !all_files + + +let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t + = Hashtbl.create 7 + +let last_file = ref "" + +let reset_filenames () = + Hashtbl.clear filename_info; last_file := "" + +let close_filenames () = + Hashtbl.iter + (fun file (num, fb) -> + match fb with Some b -> Printlines.close b | None -> ()) + filename_info; + reset_filenames() + +let enter_filename f = + let num = Hashtbl.length filename_info + 1 in + let filebuf = + if !Clflags.option_S || !Clflags.option_dasm then begin + try Some (Printlines.openfile f) + with Sys_error _ -> None + end else None in + Hashtbl.add filename_info f (num, filebuf); + (num, filebuf) + +(* Add file and line debug location, using GNU assembler-style DWARF2 + directives *) + +let print_file_line oc pref file line = + if !Clflags.option_g && file <> "" then begin + let (filenum, filebuf) = + try + Hashtbl.find filename_info file + with Not_found -> + let (filenum, filebuf as res) = enter_filename file in + fprintf oc " .file %d %S\n" filenum file; + res in + fprintf oc " .loc %d %d\n" filenum line; + match filebuf with + | None -> () + | Some fb -> Printlines.copy oc pref fb line line + end + +(* Add file and line debug location, using DWARF2 directives in the style + of Diab C 5 *) + +let print_file_line_d2 oc pref file line = + if !Clflags.option_g && file <> "" then begin + let (_, filebuf) = + try + Hashtbl.find filename_info file + with Not_found -> + enter_filename file in + if file <> !last_file then begin + fprintf oc " .d2file %S\n" file; + last_file := file + end; + fprintf oc " .d2line %d\n" line; + match filebuf with + | None -> () + | Some fb -> Printlines.copy oc pref fb line line + end + + +(** "True" annotations *) + +let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" + +let rec print_annot print_preg sp_reg_name oc = function + | AA_base x -> print_preg oc x + | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n) + | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) + | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) + | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) + | AA_loadstack(chunk, ofs) -> + fprintf oc "mem(%s + %ld, %ld)" + sp_reg_name + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | AA_addrstack ofs -> + fprintf oc "(%s + %ld)" + sp_reg_name + (camlint_of_coqint ofs) + | AA_loadglobal(chunk, id, ofs) -> + fprintf oc "mem(\"%s\" + %ld, %ld)" + (extern_atom id) + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | AA_addrglobal(id, ofs) -> + fprintf oc "(\"%s\" + %ld)" + (extern_atom id) + (camlint_of_coqint ofs) + | AA_longofwords(hi, lo) -> + fprintf oc "(%a * 0x100000000 + %a)" + (print_annot print_preg sp_reg_name) hi + (print_annot print_preg sp_reg_name) lo + +let print_annot_text print_preg sp_reg_name oc txt args = + let print_fragment = function + | Str.Text s -> + output_string oc s + | Str.Delim "%%" -> + output_char oc '%' + | Str.Delim s -> + let n = int_of_string (String.sub s 1 (String.length s - 1)) in + try + print_annot print_preg sp_reg_name oc (List.nth args (n-1)) + with Failure _ -> + fprintf oc "<bad parameter %s>" s in + List.iter print_fragment (Str.full_split re_annot_param txt); + fprintf oc "\n" + +let print_annot_stmt print_preg sp_reg_name oc txt tys args = + print_annot_text print_preg sp_reg_name oc txt args + +let print_annot_val print_preg oc txt args = + print_annot_text print_preg "<internal error>" oc txt + (List.map (fun r -> AA_base r) args) + +(** Inline assembly *) + +let re_asm_param = Str.regexp "%%\\|%[0-9]+" + +let print_inline_asm print_preg oc txt sg args res = + let operands = + if sg.sig_res = None then args else res @ args in + let print_fragment = function + | Str.Text s -> + output_string oc s + | Str.Delim "%%" -> + output_char oc '%' + | Str.Delim s -> + let n = int_of_string (String.sub s 1 (String.length s - 1)) in + try + print_preg oc (List.nth operands n) + with Failure _ -> + fprintf oc "<bad parameter %s>" s in + List.iter print_fragment (Str.full_split re_asm_param txt); + fprintf oc "\n" + + +(** Print CompCert version and command-line as asm comment *) + +let print_version_and_options oc comment = + fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version; + fprintf oc "%s Command line:" comment; + for i = 1 to Array.length Sys.argv - 1 do + fprintf oc " %s" Sys.argv.(i) + done; + fprintf oc "\n" diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index c286e946..aa4efc53 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -585,13 +585,11 @@ let add_interfs_instr g instr live = (* like a move *) IRC.add_pref g arg res | EF_inline_asm(txt, sg, clob), _, _ -> - (* clobbered regs interfere with live set - and also with res and args for GCC compatibility *) + (* clobbered regs interfere with res and args for GCC compatibility *) List.iter (fun c -> - match Machregsaux.register_by_name (extern_atom c) with + match Machregs.register_by_name c with | None -> () | Some mr -> - add_interfs_destroyed g across [mr]; add_interfs_list_mreg g args mr; if sg.sig_res <> None then add_interfs_list_mreg g res mr) clob diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index f4a1935f..7f41512e 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -508,14 +508,14 @@ Qed. (** A variant of [index_contains], up to a memory injection. *) Definition index_contains_inj (j: meminj) (m: mem) (sp: block) (idx: frame_index) (v: val) : Prop := - exists v', index_contains m sp idx v' /\ val_inject j v v'. + exists v', index_contains m sp idx v' /\ Val.inject j v v'. Lemma gss_index_contains_inj: forall j idx m m' sp v v', Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v' = Some m' -> index_valid idx -> Val.has_type v (type_of_index idx) -> - val_inject j v v' -> + Val.inject j v v' -> index_contains_inj j m' sp idx v. Proof. intros. exploit gss_index_contains_base; eauto. intros [v'' [A B]]. @@ -530,7 +530,7 @@ Lemma gss_index_contains_inj': forall j idx m m' sp v v', Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v' = Some m' -> index_valid idx -> - val_inject j v v' -> + Val.inject j v v' -> index_contains_inj j m' sp idx (Val.load_result (chunk_of_type (type_of_index idx)) v). Proof. intros. exploit gss_index_contains_base; eauto. intros [v'' [A B]]. @@ -598,7 +598,7 @@ Hint Resolve store_other_index_contains_inj index_contains_inj_incr: stacking. (** Agreement with Mach register states *) Definition agree_regs (j: meminj) (ls: locset) (rs: regset) : Prop := - forall r, val_inject j (ls (R r)) (rs r). + forall r, Val.inject j (ls (R r)) (rs r). (** Agreement over data stored in memory *) @@ -693,14 +693,14 @@ Definition agree_callee_save (ls ls0: locset) : Prop := Lemma agree_reg: forall j ls rs r, - agree_regs j ls rs -> val_inject j (ls (R r)) (rs r). + agree_regs j ls rs -> Val.inject j (ls (R r)) (rs r). Proof. intros. auto. Qed. Lemma agree_reglist: forall j ls rs rl, - agree_regs j ls rs -> val_list_inject j (reglist ls rl) (rs##rl). + agree_regs j ls rs -> Val.inject_list j (reglist ls rl) (rs##rl). Proof. induction rl; simpl; intros. auto. constructor. eauto with stacking. auto. @@ -713,7 +713,7 @@ Hint Resolve agree_reg agree_reglist: stacking. Lemma agree_regs_set_reg: forall j ls rs r v v', agree_regs j ls rs -> - val_inject j v v' -> + Val.inject j v v' -> agree_regs j (Locmap.set (R r) v ls) (Regmap.set r v' rs). Proof. intros; red; intros. @@ -725,7 +725,7 @@ Qed. Lemma agree_regs_set_regs: forall j rl vl vl' ls rs, agree_regs j ls rs -> - val_list_inject j vl vl' -> + Val.inject_list j vl vl' -> agree_regs j (Locmap.setlist (map R rl) vl ls) (set_regs rl vl' rs). Proof. induction rl; simpl; intros. @@ -850,7 +850,7 @@ Lemma agree_frame_set_local: forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'', agree_frame j ls ls0 m sp m' sp' parent retaddr -> slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true -> - val_inject j v v' -> + Val.inject j v v' -> Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_local ofs ty)) v' = Some m'' -> agree_frame j (Locmap.set (S Local ofs ty) v ls) ls0 m sp m'' sp' parent retaddr. Proof. @@ -889,7 +889,7 @@ Lemma agree_frame_set_outgoing: forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'', agree_frame j ls ls0 m sp m' sp' parent retaddr -> slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true -> - val_inject j v v' -> + Val.inject j v v' -> Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_arg ofs ty)) v' = Some m'' -> agree_frame j (Locmap.set (S Outgoing ofs ty) v ls) ls0 m sp m'' sp' parent retaddr. Proof. @@ -981,7 +981,7 @@ Lemma agree_frame_parallel_stores: forall j ls ls0 m sp m' sp' parent retaddr chunk addr addr' v v' m1 m1', agree_frame j ls ls0 m sp m' sp' parent retaddr -> Mem.inject j m m' -> - val_inject j addr addr' -> + Val.inject j addr addr' -> Mem.storev chunk m addr v = Some m1 -> Mem.storev chunk m' addr' v' = Some m1' -> agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. @@ -1669,7 +1669,7 @@ Hypothesis mkindex_val: index_contains_inj j m sp (mkindex (number r)) (ls0 (R r)). Definition agree_unused (ls0: locset) (rs: regset) : Prop := - forall r, ~(mreg_within_bounds b r) -> val_inject j (ls0 (R r)) (rs r). + forall r, ~(mreg_within_bounds b r) -> Val.inject j (ls0 (R r)) (rs r). Lemma restore_callee_save_regs_correct: forall l rs k, @@ -1681,7 +1681,7 @@ Lemma restore_callee_save_regs_correct: (State cs fb (Vptr sp Int.zero) (restore_callee_save_regs bound number mkindex ty fe l k) rs m) E0 (State cs fb (Vptr sp Int.zero) k rs' m) - /\ (forall r, In r l -> val_inject j (ls0 (R r)) (rs' r)) + /\ (forall r, In r l -> Val.inject j (ls0 (R r)) (rs' r)) /\ (forall r, ~(In r l) -> rs' r = rs r) /\ agree_unused ls0 rs'. Proof. @@ -1734,7 +1734,7 @@ Lemma restore_callee_save_correct: E0 (State cs fb (Vptr sp' Int.zero) k rs' m') /\ (forall r, In r int_callee_save_regs \/ In r float_callee_save_regs -> - val_inject j (ls0 (R r)) (rs' r)) + Val.inject j (ls0 (R r)) (rs' r)) /\ (forall r, ~(In r int_callee_save_regs) -> ~(In r float_callee_save_regs) -> @@ -1986,7 +1986,7 @@ Qed. Lemma match_stacks_parallel_stores: forall j m m' chunk addr addr' v v' m1 m1', Mem.inject j m m' -> - val_inject j addr addr' -> + Val.inject j addr addr' -> Mem.storev chunk m addr v = Some m1 -> Mem.storev chunk m' addr' v' = Some m1' -> forall cs cs' sg bound bound', @@ -2327,7 +2327,7 @@ Hypothesis AGCS: agree_callee_save ls (parent_locset cs). Lemma transl_external_argument: forall l, In l (loc_arguments sg) -> - exists v, extcall_arg rs m' (parent_sp cs') l v /\ val_inject j (ls l) v. + exists v, extcall_arg rs m' (parent_sp cs') l v /\ Val.inject j (ls l) v. Proof. intros. assert (loc_argument_acceptable l). apply loc_arguments_acceptable with sg; auto. @@ -2354,7 +2354,7 @@ Lemma transl_external_arguments_rec: forall locs, incl locs (loc_arguments sg) -> exists vl, - list_forall2 (extcall_arg rs m' (parent_sp cs')) locs vl /\ val_list_inject j ls##locs vl. + list_forall2 (extcall_arg rs m' (parent_sp cs')) locs vl /\ Val.inject_list j ls##locs vl. Proof. induction locs; simpl; intros. exists (@nil val); split. constructor. constructor. @@ -2366,7 +2366,7 @@ Qed. Lemma transl_external_arguments: exists vl, extcall_arguments rs m' (parent_sp cs') sg vl /\ - val_list_inject j (ls ## (loc_arguments sg)) vl. + Val.inject_list j (ls ## (loc_arguments sg)) vl. Proof. unfold extcall_arguments. apply transl_external_arguments_rec. @@ -2402,7 +2402,7 @@ Lemma transl_annot_arg_correct: (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_arg a) -> slot_within_bounds b sl ofs ty) -> exists v', eval_annot_arg ge rs (Vptr sp' Int.zero) m' (transl_annot_arg fe a) v' - /\ val_inject j v v'. + /\ Val.inject j v v'. Proof. Local Opaque fe offset_of_index. induction 1; simpl; intros VALID BOUNDS. @@ -2424,7 +2424,7 @@ Local Transparent fe. eapply agree_bounds; eauto. eapply Mem.valid_access_perm. eapply Mem.load_valid_access; eauto. - econstructor; split; eauto with aarg. unfold Val.add. rewrite ! Int.add_zero_l. econstructor. eapply agree_inj; eauto. auto. -- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)). +- assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)). { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) eqn:FS; auto. econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto. } @@ -2436,7 +2436,7 @@ Local Transparent fe. - destruct IHeval_annot_arg1 as (v1 & A1 & B1); auto using in_or_app. destruct IHeval_annot_arg2 as (v2 & A2 & B2); auto using in_or_app. exists (Val.longofwords v1 v2); split; auto with aarg. - apply val_longofwords_inject; auto. + apply Val.longofwords_inject; auto. Qed. Lemma transl_annot_args_correct: @@ -2446,7 +2446,7 @@ Lemma transl_annot_args_correct: (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args al) -> slot_within_bounds b sl ofs ty) -> exists vl', eval_annot_args ge rs (Vptr sp' Int.zero) m' (List.map (transl_annot_arg fe) al) vl' - /\ val_list_inject j vl vl'. + /\ Val.inject_list j vl vl'. Proof. induction 1; simpl; intros VALID BOUNDS. - exists (@nil val); split; constructor. @@ -2618,7 +2618,7 @@ Proof. - (* Lop *) assert (exists v', eval_operation ge (Vptr sp' Int.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v' - /\ val_inject j v v'). + /\ Val.inject j v v'). eapply eval_operation_inject; eauto. eapply match_stacks_preserves_globals; eauto. eapply agree_inj; eauto. eapply agree_reglist; eauto. @@ -2636,7 +2636,7 @@ Proof. - (* Lload *) assert (exists a', eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' - /\ val_inject j a a'). + /\ Val.inject j a a'). eapply eval_addressing_inject; eauto. eapply match_stacks_preserves_globals; eauto. eapply agree_inj; eauto. eapply agree_reglist; eauto. @@ -2654,7 +2654,7 @@ Proof. - (* Lstore *) assert (exists a', eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' - /\ val_inject j a a'). + /\ Val.inject j a a'). eapply eval_addressing_inject; eauto. eapply match_stacks_preserves_globals; eauto. eapply agree_inj; eauto. eapply agree_reglist; eauto. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 90d7f270..85e7a360 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -554,7 +554,7 @@ Qed. Lemma symbol_address_inject: forall j id ofs, meminj_preserves_globals j -> kept id -> - val_inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs). + Val.inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs). Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. exploit symbols_inject_2; eauto. intros (b' & TFS & INJ). rewrite TFS. @@ -564,17 +564,17 @@ Qed. (** Semantic preservation *) Definition regset_inject (f: meminj) (rs rs': regset): Prop := - forall r, val_inject f rs#r rs'#r. + forall r, Val.inject f rs#r rs'#r. Lemma regs_inject: - forall f rs rs', regset_inject f rs rs' -> forall l, val_list_inject f rs##l rs'##l. + forall f rs rs', regset_inject f rs rs' -> forall l, Val.inject_list f rs##l rs'##l. Proof. induction l; simpl. constructor. constructor; auto. Qed. Lemma set_reg_inject: forall f rs rs' r v v', - regset_inject f rs rs' -> val_inject f v v' -> + regset_inject f rs rs' -> Val.inject f v v' -> regset_inject f (rs#r <- v) (rs'#r <- v'). Proof. intros; red; intros. rewrite ! Regmap.gsspec. destruct (peq r0 r); auto. @@ -593,7 +593,7 @@ Proof. Qed. Lemma init_regs_inject: - forall f args args', val_list_inject f args args' -> + forall f args args', Val.inject_list f args args' -> forall params, regset_inject f (init_regs args params) (init_regs args' params). Proof. @@ -689,13 +689,13 @@ Inductive match_states: state -> state -> Prop := | match_states_call: forall s fd args m ts targs tm j (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm)) (KEPT: forall id, ref_fundef fd id -> kept id) - (ARGINJ: val_list_inject j args targs) + (ARGINJ: Val.inject_list j args targs) (MEMINJ: Mem.inject j m tm), match_states (Callstate s fd args m) (Callstate ts fd targs tm) | match_states_return: forall s res m ts tres tm j (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm)) - (RESINJ: val_inject j res tres) + (RESINJ: Val.inject j res tres) (MEMINJ: Mem.inject j m tm), match_states (Returnstate s res m) (Returnstate ts tres tm). @@ -706,10 +706,10 @@ Lemma external_call_inject: external_call ef ge vargs m1 t vres m2 -> (forall id, In id (globals_external ef) -> kept id) -> Mem.inject f m1 m1' -> - val_list_inject f vargs vargs' -> + Val.inject_list f vargs vargs' -> exists f', exists vres', exists m2', external_call ef tge vargs' m1' t vres' m2' - /\ val_inject f' vres vres' + /\ Val.inject f' vres vres' /\ Mem.inject f' m2 m2' /\ Mem.unchanged_on (loc_unmapped f) m1 m2 /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' @@ -751,7 +751,7 @@ Lemma eval_annot_arg_inject: (forall id, In id (globals_of_annot_arg a) -> kept id) -> exists v', eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' a v' - /\ val_inject j v v'. + /\ Val.inject j v v'. Proof. induction 1; intros SP GL RS MI K; simpl in K. - exists rs'#x; split; auto. constructor. @@ -762,7 +762,7 @@ Proof. - simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r. intros (v' & A & B). exists v'; auto with aarg. - econstructor; split; eauto with aarg. simpl. econstructor; eauto. rewrite Int.add_zero; auto. -- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). +- assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. @@ -776,7 +776,7 @@ Proof. - destruct IHeval_annot_arg1 as (v1' & A1 & B1); eauto using in_or_app. destruct IHeval_annot_arg2 as (v2' & A2 & B2); eauto using in_or_app. exists (Val.longofwords v1' v2'); split; auto with aarg. - apply val_longofwords_inject; auto. + apply Val.longofwords_inject; auto. Qed. Lemma eval_annot_args_inject: @@ -789,7 +789,7 @@ Lemma eval_annot_args_inject: (forall id, In id (globals_of_annot_args al) -> kept id) -> exists vl', eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' al vl' - /\ val_list_inject j vl vl'. + /\ Val.inject_list j vl vl'. Proof. induction 1; intros. - exists (@nil val); split; constructor. @@ -814,7 +814,7 @@ Proof. - (* op *) assert (A: exists tv, eval_operation tge (Vptr tsp Int.zero) op trs##args tm = Some tv - /\ val_inject j v tv). + /\ Val.inject j v tv). { apply eval_operation_inj with (ge1 := ge) (m1 := m) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. @@ -832,7 +832,7 @@ Proof. - (* load *) assert (A: exists ta, eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta - /\ val_inject j a ta). + /\ Val.inject j a ta). { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. apply KEPT. red. exists pc, (Iload chunk addr args dst pc'); auto. @@ -847,7 +847,7 @@ Proof. - (* store *) assert (A: exists ta, eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta - /\ val_inject j a ta). + /\ Val.inject j a ta). { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. apply KEPT. red. exists pc, (Istore chunk addr args src pc'); auto. @@ -961,7 +961,7 @@ Proof. econstructor; split. eapply exec_function_internal; eauto. eapply match_states_regular with (j := j'); eauto. - apply init_regs_inject; auto. apply val_list_inject_incr with j; auto. + apply init_regs_inject; auto. apply val_inject_list_incr with j; auto. - (* external function *) exploit external_call_inject; eauto. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 8720ce50..28934ce9 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -923,7 +923,7 @@ Proof. rewrite JBELOW in H by auto. eapply inj_of_bc_inv; eauto. rewrite H; congruence. } - assert (VMTOP: forall v v', val_inject j' v v' -> vmatch bc' v Vtop). + assert (VMTOP: forall v v', Val.inject j' v v' -> vmatch bc' v Vtop). { intros. inv H; constructor. eapply PMTOP; eauto. } diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index ff3ccfa1..b4c1df61 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3690,7 +3690,7 @@ Proof. Qed. Lemma vmatch_inj: - forall bc v x, vmatch bc v x -> val_inject (inj_of_bc bc) v v. + forall bc v x, vmatch bc v x -> Val.inject (inj_of_bc bc) v v. Proof. induction 1; econstructor. eapply pmatch_inj; eauto. rewrite Int.add_zero; auto. @@ -3698,7 +3698,7 @@ Proof. Qed. Lemma vmatch_list_inj: - forall bc vl xl, list_forall2 (vmatch bc) vl xl -> val_list_inject (inj_of_bc bc) vl vl. + forall bc vl xl, list_forall2 (vmatch bc) vl xl -> Val.inject_list (inj_of_bc bc) vl vl. Proof. induction 1; constructor. eapply vmatch_inj; eauto. auto. Qed. @@ -3761,7 +3761,7 @@ Proof. Qed. Lemma vmatch_inj_top: - forall bc v v', val_inject (inj_of_bc bc) v v' -> vmatch bc v Vtop. + forall bc v v', Val.inject (inj_of_bc bc) v v' -> vmatch bc v Vtop. Proof. intros. inv H; constructor. eapply pmatch_inj_top; eauto. Qed. |