diff options
65 files changed, 1434 insertions, 968 deletions
@@ -1,12 +1,87 @@ +Release 2.5, 2015-06-xx +======================= + +Language features: +- Extended inline assembly in the style of GCC. (See section 6.5 + of the user's manual.) The implementation is not as complete + as that of GCC or Clang. In particular, the only constraints + supported over operands are "r" (register), "m" (memory), and + "i" (integer immediate). + +Code generation and optimization: +- Revised translation of '||' and '&&' to Clight so as to + produce well-typed Clight code. +- More prudent value analysis of uninitialized declarations of + "const" global variables. +- Revised handling of "common" global declarations, fixes an issue + with uninitialized declarations of "const" global variables. + +Improvements in confidence: +- Formalized the typing rules for CompCert C in Coq and verified + a type-checker, which is used to produce the type annotations + in CompCert C ASTs, rather than trusting the types produced by + the Elab pass. +- Coq proof of correctness for the Unusedglob pass (elimination + of unreferenced static global definitions). The Coq AST for + compilation units now records which globals are static. +- More careful semantics of comparisons between a non-null pointer + and the null pointer. The comparison is undefined if the non-null + pointer is out of bounds. + +Usability: +- Generation of DWARF v2 debugging information in "-g" mode. + The information describes C types, global variables, functions, + but not yet function-local variables. This is currently available + only for the PowerPC/Diab target. +- Added command-line options to turn individual optimizations on or off, + and a "-O0" option to turn them all off. +- Revised handling of arguments to __builtin_annot so that no code + is generated for an argument that is a global variable or a local + variable whose address is taken. - In string and character literals, treat illegal escape sequences (e.g. "\%" or "\0") as an error instead of a warning. -- Upgraded Flocq to version 2.4.0. +- Warn if floating-point literals overflow or underflow when converted + to FP numbers. - cchecklink: added option "-files-from" to read .sdump file names from a file or from standard input. -- Revised handling of "common" global declarations, fixes an issue - with uninitialized declarations of "const" global variables. -- Use a Makefile instead of ocamlbuild to compile the OCaml code. +- In "-g -S" mode, annotate the generated .s file with comments + containing the C source code. +- Recognize and accept more of GCC's alternate keywords, e.g. __signed, + __volatile__, etc. + +ABI conformance: +- Improved ABI conformance for passing values of struct or union types + as function arguments or results. +- Support the "va_arg" macro from <stdarg.h> in the case of arguments + of struct or union types. + +Coq development: +- In the CompCert C and Clight ASTs, struct and union types are now + represented by name instead of by structure. A separate environment + maps these names to struct/union definitions. This avoids + bad algorithmic complexity of operations over structural types. +- Introduce symbol environments (type Senv.t) as a restricted view on + global environments (type Genv.t). +- Upgraded the Flocq library to version 2.4.0. +Bug fixing: +- Issue #4: exponential behaviors with deeply-nested struct types. +- Issue #6: mismatch on the definition of wchar_t +- Issue #10: definition of composite type missing from the environment. +- Issue #13: improved handling of wide string literals +- Issue #15: variable-argument functions are not eligible for inlining. +- Issue #19: support empty "switch" statements +- Issue #20: ABI incompatibility wrt struct passing on IA32. +- Issue #28: missing type decay in __builtin_memcpy_aligned applied to arrays. +- Issue #42: emit error if "static" definition follows non-"static" declaration. +- Issue #44: OSX assembler does not recognize ".global" directive. +- Protect against redefinition of the __i64_xxx helper library functions. +- Revised handling of nonstandard attributes in C type compatibility check. + +Miscellaneous: +- When preprocessing with gcc or clang, use "-std=c99" mode to force + C99 conformance. +- Use a Makefile instead of ocamlbuild to compile the OCaml code. Release 2.4, 2014-09-17 diff --git a/arm/Machregs.v b/arm/Machregs.v index f373b434..f46f2904 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +Require Import String. Require Import Coqlib. Require Import Maps. Require Import AST. @@ -75,6 +76,28 @@ End IndexedMreg. Definition is_stack_reg (r: mreg) : bool := false. +(** ** Names of registers *) + +Local Open Scope string_scope. + +Definition register_names := + ("R0", R0) :: ("R1", R1) :: ("R2", R2) :: ("R3", R3) :: + ("R4", R4) :: ("R5", R5) :: ("R6", R6) :: ("R7", R7) :: + ("R8", R8) :: ("R9", R9) :: ("R10", R10) :: ("R11", R11) :: + ("R12", R12) :: + ("F0", F0) :: ("F1", F1) :: ("F2", F2) :: ("F3", F3) :: + ("F4", F4) :: ("F5", F5) :: ("F6", F6) :: ("F7", F7) :: + ("F8", F8) :: ("F9", F9) :: ("F10", F10) :: ("F11", F11) :: + ("F12", F12) ::("F13", F13) ::("F14", F14) :: ("F15", F15) :: nil. + +Definition register_by_name (s: string) : option mreg := + let fix assoc (l: list (string * mreg)) : option mreg := + match l with + | nil => None + | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l' + end + in assoc register_names. + (** ** Destroyed registers, preferred registers *) Definition destroyed_by_op (op: operation): list mreg := @@ -95,9 +118,20 @@ Definition destroyed_by_cond (cond: condition): list mreg := Definition destroyed_by_jumptable: list mreg := nil. +Fixpoint destroyed_by_clobber (cl: list string): list mreg := + match cl with + | nil => nil + | c1 :: cl => + match register_by_name c1 with + | Some r => r :: destroyed_by_clobber cl + | None => destroyed_by_clobber cl + end + end. + Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_memcpy sz al => if zle sz 32 then F7 :: nil else R2 :: R3 :: R12 :: nil + | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil end. diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml index 44e6b192..d59ec8b8 100644 --- a/arm/Machregsaux.ml +++ b/arm/Machregsaux.ml @@ -12,41 +12,24 @@ (** Auxiliary functions on machine registers *) +open Camlcoq open Machregs -let register_names = [ - ("R0", R0); ("R1", R1); ("R2", R2); ("R3", R3); - ("R4", R4); ("R5", R5); ("R6", R6); ("R7", R7); - ("R8", R8); ("R9", R9); ("R10", R10); ("R11", R11); - ("R12", R12); - ("F0", F0); ("F1", F1); ("F2", F2); ("F3", F3); - ("F4", F4); ("F5", F5); ("F6", F6); ("F7", F7); - ("F8", F8); ("F9", F9); ("F10", F10); ("F11", F11); - ("F12", F12);("F13", F13);("F14", F14); ("F15", F15) -] +let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31 + +let _ = + List.iter + (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s)) + Machregs.register_names let scratch_register_names = [ "R14" ] let name_of_register r = - let rec rev_assoc = function - | [] -> None - | (a, b) :: rem -> if b = r then Some a else rev_assoc rem - in rev_assoc register_names + try Some (Hashtbl.find register_names r) with Not_found -> None let register_by_name s = - try - Some(List.assoc (String.uppercase s) register_names) - with Not_found -> - None + Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s)) let can_reserve_register r = List.mem r Conventions1.int_callee_save_regs || List.mem r Conventions1.float_callee_save_regs - -let mregs_of_clobber idl = - List.fold_left - (fun l c -> - match register_by_name (Camlcoq.extern_atom c) with - | Some r -> r :: l - | None -> l) - [] idl diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli index f0feec96..d4877a62 100644 --- a/arm/Machregsaux.mli +++ b/arm/Machregsaux.mli @@ -16,4 +16,3 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val scratch_register_names: string list val can_reserve_register: Machregs.mreg -> bool -val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list @@ -808,40 +808,40 @@ Hypothesis valid_different_pointers_inj: Ltac InvInject := match goal with - | [ H: val_inject _ (Vint _) _ |- _ ] => + | [ H: Val.inject _ (Vint _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vfloat _) _ |- _ ] => + | [ H: Val.inject _ (Vfloat _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vsingle _) _ |- _ ] => + | [ H: Val.inject _ (Vsingle _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vptr _ _) _ |- _ ] => + | [ H: Val.inject _ (Vptr _ _) _ |- _ ] => inv H; InvInject - | [ H: val_list_inject _ nil _ |- _ ] => + | [ H: Val.inject_list _ nil _ |- _ ] => inv H; InvInject - | [ H: val_list_inject _ (_ :: _) _ |- _ ] => + | [ H: Val.inject_list _ (_ :: _) _ |- _ ] => inv H; InvInject | _ => idtac end. Remark eval_shift_inj: - forall s v v', val_inject f v v' -> val_inject f (eval_shift s v) (eval_shift s v'). + forall s v v', Val.inject f v v' -> Val.inject f (eval_shift s v) (eval_shift s v'). Proof. intros. inv H; destruct s; simpl; auto; rewrite s_range; auto. Qed. Lemma eval_condition_inj: forall cond vl1 vl2 b, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. Proof. intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl. - eauto 4 using val_cmp_bool_inject. - eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies. - eauto using val_cmp_bool_inject, eval_shift_inj. - eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies, eval_shift_inj. - eauto 4 using val_cmp_bool_inject. - eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies. + eauto 4 using Val.cmp_bool_inject. + eauto 4 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. + eauto using Val.cmp_bool_inject, eval_shift_inj. + eauto 4 using Val.cmpu_bool_inject, Mem.valid_pointer_implies, eval_shift_inj. + eauto 4 using Val.cmp_bool_inject. + eauto 4 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; simpl in H0; inv H0; auto. @@ -854,7 +854,7 @@ Qed. Ltac TrivialExists := match goal with - | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] => + | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] => exists v1; split; auto | _ => idtac end. @@ -863,28 +863,28 @@ Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, (forall id ofs, In id (globals_operation op) -> - val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> - val_inject f sp1 sp2 -> - val_list_inject f vl1 vl2 -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> eval_operation ge1 sp1 op vl1 m1 = Some v1 -> - exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. + exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. apply GL; simpl; auto. - apply Values.val_add_inject; auto. + apply Values.Val.add_inject; auto. inv H4; simpl; auto. inv H4; simpl; auto. - apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. apply eval_shift_inj; auto. - apply Values.val_add_inject; auto. + apply Values.Val.add_inject; auto. + apply Values.Val.add_inject; auto. apply eval_shift_inj; auto. + apply Values.Val.add_inject; auto. - apply Values.val_sub_inject; auto. - apply Values.val_sub_inject; auto. apply eval_shift_inj; auto. - apply Values.val_sub_inject; auto. apply eval_shift_inj; auto. - apply (@Values.val_sub_inject f (Vint i) (Vint i) v v'); auto. + apply Values.Val.sub_inject; auto. + apply Values.Val.sub_inject; auto. apply eval_shift_inj; auto. + apply Values.Val.sub_inject; auto. apply eval_shift_inj; auto. + apply (@Values.Val.sub_inject f (Vint i) (Vint i) v v'); auto. inv H4; inv H2; simpl; auto. - apply Values.val_add_inject; auto. inv H4; inv H2; simpl; auto. + apply Values.Val.add_inject; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H3; simpl in H1; inv H1. simpl. @@ -958,17 +958,17 @@ Lemma eval_addressing_inj: forall addr sp1 vl1 sp2 vl2 v1, (forall id ofs, In id (globals_addressing addr) -> - val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> - val_inject f sp1 sp2 -> - val_list_inject f vl1 vl2 -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> eval_addressing ge1 sp1 addr vl1 = Some v1 -> - exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. + exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. - apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. apply eval_shift_inj; auto. - apply Values.val_add_inject; auto. + apply Values.Val.add_inject; auto. + apply Values.Val.add_inject; auto. + apply Values.Val.add_inject; auto. apply eval_shift_inj; auto. + apply Values.Val.add_inject; auto. Qed. End EVAL_COMPAT. @@ -1034,7 +1034,7 @@ Proof. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends. apply valid_different_pointers_extends; auto. - rewrite <- val_list_inject_lessdef. eauto. auto. + rewrite <- val_inject_list_lessdef. eauto. auto. Qed. Lemma eval_operation_lessdef: @@ -1044,10 +1044,10 @@ Lemma eval_operation_lessdef: eval_operation genv sp op vl1 m1 = Some v1 -> exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2. Proof. - intros. rewrite val_list_inject_lessdef in H. + intros. rewrite val_inject_list_lessdef in H. assert (exists v2 : val, eval_operation genv sp op vl2 m2 = Some v2 - /\ val_inject (fun b => Some(b, 0)) v1 v2). + /\ Val.inject (fun b => Some(b, 0)) v1 v2). eapply eval_operation_inj with (m1 := m1) (sp1 := sp). apply valid_pointer_extends; auto. apply weak_valid_pointer_extends; auto. @@ -1065,10 +1065,10 @@ Lemma eval_addressing_lessdef: eval_addressing genv sp addr vl1 = Some v1 -> exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2. Proof. - intros. rewrite val_list_inject_lessdef in H. + intros. rewrite val_inject_list_lessdef in H. assert (exists v2 : val, eval_addressing genv sp addr vl2 = Some v2 - /\ val_inject (fun b => Some(b, 0)) v1 v2). + /\ Val.inject (fun b => Some(b, 0)) v1 v2). eapply eval_addressing_inj with (sp1 := sp). intros. rewrite <- val_inject_lessdef; auto. rewrite <- val_inject_lessdef; auto. @@ -1092,7 +1092,7 @@ Variable delta: Z. Hypothesis sp_inj: f sp1 = Some(sp2, delta). Remark symbol_address_inject: - forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). + forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. @@ -1101,7 +1101,7 @@ Qed. Lemma eval_condition_inject: forall cond vl1 vl2 b m1 m2, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. @@ -1115,11 +1115,11 @@ Qed. Lemma eval_addressing_inject: forall addr vl1 vl2 v1, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> exists v2, eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 - /\ val_inject f v1 v2. + /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_addressing. simpl. @@ -1129,12 +1129,12 @@ Qed. Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> exists v2, eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 - /\ val_inject f v1 v2. + /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_operation. simpl. diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index 96d13943..886f6de3 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -52,6 +52,14 @@ let print_condition reg pp = function fprintf pp "%a %sf 0.0" reg r1 (comparison_name c) | (Cnotcompfzero c, [r1]) -> fprintf pp "%a not(%sf) 0.0" reg r1 (comparison_name c) + | (Ccompfs c, [r1;r2]) -> + fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2 + | (Cnotcompfs c, [r1;r2]) -> + fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2 + | (Ccompfszero c, [r1]) -> + fprintf pp "%a %sfs 0.0" reg r1 (comparison_name c) + | (Cnotcompfszero c, [r1]) -> + fprintf pp "%a not(%sfs) 0.0" reg r1 (comparison_name c) | _ -> fprintf pp "<bad condition>" @@ -59,6 +67,7 @@ let print_operation reg pp = function | Omove, [r1] -> reg pp r1 | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n) | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n) + | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n) | Oaddrsymbol(id, ofs), [] -> fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs) | Oaddrstack ofs, [] -> @@ -100,9 +109,21 @@ let print_operation reg pp = function | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2 | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2 | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2 + | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1 + | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1 + | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2 + | Osubfs, [r1;r2] -> fprintf pp "%a -fs %a" reg r1 reg r2 + | Omulfs, [r1;r2] -> fprintf pp "%a *fs %a" reg r1 reg r2 + | Odivfs, [r1;r2] -> fprintf pp "%a /fs %a" reg r1 reg r2 | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 + | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1 | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 + | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1 + | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1 + | Ointuofsingle, [r1] -> fprintf pp "intuofsingle(%a)" reg r1 + | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1 + | Osingleofintu, [r1] -> fprintf pp "singleofintu(%a)" reg r1 | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2 | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1 | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1 diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index c77572db..505c3265 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -300,7 +300,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (* Emit .file / .loc debugging directives *) let print_file_line oc file line = - PrintAnnot.print_file_line oc comment file line + print_file_line oc comment file line let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) @@ -320,12 +320,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "sp" oc txt targs args + print_annot_stmt preg "sp" oc txt targs args end let print_annot_val oc txt args res = fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_val preg oc txt args; + print_annot_val preg oc txt args; match args, res with | [IR src], [IR dst] -> if dst = src then 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1) @@ -1005,7 +1005,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = print_annot_val oc (extern_atom txt) args res | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; + print_inline_asm preg oc (extern_atom txt) sg args res; fprintf oc "%s end inline assembly\n" comment; 5 (* hoping this is an upper bound... *) | _ -> 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. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 94f13aa1..71328c71 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -437,10 +437,10 @@ let convertAttr a = let n = Cutil.alignas_attribute a in if n > 0 then Some (N.of_int (log2 n)) else None } -let convertCallconv va attr = +let convertCallconv va unproto attr = let sr = Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in - { cc_vararg = va; cc_structret = sr <> [] } + { cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] } (** Types *) @@ -494,7 +494,7 @@ let rec convertTyp env t = | Some tl -> convertParams env tl end, convertTyp env tres, - convertCallconv va a) + convertCallconv va (targs = None) a) | C.TNamed _ -> convertTyp env (Cutil.unroll env t) | C.TStruct(id, a) -> @@ -626,7 +626,6 @@ let ewrap = function error ("retyping error: " ^ string_of_errmsg msg); ezero let rec convertExpr env e = - (*let ty = convertTyp env e.etyp in*) match e.edesc with | C.EVar _ | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) @@ -734,9 +733,8 @@ let rec convertExpr env e = ewrap (Ctyping.eseqor (convertExpr env e1) (convertExpr env e2)) | C.EConditional(e1, e2, e3) -> - ewrap (Ctyping.econdition' (convertExpr env e1) - (convertExpr env e2) (convertExpr env e3) - (convertTyp env e.etyp)) + ewrap (Ctyping.econdition (convertExpr env e1) + (convertExpr env e2) (convertExpr env e3)) | C.ECast(ty1, e1) -> ewrap (Ctyping.ecast (convertTyp env ty1) (convertExpr env e1)) | C.ECompound(ty1, ie) -> @@ -798,7 +796,8 @@ let rec convertExpr env e = let targs = convertTypArgs env [] args and tres = convertTyp env e.etyp in let sg = - signature_of_type targs tres {cc_vararg = true; cc_structret = false} in + signature_of_type targs tres + {cc_vararg = true; cc_unproto = false; cc_structret = false} in Ebuiltin(EF_external(intern_string "printf", sg), targs, convertExprList env args, tres) @@ -847,7 +846,7 @@ let convertAsm loc env txt outputs inputs clobber = let (txt', output', inputs') = ExtendedAsm.transf_asm loc env txt outputs inputs clobber in let clobber' = - List.map intern_string clobber in + List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in let ty_res = match output' with None -> TVoid [] | Some e -> e.etyp in (* Build the Ebuiltin expression *) @@ -1033,11 +1032,12 @@ let convertFundef loc env fd = a_access = Sections.Access_default; a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *) a_loc = loc }; - (id', Gfun(Internal {fn_return = ret; - fn_callconv = convertCallconv fd.fd_vararg fd.fd_attrib; - fn_params = params; - fn_vars = vars; - fn_body = body'})) + (id', Gfun(Internal + {fn_return = ret; + fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; + fn_params = params; + fn_vars = vars; + fn_body = body'})) (** External function declaration *) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 17c59b97..dfc69412 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -163,7 +163,7 @@ Qed. [f b = Some(b', ofs)] means that C#minor block [b] corresponds to a sub-block of Cminor block [b] at offset [ofs]. - A memory injection [f] defines a relation [val_inject f] between + A memory injection [f] defines a relation [Val.inject f] between values and a relation [Mem.inject f] between memory states. These relations will be used intensively in our proof of simulation between C#minor and Cminor executions. *) @@ -171,7 +171,7 @@ Qed. (** ** Matching between Cshaprminor's temporaries and Cminor's variables *) Definition match_temps (f: meminj) (le: Csharpminor.temp_env) (te: env) : Prop := - forall id v, le!id = Some v -> exists v', te!(id) = Some v' /\ val_inject f v v'. + forall id v, le!id = Some v -> exists v', te!(id) = Some v' /\ Val.inject f v v'. Lemma match_temps_invariant: forall f f' le te, @@ -185,7 +185,7 @@ Qed. Lemma match_temps_assign: forall f le te id v tv, match_temps f le te -> - val_inject f v tv -> + Val.inject f v tv -> match_temps f (PTree.set id v le) (PTree.set id tv te). Proof. intros; red; intros. rewrite PTree.gsspec in *. destruct (peq id0 id). @@ -197,7 +197,7 @@ Qed. Inductive match_var (f: meminj) (sp: block): option (block * Z) -> option Z -> Prop := | match_var_local: forall b sz ofs, - val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> + Val.inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> match_var f sp (Some(b, sz)) (Some ofs) | match_var_global: match_var f sp None None. @@ -553,7 +553,7 @@ Qed. Lemma match_callstack_set_temp: forall f cenv e le te sp lo hi cs bound tbound m tm tf id v tv, - val_inject f v tv -> + Val.inject f v tv -> match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) bound tbound -> match_callstack f m tm (Frame cenv tf e (PTree.set id v le) (PTree.set id tv te) sp lo hi :: cs) bound tbound. Proof. @@ -1119,7 +1119,7 @@ Fixpoint set_params' (vl: list val) (il: list ident) (te: Cminor.env) : Cminor.e Lemma bind_parameters_agree_rec: forall f vars vals tvals le1 le2 te, bind_parameters vars vals le1 = Some le2 -> - val_list_inject f vals tvals -> + Val.inject_list f vals tvals -> match_temps f le1 te -> match_temps f le2 (set_params' tvals vars te). Proof. @@ -1213,7 +1213,7 @@ Qed. Lemma bind_parameters_agree: forall f params temps vals tvals le, bind_parameters params vals (create_undef_temps temps) = Some le -> - val_list_inject f vals tvals -> + Val.inject_list f vals tvals -> list_norepet params -> list_disjoint params temps -> match_temps f le (set_locals temps (set_params tvals params)). @@ -1238,7 +1238,7 @@ Theorem match_callstack_function_entry: list_disjoint (Csharpminor.fn_params fn) (Csharpminor.fn_temps fn) -> alloc_variables Csharpminor.empty_env m (Csharpminor.fn_vars fn) e m' -> bind_parameters (Csharpminor.fn_params fn) args (create_undef_temps fn.(fn_temps)) = Some le -> - val_list_inject f args targs -> + Val.inject_list f args targs -> Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) -> match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) -> Mem.inject f m tm -> @@ -1259,39 +1259,39 @@ Qed. (** * Compatibility of evaluation functions with respect to memory injections. *) Remark val_inject_val_of_bool: - forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). + forall f b, Val.inject f (Val.of_bool b) (Val.of_bool b). Proof. intros; destruct b; constructor. Qed. Remark val_inject_val_of_optbool: - forall f ob, val_inject f (Val.of_optbool ob) (Val.of_optbool ob). + forall f ob, Val.inject f (Val.of_optbool ob) (Val.of_optbool ob). Proof. intros; destruct ob; simpl. destruct b; constructor. constructor. Qed. Ltac TrivialExists := match goal with - | [ |- exists y, Some ?x = Some y /\ val_inject _ _ _ ] => + | [ |- exists y, Some ?x = Some y /\ Val.inject _ _ _ ] => exists x; split; [auto | try(econstructor; eauto)] - | [ |- exists y, _ /\ val_inject _ (Vint ?x) _ ] => + | [ |- exists y, _ /\ Val.inject _ (Vint ?x) _ ] => exists (Vint x); split; [eauto with evalexpr | constructor] - | [ |- exists y, _ /\ val_inject _ (Vfloat ?x) _ ] => + | [ |- exists y, _ /\ Val.inject _ (Vfloat ?x) _ ] => exists (Vfloat x); split; [eauto with evalexpr | constructor] - | [ |- exists y, _ /\ val_inject _ (Vlong ?x) _ ] => + | [ |- exists y, _ /\ Val.inject _ (Vlong ?x) _ ] => exists (Vlong x); split; [eauto with evalexpr | constructor] | _ => idtac end. -(** Compatibility of [eval_unop] with respect to [val_inject]. *) +(** Compatibility of [eval_unop] with respect to [Val.inject]. *) Lemma eval_unop_compat: forall f op v1 tv1 v, eval_unop op v1 = Some v -> - val_inject f v1 tv1 -> + Val.inject f v1 tv1 -> exists tv, eval_unop op tv1 = Some tv - /\ val_inject f v tv. + /\ Val.inject f v tv. Proof. destruct op; simpl; intros. inv H; inv H0; simpl; TrivialExists. @@ -1329,17 +1329,17 @@ Proof. inv H0; simpl in H; inv H. simpl. TrivialExists. Qed. -(** Compatibility of [eval_binop] with respect to [val_inject]. *) +(** Compatibility of [eval_binop] with respect to [Val.inject]. *) Lemma eval_binop_compat: forall f op v1 tv1 v2 tv2 v m tm, eval_binop op v1 v2 m = Some v -> - val_inject f v1 tv1 -> - val_inject f v2 tv2 -> + Val.inject f v1 tv1 -> + Val.inject f v2 tv2 -> Mem.inject f m tm -> exists tv, eval_binop op tv1 tv2 tm = Some tv - /\ val_inject f v tv. + /\ Val.inject f v tv. Proof. destruct op; simpl; intros. inv H; inv H0; inv H1; TrivialExists. @@ -1401,7 +1401,7 @@ Proof. destruct (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E. replace (Val.cmpu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b). destruct b; simpl; constructor. - symmetry. eapply val_cmpu_bool_inject; eauto. + symmetry. eapply Val.cmpu_bool_inject; eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. @@ -1429,7 +1429,7 @@ Lemma var_addr_correct: eval_var_addr ge e id b -> exists tv, eval_expr tge (Vptr sp Int.zero) te tm (var_addr cenv id) tv - /\ val_inject f (Vptr b Int.zero) tv. + /\ Val.inject f (Vptr b Int.zero) tv. Proof. unfold var_addr; intros. assert (match_var f sp e!id cenv!id). @@ -1474,7 +1474,7 @@ Qed. Remark bool_of_val_inject: forall f v tv b, - Val.bool_of_val v b -> val_inject f v tv -> Val.bool_of_val tv b. + Val.bool_of_val v b -> Val.inject f v tv -> Val.bool_of_val tv b. Proof. intros. inv H0; inv H; constructor; auto. Qed. @@ -1484,7 +1484,7 @@ Lemma transl_constant_correct: Csharpminor.eval_constant cst = Some v -> exists tv, eval_constant tge sp (transl_constant cst) = Some tv - /\ val_inject f v tv. + /\ Val.inject f v tv. Proof. destruct cst; simpl; intros; inv H. exists (Vint i); auto. @@ -1505,7 +1505,7 @@ Lemma transl_expr_correct: (TR: transl_expr cenv a = OK ta), exists tv, eval_expr tge (Vptr sp Int.zero) te tm ta tv - /\ val_inject f v tv. + /\ Val.inject f v tv. Proof. induction 3; intros; simpl in TR; try (monadInv TR). (* Etempvar *) @@ -1543,7 +1543,7 @@ Lemma transl_exprlist_correct: (TR: transl_exprlist cenv a = OK ta), exists tv, eval_exprlist tge (Vptr sp Int.zero) te tm ta tv - /\ val_list_inject f v tv. + /\ Val.inject_list f v tv. Proof. induction 3; intros; monadInv TR. exists (@nil val); split. constructor. constructor. @@ -1610,7 +1610,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm)) (MK: match_cont k tk cenv nil cs) (ISCC: Csharpminor.is_call_cont k) - (ARGSINJ: val_list_inject f args targs), + (ARGSINJ: Val.inject_list f args targs), match_states (Csharpminor.Callstate fd args k m) (Callstate tfd targs tk tm) | match_returnstate: @@ -1618,7 +1618,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := (MINJ: Mem.inject f m tm) (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm)) (MK: match_cont k tk cenv nil cs) - (RESINJ: val_inject f v tv), + (RESINJ: Val.inject f v tv), match_states (Csharpminor.Returnstate v k m) (Returnstate tv tk tm). @@ -1626,7 +1626,7 @@ Remark val_inject_function_pointer: forall bound v fd f tv, Genv.find_funct ge v = Some fd -> match_globalenvs f bound -> - val_inject f v tv -> + Val.inject f v tv -> tv = v. Proof. intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v. diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 2a5d17bc..6284660c 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -1054,13 +1054,13 @@ Hypothesis valid_different_pointers_inj: b1' <> b2' \/ Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). -Remark val_inject_vtrue: forall f, val_inject f Vtrue Vtrue. +Remark val_inject_vtrue: forall f, Val.inject f Vtrue Vtrue. Proof. unfold Vtrue; auto. Qed. -Remark val_inject_vfalse: forall f, val_inject f Vfalse Vfalse. +Remark val_inject_vfalse: forall f, Val.inject f Vfalse Vfalse. Proof. unfold Vfalse; auto. Qed. -Remark val_inject_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). +Remark val_inject_of_bool: forall f b, Val.inject f (Val.of_bool b) (Val.of_bool b). Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. Qed. @@ -1075,8 +1075,8 @@ Ltac TrivialInject := Lemma sem_cast_inject: forall v1 ty1 ty v tv1, sem_cast v1 ty1 ty = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> + exists tv, sem_cast tv1 ty1 ty = Some tv /\ Val.inject f v tv. Proof. unfold sem_cast; intros; destruct (classify_cast ty1 ty); inv H0; inv H; TrivialInject. @@ -1093,8 +1093,8 @@ Qed. Lemma sem_unary_operation_inj: forall op v1 ty v tv1, sem_unary_operation op v1 ty m = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> + exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ Val.inject f v tv. Proof. unfold sem_unary_operation; intros. destruct op. (* notbool *) @@ -1118,15 +1118,15 @@ Definition optval_self_injects (ov: option val) : Prop := Remark sem_binarith_inject: forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2', sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 = Some v -> - val_inject f v1 v1' -> val_inject f v2 v2' -> + Val.inject f v1 v1' -> Val.inject f v2 v2' -> (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) -> (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) -> (forall n1 n2, optval_self_injects (sem_float n1 n2)) -> (forall n1 n2, optval_self_injects (sem_single n1 n2)) -> - exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ val_inject f v v'. + exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ Val.inject f v v'. Proof. intros. - assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> val_inject f v v). + assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> Val.inject f v v). { intros. subst ov; simpl in H7. destruct v0; contradiction || constructor. } @@ -1144,8 +1144,8 @@ Qed. Remark sem_shift_inject: forall sem_int sem_long v1 t1 v2 t2 v v1' v2', sem_shift sem_int sem_long v1 t1 v2 t2 = Some v -> - val_inject f v1 v1' -> val_inject f v2 v2' -> - exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ val_inject f v v'. + Val.inject f v1 v1' -> Val.inject f v2 v2' -> + exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ Val.inject f v v'. Proof. intros. exists v. unfold sem_shift in *; destruct (classify_shift t1 t2); inv H0; inv H1; try discriminate. @@ -1158,9 +1158,9 @@ Qed. Remark sem_cmp_inj: forall cmp v1 tv1 ty1 v2 tv2 ty2 v, sem_cmp cmp v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> - val_inject f v2 tv2 -> - exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> + Val.inject f v2 tv2 -> + exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. intros. unfold sem_cmp in *; destruct (classify_cmp ty1 ty2). @@ -1168,21 +1168,21 @@ Proof. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b). simpl. TrivialInject. - symmetry. eapply val_cmpu_bool_inject; eauto. + symmetry. eapply Val.cmpu_bool_inject; eauto. - (* pointer - long *) destruct v2; try discriminate. inv H1. set (v2 := Vint (Int.repr (Int64.unsigned i))) in *. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 v2) with (Some b). simpl. TrivialInject. - symmetry. eapply val_cmpu_bool_inject with (v2 := v2); eauto. constructor. + symmetry. eapply Val.cmpu_bool_inject with (v2 := v2); eauto. constructor. - (* long - pointer *) destruct v1; try discriminate. inv H0. set (v1 := Vint (Int.repr (Int64.unsigned i))) in *. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. replace (Val.cmpu_bool (Mem.valid_pointer m') cmp v1 tv2) with (Some b). simpl. TrivialInject. - symmetry. eapply val_cmpu_bool_inject with (v1 := v1); eauto. constructor. + symmetry. eapply Val.cmpu_bool_inject with (v1 := v1); eauto. constructor. - (* numerical - numerical *) assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))). { @@ -1194,8 +1194,8 @@ Qed. Lemma sem_binary_operation_inj: forall cenv op v1 ty1 v2 ty2 v tv1 tv2, sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> val_inject f v2 tv2 -> - exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> Val.inject f v2 tv2 -> + exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. unfold sem_binary_operation; intros; destruct op. - (* add *) @@ -1269,7 +1269,7 @@ Qed. Lemma bool_val_inj: forall v ty b tv, bool_val v ty m = Some b -> - val_inject f v tv -> + Val.inject f v tv -> bool_val tv ty m' = Some b. Proof. unfold bool_val; intros. @@ -1283,9 +1283,9 @@ End GENERIC_INJECTION. Lemma sem_unary_operation_inject: forall f m m' op v1 ty1 v tv1, sem_unary_operation op v1 ty1 m = Some v -> - val_inject f v1 tv1 -> + Val.inject f v1 tv1 -> Mem.inject f m m' -> - exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ val_inject f v tv. + exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ Val.inject f v tv. Proof. intros. eapply sem_unary_operation_inj; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. @@ -1294,9 +1294,9 @@ Qed. Lemma sem_binary_operation_inject: forall f m m' cenv op v1 ty1 v2 ty2 v tv1 tv2, sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> val_inject f v2 tv2 -> + Val.inject f v1 tv1 -> Val.inject f v2 tv2 -> Mem.inject f m m' -> - exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. intros. eapply sem_binary_operation_inj; eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. @@ -1308,7 +1308,7 @@ Qed. Lemma bool_val_inject: forall f m m' v ty b tv, bool_val v ty m = Some b -> - val_inject f v tv -> + Val.inject f v tv -> Mem.inject f m m' -> bool_val tv ty m' = Some b. Proof. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 8ea4e077..db059791 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -208,13 +208,22 @@ Definition type_of_fundef (f: fundef) : type := (** ** Programs *) -(** A program is composed of: +(** A "pre-program", as produced by the elaborator is composed of: - a list of definitions of functions and global variables; - the names of functions and global variables that are public (not static); - the name of the function that acts as entry point ("main" function). -- a list of definitions for structure and union names; -- the corresponding composite environment; -*) +- a list of definitions for structure and union names + +A program is composed of the same information, plus the corresponding +composite environment, and a proof that this environment is consistent +with the composite definitions. *) + +Record pre_program : Type := { + pprog_defs: list (ident * globdef fundef type); + pprog_public: list ident; + pprog_main: ident; + pprog_types: list composite_definition +}. Record program : Type := { prog_defs: list (ident * globdef fundef type); @@ -232,20 +241,15 @@ Definition program_of_program (p: program) : AST.program fundef type := Coercion program_of_program: program >-> AST.program. -Program Definition make_program (types: list composite_definition) - (defs: list (ident * globdef fundef type)) - (public: list ident) - (main: ident): res program := - match build_composite_env types with - | OK env => - OK {| prog_defs := defs; - prog_public := public; - prog_main := main; - prog_types := types; - prog_comp_env := env; +Program Definition program_of_pre_program (p: pre_program) : res program := + match build_composite_env p.(pprog_types) with + | Error e => Error e + | OK ce => + OK {| prog_defs := p.(pprog_defs); + prog_public := p.(pprog_public); + prog_main := p.(pprog_main); + prog_types := p.(pprog_types); + prog_comp_env := ce; prog_comp_env_eq := _ |} - | Error msg => - Error msg end. - diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 2582fff8..cde9ad11 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -157,31 +157,111 @@ Definition type_deref (ty: type) : res type := | _ => Error (msg "operator prefix *") end. +(** Inferring the type of a conditional expression: the merge of the types + of the two arms. *) + +Definition attr_combine (a1 a2: attr) : attr := + {| attr_volatile := a1.(attr_volatile) || a2.(attr_volatile); + attr_alignas := + match a1.(attr_alignas), a2.(attr_alignas) with + | None, al2 => al2 + | al1, None => al1 + | Some n1, Some n2 => Some (N.max n1 n2) + end + |}. + +Definition intsize_eq: forall (x y: intsize), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +Definition signedness_eq: forall (x y: signedness), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +Definition floatsize_eq: forall (x y: floatsize), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +Definition callconv_combine (cc1 cc2: calling_convention) : res calling_convention := + if bool_eq cc1.(cc_vararg) cc2.(cc_vararg) then + OK {| cc_vararg := cc1.(cc_vararg); + cc_unproto := cc1.(cc_unproto) && cc2.(cc_unproto); + cc_structret := cc1.(cc_structret) |} + else + Error (msg "incompatible calling conventions"). + +Fixpoint type_combine (ty1 ty2: type) : res type := + match ty1, ty2 with + | Tvoid, Tvoid => OK Tvoid + | Tint sz1 sg1 a1, Tint sz2 sg2 a2 => + if intsize_eq sz1 sz2 && signedness_eq sg1 sg2 + then OK (Tint sz1 sg1 (attr_combine a1 a2)) + else Error (msg "incompatible int types") + | Tlong sg1 a1, Tlong sg2 a2 => + if signedness_eq sg1 sg2 + then OK (Tlong sg1 (attr_combine a1 a2)) + else Error (msg "incompatible long types") + | Tfloat sz1 a1, Tfloat sz2 a2 => + if floatsize_eq sz1 sz2 + then OK (Tfloat sz1 (attr_combine a1 a2)) + else Error (msg "incompatible float types") + | Tpointer t1 a1, Tpointer t2 a2 => + do t <- type_combine t1 t2; OK (Tpointer t (attr_combine a1 a2)) + | Tarray t1 sz1 a1, Tarray t2 sz2 a2 => + do t <- type_combine t1 t2; + if zeq sz1 sz2 + then OK (Tarray t sz1 (attr_combine a1 a2)) + else Error (msg "incompatible array types") + | Tfunction args1 res1 cc1, Tfunction args2 res2 cc2 => + do res <- type_combine res1 res2; + do args <- + (if cc1.(cc_unproto) then OK args2 else + if cc2.(cc_unproto) then OK args1 else + typelist_combine args1 args2); + do cc <- callconv_combine cc1 cc2; + OK (Tfunction args res cc) + | Tstruct id1 a1, Tstruct id2 a2 => + if ident_eq id1 id2 + then OK (Tstruct id1 (attr_combine a1 a2)) + else Error (msg "incompatible struct types") + | Tunion id1 a1, Tunion id2 a2 => + if ident_eq id1 id2 + then OK (Tunion id1 (attr_combine a1 a2)) + else Error (msg "incompatible union types") + | _, _ => + Error (msg "incompatible types") + end + +with typelist_combine (tl1 tl2: typelist) : res typelist := + match tl1, tl2 with + | Tnil, Tnil => OK Tnil + | Tcons t1 tl1, Tcons t2 tl2 => + do t <- type_combine t1 t2; + do tl <- typelist_combine tl1 tl2; + OK (Tcons t tl) + | _, _ => + Error (msg "incompatible function types") + end. + Definition is_void (ty: type) : bool := match ty with Tvoid => true | _ => false end. -Definition type_join (ty1 ty2: type) : res type := +Definition type_conditional (ty1 ty2: type) : res type := match typeconv ty1, typeconv ty2 with - | (Tint _ _ _ | Tfloat _ _), (Tint _ _ _ | Tfloat _ _) => + | (Tint _ _ _ | Tlong _ _ | Tfloat _ _), + (Tint _ _ _ | Tlong _ _ | Tfloat _ _) => binarith_type ty1 ty2 "conditional expression" | Tpointer t1 a1, Tpointer t2 a2 => - OK (Tpointer (if is_void t1 || is_void t2 then Tvoid else t1) noattr) + let t := + if is_void t1 || is_void t2 then Tvoid else + match type_combine t1 t2 with + | OK t => t + | Error _ => Tvoid (* tolerance *) + end + in OK (Tpointer t noattr) | Tpointer t1 a1, Tint _ _ _ => OK (Tpointer t1 noattr) | Tint _ _ _, Tpointer t2 a2 => OK (Tpointer t2 noattr) - | Tvoid, Tvoid => - OK Tvoid - | Tstruct id1 a1, Tstruct id2 a2 => - if ident_eq id1 id2 - then OK (Tstruct id1 noattr) - else Error (msg "conditional expression") - | Tunion id1 a1, Tunion id2 a2 => - if ident_eq id1 id2 - then OK (Tunion id1 noattr) - else Error (msg "conditional expression") - | _, _ => - Error (msg "conditional expression") + | t1, t2 => + type_combine t1 t2 end. (** * Specification of the type system *) @@ -603,7 +683,7 @@ Definition eseqor (r1 r2: expr) : res expr := Definition econdition (r1 r2 r3: expr) : res expr := do x1 <- check_rval r1; do x2 <- check_rval r2; do x3 <- check_rval r3; do y1 <- check_bool (typeof r1); - do ty <- type_join (typeof r2) (typeof r3); + do ty <- type_conditional (typeof r2) (typeof r3); OK (Econdition r1 r2 r3 ty). Definition econdition' (r1 r2 r3: expr) (ty: type) : res expr := @@ -822,6 +902,23 @@ Definition retype_function (ce: composite_env) (e: typenv) (f: function) : res f f.(fn_vars) s). +Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fundef := + match fd with + | Internal f => do f' <- retype_function ce e f; OK (Internal f') + | External id args res cc => OK fd + end. + +Definition typecheck_program (p: program) : res program := + let e := bind_globdef (PTree.empty _) p.(prog_defs) in + let ce := p.(prog_comp_env) in + do defs <- transf_globdefs (retype_fundef ce e) (fun v => OK v) p.(prog_defs); + OK {| prog_defs := defs; + prog_public := p.(prog_public); + prog_main := p.(prog_main); + prog_types := p.(prog_types); + prog_comp_env := ce; + prog_comp_env_eq := p.(prog_comp_env_eq) |}. + (** Soundness of the smart constructors. *) Lemma check_cast_sound: @@ -882,30 +979,48 @@ Proof. destruct i; auto. Qed. -Lemma type_join_cast: +Lemma type_combine_cast: forall t1 t2 t, - type_join t1 t2 = OK t -> wt_cast t1 t /\ wt_cast t2 t. -Proof. - intros. unfold type_join in H. + type_combine t1 t2 = OK t -> + match t1 with Tarray _ _ _ => False | Tfunction _ _ _ => False | _ => True end -> + match t2 with Tarray _ _ _ => False | Tfunction _ _ _ => False | _ => True end -> + wt_cast t1 t /\ wt_cast t2 t. +Proof. + intros. + unfold wt_cast; destruct t1; try discriminate; destruct t2; simpl in H; inv H. +- simpl; split; congruence. +- destruct (intsize_eq i i0 && signedness_eq s s0); inv H3. + simpl; destruct i; split; congruence. +- destruct (signedness_eq s s0); inv H3. + simpl; split; congruence. +- destruct (floatsize_eq f f0); inv H3. + simpl; destruct f0; split; congruence. +- monadInv H3. simpl; split; congruence. +- contradiction. +- contradiction. +- destruct (ident_eq i i0); inv H3. simpl; split; congruence. +- destruct (ident_eq i i0); inv H3. simpl; split; congruence. +Qed. + +Lemma type_conditional_cast: + forall t1 t2 t, + type_conditional t1 t2 = OK t -> wt_cast t1 t /\ wt_cast t2 t. +Proof. + intros. + assert (A: forall x, match typeconv x with Tarray _ _ _ => False | Tfunction _ _ _ => False | _ => True end). + { destruct x; simpl; auto. destruct i; auto. } + assert (D: type_combine (typeconv t1) (typeconv t2) = OK t -> wt_cast t1 t /\ wt_cast t2 t). + { intros. apply type_combine_cast in H0. destruct H0; split; apply typeconv_cast; auto. + apply A. apply A. } + clear A. unfold type_conditional in H. destruct (typeconv t1) eqn:T1; try discriminate; - destruct (typeconv t2) eqn:T2; inv H. -- unfold wt_cast; simpl; split; congruence. -- eapply binarith_type_cast; eauto. -- eapply binarith_type_cast; eauto. + destruct (typeconv t2) eqn:T2; inv H; eauto using D, binarith_type_cast. - split; apply typeconv_cast; unfold wt_cast. rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. -- eapply binarith_type_cast; eauto. -- eapply binarith_type_cast; eauto. - split; apply typeconv_cast; unfold wt_cast. rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. - split; apply typeconv_cast; unfold wt_cast. rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. -- destruct (ident_eq i i0); inv H1. - split; apply typeconv_cast; unfold wt_cast. - rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. -- destruct (ident_eq i i0); inv H1. - split; apply typeconv_cast; unfold wt_cast. - rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. Qed. Section SOUNDNESS_CONSTRUCTORS. @@ -1025,7 +1140,7 @@ Lemma econdition_sound: forall r1 r2 r3 a, econdition r1 r2 r3 = OK a -> wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e r3 -> wt_expr ce e a. Proof. - intros. monadInv H. apply type_join_cast in EQ3. destruct EQ3. eauto 10 with ty. + intros. monadInv H. apply type_conditional_cast in EQ3. destruct EQ3. eauto 10 with ty. Qed. Lemma econdition'_sound: @@ -1206,6 +1321,38 @@ Proof. intros. monadInv H. constructor; simpl. eapply retype_stmt_sound; eauto. Qed. +Theorem typecheck_program_sound: + forall p p', typecheck_program p = OK p' -> wt_program p'. +Proof. + unfold typecheck_program; intros. monadInv H. + rename x into defs. + constructor; simpl. + set (ce := prog_comp_env p) in *. + set (e := bind_globdef (PTree.empty type) (prog_defs p)) in *. + set (e' := bind_globdef (PTree.empty type) defs) in *. + assert (MATCH: + list_forall2 (match_globdef (fun f tf => retype_fundef ce e f = OK tf) (fun v tv => tv = v)) (prog_defs p) defs). + { + revert EQ; generalize (prog_defs p) defs. + induction l as [ | [id gd] l ]; intros l'; simpl; intros. + inv EQ. constructor. + destruct gd as [f | v]. + destruct (retype_fundef ce e f) as [tf|msg] eqn:R; monadInv EQ. + constructor; auto. constructor; auto. + monadInv EQ. constructor; auto. destruct v; constructor; auto. } + assert (ENVS: e' = e). + { unfold e, e'. revert MATCH; generalize (prog_defs p) defs (PTree.empty type). + induction l as [ | [id gd] l ]; intros l' t M; inv M. + auto. inv H1; simpl; auto. replace (type_of_fundef f2) with (type_of_fundef f1); auto. + unfold retype_fundef in H4. destruct f1; monadInv H4; auto. monadInv EQ0; auto. + } + rewrite ENVS. + intros id f. revert MATCH; generalize (prog_defs p) defs. induction 1; simpl; intros. + contradiction. + destruct H0; auto. subst b1; inv H. destruct f1; simpl in H2. + monadInv H2. eapply retype_function_sound; eauto. congruence. +Qed. + (** * Subject reduction *) (** We show that reductions preserve well-typedness *) diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index e0fcb210..790877bd 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -358,8 +358,8 @@ Lemma sem_cast_match: forall v1 ty1 ty2 v2 v1' v2', sem_cast v1 ty1 ty2 = Some v2 -> do_cast v1' ty1 ty2 = OK v2' -> - val_inject inj v1' v1 -> - val_inject inj v2' v2. + Val.inject inj v1' v1 -> + Val.inject inj v2' v2. Proof. intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0. exploit sem_cast_inject. eexact E. eauto. @@ -369,7 +369,7 @@ Qed. Lemma bool_val_match: forall v ty b v' m, bool_val v ty Mem.empty = Some b -> - val_inject inj v v' -> + Val.inject inj v v' -> bool_val v' ty m = Some b. Proof. intros. eapply bool_val_inj; eauto. intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. @@ -382,13 +382,13 @@ Lemma constval_rvalue: eval_simple_rvalue empty_env m a v -> forall v', constval ge a = OK v' -> - val_inject inj v' v + Val.inject inj v' v with constval_lvalue: forall m a b ofs, eval_simple_lvalue empty_env m a b ofs -> forall v', constval ge a = OK v' -> - val_inject inj v' (Vptr b ofs). + Val.inject inj v' (Vptr b ofs). Proof. (* rvalue *) induction 1; intros vres CV; simpl in CV; try (monadInv CV). @@ -479,7 +479,7 @@ Theorem constval_steps: forall f r m v v' ty m', star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') -> constval ge r = OK v -> - m' = m /\ ty = typeof r /\ val_inject inj v v'. + m' = m /\ ty = typeof r /\ Val.inject inj v v'. Proof. intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. intros [A [B C]]. intuition. eapply constval_rvalue; eauto. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 39de282b..d890c820 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -123,7 +123,7 @@ let rec name_cdecl id ty = if not first then Buffer.add_string b ", "; Buffer.add_string b (name_cdecl "" t1); add_args false tl in - add_args true args; + if not cconv.cc_unproto then add_args true args; Buffer.add_char b ')'; name_cdecl (Buffer.contents b) res | Tstruct(name, a) -> @@ -299,9 +299,9 @@ and extended_asm p txt res args clob = begin match clob with | [] -> () | c1 :: cl -> - fprintf p "@ : @[<hov 0>%S" (extern_atom c1); + fprintf p "@ : @[<hov 0>%S" (camlstring_of_coqstring c1); List.iter - (fun c -> fprintf p ",@ %S" (extern_atom c)) + (fun c -> fprintf p ",@ %S" (camlstring_of_coqstring c)) cl; fprintf p "@]" end; diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 3364ec6a..2a50f985 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -107,7 +107,7 @@ Inductive match_var (f: meminj) (cenv: compilenv) (e: env) (m: mem) (te: env) (t (MODE: access_mode ty = By_value chunk) (LOAD: Mem.load chunk m b 0 = Some v) (TLENV: tle!(id) = Some tv) - (VINJ: val_inject f v tv), + (VINJ: Val.inject f v tv), match_var f cenv e m te tle id | match_var_not_lifted: forall b ty b' (ENV: e!id = Some(b, ty)) @@ -130,7 +130,7 @@ Record match_envs (f: meminj) (cenv: compilenv) me_temps: forall id v, le!id = Some v -> - (exists tv, tle!id = Some tv /\ val_inject f v tv) + (exists tv, tle!id = Some tv /\ Val.inject f v tv) /\ (VSet.mem id cenv = true -> v = Vundef); me_inj: forall id1 b1 ty1 id2 b2 ty2, e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2; @@ -327,7 +327,7 @@ Qed. Lemma val_casted_inject: forall f v v' ty, - val_inject f v v' -> val_casted v ty -> val_casted v' ty. + Val.inject f v v' -> val_casted v ty -> val_casted v' ty. Proof. intros. inv H; auto. inv H0; constructor. @@ -383,7 +383,7 @@ Lemma match_envs_assign_lifted: match_envs f cenv e le m lo hi te tle tlo thi -> e!id = Some(b, ty) -> val_casted v ty -> - val_inject f v tv -> + Val.inject f v tv -> assign_loc ge ty m b Int.zero v m' -> VSet.mem id cenv = true -> match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi. @@ -415,7 +415,7 @@ Qed. Lemma match_envs_set_temp: forall f cenv e le m lo hi te tle tlo thi id v tv x, match_envs f cenv e le m lo hi te tle tlo thi -> - val_inject f v tv -> + Val.inject f v tv -> check_temp cenv id = OK x -> match_envs f cenv e (PTree.set id v le) m lo hi te (PTree.set id tv tle) tlo thi. Proof. @@ -436,7 +436,7 @@ Qed. Lemma match_envs_set_opttemp: forall f cenv e le m lo hi te tle tlo thi optid v tv x, match_envs f cenv e le m lo hi te tle tlo thi -> - val_inject f v tv -> + Val.inject f v tv -> check_opttemp cenv optid = OK x -> match_envs f cenv e (set_opttemp optid v le) m lo hi te (set_opttemp optid tv tle) tlo thi. Proof. @@ -993,8 +993,8 @@ Qed. Lemma assign_loc_inject: forall f ty m loc ofs v m' tm loc' ofs' v', assign_loc ge ty m loc ofs v m' -> - val_inject f (Vptr loc ofs) (Vptr loc' ofs') -> - val_inject f v v' -> + Val.inject f (Vptr loc ofs) (Vptr loc' ofs') -> + Val.inject f v v' -> Mem.inject f m tm -> exists tm', assign_loc tge ty tm loc' ofs' v' tm' @@ -1095,7 +1095,7 @@ Theorem store_params_correct: forall s tm tle1 tle2 targs, list_norepet (var_names params) -> list_forall2 val_casted args (map snd params) -> - val_list_inject j args targs -> + Val.inject_list j args targs -> match_envs j cenv e le m lo hi te tle1 tlo thi -> Mem.inject j m tm -> (forall id, ~In id (var_names params) -> tle2!id = tle1!id) -> @@ -1388,8 +1388,8 @@ Qed. Lemma deref_loc_inject: forall ty loc ofs v loc' ofs', deref_loc ty m loc ofs v -> - val_inject f (Vptr loc ofs) (Vptr loc' ofs') -> - exists tv, deref_loc ty tm loc' ofs' tv /\ val_inject f v tv. + Val.inject f (Vptr loc ofs) (Vptr loc' ofs') -> + exists tv, deref_loc ty tm loc' ofs' tv /\ Val.inject f v tv. Proof. intros. inv H. (* by value *) @@ -1405,14 +1405,14 @@ Lemma eval_simpl_expr: forall a v, eval_expr ge e le m a v -> compat_cenv (addr_taken_expr a) cenv -> - exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ val_inject f v tv + exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ Val.inject f v tv with eval_simpl_lvalue: forall a b ofs, eval_lvalue ge e le m a b ofs -> compat_cenv (addr_taken_expr a) cenv -> match a with Evar id ty => VSet.mem id cenv = false | _ => True end -> - exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' /\ val_inject f (Vptr b ofs) (Vptr b' ofs'). + exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' /\ Val.inject f (Vptr b ofs) (Vptr b' ofs'). Proof. destruct 1; simpl; intros. @@ -1512,7 +1512,7 @@ Lemma eval_simpl_exprlist: val_casted_list vl tyl /\ exists tvl, eval_exprlist tge te tle tm (simpl_exprlist cenv al) tyl tvl - /\ val_list_inject f vl tvl. + /\ Val.inject_list f vl tvl. Proof. induction 1; simpl; intros. split. constructor. econstructor; split. constructor. auto. @@ -1729,7 +1729,7 @@ Lemma match_cont_find_funct: forall f cenv k tk m bound tbound vf fd tvf, match_cont f cenv k tk m bound tbound -> Genv.find_funct ge vf = Some fd -> - val_inject f vf tvf -> + Val.inject f vf tvf -> exists tfd, Genv.find_funct tge tvf = Some tfd /\ transf_fundef fd = OK tfd. Proof. intros. exploit match_cont_globalenv; eauto. intros [bound1 MG]. destruct MG. @@ -1761,7 +1761,7 @@ Inductive match_states: state -> state -> Prop := (TRFD: transf_fundef fd = OK tfd) (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm)) (MINJ: Mem.inject j m tm) - (AINJ: val_list_inject j vargs tvargs) + (AINJ: Val.inject_list j vargs tvargs) (FUNTY: type_of_fundef fd = Tfunction targs tres cconv) (ANORM: val_casted_list vargs targs), match_states (Callstate fd vargs k m) @@ -1770,7 +1770,7 @@ Inductive match_states: state -> state -> Prop := forall v k m tv tk tm j (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm)) (MINJ: Mem.inject j m tm) - (RINJ: val_inject j v tv), + (RINJ: Val.inject j v tv), match_states (Returnstate v k m) (Returnstate tv tk tm). @@ -2171,7 +2171,7 @@ Proof. eauto. eapply list_norepet_append_left; eauto. apply val_casted_list_params. unfold type_of_function in FUNTY. congruence. - apply val_list_inject_incr with j'; eauto. + apply val_inject_list_incr with j'; eauto. eexact B. eexact C. intros. apply (create_undef_temps_lifted id f). auto. intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto. diff --git a/common/AST.v b/common/AST.v index 2550844b..387eb6b2 100644 --- a/common/AST.v +++ b/common/AST.v @@ -100,12 +100,13 @@ These signatures are used in particular to determine appropriate calling conventions for the function. *) Record calling_convention : Type := mkcallconv { - cc_vararg: bool; - cc_structret: bool + cc_vararg: bool; (**r variable-arity function *) + cc_unproto: bool; (**r old-style unprototyped function *) + cc_structret: bool (**r function returning a struct *) }. Definition cc_default := - {| cc_vararg := false; cc_structret := false |}. + {| cc_vararg := false; cc_unproto := false; cc_structret := false |}. Record signature : Type := mksignature { sig_args: list typ; @@ -584,7 +585,7 @@ Inductive external_function : Type := (** Another form of annotation that takes one argument, produces an event carrying the text and the value of this argument, and returns the value of the argument. *) - | EF_inline_asm (text: ident) (sg: signature) (clobbers: list ident). + | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string). (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic @@ -642,7 +643,7 @@ Proof. generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros. decide equality. apply list_eq_dec. auto. - apply list_eq_dec. auto. + apply list_eq_dec. apply String.string_dec. Defined. Global Opaque external_function_eq. diff --git a/common/Determinism.v b/common/Determinism.v index d0099ba9..7ea19663 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -36,7 +36,7 @@ Require Import Behaviors. that this external call succeeds, has result [r], and changes the world to [w]. *) -Inductive world: Type := +CoInductive world: Type := World (io: ident -> list eventval -> option (eventval * world)) (vload: memory_chunk -> ident -> int -> option (eventval * world)) (vstore: memory_chunk -> ident -> int -> eventval -> option world). diff --git a/common/Events.v b/common/Events.v index 3bec15db..78162fff 100644 --- a/common/Events.v +++ b/common/Events.v @@ -453,7 +453,7 @@ Hypothesis symb_inj: symbols_inject. Lemma eventval_match_inject: forall ev ty v1 v2, - eventval_match ge1 ev ty v1 -> val_inject f v1 v2 -> eventval_match ge2 ev ty v2. + eventval_match ge1 ev ty v1 -> Val.inject f v1 v2 -> eventval_match ge2 ev ty v2. Proof. intros. inv H; inv H0; try constructor; auto. destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b3 [EQ FS]]. rewrite H4 in EQ; inv EQ. @@ -463,7 +463,7 @@ Qed. Lemma eventval_match_inject_2: forall ev ty v1, eventval_match ge1 ev ty v1 -> - exists v2, eventval_match ge2 ev ty v2 /\ val_inject f v1 v2. + exists v2, eventval_match ge2 ev ty v2 /\ Val.inject f v1 v2. Proof. intros. inv H; try (econstructor; split; eauto; constructor; fail). destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b2 [EQ FS]]. @@ -473,7 +473,7 @@ Qed. Lemma eventval_list_match_inject: forall evl tyl vl1, eventval_list_match ge1 evl tyl vl1 -> - forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match ge2 evl tyl vl2. + forall vl2, Val.inject_list f vl1 vl2 -> eventval_list_match ge2 evl tyl vl2. Proof. induction 1; intros. inv H; constructor. inv H1. constructor. eapply eventval_match_inject; eauto. eauto. @@ -669,10 +669,10 @@ Record extcall_properties (sem: extcall_sem) exists b2, f b1 = Some(b2, 0) /\ Senv.find_symbol ge2 id = Some b2) -> sem ge1 vargs m1 t vres m2 -> Mem.inject f m1 m1' -> - val_list_inject f vargs vargs' -> + Val.inject_list f vargs vargs' -> exists f', exists vres', exists m2', sem ge2 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' @@ -735,9 +735,9 @@ Lemma volatile_load_inject: forall ge1 ge2 f chunk m b ofs t v b' ofs' m', symbols_inject f ge1 ge2 -> volatile_load ge1 chunk m b ofs t v -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> Mem.inject f m m' -> - exists v', volatile_load ge2 chunk m' b' ofs' t v' /\ val_inject f v v'. + exists v', volatile_load ge2 chunk m' b' ofs' t v' /\ Val.inject f v v'. Proof. intros until m'; intros SI VL VI MI. generalize SI; intros (A & B & C & D). inv VL. @@ -747,7 +747,7 @@ Proof. rewrite Int.add_zero. exists (Val.load_result chunk v2); split. constructor; auto. erewrite D; eauto. - apply val_load_result_inject. auto. + apply Val.load_result_inject. auto. - (* normal load *) exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros (v2 & X & Y). exists v2; split; auto. @@ -852,7 +852,7 @@ Proof. (* inject *) inv H1. inv H3. exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). - assert (val_inject f (Vptr b ofs) (Vptr b2 ofs)). + assert (Val.inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. econstructor; eauto. @@ -934,8 +934,8 @@ Lemma volatile_store_inject: forall ge1 ge2 f chunk m1 b ofs v t m2 m1' b' ofs' v', symbols_inject f ge1 ge2 -> volatile_store ge1 chunk m1 b ofs v t m2 -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> - val_inject f v v' -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f v v' -> Mem.inject f m1 m1' -> exists m2', volatile_store ge2 chunk m1' b' ofs' v' t m2' @@ -950,7 +950,7 @@ Proof. inv AI. exploit Q; eauto. intros [A B]. subst delta. rewrite Int.add_zero. exists m1'; split. constructor; auto. erewrite S; eauto. - eapply eventval_match_inject; eauto. apply val_load_result_inject. auto. + eapply eventval_match_inject; eauto. apply Val.load_result_inject. auto. intuition auto with mem. - (* normal store *) inversion AI; subst. @@ -1058,7 +1058,7 @@ Proof. (* mem inject *) rewrite volatile_store_global_charact in H1. destruct H1 as [b [P Q]]. exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). - assert (val_inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto. + assert (Val.inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto. exploit ec_mem_inject. eapply volatile_store_ok. eauto. intuition. eexact Q. eauto. constructor. eauto. eauto. intros [f' [vres' [m2' [A [B [C [D [E G]]]]]]]]. exists f'; exists vres'; exists m2'; intuition. @@ -1552,10 +1552,10 @@ Lemma external_call_mem_inject: meminj_preserves_globals ge f -> external_call ef ge vargs m1 t vres m2 -> 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 ge 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' @@ -1644,11 +1644,11 @@ Proof. Qed. Lemma decode_longs_inject: - forall f tyl vl1 vl2, val_list_inject f vl1 vl2 -> val_list_inject f (decode_longs tyl vl1) (decode_longs tyl vl2). + forall f tyl vl1 vl2, Val.inject_list f vl1 vl2 -> Val.inject_list f (decode_longs tyl vl1) (decode_longs tyl vl2). Proof. induction tyl; simpl; intros. auto. - destruct a; inv H; auto. inv H1; auto. constructor; auto. apply val_longofwords_inject; auto. + destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_inject; auto. Qed. Lemma encode_long_lessdef: @@ -1659,10 +1659,10 @@ Proof. Qed. Lemma encode_long_inject: - forall f oty v1 v2, val_inject f v1 v2 -> val_list_inject f (encode_long oty v1) (encode_long oty v2). + forall f oty v1 v2, Val.inject f v1 v2 -> Val.inject_list f (encode_long oty v1) (encode_long oty v2). Proof. intros. destruct oty as [[]|]; simpl; auto. - constructor. apply val_hiword_inject; auto. constructor. apply val_loword_inject; auto. auto. + constructor. apply Val.hiword_inject; auto. constructor. apply Val.loword_inject; auto. auto. Qed. Lemma encode_long_has_type: @@ -1736,10 +1736,10 @@ Lemma external_call_mem_inject': meminj_preserves_globals ge f -> external_call' ef ge vargs m1 t vres m2 -> Mem.inject f m1 m1' -> - val_list_inject f vargs vargs' -> + Val.inject_list f vargs vargs' -> exists f' vres' m2', external_call' ef ge vargs' m1' t vres' m2' - /\ val_list_inject f' vres vres' + /\ Val.inject_list 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' diff --git a/common/Memdata.v b/common/Memdata.v index 96278a29..9c64563b 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -726,7 +726,7 @@ Inductive memval_inject (f: meminj): memval -> memval -> Prop := forall n, memval_inject f (Byte n) (Byte n) | memval_inject_frag: forall v1 v2 q n, - val_inject f v1 v2 -> + Val.inject f v1 v2 -> memval_inject f (Fragment v1 q n) (Fragment v2 q n) | memval_inject_undef: forall mv, memval_inject f Undef mv. @@ -738,7 +738,7 @@ Proof. Qed. (** [decode_val], applied to lists of memory values that are pairwise - related by [memval_inject], returns values that are related by [val_inject]. *) + related by [memval_inject], returns values that are related by [Val.inject]. *) Lemma proj_bytes_inject: forall f vl vl', @@ -759,7 +759,7 @@ Lemma check_value_inject: list_forall2 (memval_inject f) vl vl' -> forall v v' q n, check_value n v q vl = true -> - val_inject f v v' -> v <> Vundef -> + Val.inject f v v' -> v <> Vundef -> check_value n v' q vl' = true. Proof. induction 1; intros; destruct n; simpl in *; auto. @@ -774,7 +774,7 @@ Qed. Lemma proj_value_inject: forall f q vl1 vl2, list_forall2 (memval_inject f) vl1 vl2 -> - val_inject f (proj_value q vl1) (proj_value q vl2). + Val.inject f (proj_value q vl1) (proj_value q vl2). Proof. intros. unfold proj_value. inversion H; subst. auto. inversion H0; subst; auto. @@ -819,26 +819,26 @@ Qed. Theorem decode_val_inject: forall f vl1 vl2 chunk, list_forall2 (memval_inject f) vl1 vl2 -> - val_inject f (decode_val chunk vl1) (decode_val chunk vl2). + Val.inject f (decode_val chunk vl1) (decode_val chunk vl2). Proof. intros. unfold decode_val. destruct (proj_bytes vl1) as [bl1|] eqn:PB1. exploit proj_bytes_inject; eauto. intros PB2. rewrite PB2. destruct chunk; constructor. assert (A: forall q fn, - val_inject f (Val.load_result chunk (proj_value q vl1)) + Val.inject f (Val.load_result chunk (proj_value q vl1)) (match proj_bytes vl2 with | Some bl => fn bl | None => Val.load_result chunk (proj_value q vl2) end)). { intros. destruct (proj_bytes vl2) as [bl2|] eqn:PB2. rewrite proj_value_undef. destruct chunk; auto. eapply proj_bytes_not_inject; eauto. congruence. - apply val_load_result_inject. apply proj_value_inject; auto. + apply Val.load_result_inject. apply proj_value_inject; auto. } destruct chunk; auto. Qed. -(** Symmetrically, [encode_val], applied to values related by [val_inject], +(** Symmetrically, [encode_val], applied to values related by [Val.inject], returns lists of memory values that are pairwise related by [memval_inject]. *) @@ -870,7 +870,7 @@ Proof. Qed. Lemma inj_value_inject: - forall f v1 v2 q, val_inject f v1 v2 -> list_forall2 (memval_inject f) (inj_value q v1) (inj_value q v2). + forall f v1 v2 q, Val.inject f v1 v2 -> list_forall2 (memval_inject f) (inj_value q v1) (inj_value q v2). Proof. intros. Local Transparent inj_value. @@ -880,7 +880,7 @@ Qed. Theorem encode_val_inject: forall f v1 v2 chunk, - val_inject f v1 v2 -> + Val.inject f v1 v2 -> list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2). Proof. intros. inversion H; subst; simpl; destruct chunk; diff --git a/common/Memory.v b/common/Memory.v index 45c2497b..3d781cac 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -2303,7 +2303,7 @@ Lemma load_inj: mem_inj f m1 m2 -> load chunk m1 b1 ofs = Some v1 -> f b1 = Some (b2, delta) -> - exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2. + exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2. Proof. intros. exists (decode_val chunk (getN (size_chunk_nat chunk) (ofs + delta) (m2.(mem_contents)#b2))). @@ -2367,7 +2367,7 @@ Lemma store_mapped_inj: store chunk m1 b1 ofs v1 = Some n1 -> meminj_no_overlap f m1 -> f b1 = Some (b2, delta) -> - val_inject f v1 v2 -> + Val.inject f v1 v2 -> exists n2, store chunk m2 b2 (ofs + delta) v2 = Some n2 /\ mem_inj f n1 n2. @@ -3250,7 +3250,7 @@ Theorem valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> valid_pointer m1 b (Int.unsigned ofs) = true -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> valid_pointer m2 b' (Int.unsigned ofs') = true. Proof. intros. inv H1. @@ -3263,7 +3263,7 @@ Theorem weak_valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> weak_valid_pointer m1 b (Int.unsigned ofs) = true -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> weak_valid_pointer m2 b' (Int.unsigned ofs') = true. Proof. intros. inv H1. @@ -3376,7 +3376,7 @@ Theorem load_inject: inject f m1 m2 -> load chunk m1 b1 ofs = Some v1 -> f b1 = Some (b2, delta) -> - exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2. + exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2. Proof. intros. inv H. eapply load_inj; eauto. Qed. @@ -3385,8 +3385,8 @@ Theorem loadv_inject: forall f m1 m2 chunk a1 a2 v1, inject f m1 m2 -> loadv chunk m1 a1 = Some v1 -> - val_inject f a1 a2 -> - exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f v1 v2. + Val.inject f a1 a2 -> + exists v2, loadv chunk m2 a2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. inv H1; simpl in H0; try discriminate. exploit load_inject; eauto. intros [v2 [LOAD INJ]]. @@ -3414,7 +3414,7 @@ Theorem store_mapped_inject: inject f m1 m2 -> store chunk m1 b1 ofs v1 = Some n1 -> f b1 = Some (b2, delta) -> - val_inject f v1 v2 -> + Val.inject f v1 v2 -> exists n2, store chunk m2 b2 (ofs + delta) v2 = Some n2 /\ inject f n1 n2. @@ -3484,8 +3484,8 @@ Theorem storev_mapped_inject: forall f chunk m1 a1 v1 n1 m2 a2 v2, inject f m1 m2 -> storev chunk m1 a1 v1 = Some n1 -> - val_inject f a1 a2 -> - val_inject f v1 v2 -> + Val.inject f a1 a2 -> + Val.inject f v1 v2 -> exists n2, storev chunk m2 a2 v2 = Some n2 /\ inject f n1 n2. Proof. @@ -3977,14 +3977,14 @@ Qed. Lemma val_lessdef_inject_compose: forall f v1 v2 v3, - Val.lessdef v1 v2 -> val_inject f v2 v3 -> val_inject f v1 v3. + Val.lessdef v1 v2 -> Val.inject f v2 v3 -> Val.inject f v1 v3. Proof. intros. inv H. auto. auto. Qed. Lemma val_inject_lessdef_compose: forall f v1 v2 v3, - val_inject f v1 v2 -> Val.lessdef v2 v3 -> val_inject f v1 v3. + Val.inject f v1 v2 -> Val.lessdef v2 v3 -> Val.inject f v1 v3. Proof. intros. inv H0. auto. inv H. auto. Qed. @@ -4113,7 +4113,7 @@ Theorem store_inject_neutral: store chunk m b ofs v = Some m' -> inject_neutral thr m -> Plt b thr -> - val_inject (flat_inj thr) v v -> + Val.inject (flat_inj thr) v v -> inject_neutral thr m'. Proof. intros; red. diff --git a/common/Memtype.v b/common/Memtype.v index d94c895f..43fc708f 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -927,7 +927,7 @@ Axiom weak_valid_pointer_extends: - if [f b = Some(b', ofs)], the block [b] of [m2] corresponds to a sub-block at offset [ofs] of the block [b'] in [m2]. -A memory injection [f] defines a relation [val_inject] between values +A memory injection [f] defines a relation [Val.inject] between values that is the identity for integer and float values, and relocates pointer values as prescribed by [f]. (See module [Values].) @@ -1000,14 +1000,14 @@ Axiom valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> valid_pointer m1 b (Int.unsigned ofs) = true -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> valid_pointer m2 b' (Int.unsigned ofs') = true. Axiom weak_valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> weak_valid_pointer m1 b (Int.unsigned ofs) = true -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> weak_valid_pointer m2 b' (Int.unsigned ofs') = true. Axiom inject_no_overlap: @@ -1037,14 +1037,14 @@ Axiom load_inject: inject f m1 m2 -> load chunk m1 b1 ofs = Some v1 -> f b1 = Some (b2, delta) -> - exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2. + exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2. Axiom loadv_inject: forall f m1 m2 chunk a1 a2 v1, inject f m1 m2 -> loadv chunk m1 a1 = Some v1 -> - val_inject f a1 a2 -> - exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f v1 v2. + Val.inject f a1 a2 -> + exists v2, loadv chunk m2 a2 = Some v2 /\ Val.inject f v1 v2. Axiom loadbytes_inject: forall f m1 m2 b1 ofs len b2 delta bytes1, @@ -1059,7 +1059,7 @@ Axiom store_mapped_inject: inject f m1 m2 -> store chunk m1 b1 ofs v1 = Some n1 -> f b1 = Some (b2, delta) -> - val_inject f v1 v2 -> + Val.inject f v1 v2 -> exists n2, store chunk m2 b2 (ofs + delta) v2 = Some n2 /\ inject f n1 n2. @@ -1085,8 +1085,8 @@ Axiom storev_mapped_inject: forall f chunk m1 a1 v1 n1 m2 a2 v2, inject f m1 m2 -> storev chunk m1 a1 v1 = Some n1 -> - val_inject f a1 a2 -> - val_inject f v1 v2 -> + Val.inject f a1 a2 -> + Val.inject f v1 v2 -> exists n2, storev chunk m2 a2 v2 = Some n2 /\ inject f n1 n2. @@ -1221,7 +1221,7 @@ Axiom store_inject_neutral: store chunk m b ofs v = Some m' -> inject_neutral thr m -> Plt b thr -> - val_inject (flat_inj thr) v v -> + Val.inject (flat_inj thr) v v -> inject_neutral thr m'. Axiom drop_inject_neutral: diff --git a/common/Values.v b/common/Values.v index 12b380b7..8877f9a7 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1477,8 +1477,6 @@ Proof. intros. inv H; auto. Qed. -End Val. - (** * Values and memory injections *) (** A memory injection [f] is a function from addresses to either [None] @@ -1496,62 +1494,62 @@ Definition meminj : Type := block -> option (block * Z). as prescribed by the memory injection. Moreover, [Vundef] values inject into any other value. *) -Inductive val_inject (mi: meminj): val -> val -> Prop := - | val_inject_int: - forall i, val_inject mi (Vint i) (Vint i) - | val_inject_long: - forall i, val_inject mi (Vlong i) (Vlong i) - | val_inject_float: - forall f, val_inject mi (Vfloat f) (Vfloat f) - | val_inject_single: - forall f, val_inject mi (Vsingle f) (Vsingle f) - | val_inject_ptr: +Inductive inject (mi: meminj): val -> val -> Prop := + | inject_int: + forall i, inject mi (Vint i) (Vint i) + | inject_long: + forall i, inject mi (Vlong i) (Vlong i) + | inject_float: + forall f, inject mi (Vfloat f) (Vfloat f) + | inject_single: + forall f, inject mi (Vsingle f) (Vsingle f) + | inject_ptr: forall b1 ofs1 b2 ofs2 delta, mi b1 = Some (b2, delta) -> ofs2 = Int.add ofs1 (Int.repr delta) -> - val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2) + inject mi (Vptr b1 ofs1) (Vptr b2 ofs2) | val_inject_undef: forall v, - val_inject mi Vundef v. + inject mi Vundef v. -Hint Constructors val_inject. +Hint Constructors inject. -Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:= - | val_nil_inject : - val_list_inject mi nil nil - | val_cons_inject : forall v v' vl vl' , - val_inject mi v v' -> val_list_inject mi vl vl'-> - val_list_inject mi (v :: vl) (v' :: vl'). +Inductive inject_list (mi: meminj): list val -> list val-> Prop:= + | inject_list_nil : + inject_list mi nil nil + | inject_list_cons : forall v v' vl vl' , + inject mi v v' -> inject_list mi vl vl'-> + inject_list mi (v :: vl) (v' :: vl'). -Hint Resolve val_nil_inject val_cons_inject. +Hint Resolve inject_list_nil inject_list_cons. Section VAL_INJ_OPS. Variable f: meminj. -Lemma val_load_result_inject: +Lemma load_result_inject: forall chunk v1 v2, - val_inject f v1 v2 -> - val_inject f (Val.load_result chunk v1) (Val.load_result chunk v2). + inject f v1 v2 -> + inject f (Val.load_result chunk v1) (Val.load_result chunk v2). Proof. intros. inv H; destruct chunk; simpl; econstructor; eauto. Qed. -Remark val_add_inject: +Remark add_inject: forall v1 v1' v2 v2', - val_inject f v1 v1' -> - val_inject f v2 v2' -> - val_inject f (Val.add v1 v2) (Val.add v1' v2'). + inject f v1 v1' -> + inject f v2 v2' -> + inject f (Val.add v1 v2) (Val.add v1' v2'). Proof. intros. inv H; inv H0; simpl; econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. Qed. -Remark val_sub_inject: +Remark sub_inject: forall v1 v1' v2 v2', - val_inject f v1 v1' -> - val_inject f v2 v2' -> - val_inject f (Val.sub v1 v2) (Val.sub v1' v2'). + inject f v1 v1' -> + inject f v2 v2' -> + inject f (Val.sub v1 v2) (Val.sub v1' v2'). Proof. intros. inv H; inv H0; simpl; auto. econstructor; eauto. rewrite Int.sub_add_l. auto. @@ -1559,10 +1557,10 @@ Proof. rewrite Int.sub_shifted. auto. Qed. -Lemma val_cmp_bool_inject: +Lemma cmp_bool_inject: forall c v1 v2 v1' v2' b, - val_inject f v1 v1' -> - val_inject f v2 v2' -> + inject f v1 v1' -> + inject f v2 v2' -> Val.cmp_bool c v1 v2 = Some b -> Val.cmp_bool c v1' v2' = Some b. Proof. @@ -1602,10 +1600,10 @@ Hypothesis valid_different_ptrs_inj: b1' <> b2' \/ Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). -Lemma val_cmpu_bool_inject: +Lemma cmpu_bool_inject: forall c v1 v2 v1' v2' b, - val_inject f v1 v1' -> - val_inject f v2 v2' -> + inject f v1 v1' -> + inject f v2 v2' -> Val.cmpu_bool valid_ptr1 c v1 v2 = Some b -> Val.cmpu_bool valid_ptr2 c v1' v2' = Some b. Proof. @@ -1644,27 +1642,31 @@ Proof. now erewrite !valid_ptr_inj by eauto. Qed. -Lemma val_longofwords_inject: +Lemma longofwords_inject: forall v1 v2 v1' v2', - val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.longofwords v1 v2) (Val.longofwords v1' v2'). + inject f v1 v1' -> inject f v2 v2' -> inject f (Val.longofwords v1 v2) (Val.longofwords v1' v2'). Proof. intros. unfold Val.longofwords. inv H; auto. inv H0; auto. Qed. -Lemma val_loword_inject: - forall v v', val_inject f v v' -> val_inject f (Val.loword v) (Val.loword v'). +Lemma loword_inject: + forall v v', inject f v v' -> inject f (Val.loword v) (Val.loword v'). Proof. intros. unfold Val.loword; inv H; auto. Qed. -Lemma val_hiword_inject: - forall v v', val_inject f v v' -> val_inject f (Val.hiword v) (Val.hiword v'). +Lemma hiword_inject: + forall v v', inject f v v' -> inject f (Val.hiword v) (Val.hiword v'). Proof. intros. unfold Val.hiword; inv H; auto. Qed. End VAL_INJ_OPS. +End Val. + +Notation meminj := Val.meminj. + (** Monotone evolution of a memory injection. *) Definition inject_incr (f1 f2: meminj) : Prop := @@ -1684,33 +1686,33 @@ Qed. Lemma val_inject_incr: forall f1 f2 v v', inject_incr f1 f2 -> - val_inject f1 v v' -> - val_inject f2 v v'. + Val.inject f1 v v' -> + Val.inject f2 v v'. Proof. intros. inv H0; eauto. Qed. -Lemma val_list_inject_incr: +Lemma val_inject_list_incr: forall f1 f2 vl vl' , - inject_incr f1 f2 -> val_list_inject f1 vl vl' -> - val_list_inject f2 vl vl'. + inject_incr f1 f2 -> Val.inject_list f1 vl vl' -> + Val.inject_list f2 vl vl'. Proof. induction vl; intros; inv H0. auto. constructor. eapply val_inject_incr; eauto. auto. Qed. -Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr. +Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr. Lemma val_inject_lessdef: - forall v1 v2, Val.lessdef v1 v2 <-> val_inject (fun b => Some(b, 0)) v1 v2. + forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2. Proof. intros; split; intros. inv H; auto. destruct v2; econstructor; eauto. rewrite Int.add_zero; auto. inv H; auto. inv H0. rewrite Int.add_zero; auto. Qed. -Lemma val_list_inject_lessdef: - forall vl1 vl2, Val.lessdef_list vl1 vl2 <-> val_list_inject (fun b => Some(b, 0)) vl1 vl2. +Lemma val_inject_list_lessdef: + forall vl1 vl2, Val.lessdef_list vl1 vl2 <-> Val.inject_list (fun b => Some(b, 0)) vl1 vl2. Proof. intros; split. induction 1; constructor; auto. apply val_inject_lessdef; auto. @@ -1723,7 +1725,7 @@ Definition inject_id : meminj := fun b => Some(b, 0). Lemma val_inject_id: forall v1 v2, - val_inject inject_id v1 v2 <-> Val.lessdef v1 v2. + Val.inject inject_id v1 v2 <-> Val.lessdef v1 v2. Proof. intros; split; intros. inv H; auto. @@ -1747,8 +1749,8 @@ Definition compose_meminj (f f': meminj) : meminj := Lemma val_inject_compose: forall f f' v1 v2 v3, - val_inject f v1 v2 -> val_inject f' v2 v3 -> - val_inject (compose_meminj f f') v1 v3. + Val.inject f v1 v2 -> Val.inject f' v2 v3 -> + Val.inject (compose_meminj f f') v1 v3. Proof. intros. inv H; auto; inv H0; auto. econstructor. unfold compose_meminj; rewrite H1; rewrite H3; eauto. diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 99b93c25..570572fa 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -15,8 +15,7 @@ (* Elimination of bit fields in structs *) -(* Assumes: unblocked code. - Preserves: unblocked code. *) +(* Assumes: nothing. *) open Printf open Machine @@ -46,6 +45,10 @@ type bitfield_info = let bitfield_table = (Hashtbl.create 57: (ident * string, bitfield_info) Hashtbl.t) +let is_bitfield structid fieldname = + try Some (Hashtbl.find bitfield_table (structid, fieldname)) + with Not_found -> None + (* Signedness issues *) let unsigned_ikind_for_carrier nbits = @@ -218,6 +221,78 @@ let bitfield_assign env bf carrier newval = and oldval_masked = ebinint env Oand carrier notmsk in ebinint env Oor oldval_masked newval_masked +(* Initialize a bitfield *) + +(* Reference C code: + +unsigned int bitfield_init(int ofs, int sz, unsigned int y) +{ + unsigned int mask = (1U << sz) - 1; + return (y & mask) << ofs; +} +*) + +let bitfield_initializer bf i = + match i with + | Init_single e -> + let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in + let e_mask = + {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); + etyp = TInt(IUInt, [])} in + let e_and = + {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[])); + etyp = TInt(IUInt,[])} in + {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt, + TInt(IUInt, [])); + etyp = TInt(IUInt, [])} + | _ -> + assert false + +(* Associate to the left so that it prints more nicely *) + +let or_expr_list = function + | [] -> intconst 0L IUInt + | [e] -> e + | e1 :: el -> + List.fold_left + (fun accu e -> + {edesc = EBinop(Oor, accu, e, TInt(IUInt,[])); + etyp = TInt(IUInt,[])}) + e1 el + +(* Initialize the carrier for consecutive bitfields *) + +let rec pack_bitfield_init id carrier fld_init_list = + match fld_init_list with + | [] -> ([], []) + | (fld, i) :: rem -> + match is_bitfield id fld.fld_name with + | None -> + ([], fld_init_list) + | Some bf -> + if bf.bf_carrier <> carrier then + ([], fld_init_list) + else begin + let (el, rem') = pack_bitfield_init id carrier rem in + (bitfield_initializer bf i :: el, rem') + end + +let rec transf_struct_init id fld_init_list = + match fld_init_list with + | [] -> [] + | (fld, i) :: rem -> + match is_bitfield id fld.fld_name with + | None -> + (fld, i) :: transf_struct_init id rem + | Some bf -> + let (el, rem') = + pack_bitfield_init id bf.bf_carrier fld_init_list in + ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ; + fld_bitfield = None}, + Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el); + etyp = bf.bf_carrier_typ}) + :: transf_struct_init id rem' + (* Check whether a field access (e.f or e->f) is a bitfield access. If so, return carrier expression (e and *e, respectively) and bitfield_info *) @@ -246,194 +321,134 @@ let rec is_bitfield_access env e = (* Expressions *) -let transf_expr env ctx e = - - let rec texp ctx e = - match e.edesc with - | EConst _ -> e - | ESizeof _ -> e - | EAlignof _ -> e - | EVar _ -> e - - | EUnop(Odot s, e1) -> - begin match is_bitfield_access env e with - | None -> - {edesc = EUnop(Odot s, texp Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_read ex bf - end - | EUnop(Oarrow s, e1) -> - begin match is_bitfield_access env e with - | None -> - {edesc = EUnop(Oarrow s, texp Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_read ex bf - end - | EUnop((Opreincr|Opredecr) as op, e1) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EUnop(op, texp Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_pre ctx (op_for_incr_decr op) ex bf e1.etyp - end - | EUnop((Opostincr|Opostdecr) as op, e1) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EUnop(op, texp Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_post ctx (op_for_incr_decr op) ex bf e1.etyp - end - | EUnop(op, e1) -> - {edesc = EUnop(op, texp Val e1); etyp = e.etyp} - - | EBinop(Oassign, e1, e2, ty) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EBinop(Oassign, texp Val e1, texp Val e2, ty); - etyp = e.etyp} - | Some(ex, bf) -> - transf_assign ctx ex bf e2 +let rec transf_exp env ctx e = + match e.edesc with + | EConst _ -> e + | ESizeof _ -> e + | EAlignof _ -> e + | EVar _ -> e + + | EUnop(Odot s, e1) -> + begin match is_bitfield_access env e with + | None -> + {edesc = EUnop(Odot s, transf_exp env Val e1); etyp = e.etyp} + | Some(ex, bf) -> + transf_read env ex bf + end + | EUnop(Oarrow s, e1) -> + begin match is_bitfield_access env e with + | None -> + {edesc = EUnop(Oarrow s, transf_exp env Val e1); etyp = e.etyp} + | Some(ex, bf) -> + transf_read env ex bf end - | EBinop((Oadd_assign|Osub_assign|Omul_assign|Odiv_assign - |Omod_assign|Oand_assign|Oor_assign|Oxor_assign - |Oshl_assign|Oshr_assign) as op, - e1, e2, ty) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EBinop(op, texp Val e1, texp Val e2, ty); etyp = e.etyp} - | Some(ex, bf) -> - transf_assignop ctx (op_for_assignop op) ex bf e2 ty + | EUnop((Opreincr|Opredecr) as op, e1) -> + begin match is_bitfield_access env e1 with + | None -> + {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp} + | Some(ex, bf) -> + transf_pre env ctx (op_for_incr_decr op) ex bf e1.etyp end - | EBinop(Ocomma, e1, e2, ty) -> - {edesc = EBinop(Ocomma, texp Effects e1, texp Val e2, ty); - etyp = e.etyp} - | EBinop(op, e1, e2, ty) -> - {edesc = EBinop(op, texp Val e1, texp Val e2, ty); etyp = e.etyp} - - | EConditional(e1, e2, e3) -> - {edesc = EConditional(texp Val e1, texp ctx e2, texp ctx e3); - etyp = e.etyp} - | ECast(ty, e1) -> - {edesc = ECast(ty, texp Val e1); etyp = e.etyp} - | ECompound _ -> - assert false (* does not occur in unblocked code *) - | ECall(e1, el) -> - {edesc = ECall(texp Val e1, List.map (texp Val) el); etyp = e.etyp} - - and transf_read e bf = - bitfield_extract env bf - {edesc = EUnop(Odot bf.bf_carrier, texp Val e); etyp = bf.bf_carrier_typ} - - and transf_assign ctx e1 bf e2 = - bind_lvalue env (texp Val e1) (fun base -> - let carrier = - {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in - let asg = - eassign carrier (bitfield_assign env bf carrier (texp Val e2)) in - if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) - - and transf_assignop ctx op e1 bf e2 tyres = - bind_lvalue env (texp Val e1) (fun base -> + | EUnop((Opostincr|Opostdecr) as op, e1) -> + begin match is_bitfield_access env e1 with + | None -> + {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp} + | Some(ex, bf) -> + transf_post env ctx (op_for_incr_decr op) ex bf e1.etyp + end + | EUnop(op, e1) -> + {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp} + + | EBinop(Oassign, e1, e2, ty) -> + begin match is_bitfield_access env e1 with + | None -> + {edesc = EBinop(Oassign, transf_exp env Val e1, + transf_exp env Val e2, ty); + etyp = e.etyp} + | Some(ex, bf) -> + transf_assign env ctx ex bf e2 + end + | EBinop((Oadd_assign|Osub_assign|Omul_assign|Odiv_assign + |Omod_assign|Oand_assign|Oor_assign|Oxor_assign + |Oshl_assign|Oshr_assign) as op, + e1, e2, ty) -> + begin match is_bitfield_access env e1 with + | None -> + {edesc = EBinop(op, transf_exp env Val e1, + transf_exp env Val e2, ty); etyp = e.etyp} + | Some(ex, bf) -> + transf_assignop env ctx (op_for_assignop op) ex bf e2 ty + end + | EBinop(Ocomma, e1, e2, ty) -> + {edesc = EBinop(Ocomma, transf_exp env Effects e1, + transf_exp env Val e2, ty); + etyp = e.etyp} + | EBinop(op, e1, e2, ty) -> + {edesc = EBinop(op, transf_exp env Val e1, transf_exp env Val e2, ty); + etyp = e.etyp} + + | EConditional(e1, e2, e3) -> + {edesc = EConditional(transf_exp env Val e1, + transf_exp env ctx e2, transf_exp env ctx e3); + etyp = e.etyp} + | ECast(ty, e1) -> + {edesc = ECast(ty, transf_exp env Val e1); etyp = e.etyp} + | ECompound(ty, i) -> + {edesc = ECompound(ty, transf_init env i); etyp = e.etyp} + | ECall(e1, el) -> + {edesc = ECall(transf_exp env Val e1, List.map (transf_exp env Val) el); + etyp = e.etyp} + +and transf_read env e bf = + bitfield_extract env bf + {edesc = EUnop(Odot bf.bf_carrier, transf_exp env Val e); + etyp = bf.bf_carrier_typ} + +and transf_assign env ctx e1 bf e2 = + bind_lvalue env (transf_exp env Val e1) (fun base -> + let carrier = + {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in + let asg = + eassign carrier (bitfield_assign env bf carrier (transf_exp env Val e2)) in + if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) + +and transf_assignop env ctx op e1 bf e2 tyres = + bind_lvalue env (transf_exp env Val e1) (fun base -> + let carrier = + {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in + let rhs = + {edesc = EBinop(op, bitfield_extract env bf carrier, transf_exp env Val e2, tyres); + etyp = tyres} in + let asg = + eassign carrier (bitfield_assign env bf carrier rhs) in + if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) + +and transf_pre env ctx op e1 bf tyfield = + transf_assignop env ctx op e1 bf (intconst 1L IInt) + (unary_conversion env tyfield) + +and transf_post env ctx op e1 bf tyfield = + if ctx = Effects then + transf_pre env ctx op e1 bf tyfield + else begin + bind_lvalue env (transf_exp env Val e1) (fun base -> let carrier = {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in + let temp = mk_temp env tyfield in + let tyres = unary_conversion env tyfield in + let settemp = eassign temp (bitfield_extract env bf carrier) in let rhs = - {edesc = EBinop(op, bitfield_extract env bf carrier, texp Val e2, tyres); - etyp = tyres} in + {edesc = EBinop(op, temp, intconst 1L IInt, tyres); etyp = tyres} in let asg = eassign carrier (bitfield_assign env bf carrier rhs) in - if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) - - and transf_pre ctx op e1 bf tyfield = - transf_assignop ctx op e1 bf (intconst 1L IInt) - (unary_conversion env tyfield) - - and transf_post ctx op e1 bf tyfield = - if ctx = Effects then - transf_pre ctx op e1 bf tyfield - else begin - bind_lvalue env (texp Val e1) (fun base -> - let carrier = - {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in - let temp = mk_temp env tyfield in - let tyres = unary_conversion env tyfield in - let settemp = eassign temp (bitfield_extract env bf carrier) in - let rhs = - {edesc = EBinop(op, temp, intconst 1L IInt, tyres); etyp = tyres} in - let asg = - eassign carrier (bitfield_assign env bf carrier rhs) in - ecomma (ecomma settemp asg) temp) - end - - in texp ctx e - -(* Statements *) - -let transf_stmt env s = - Transform.stmt (fun loc env ctx e -> transf_expr env ctx e) env s - -(* Functions *) - -let transf_fundef env f = - Transform.fundef transf_stmt env f + ecomma (ecomma settemp asg) temp) + end (* Initializers *) -let bitfield_initializer bf i = - match i with - | Init_single e -> - let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in - let e_mask = - {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); - etyp = TInt(IUInt, [])} in - let e_and = - {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[])); - etyp = TInt(IUInt,[])} in - {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt, - TInt(IUInt, [])); - etyp = TInt(IUInt, [])} - | _ -> assert false - -let rec pack_bitfield_init id carrier fld_init_list = - match fld_init_list with - | [] -> ([], []) - | (fld, i) :: rem -> - try - let bf = Hashtbl.find bitfield_table (id, fld.fld_name) in - if bf.bf_carrier <> carrier then - ([], fld_init_list) - else begin - let (el, rem') = pack_bitfield_init id carrier rem in - (bitfield_initializer bf i :: el, rem') - end - with Not_found -> - ([], fld_init_list) - -let rec or_expr_list = function - | [] -> assert false - | [e] -> e - | e1 :: el -> - {edesc = EBinop(Oor, e1, or_expr_list el, TInt(IUInt,[])); - etyp = TInt(IUInt,[])} - -let rec transf_struct_init id fld_init_list = - match fld_init_list with - | [] -> [] - | (fld, i) :: rem -> - try - let bf = Hashtbl.find bitfield_table (id, fld.fld_name) in - let (el, rem') = - pack_bitfield_init id bf.bf_carrier fld_init_list in - ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ; - fld_bitfield = None}, - Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el); - etyp = bf.bf_carrier_typ}) - :: transf_struct_init id rem' - with Not_found -> - (fld, i) :: transf_struct_init id rem - -let rec transf_init env i = +and transf_init env i = match i with - | Init_single e -> Init_single (transf_expr env Val e) + | Init_single e -> Init_single (transf_exp env Val e) | Init_array il -> Init_array (List.map (transf_init env) il) | Init_struct(id, fld_init_list) -> let fld_init_list' = @@ -441,10 +456,25 @@ let rec transf_init env i = Init_struct(id, transf_struct_init id fld_init_list') | Init_union(id, fld, i) -> Init_union(id, fld, transf_init env i) +(* Declarations *) + let transf_decl env (sto, id, ty, init_opt) = (sto, id, ty, match init_opt with None -> None | Some i -> Some(transf_init env i)) +(* Statements *) + +let transf_stmt env s = + Transform.stmt + ~expr:(fun loc env ctx e -> transf_exp env ctx e) + ~decl:transf_decl + env s + +(* Functions *) + +let transf_fundef env f = + Transform.fundef transf_stmt env f + (* Programs *) let program p = diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 4d6d2137..221bd7cc 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -574,6 +574,19 @@ let is_function_type env t = | TFun _ -> true | _ -> false +(* Find the info for a field access *) + +let field_of_dot_access env t m = + match unroll env t with + | TStruct(id, _) -> Env.find_struct_member env (id, m) + | TUnion(id, _) -> Env.find_union_member env (id, m) + | _ -> assert false + +let field_of_arrow_access env t m = + match unroll env t with + | TPtr(t, _) | TArray(t, _, _) -> field_of_dot_access env t m + | _ -> assert false + (* Ranking of integer kinds *) let integer_rank = function @@ -964,8 +977,7 @@ let rec subst_stmt phi s = | Sskip | Sbreak | Scontinue - | Sgoto _ - | Sasm _ -> s.sdesc + | Sgoto _ -> s.sdesc | Sdo e -> Sdo (subst_expr phi e) | Sseq(s1, s2) -> Sseq (subst_stmt phi s1, subst_stmt phi s2) | Sif(e, s1, s2) -> @@ -981,6 +993,13 @@ let rec subst_stmt phi s = | Sreturn (Some e) -> Sreturn (Some (subst_expr phi e)) | Sblock sl -> Sblock (List.map (subst_stmt phi) sl) | Sdecl d -> Sdecl (subst_decl phi d) + | Sasm(attr, template, outputs, inputs, clob) -> + let subst_asm_operand (lbl, cstr, e) = + (lbl, cstr, subst_expr phi e) in + Sasm(attr, template, + List.map subst_asm_operand outputs, + List.map subst_asm_operand inputs, + clob) } diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 9d41f8fa..b1f77944 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -195,6 +195,10 @@ val fundef_typ: fundef -> typ val int_representable: int64 -> int -> bool -> bool (* Is the given int64 representable with the given number of bits and signedness? *) +val field_of_dot_access: Env.t -> typ -> string -> field + (* Return the field info for a [x.field] access *) +val field_of_arrow_access: Env.t -> typ -> string -> field + (* Return the field info for a [x->field] access *) (* Constructors *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index a1dd552b..bcf90f5e 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -365,6 +365,14 @@ let typespec_rank = function (* Don't change this *) let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2) +(* Is a specifier an anonymous struct/union in the sense of ISO C2011? *) + +let is_anonymous_composite spec = + List.exists + (function SpecType(Tstruct_union(_, None, Some _, _)) -> true + | _ -> false) + spec + (* Elaboration of a type specifier. Returns 5-tuple: (storage class, "inline" flag, "typedef" flag, elaborated type, new env) Optional argument "only" is true if this is a standalone @@ -617,6 +625,7 @@ and elab_init_name_group loc env (spec, namelist) = (* Elaboration of a field group *) and elab_field_group env (Field_group (spec, fieldlist, loc)) = + let fieldlist = List.map ( function | (None, x) -> (Name ("", JUSTBASE, [], cabslu), x) @@ -629,6 +638,11 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) = if sto <> Storage_default then error loc "non-default storage in struct or union"; + if fieldlist = [] then + if is_anonymous_composite spec then + error loc "ISO C99 does not support anonymous structs/unions" + else + warning loc "declaration does not declare any members"; let elab_bitfield (Name (_, _, _, loc), optbitsize) (id, ty) = let optbitsize' = @@ -764,7 +778,9 @@ and elab_enum_item env ((s, exp), loc) nextval = "value of enumerator '%s' is not a compile-time constant" s; (nextval, Some exp') in if redef Env.lookup_ident env s then - error loc "redefinition of enumerator '%s'" s; + error loc "redefinition of identifier '%s'" s; + if redef Env.lookup_typedef env s then + error loc "redefinition of typedef '%s' as different kind of symbol" s; if not (int_representable v (8 * sizeof_ikind enum_ikind) (is_signed_ikind enum_ikind)) then warning loc "the value of '%s' is not representable with type %a" s Cprint.typ (TInt(enum_ikind, [])); @@ -1406,6 +1422,23 @@ let elab_expr loc env a = let b1 = elab a1 in if not (is_lvalue b1 || is_function_type env b1.etyp) then err "argument of '&' is not an l-value"; + begin match b1.edesc with + | EVar id -> + begin match wrap Env.find_ident loc env id with + | Env.II_ident(Storage_register, _) -> + err "address of register variable '%s' requested" id.name + | _ -> () + end + | EUnop(Odot f, b2) -> + let fld = wrap2 field_of_dot_access loc env b2.etyp f in + if fld.fld_bitfield <> None then + err "address of bit-field '%s' requested" f + | EUnop(Oarrow f, b2) -> + let fld = wrap2 field_of_arrow_access loc env b2.etyp f in + if fld.fld_bitfield <> None then + err "address of bit-field '%s' requested" f + | _ -> () + end; { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.etyp, []) } | UNARY(MEMOF, a1) -> @@ -1753,11 +1786,15 @@ let enter_typedefs loc env sto dl = error loc "initializer in typedef"; if redef Env.lookup_typedef env s then error loc "redefinition of typedef '%s'" s; + if redef Env.lookup_ident env s then + error loc "redefinition of identifier '%s' as different kind of symbol" s; let (id, env') = Env.enter_typedef env s ty in emit_elab loc (Gtypedef(id, ty)); env') env dl let enter_or_refine_ident local loc env s sto ty = + if redef Env.lookup_typedef env s then + error loc "redefinition of typedef '%s' as different kind of symbol" s; match previous_def Env.lookup_ident env s with | Some(id, II_ident(old_sto, old_ty)) when sto = Storage_extern || Env.in_current_scope env id -> @@ -1770,15 +1807,23 @@ let enter_or_refine_ident local loc env s sto ty = | None -> warning loc "redefinition of '%s' with incompatible type" s; ty in let new_sto = - if old_sto = Storage_extern then sto else - if sto = Storage_extern then old_sto else - if old_sto = sto then sto else begin - warning loc "redefinition of '%s' with incompatible storage class" s; - sto - end in + (* The only case not allowed is removing static *) + match old_sto,sto with + | Storage_static,Storage_static + | Storage_extern,Storage_extern + | Storage_register,Storage_register + | Storage_default,Storage_default -> sto + | _,Storage_static -> + error loc "static redefinition of '%s' after non-static definition" s; sto + | Storage_static,_ -> Storage_static (* Static stays static *) + | Storage_extern,_ -> sto + | _,Storage_extern -> old_sto + | _,Storage_register + | Storage_register,_ -> Storage_register + in (id, new_sto, Env.add_ident env id new_sto new_ty) | Some(id, II_enum v) when Env.in_current_scope env id -> - error loc "illegal redefinition of enumerator '%s'" s; + error loc "redefinition of enumerator '%s'" s; (id, sto, Env.add_ident env id sto ty) | _ -> let (id, env') = Env.enter_ident env s sto ty in (id, sto, env') @@ -1823,7 +1868,7 @@ let enter_decdefs local loc env sto dl = let elab_fundef env spec name body loc = let (s, sto, inline, ty, env1) = elab_name env spec name in if sto = Storage_register then - error loc "a function definition cannot have 'register' storage class"; + fatal_error loc "a function definition cannot have 'register' storage class"; (* Fix up the type. We can have params = None but only for an old-style parameterless function "int f() {...}" *) let ty = diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index 94d23102..fbf8d569 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -161,9 +161,10 @@ let transf_outputs loc env = function let check_clobbers loc clob = List.iter (fun c -> - if Machregsaux.register_by_name c <> None - || List.mem c Machregsaux.scratch_register_names - || c = "memory" || c = "cc" + let c' = String.uppercase c in + if Machregsaux.register_by_name c' <> None + || List.mem c' Machregsaux.scratch_register_names + || c' = "MEMORY" || c' = "CC" then () else error "%aError: unrecognized asm register clobber '%s'" formatloc loc c) diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index 1f602fc1..ca6c9da5 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -317,7 +317,7 @@ let transf_expr loc env ctx e = (* Statements *) let transf_stmt env s = - Transform.stmt transf_expr env s + Transform.stmt ~expr:transf_expr env s (* Functions *) diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 645465c3..317847a7 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -21,8 +21,8 @@ let transform_program t p name = let run_pass pass flag p = if CharSet.mem flag t then pass p else p in let p1 = (run_pass StructReturn.program 's' (run_pass PackedStructs.program 'p' - (run_pass Bitfields.program 'f' (run_pass Unblock.program 'b' + (run_pass Bitfields.program 'f' p)))) in let debug = if !Clflags.option_g && Configuration.advanced_debug then diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index 8bfc6954..660f1d9b 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -423,6 +423,7 @@ let transf_decl env (sto, id, ty, init) = let transf_funbody env body optres = let transf_expr ctx e = transf_expr env ctx e in +let transf_asm_operand (lbl, cstr, e) = (lbl, cstr, transf_expr Val e) in (* Function returns: return kind scalar -> return e @@ -484,7 +485,10 @@ let rec transf_stmt s = {s with sdesc = Sblock(List.map transf_stmt sl)} | Sdecl d -> {s with sdesc = Sdecl(transf_decl env d)} - | Sasm _ -> s + | Sasm(attr, template, outputs, inputs, clob) -> + {s with sdesc = Sasm(attr, template, + List.map transf_asm_operand outputs, + List.map transf_asm_operand inputs, clob)} in transf_stmt body diff --git a/cparser/Transform.ml b/cparser/Transform.ml index 3b6f10f6..6cdd8a6b 100644 --- a/cparser/Transform.ml +++ b/cparser/Transform.ml @@ -138,37 +138,46 @@ let expand_postincrdecr ~read ~write env ctx op l = ecomma (eassign tmp (read l)) (ecomma (write l newval) tmp)) (* Generic transformation of a statement, transforming expressions within - and preserving the statement structure. Applies only to unblocked code. *) + and preserving the statement structure. + If [decl] is not given, it applies only to unblocked code. *) -let stmt trexpr env s = +let stmt ~expr ?(decl = fun env decl -> assert false) env s = let rec stm s = match s.sdesc with | Sskip -> s | Sdo e -> - {s with sdesc = Sdo(trexpr s.sloc env Effects e)} + {s with sdesc = Sdo(expr s.sloc env Effects e)} | Sseq(s1, s2) -> {s with sdesc = Sseq(stm s1, stm s2)} | Sif(e, s1, s2) -> - {s with sdesc = Sif(trexpr s.sloc env Val e, stm s1, stm s2)} + {s with sdesc = Sif(expr s.sloc env Val e, stm s1, stm s2)} | Swhile(e, s1) -> - {s with sdesc = Swhile(trexpr s.sloc env Val e, stm s1)} + {s with sdesc = Swhile(expr s.sloc env Val e, stm s1)} | Sdowhile(s1, e) -> - {s with sdesc = Sdowhile(stm s1, trexpr s.sloc env Val e)} + {s with sdesc = Sdowhile(stm s1, expr s.sloc env Val e)} | Sfor(s1, e, s2, s3) -> - {s with sdesc = Sfor(stm s1, trexpr s.sloc env Val e, stm s2, stm s3)} + {s with sdesc = Sfor(stm s1, expr s.sloc env Val e, stm s2, stm s3)} | Sbreak -> s | Scontinue -> s | Sswitch(e, s1) -> - {s with sdesc = Sswitch(trexpr s.sloc env Val e, stm s1)} + {s with sdesc = Sswitch(expr s.sloc env Val e, stm s1)} | Slabeled(lbl, s) -> {s with sdesc = Slabeled(lbl, stm s)} | Sgoto lbl -> s | Sreturn None -> s | Sreturn (Some e) -> - {s with sdesc = Sreturn(Some(trexpr s.sloc env Val e))} - | Sasm _ -> s - | Sblock _ | Sdecl _ -> - assert false (* should not occur in unblocked code *) + {s with sdesc = Sreturn(Some(expr s.sloc env Val e))} + | Sasm(attr, template, outputs, inputs, clob) -> + let asm_operand (lbl, cstr, e) = + (lbl, cstr, expr s.sloc env Val e) in + {s with sdesc = Sasm(attr, template, + List.map asm_operand outputs, + List.map asm_operand inputs, clob)} + | Sblock sl -> + {s with sdesc = Sblock (List.map stm sl)} + | Sdecl d -> + {s with sdesc = Sdecl (decl env d)} + in stm s (* Generic transformation of a function definition *) diff --git a/cparser/Transform.mli b/cparser/Transform.mli index 718a2f9c..57a4737b 100644 --- a/cparser/Transform.mli +++ b/cparser/Transform.mli @@ -50,8 +50,10 @@ val expand_postincrdecr : (** Generic transformation of a statement *) -val stmt : (C.location -> Env.t -> context -> C.exp -> C.exp) -> - Env.t -> C.stmt -> C.stmt +val stmt : + expr: (C.location -> Env.t -> context -> C.exp -> C.exp) -> + ?decl: (Env.t -> C.decl -> C.decl) -> + Env.t -> C.stmt -> C.stmt (** Generic transformation of a function definition *) diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 4013db9b..91f50552 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -225,7 +225,13 @@ let rec unblock_stmt env s = {s with sdesc = Sreturn(Some (expand_expr true env e))} | Sblock sl -> unblock_block env sl | Sdecl d -> assert false - | Sasm _ -> s + | Sasm(attr, template, outputs, inputs, clob) -> + let expand_asm_operand (lbl, cstr, e) = + (lbl, cstr, expand_expr true env e) in + {s with sdesc = Sasm(attr, template, + List.map expand_asm_operand outputs, + List.map expand_asm_operand inputs, clob)} + and unblock_block env = function | [] -> sskip diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml index b1eea8f3..a352e99f 100644 --- a/debug/CtoDwarf.ml +++ b/debug/CtoDwarf.ml @@ -459,7 +459,7 @@ let union_to_dwarf (n,at,m) env gloc = (* Translate global declarations to there dwarf representation *) let globdecl_to_dwarf env (typs,decls) decl = - PrintAnnot.add_file (fst decl.gloc); + PrintAsmaux.add_file (fst decl.gloc); match decl.gdesc with | Gtypedef (n,t) -> let ret = typedef_to_dwarf (n,t) decl.gloc in typs@ret,decls diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index dec3279e..13d4049e 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -328,12 +328,13 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_string oc bt.base_type_name let print_compilation_unit oc tag = + let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Configuration.version Configuration.arch in print_string oc (Sys.getcwd ()); print_addr oc (get_start_addr ()); print_addr oc (get_end_addr ()); print_uleb128 oc 1; print_string oc tag.compile_unit_name; - print_string oc ("CompCert "^Configuration.version); + print_string oc prod_name; print_addr oc (get_stmt_list_addr ()) let print_const_type oc ct = diff --git a/driver/Driver.ml b/driver/Driver.ml index 380209ab..480cf665 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -502,6 +502,8 @@ let cmdline_actions = Exact "-E", Set option_E; Exact "-S", Set option_S; Exact "-o", String(fun s -> option_o := Some s); + Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in + option_o := Some s); (* Preprocessing options *) Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options); diff --git a/driver/Interp.ml b/driver/Interp.ml index b16d2cae..f453af95 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -402,7 +402,7 @@ let do_inline_assembly txt sg ge w args m = None (* Implementing external functions producing observable events *) let rec world ge m = - Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m) + lazy (Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m)) and world_io ge m id args = None diff --git a/extraction/extraction.v b/extraction/extraction.v index 4c400036..ecd2853a 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -77,9 +77,6 @@ Extract Constant Allocation.regalloc => "Regalloc.regalloc". (* Linearize *) Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". -(* Bounds *) -Extract Constant Bounds.mregs_of_clobber => "Machregsaux.mregs_of_clobber". - (* SimplExpr *) Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident". Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2. @@ -159,11 +156,11 @@ Separate Extraction Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env - Csyntax.make_program Clight.make_program Initializers.transl_init Initializers.constval Csyntax.Eindex Csyntax.Epreincr - Ctyping.retype_function Ctyping.econdition' + Ctyping.typecheck_program Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr + Clight.make_program Conventions1.dummy_int_reg Conventions1.dummy_float_reg RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin diff --git a/ia32/Machregs.v b/ia32/Machregs.v index a9f2b6c4..65e27599 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -69,6 +69,25 @@ End IndexedMreg. Definition is_stack_reg (r: mreg) : bool := match r with FP0 => true | _ => false end. +(** ** Names of registers *) + +Local Open Scope string_scope. + +Definition register_names := + ("EAX", AX) :: ("EBX", BX) :: ("ECX", CX) :: ("EDX", DX) :: + ("ESI", SI) :: ("EDI", DI) :: ("EBP", BP) :: + ("XMM0", X0) :: ("XMM1", X1) :: ("XMM2", X2) :: ("XMM3", X3) :: + ("XMM4", X4) :: ("XMM5", X5) :: ("XMM6", X6) :: ("XMM7", X7) :: + ("ST0", FP0) :: nil. + +Definition register_by_name (s: string) : option mreg := + let fix assoc (l: list (string * mreg)) : option mreg := + match l with + | nil => None + | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l' + end + in assoc register_names. + (** ** Destroyed registers, preferred registers *) Definition destroyed_by_op (op: operation): list mreg := @@ -100,7 +119,15 @@ Definition destroyed_by_cond (cond: condition): list mreg := Definition destroyed_by_jumptable: list mreg := nil. -Local Open Scope string_scope. +Fixpoint destroyed_by_clobber (cl: list string): list mreg := + match cl with + | nil => nil + | c1 :: cl => + match register_by_name c1 with + | Some r => r :: destroyed_by_clobber cl + | None => destroyed_by_clobber cl + end + end. Definition builtin_write16_reversed := ident_of_string "__builtin_write16_reversed". Definition builtin_write32_reversed := ident_of_string "__builtin_write32_reversed". @@ -115,6 +142,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := if ident_eq id builtin_write16_reversed || ident_eq id builtin_write32_reversed then CX :: DX :: nil else nil + | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil end. diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml index 5e98b58b..6485e752 100644 --- a/ia32/Machregsaux.ml +++ b/ia32/Machregsaux.ml @@ -12,38 +12,25 @@ (** Auxiliary functions on machine registers *) +open Camlcoq open Machregs -let register_names = [ - ("EAX", AX); ("EBX", BX); ("ECX", CX); ("EDX", DX); - ("ESI", SI); ("EDI", DI); ("EBP", BP); - ("XMM0", X0); ("XMM1", X1); ("XMM2", X2); ("XMM3", X3); - ("XMM4", X4); ("XMM5", X5); ("XMM6", X6); ("XMM7", X7); - ("ST0", FP0) -] +let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31 + +let _ = + List.iter + (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s)) + Machregs.register_names let scratch_register_names = [] let name_of_register r = - let rec rev_assoc = function - | [] -> None - | (a, b) :: rem -> if b = r then Some a else rev_assoc rem - in rev_assoc register_names + try Some (Hashtbl.find register_names r) with Not_found -> None let register_by_name s = - try - Some(List.assoc (String.uppercase s) register_names) - with Not_found -> - None + Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s)) let can_reserve_register r = List.mem r Conventions1.int_callee_save_regs || List.mem r Conventions1.float_callee_save_regs -let mregs_of_clobber idl = - List.fold_left - (fun l c -> - match register_by_name (Camlcoq.extern_atom c) with - | Some r -> r :: l - | None -> l) - [] idl diff --git a/ia32/Machregsaux.mli b/ia32/Machregsaux.mli index f0feec96..d4877a62 100644 --- a/ia32/Machregsaux.mli +++ b/ia32/Machregsaux.mli @@ -16,4 +16,3 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val scratch_register_names: string list val can_reserve_register: Machregs.mreg -> bool -val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list @@ -755,30 +755,30 @@ Hypothesis valid_different_pointers_inj: Ltac InvInject := match goal with - | [ H: val_inject _ (Vint _) _ |- _ ] => + | [ H: Val.inject _ (Vint _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vfloat _) _ |- _ ] => + | [ H: Val.inject _ (Vfloat _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vptr _ _) _ |- _ ] => + | [ H: Val.inject _ (Vptr _ _) _ |- _ ] => inv H; InvInject - | [ H: val_list_inject _ nil _ |- _ ] => + | [ H: Val.inject_list _ nil _ |- _ ] => inv H; InvInject - | [ H: val_list_inject _ (_ :: _) _ |- _ ] => + | [ H: Val.inject_list _ (_ :: _) _ |- _ ] => inv H; InvInject | _ => idtac end. Lemma eval_condition_inj: forall cond vl1 vl2 b, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. Proof. intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. inv H3; inv H2; simpl in H0; inv H0; auto. - eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies. + eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. inv H3; simpl in H0; inv H0; auto. - eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies. + eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; inv H2; simpl in H0; inv H0; auto. @@ -789,7 +789,7 @@ Qed. Ltac TrivialExists := match goal with - | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] => + | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] => exists v1; split; auto | _ => idtac end. @@ -798,32 +798,32 @@ Lemma eval_addressing_inj: forall addr sp1 vl1 sp2 vl2 v1, (forall id ofs, In id (globals_addressing addr) -> - val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> - val_inject f sp1 sp2 -> - val_list_inject f vl1 vl2 -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> eval_addressing ge1 sp1 addr vl1 = Some v1 -> - exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. + exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. - apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. inv H5; simpl; auto. - apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H3; simpl; auto. + apply Values.Val.add_inject; auto. + apply Values.Val.add_inject; auto. apply Values.Val.add_inject; auto. + apply Values.Val.add_inject; auto. inv H5; simpl; auto. + apply Values.Val.add_inject; auto. apply Values.Val.add_inject; auto. inv H3; simpl; auto. apply H; simpl; auto. - apply Values.val_add_inject; auto. apply H; simpl; auto. - apply Values.val_add_inject; auto. apply H; simpl; auto. inv H5; simpl; auto. - apply Values.val_add_inject; auto. + apply Values.Val.add_inject; auto. apply H; simpl; auto. + apply Values.Val.add_inject; auto. apply H; simpl; auto. inv H5; simpl; auto. + apply Values.Val.add_inject; auto. Qed. Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, (forall id ofs, In id (globals_operation op) -> - val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> - val_inject f sp1 sp2 -> - val_list_inject f vl1 vl2 -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> eval_operation ge1 sp1 op vl1 m1 = Some v1 -> - exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. + exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. apply GL; simpl; auto. @@ -959,7 +959,7 @@ Proof. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends. apply valid_different_pointers_extends; auto. - rewrite <- val_list_inject_lessdef. eauto. auto. + rewrite <- val_inject_list_lessdef. eauto. auto. Qed. Lemma eval_operation_lessdef: @@ -969,10 +969,10 @@ Lemma eval_operation_lessdef: eval_operation genv sp op vl1 m1 = Some v1 -> exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2. Proof. - intros. rewrite val_list_inject_lessdef in H. + intros. rewrite val_inject_list_lessdef in H. assert (exists v2 : val, eval_operation genv sp op vl2 m2 = Some v2 - /\ val_inject (fun b => Some(b, 0)) v1 v2). + /\ Val.inject (fun b => Some(b, 0)) v1 v2). eapply eval_operation_inj with (m1 := m1) (sp1 := sp). apply valid_pointer_extends; auto. apply weak_valid_pointer_extends; auto. @@ -991,10 +991,10 @@ Lemma eval_addressing_lessdef: eval_addressing genv sp addr vl1 = Some v1 -> exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2. Proof. - intros. rewrite val_list_inject_lessdef in H. + intros. rewrite val_inject_list_lessdef in H. assert (exists v2 : val, eval_addressing genv sp addr vl2 = Some v2 - /\ val_inject (fun b => Some(b, 0)) v1 v2). + /\ Val.inject (fun b => Some(b, 0)) v1 v2). eapply eval_addressing_inj with (sp1 := sp). intros. rewrite <- val_inject_lessdef; auto. rewrite <- val_inject_lessdef; auto. @@ -1018,7 +1018,7 @@ Variable delta: Z. Hypothesis sp_inj: f sp1 = Some(sp2, delta). Remark symbol_address_inject: - forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). + forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. @@ -1027,7 +1027,7 @@ Qed. Lemma eval_condition_inject: forall cond vl1 vl2 b m1 m2, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. @@ -1041,11 +1041,11 @@ Qed. Lemma eval_addressing_inject: forall addr vl1 vl2 v1, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> exists v2, eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 - /\ val_inject f v1 v2. + /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_addressing. simpl. @@ -1055,12 +1055,12 @@ Qed. Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> exists v2, eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 - /\ val_inject f v1 v2. + /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_operation. simpl. diff --git a/ia32/PrintOp.ml b/ia32/PrintOp.ml index fb9a7cc5..1f7f4a65 100644 --- a/ia32/PrintOp.ml +++ b/ia32/PrintOp.ml @@ -38,6 +38,10 @@ let print_condition reg pp = function fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2 | (Cnotcompf c, [r1;r2]) -> fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2 + | (Ccompfs c, [r1;r2]) -> + fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2 + | (Cnotcompfs c, [r1;r2]) -> + fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2 | (Cmaskzero n, [r1]) -> fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n) | (Cmasknotzero n, [r1]) -> @@ -100,10 +104,18 @@ let print_operation reg pp = function | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2 | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2 | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2 + | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1 + | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1 + | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2 + | Osubfs, [r1;r2] -> fprintf pp "%a -fs %a" reg r1 reg r2 + | Omulfs, [r1;r2] -> fprintf pp "%a *fs %a" reg r1 reg r2 + | Odivfs, [r1;r2] -> fprintf pp "%a /fs %a" reg r1 reg r2 | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1 | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 + | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1 + | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1 | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2 | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1 | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1 diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index ca07a172..a53a8fbd 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -323,7 +323,7 @@ module Target(System: SYSTEM):TARGET = (* Emit .file / .loc debugging directives *) let print_file_line oc file line = - PrintAnnot.print_file_line oc comment file line + print_file_line oc comment file line let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) @@ -345,12 +345,12 @@ module Target(System: SYSTEM):TARGET = (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "%esp" oc txt targs args + print_annot_stmt preg "%esp" oc txt targs args end let print_annot_val oc txt args res = fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_val preg oc txt args; + print_annot_val preg oc txt args; match args, res with | [IR src], [IR dst] -> if dst <> src then fprintf oc " movl %a, %a\n" ireg src ireg dst @@ -873,7 +873,7 @@ module Target(System: SYSTEM):TARGET = print_annot_val oc (extern_atom txt) args res | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; + print_inline_asm preg oc (extern_atom txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index f7ed7793..3b7cbb76 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +Require Import String. Require Import Coqlib. Require Import Maps. Require Import AST. @@ -97,6 +98,36 @@ End IndexedMreg. Definition is_stack_reg (r: mreg) : bool := false. +(** ** Names of registers *) + +Local Open Scope string_scope. + +Definition register_names := + ("R3", R3) :: ("R4", R4) :: ("R5", R5) :: ("R6", R6) :: + ("R7", R7) :: ("R8", R8) :: ("R9", R9) :: ("R10", R10) :: + ("R11", R11) :: ("R12", R12) :: + ("R14", R14) :: ("R15", R15) :: ("R16", R16) :: + ("R17", R17) :: ("R18", R18) :: ("R19", R19) :: ("R20", R20) :: + ("R21", R21) :: ("R22", R22) :: ("R23", R23) :: ("R24", R24) :: + ("R25", R25) :: ("R26", R26) :: ("R27", R27) :: ("R28", R28) :: + ("R29", R29) :: ("R30", R30) :: ("R31", R31) :: + ("F0", F0) :: ("F1", F1) :: ("F2", F2) :: ("F3", F3) :: ("F4", F4) :: + ("F5", F5) :: ("F6", F6) :: ("F7", F7) :: ("F8", F8) :: + ("F9", F9) :: ("F10", F10) :: ("F11", F11) :: ("F12", F12) :: + ("F13", F13) :: ("F14", F14) :: ("F15", F15) :: + ("F16", F16) :: ("F17", F17) :: ("F18", F18) :: ("F19", F19) :: + ("F20", F20) :: ("F21", F21) :: ("F22", F22) :: ("F23", F23) :: + ("F24", F24) :: ("F25", F25) :: ("F26", F26) :: ("F27", F27) :: + ("F28", F28) :: ("F29", F29) :: ("F30", F30) :: ("F31", F31) :: nil. + +Definition register_by_name (s: string) : option mreg := + let fix assoc (l: list (string * mreg)) : option mreg := + match l with + | nil => None + | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l' + end + in assoc register_names. + (** ** Destroyed registers, preferred registers *) Definition destroyed_by_op (op: operation): list mreg := @@ -119,6 +150,16 @@ Definition destroyed_by_cond (cond: condition): list mreg := Definition destroyed_by_jumptable: list mreg := R12 :: nil. +Fixpoint destroyed_by_clobber (cl: list string): list mreg := + match cl with + | nil => nil + | c1 :: cl => + match register_by_name c1 with + | Some r => r :: destroyed_by_clobber cl + | None => destroyed_by_clobber cl + end + end. + Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_builtin _ _ => F13 :: nil @@ -128,6 +169,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := | EF_vstore_global Mint64 _ _ => R10 :: R11 :: R12 :: nil | EF_vstore_global _ _ _ => R11 :: R12 :: nil | EF_memcpy _ _ => R11 :: R12 :: F13 :: nil + | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil end. diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml index ba111089..8c3017ff 100644 --- a/powerpc/Machregsaux.ml +++ b/powerpc/Machregsaux.ml @@ -12,49 +12,24 @@ (** Auxiliary functions on machine registers *) +open Camlcoq open Machregs -let register_names = [ - ("R3", R3); ("R4", R4); ("R5", R5); ("R6", R6); - ("R7", R7); ("R8", R8); ("R9", R9); ("R10", R10); - ("R11", R11); ("R12", R12); - ("R14", R14); ("R15", R15); ("R16", R16); - ("R17", R17); ("R18", R18); ("R19", R19); ("R20", R20); - ("R21", R21); ("R22", R22); ("R23", R23); ("R24", R24); - ("R25", R25); ("R26", R26); ("R27", R27); ("R28", R28); - ("R29", R29); ("R30", R30); ("R31", R31); - ("F0", F0); ("F1", F1); ("F2", F2); ("F3", F3); ("F4", F4); - ("F5", F5); ("F6", F6); ("F7", F7); ("F8", F8); - ("F9", F9); ("F10", F10); ("F11", F11); ("F12", F12); - ("F13", F13); ("F14", F14); ("F15", F15); - ("F16", F16); ("F17", F17); ("F18", F18); ("F19", F19); - ("F20", F20); ("F21", F21); ("F22", F22); ("F23", F23); - ("F24", F24); ("F25", F25); ("F26", F26); ("F27", F27); - ("F28", F28); ("F29", F29); ("F30", F30); ("F31", F31) -] +let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31 + +let _ = + List.iter + (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s)) + Machregs.register_names let scratch_register_names = [ "R0" ] let name_of_register r = - let rec rev_assoc = function - | [] -> None - | (a, b) :: rem -> if b = r then Some a else rev_assoc rem - in rev_assoc register_names + try Some (Hashtbl.find register_names r) with Not_found -> None let register_by_name s = - try - Some(List.assoc (String.uppercase s) register_names) - with Not_found -> - None + Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s)) let can_reserve_register r = List.mem r Conventions1.int_callee_save_regs || List.mem r Conventions1.float_callee_save_regs - -let mregs_of_clobber idl = - List.fold_left - (fun l c -> - match register_by_name (Camlcoq.extern_atom c) with - | Some r -> r :: l - | None -> l) - [] idl diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli index f0feec96..d4877a62 100644 --- a/powerpc/Machregsaux.mli +++ b/powerpc/Machregsaux.mli @@ -16,4 +16,3 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val scratch_register_names: string list val can_reserve_register: Machregs.mreg -> bool -val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list diff --git a/powerpc/Op.v b/powerpc/Op.v index 4c1168cd..3ff08791 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -677,32 +677,32 @@ Hypothesis valid_different_pointers_inj: Ltac InvInject := match goal with - | [ H: val_inject _ (Vint _) _ |- _ ] => + | [ H: Val.inject _ (Vint _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vfloat _) _ |- _ ] => + | [ H: Val.inject _ (Vfloat _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vsingle _) _ |- _ ] => + | [ H: Val.inject _ (Vsingle _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vptr _ _) _ |- _ ] => + | [ H: Val.inject _ (Vptr _ _) _ |- _ ] => inv H; InvInject - | [ H: val_list_inject _ nil _ |- _ ] => + | [ H: Val.inject_list _ nil _ |- _ ] => inv H; InvInject - | [ H: val_list_inject _ (_ :: _) _ |- _ ] => + | [ H: Val.inject_list _ (_ :: _) _ |- _ ] => inv H; InvInject | _ => idtac end. Lemma eval_condition_inj: forall cond vl1 vl2 b, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. Proof. intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. inv H3; inv H2; simpl in H0; inv H0; auto. - eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies. + eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. inv H3; simpl in H0; inv H0; auto. - eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies. + eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; try discriminate; auto. @@ -711,7 +711,7 @@ Qed. Ltac TrivialExists := match goal with - | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] => + | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] => exists v1; split; auto | _ => idtac end. @@ -720,20 +720,20 @@ Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, (forall id ofs, In id (globals_operation op) -> - val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> - val_inject f sp1 sp2 -> - val_list_inject f vl1 vl2 -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> eval_operation ge1 sp1 op vl1 m1 = Some v1 -> - exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. + exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. apply GL; simpl; auto. - apply Values.val_add_inject; auto. + apply Values.Val.add_inject; auto. inv H4; simpl; auto. inv H4; simpl; auto. - apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. apply GL; simpl; auto. + apply Values.Val.add_inject; auto. + apply Values.Val.add_inject; auto. + apply Values.Val.add_inject; auto. apply GL; simpl; auto. inv H4; inv H2; simpl; auto. econstructor; eauto. rewrite Int.sub_add_l. auto. destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. @@ -797,16 +797,16 @@ Lemma eval_addressing_inj: forall addr sp1 vl1 sp2 vl2 v1, (forall id ofs, In id (globals_addressing addr) -> - val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> - val_inject f sp1 sp2 -> - val_list_inject f vl1 vl2 -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> eval_addressing ge1 sp1 addr vl1 = Some v1 -> - exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. + exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists; - auto using Values.val_add_inject. + auto using Values.Val.add_inject. apply H; simpl; auto. - apply Values.val_add_inject; auto. apply H; simpl; auto. + apply Values.Val.add_inject; auto. apply H; simpl; auto. Qed. End EVAL_COMPAT. @@ -872,7 +872,7 @@ Proof. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends; auto. apply valid_different_pointers_extends; auto. - rewrite <- val_list_inject_lessdef. eauto. auto. + rewrite <- val_inject_list_lessdef. eauto. auto. Qed. Lemma eval_operation_lessdef: @@ -882,10 +882,10 @@ Lemma eval_operation_lessdef: eval_operation genv sp op vl1 m1 = Some v1 -> exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2. Proof. - intros. rewrite val_list_inject_lessdef in H. + intros. rewrite val_inject_list_lessdef in H. assert (exists v2 : val, eval_operation genv sp op vl2 m2 = Some v2 - /\ val_inject (fun b => Some(b, 0)) v1 v2). + /\ Val.inject (fun b => Some(b, 0)) v1 v2). eapply eval_operation_inj with (m1 := m1) (sp1 := sp). apply valid_pointer_extends; auto. apply weak_valid_pointer_extends; auto. @@ -903,10 +903,10 @@ Lemma eval_addressing_lessdef: eval_addressing genv sp addr vl1 = Some v1 -> exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2. Proof. - intros. rewrite val_list_inject_lessdef in H. + intros. rewrite val_inject_list_lessdef in H. assert (exists v2 : val, eval_addressing genv sp addr vl2 = Some v2 - /\ val_inject (fun b => Some(b, 0)) v1 v2). + /\ Val.inject (fun b => Some(b, 0)) v1 v2). eapply eval_addressing_inj with (sp1 := sp). intros. rewrite <- val_inject_lessdef; auto. rewrite <- val_inject_lessdef; auto. @@ -930,7 +930,7 @@ Variable delta: Z. Hypothesis sp_inj: f sp1 = Some(sp2, delta). Remark symbol_address_inject: - forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). + forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. @@ -939,7 +939,7 @@ Qed. Lemma eval_condition_inject: forall cond vl1 vl2 b m1 m2, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. @@ -953,11 +953,11 @@ Qed. Lemma eval_addressing_inject: forall addr vl1 vl2 v1, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> exists v2, eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 - /\ val_inject f v1 v2. + /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_addressing. simpl. @@ -967,12 +967,12 @@ Qed. Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> exists v2, eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 - /\ val_inject f v1 v2. + /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_operation. simpl. diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index 664280f9..b0213014 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -49,6 +49,7 @@ let print_operation reg pp = function | Omove, [r1] -> reg pp r1 | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n) | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n) + | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n) | Oaddrsymbol(id, ofs), [] -> fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs) | Oaddrstack ofs, [] -> @@ -95,7 +96,14 @@ let print_operation reg pp = function | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2 | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2 | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2 + | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1 + | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1 + | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2 + | Osubfs, [r1;r2] -> fprintf pp "%a -fs %a" reg r1 reg r2 + | Omulfs, [r1;r2] -> fprintf pp "%a *fs %a" reg r1 reg r2 + | Odivfs, [r1;r2] -> fprintf pp "%a /fs %a" reg r1 reg r2 | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1 + | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 | Ofloatofwords, [r1;r2] -> fprintf pp "floatofwords(%a,%a)" reg r1 reg r2 | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2 diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index b05b29c0..3789d62e 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -132,7 +132,7 @@ module Linux_System : SYSTEM = let print_file_line oc file line = - PrintAnnot.print_file_line oc comment file line + print_file_line oc comment file line (* Emit .cfi directives *) let cfi_startproc = cfi_startproc @@ -203,7 +203,7 @@ module Diab_System : SYSTEM = | Section_debug_abbrev -> ".debug_abbrev,,n" let print_file_line oc file line = - PrintAnnot.print_file_line_d2 oc comment file line + print_file_line_d2 oc comment file line (* Emit .cfi directives *) let cfi_startproc oc = () @@ -240,10 +240,10 @@ module Diab_System : SYSTEM = end_addr := label_end; fprintf oc "%a:\n" label label_end; fprintf oc " .text\n"; - PrintAnnot.StringSet.iter (fun file -> + StringSet.iter (fun file -> let label = new_label () in Hashtbl.add filenum file label; - fprintf oc ".L%d: .d2filenum \"%s\"\n" label file) !PrintAnnot.all_files; + fprintf oc ".L%d: .d2filenum \"%s\"\n" label file) !all_files; fprintf oc " .d2_line_end\n" end @@ -331,7 +331,7 @@ module Target (System : SYSTEM):TARGET = (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg_annot "R1" oc txt targs args + print_annot_stmt preg_annot "R1" oc txt targs args end (* Determine if the displacement of a conditional branch fits the short form *) @@ -652,7 +652,7 @@ module Target (System : SYSTEM):TARGET = begin match ef with | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; + print_inline_asm preg oc (extern_atom txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false diff --git a/test/regression/Makefile b/test/regression/Makefile index 1ffe586c..94c212d2 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -17,7 +17,7 @@ TESTS=int32 int64 floats floats-basics \ volatile1 volatile2 volatile3 \ funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \ sizeof1 sizeof2 binops bool for1 switch switch2 compound \ - decl1 interop1 + decl1 interop1 bitfields9 # Can run, but only in compiled mode, and have reference output in Results diff --git a/test/regression/Results/bitfields9 b/test/regression/Results/bitfields9 new file mode 100644 index 00000000..ca74f1f4 --- /dev/null +++ b/test/regression/Results/bitfields9 @@ -0,0 +1,10 @@ +glob_s = { a = -12, b = 1 } +glob_t = { c = 123, d = 0, e = -45 } +loc_s = { a = 11, b = 2 } +loc_t = { c = 11, d = 1, e = 2 } +compound_s = { a = 2, b = 3 } +compound_t = { c = 2, d = 0, e = -11 } +loc_s = { a = 7, b = 2 } +loc_t = { c = 7, d = 1, e = 50 } +compound_s = { a = -14, b = 3 } +compound_t = { c = 50, d = 0, e = -7 } diff --git a/test/regression/bitfields9.c b/test/regression/bitfields9.c new file mode 100644 index 00000000..b33c4064 --- /dev/null +++ b/test/regression/bitfields9.c @@ -0,0 +1,49 @@ +#include <stdio.h> + +/* Initialization of bit-fields */ + +struct s { + signed char a: 6; + unsigned int b: 2; +}; + +struct t { + unsigned int c: 16; + unsigned int d: 1; + short e: 8; +}; + +void print_s(char * msg, struct s p) +{ + printf("%s = { a = %d, b = %d }\n", msg, p.a, p.b); +} + +void print_t(char * msg, struct t p) +{ + printf("%s = { c = %d, d = %d, e = %d }\n", msg, p.c, p.d, p.e); +} + +/* Global initialization */ +struct s glob_s = { -12, 1 }; +struct t glob_t = { 123, 0, -45 }; + +/* Local initialization */ +void f(int x, int y) +{ + struct s loc_s = { x, y }; + struct t loc_t = { x, 1, y }; + print_s("loc_s", loc_s); + print_t("loc_t", loc_t); + print_s("compound_s", (struct s) { y, x }); + print_t("compound_t", (struct t) { y, 0, -x }); +} + +int main() +{ + print_s("glob_s", glob_s); + print_t("glob_t", glob_t); + f(11, 2); + f(7, 50); + return 0; +} + diff --git a/test/regression/extasm.c b/test/regression/extasm.c index 4925392e..00a1cd57 100644 --- a/test/regression/extasm.c +++ b/test/regression/extasm.c @@ -1,7 +1,7 @@ /* Testing extended asm. To run the test, compile with -S and grep "TEST" in the generated .s */ -int clobbers(int x) +int clobbers(int x, int z) { int y; asm("TEST0 out:%0 in:%1" : "=r"(y) : "r"(x) : "cc" @@ -10,10 +10,10 @@ int clobbers(int x) #elif defined(__arm__) , "r0", "r1", "r4" #elif defined(__PPC__) - , "r3", "r4", "r31" + , "r0", "r3", "r4", "r31" #endif ); - return y; + return y + z; } int main() |