diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/AST.v | 43 | ||||
-rw-r--r-- | common/DebugPrint.ml | 144 | ||||
-rw-r--r-- | common/Events.v | 66 | ||||
-rw-r--r-- | common/Memdata.v | 8 | ||||
-rw-r--r-- | common/Memory.v | 156 | ||||
-rw-r--r-- | common/PrintAST.ml | 15 | ||||
-rw-r--r-- | common/Sections.ml | 25 | ||||
-rw-r--r-- | common/Sections.mli | 4 | ||||
-rw-r--r-- | common/Switchaux.ml | 3 | ||||
-rw-r--r-- | common/Values.v | 212 |
10 files changed, 648 insertions, 28 deletions
diff --git a/common/AST.v b/common/AST.v index 2259d74c..868364cd 100644 --- a/common/AST.v +++ b/common/AST.v @@ -18,7 +18,7 @@ the abstract syntax trees of many of the intermediate languages. *) Require Import String. -Require Import Coqlib Maps Errors Integers Floats. +Require Import Coqlib Maps Errors Integers Floats BinPos. Require Archi. Set Implicit Arguments. @@ -233,6 +233,16 @@ Definition chunk_of_type (ty: typ) := Lemma chunk_of_Tptr: chunk_of_type Tptr = Mptr. Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed. +(** Trapping mode: does undefined behavior result in a trap or an undefined value (e.g. for loads) *) +Inductive trapping_mode : Type := TRAP | NOTRAP. + +Definition trapping_mode_eq : forall x y : trapping_mode, + { x=y } + { x <> y}. +Proof. + decide equality. +Defined. + + (** Initialization data for global variables. *) Inductive init_data: Type := @@ -455,6 +465,11 @@ Qed. (** * External functions *) +(* Identifiers for profiling information *) +Parameter profiling_id : Type. +Axiom profiling_id_eq : forall (x y : profiling_id), {x=y} + {x<>y}. +Definition profiling_kind := Z.t. + (** For most languages, the functions composing the program are either internal functions, defined within the language, or external functions, defined outside. External functions include system calls but also @@ -505,10 +520,13 @@ Inductive external_function : Type := used with caution, as it can invalidate the semantic preservation theorem. Generated only if [-finline-asm] is given. *) - | EF_debug (kind: positive) (text: ident) (targs: list typ). + | EF_debug (kind: positive) (text: ident) (targs: list typ) (** Transport debugging information from the front-end to the generated assembly. Takes zero, one or several arguments like [EF_annot]. Unlike [EF_annot], produces no observable event. *) + | EF_profiling (id: profiling_id) (kind : profiling_kind). + (** Count one profiling event for this identifier and kind. + Takes no argument. Produces no observable event. *) (** The type signature of an external function. *) @@ -526,6 +544,7 @@ Definition ef_sig (ef: external_function): signature := | EF_annot_val kind text targ => mksignature (targ :: nil) targ cc_default | EF_inline_asm text sg clob => sg | EF_debug kind text targs => mksignature targs Tvoid cc_default + | EF_profiling id kind => mksignature nil Tvoid cc_default end. (** Whether an external function should be inlined by the compiler. *) @@ -544,6 +563,7 @@ Definition ef_inline (ef: external_function) : bool := | EF_annot_val kind Text rg => true | EF_inline_asm text sg clob => true | EF_debug kind text targs => true + | EF_profiling id kind => true end. (** Whether an external function must reload its arguments. *) @@ -559,7 +579,7 @@ Definition ef_reloads (ef: external_function) : bool := Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}. Proof. - generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. + generalize profiling_id_eq ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. decide equality. Defined. Global Opaque external_function_eq. @@ -670,11 +690,28 @@ Inductive builtin_arg (A: Type) : Type := | BA_splitlong (hi lo: builtin_arg A) | BA_addptr (a1 a2: builtin_arg A). +Definition builtin_arg_eq {A: Type}: + (forall x y : A, {x = y} + {x <> y}) -> + forall (ba1 ba2: (builtin_arg A)), {ba1=ba2} + {ba1<>ba2}. +Proof. + intro. generalize Integers.int_eq int64_eq float_eq float32_eq chunk_eq ptrofs_eq ident_eq. + decide equality. +Defined. +Global Opaque builtin_arg_eq. + Inductive builtin_res (A: Type) : Type := | BR (x: A) | BR_none | BR_splitlong (hi lo: builtin_res A). +Definition builtin_res_eq {A: Type}: + (forall x y : A, {x = y} + {x <> y}) -> + forall (a b: builtin_res A), {a=b} + {a<>b}. +Proof. + intro. decide equality. +Defined. +Global Opaque builtin_res_eq. + Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident := match a with | BA_loadglobal chunk id ofs => id :: nil diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml new file mode 100644 index 00000000..83a485b0 --- /dev/null +++ b/common/DebugPrint.ml @@ -0,0 +1,144 @@ +open Maps +open Camlcoq +open Registers +open RTLcommonaux + +let debug_flag = ref false + +let debug fmt = + if !debug_flag then (flush stderr; flush stdout; Printf.eprintf fmt) + else Printf.ifprintf stderr fmt + +let print_ptree_bool oc pt = + if !debug_flag then + let elements = PTree.elements pt in + begin + Printf.fprintf oc "["; + List.iter (fun (n, b) -> + if b then Printf.fprintf oc "%d, " (P.to_int n) + ) elements; + Printf.fprintf oc "]\n" + end + else () + +let print_ptree_opint oc pt = + if !debug_flag then + let elements = PTree.elements pt in + begin + Printf.fprintf oc "["; + List.iter (fun (n, op) -> + match op with + | None -> () + | Some p -> Printf.fprintf oc "%d -> %d, " (P.to_int n) (P.to_int p) + ) elements; + Printf.fprintf oc "]\n" + end + else () + +let print_intlist oc l = + let rec f oc = function + | [] -> () + | n::ln -> (Printf.fprintf oc "%d %a" (P.to_int n) f ln) + in begin + if !debug_flag then begin + Printf.fprintf oc "[%a]" f l + end + end + +let print_ptree_oplist oc pt = + if !debug_flag then + let elements = PTree.elements pt in + begin + Printf.fprintf oc "["; + List.iter (fun (n, ol) -> + match ol with + | None -> () + | Some l -> Printf.fprintf oc "%d -> %a,\n" (P.to_int n) print_intlist l + ) elements; + Printf.fprintf oc "]\n" + end + else () + +(* Adapted from backend/PrintRTL.ml: print_function *) +let print_code code = let open PrintRTL in let open Printf in + if (!debug_flag) then begin + fprintf stdout "{\n"; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements code)) in + List.iter (print_instruction stdout) instrs; + fprintf stdout "}" + end + +let ptree_printbool pt = + let elements = PTree.elements pt + in begin + if !debug_flag then begin + Printf.printf "["; + List.iter (fun (n, b) -> + if b then Printf.printf "%d, " (P.to_int n) else () + ) elements; + Printf.printf "]" + end + end + +let print_ptree printer pt = + let elements = PTree.elements pt in + begin + debug "[\n"; + List.iter (fun (n, elt) -> + debug "\t%d: %a\n" (P.to_int n) printer elt + ) elements; + debug "]\n" + end + +let print_option_pint oc o = + if !debug_flag then + match o with + | None -> Printf.fprintf oc "None" + | Some n -> Printf.fprintf oc "Some %d" (P.to_int n) + +let print_pint oc i = if !debug_flag then Printf.fprintf oc "%d" (P.to_int i) else () + +let print_regset rs = begin + debug "["; + List.iter (fun n -> debug "%d " (P.to_int n)) (Regset.elements rs); + debug "]" +end + +let print_ptree_regset pt = begin + debug "["; + List.iter (fun (n, rs) -> + debug "\n\t"; + debug "%d: " (P.to_int n); + print_regset rs + ) (PTree.elements pt); + debug "]" +end + +let print_true_nodes booltree = begin + debug "["; + List.iter (fun (n,b) -> + if b then debug "%d " (P.to_int n) + ) (PTree.elements booltree); + debug "]"; +end + + +let print_instructions insts code = + if (!debug_flag) then begin + debug "[ "; + List.iter ( + fun n -> (PrintRTL.print_instruction stdout (P.to_int n, get_some @@ PTree.get n code)) + ) insts; debug " ]" + end + +let print_arrayp arr = begin + debug "[| "; + Array.iter (fun n -> debug "%d, " (P.to_int n)) arr; + debug "|]" +end + diff --git a/common/Events.v b/common/Events.v index c4a6e7f9..360da52f 100644 --- a/common/Events.v +++ b/common/Events.v @@ -26,6 +26,7 @@ Require Import Values. Require Import Memory. Require Import Globalenvs. Require Import Builtins. +Require Import Lia. (** * Events and traces *) @@ -1379,6 +1380,11 @@ Inductive extcall_debug_sem (ge: Senv.t): | extcall_debug_sem_intro: forall vargs m, extcall_debug_sem ge vargs m E0 Vundef m. +Inductive extcall_profiling_sem (ge: Senv.t): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_profiling_sem_intro: forall vargs m, + extcall_profiling_sem ge vargs m E0 Vundef m. + Lemma extcall_debug_ok: forall targs, extcall_properties extcall_debug_sem @@ -1413,6 +1419,40 @@ Proof. split. constructor. auto. Qed. +Lemma extcall_profiling_ok: + forall targs, + extcall_properties extcall_profiling_sem + (mksignature targs Tvoid cc_default). +Proof. + intros; constructor; intros. +(* well typed *) +- inv H. simpl. auto. +(* symbols *) +- inv H0. econstructor; eauto. +(* valid blocks *) +- inv H; auto. +(* perms *) +- inv H; auto. +(* readonly *) +- inv H; auto. +(* mem extends *) +- inv H. + exists Vundef; exists m1'; intuition. + econstructor; eauto. +(* mem injects *) +- inv H0. + exists f; exists Vundef; exists m1'; intuition. + econstructor; eauto. + red; intros; congruence. +(* trace length *) +- inv H; simpl; lia. +(* receptive *) +- inv H; inv H0. exists Vundef, m1; constructor. +(* determ *) +- inv H; inv H0. + split. constructor. auto. +Qed. + (** ** Semantics of known built-in functions. *) (** Some built-in functions and runtime support functions have known semantics @@ -1531,6 +1571,7 @@ Definition external_call (ef: external_function): extcall_sem := | EF_annot_val kind txt targ => extcall_annot_val_sem txt targ | EF_inline_asm txt sg clb => inline_assembly_sem txt sg | EF_debug kind txt targs => extcall_debug_sem + | EF_profiling id kind => extcall_profiling_sem end. Theorem external_call_spec: @@ -1538,18 +1579,19 @@ Theorem external_call_spec: extcall_properties (external_call ef) (ef_sig ef). Proof. intros. unfold external_call, ef_sig; destruct ef. - apply external_functions_properties. - apply builtin_or_external_sem_ok. - apply builtin_or_external_sem_ok. - apply volatile_load_ok. - apply volatile_store_ok. - apply extcall_malloc_ok. - apply extcall_free_ok. - apply extcall_memcpy_ok. - apply extcall_annot_ok. - apply extcall_annot_val_ok. - apply inline_assembly_properties. - apply extcall_debug_ok. +- apply external_functions_properties. +- apply builtin_or_external_sem_ok. +- apply builtin_or_external_sem_ok. +- apply volatile_load_ok. +- apply volatile_store_ok. +- apply extcall_malloc_ok. +- apply extcall_free_ok. +- apply extcall_memcpy_ok. +- apply extcall_annot_ok. +- apply extcall_annot_val_ok. +- apply inline_assembly_properties. +- apply extcall_debug_ok. +- apply extcall_profiling_ok. Qed. Definition external_call_well_typed_gen ef := ec_well_typed (external_call_spec ef). diff --git a/common/Memdata.v b/common/Memdata.v index 1bd87169..c80b3754 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -24,6 +24,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. +Require Import Lia. (** * Properties of memory chunks *) @@ -45,6 +46,13 @@ Definition size_chunk (chunk: memory_chunk) : Z := | Many64 => 8 end. +Definition largest_size_chunk := 8. + +Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8. +Proof. + destruct chunk; simpl; lia. +Qed. + Lemma size_chunk_pos: forall chunk, size_chunk chunk > 0. Proof. diff --git a/common/Memory.v b/common/Memory.v index 03a6572e..e243d475 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -39,6 +39,8 @@ Require Import Floats. Require Import Values. Require Export Memdata. Require Export Memtype. +Require Import Lia. + (* To avoid useless definitions of inductors in extracted code. *) Local Unset Elimination Schemes. @@ -530,6 +532,48 @@ Proof. induction vl; simpl; intros. auto. rewrite IHvl. auto. Qed. +Remark set_setN_swap_disjoint: + forall vl: list memval, + forall v: memval, + forall m : ZMap.t memval, + forall p pl: Z, + ~ (Intv.In p (pl, pl + Z.of_nat (length vl))) -> + (setN vl pl (ZMap.set p v m)) = (ZMap.set p v (setN vl pl m)). +Proof. + induction vl; simpl; trivial. + intros. + unfold Intv.In in *; simpl in *. + rewrite ZMap.set_disjoint by lia. + apply IHvl. + lia. +Qed. + +Lemma setN_swap_disjoint: + forall vl1 vl2: list memval, + forall m : ZMap.t memval, + forall p1 p2: Z, + Intv.disjoint (p1, p1 + Z.of_nat (length vl1)) + (p2, p2 + Z.of_nat (length vl2)) -> + (setN vl1 p1 (setN vl2 p2 m)) = (setN vl2 p2 (setN vl1 p1 m)). +Proof. + induction vl1; simpl; trivial. + intros until p2. intro DISJOINT. + rewrite <- set_setN_swap_disjoint. + { rewrite IHvl1. + reflexivity. + unfold Intv.disjoint, Intv.In in *. + simpl in *. + intro. + intro BOUNDS. + apply DISJOINT. + lia. + } + unfold Intv.disjoint, Intv.In in *. + simpl in *. + apply DISJOINT. + lia. +Qed. + (** [store chunk m b ofs v] perform a write in memory state [m]. Value [v] is stored at address [b] and offset [ofs]. Return the updated memory store, or [None] if the accessed bytes @@ -1170,6 +1214,118 @@ Local Hint Resolve store_valid_block_1 store_valid_block_2: mem. Local Hint Resolve store_valid_access_1 store_valid_access_2 store_valid_access_3: mem. +Remark mem_same_proof_irr : + forall m1 m2 : mem, + (mem_contents m1) = (mem_contents m2) -> + (mem_access m1) = (mem_access m2) -> + (nextblock m1) = (nextblock m2) -> + m1 = m2. +Proof. + destruct m1 as [contents1 access1 nextblock1 access_max1 nextblock_noaccess1 default1]. + destruct m2 as [contents2 access2 nextblock2 access_max2 nextblock_noaccess2 default2]. + simpl. + intros. + subst contents2. + subst access2. + subst nextblock2. + f_equal; apply proof_irr. +Qed. + +Theorem store_store_other: + forall chunk b ofs v chunk' b' ofs' v' m0 m1 m1', + b' <> b + \/ ofs' + size_chunk chunk' <= ofs + \/ ofs + size_chunk chunk <= ofs' -> + store chunk m0 b ofs v = Some m1 -> + store chunk' m0 b' ofs' v' = Some m1' -> + store chunk' m1 b' ofs' v' = + store chunk m1' b ofs v. +Proof. + intros until m1'. + intro DISJOINT. + intros W0 W0'. + assert (valid_access m1' chunk b ofs Writable) as WRITEABLE1' by eauto with mem. + (* { + eapply store_valid_access_1. + apply W0'. + eapply store_valid_access_3. + apply W0. + } *) + assert (valid_access m1 chunk' b' ofs' Writable) as WRITABLE1 by eauto with mem. + (* { + eapply store_valid_access_1. + apply W0. + eapply store_valid_access_3. + apply W0'. + } *) + unfold store in *. + destruct (valid_access_dec m0 chunk b ofs Writable). + 2: congruence. + destruct (valid_access_dec m1 chunk' b' ofs' Writable). + 2: contradiction. + destruct (valid_access_dec m0 chunk' b' ofs' Writable). + 2: congruence. + destruct (valid_access_dec m1' chunk b ofs Writable). + 2: contradiction. + f_equal. + inv W0; simpl in *. + inv W0'; simpl in *. + apply mem_same_proof_irr; simpl; trivial. + destruct (eq_block b b'). + { subst b'. + rewrite PMap.gss. + rewrite PMap.gss. + rewrite PMap.set2. + rewrite PMap.set2. + f_equal. + apply setN_swap_disjoint. + unfold Intv.disjoint. + rewrite encode_val_length. + rewrite <- size_chunk_conv. + rewrite encode_val_length. + rewrite <- size_chunk_conv. + unfold Intv.In; simpl. + intros. + destruct DISJOINT. contradiction. + lia. + } + { + rewrite PMap.set_disjoint by congruence. + rewrite PMap.gso by congruence. + rewrite PMap.gso by congruence. + reflexivity. + } +Qed. + +Section STOREV. +Variable chunk: memory_chunk. +Variable m1: mem. +Variables addr v: val. +Variable m2: mem. +Hypothesis STORE: storev chunk m1 addr v = Some m2. + + +Theorem loadv_storev_same: + loadv chunk m2 addr = Some (Val.load_result chunk v). +Proof. + destruct addr; simpl in *; try discriminate. + eapply load_store_same. + eassumption. +Qed. + +Theorem storev_preserv_valid (b : block) (ofs: Z): valid_pointer m1 b ofs = valid_pointer m2 b ofs. +Proof. + unfold storev in STORE. + cut (valid_pointer m1 b ofs = true <-> valid_pointer m2 b ofs = true). + { destruct (valid_pointer _ _ _), (valid_pointer _ _ _); intuition congruence. } + destruct addr; try congruence. + rewrite! valid_pointer_valid_access. split. + - intros; eapply store_valid_access_1; eauto. + - intros; eapply store_valid_access_2; eauto. +Qed. + +End STOREV. + Lemma load_store_overlap: forall chunk m1 b ofs v m2 chunk' ofs' v', store chunk m1 b ofs v = Some m2 -> diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 61c76c91..c33cb2dc 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -48,6 +48,13 @@ let name_of_chunk = function | Many32 -> "any32" | Many64 -> "any64" +let spp_profiling_id () (x : Digest.t) : string = + let s = Buffer.create 32 in + for i=0 to 15 do + Printf.bprintf s "%02x" (Char.code (String.get x i)) + done; + Buffer.contents s;; + let name_of_external = function | EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name) | EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name) @@ -62,7 +69,9 @@ let name_of_external = function | EF_annot_val(kind,text, targ) -> sprintf "annot_val %S" (camlstring_of_coqstring text) | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (camlstring_of_coqstring text) | EF_debug(kind, text, targs) -> - sprintf "debug%d %S" (P.to_int kind) (extern_atom text) + sprintf "debug%d %S" (P.to_int kind) (extern_atom text) + | EF_profiling(id, kind) -> + sprintf "profiling %a %d" spp_profiling_id id (Z.to_int kind) let rec print_builtin_arg px oc = function | BA x -> px oc x @@ -99,3 +108,7 @@ let rec print_builtin_res px oc = function fprintf oc "splitlong(%a, %a)" (print_builtin_res px) hi (print_builtin_res px) lo +let print_trapping_mode oc = function + | TRAP -> () + | NOTRAP -> output_string oc " [notrap]" + diff --git a/common/Sections.ml b/common/Sections.ml index 794b8470..c256628e 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -23,7 +23,7 @@ type initialized = type section_name = | Section_text - | Section_data of initialized + | Section_data of initialized * bool (* true = thread local ? *) | Section_small_data of initialized | Section_const of initialized | Section_small_const of initialized @@ -54,9 +54,9 @@ type section_info = { } let default_section_info = { - sec_name_init = Section_data Init; - sec_name_init_reloc = Section_data Init_reloc; - sec_name_uninit = Section_data Uninit; + sec_name_init = Section_data (Init, false); + sec_name_init_reloc = Section_data (Init_reloc, false); + sec_name_uninit = Section_data (Uninit, false); sec_writable = true; sec_executable = false; sec_access = Access_default @@ -72,9 +72,15 @@ let builtin_sections = [ sec_writable = false; sec_executable = true; sec_access = Access_default}; "DATA", - {sec_name_init = Section_data Init; - sec_name_init_reloc = Section_data Init_reloc; - sec_name_uninit = Section_data Uninit; + {sec_name_init = Section_data (Init, false); + sec_name_init_reloc = Section_data (Init_reloc, false); + sec_name_uninit = Section_data (Uninit, false); + sec_writable = true; sec_executable = false; + sec_access = Access_default}; + "TDATA", + {sec_name_init = Section_data (Init, true); + sec_name_init_reloc = Section_data (Init_reloc, true); + sec_name_uninit = Section_data (Uninit, true); sec_writable = true; sec_executable = false; sec_access = Access_default}; "SDATA", @@ -195,7 +201,7 @@ let get_attr_section loc attr = (* Determine section for a variable definition *) -let for_variable env loc id ty init = +let for_variable env loc id ty init thrl = let attr = Cutil.attributes_of_type env ty in let readonly = List.mem C.AConst attr && not(List.mem C.AVolatile attr) in let si = @@ -214,7 +220,8 @@ let for_variable env loc id ty init = let name = if readonly then if size <= !Clflags.option_small_const then "SCONST" else "CONST" - else if size <= !Clflags.option_small_data then "SDATA" else "DATA" in + else if size <= !Clflags.option_small_data then "SDATA" else + if thrl then "TDATA" else "DATA" in try Hashtbl.find current_section_table name with Not_found -> diff --git a/common/Sections.mli b/common/Sections.mli index 8ec98e40..6d1d9c69 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -24,7 +24,7 @@ type initialized = type section_name = | Section_text - | Section_data of initialized + | Section_data of initialized * bool (* true = thread local? *) | Section_small_data of initialized | Section_const of initialized | Section_small_const of initialized @@ -52,7 +52,7 @@ val define_section: -> ?writable:bool -> ?executable:bool -> ?access:access_mode -> unit -> unit val use_section_for: AST.ident -> string -> bool -val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> initialized -> +val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> initialized -> bool -> section_name * access_mode val for_function: Env.t -> C.location -> AST.ident -> C.attributes -> section_name list val for_stringlit: unit -> section_name diff --git a/common/Switchaux.ml b/common/Switchaux.ml index 47ded8ee..eb1ab8bc 100644 --- a/common/Switchaux.ml +++ b/common/Switchaux.ml @@ -81,6 +81,7 @@ let compile_switch_as_jumptable default cases minkey maxkey = CTaction default) let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) = + (* DM Settings this to constant false disables jump tables *) let span = Z.sub maxkey minkey in assert (Z.ge span Z.zero); let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases) @@ -88,7 +89,7 @@ let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) = numcases >= 7 (* small jump tables are always less efficient *) && Z.le table_size tree_size && Z.lt span (Z.of_uint Sys.max_array_length) - + let compile_switch modulus default table = let (tbl, keys) = normalize_table table in if ZSet.is_empty keys then CTaction default else begin diff --git a/common/Values.v b/common/Values.v index 891c9a88..87ebea00 100644 --- a/common/Values.v +++ b/common/Values.v @@ -21,6 +21,7 @@ Require Import Coqlib. Require Import AST. Require Import Integers. Require Import Floats. +Require Import Lia. Definition block : Type := positive. Definition eq_block := peq. @@ -90,6 +91,27 @@ Definition has_type (v: val) (t: typ) : Prop := | _, _ => False end. +Definition has_type_b (v: val) (t: typ) := + match v, t with + | Vundef, _ => true + | Vint _, Tint => true + | Vlong _, Tlong => true + | Vfloat _, Tfloat => true + | Vsingle _, Tsingle => true + | Vptr _ _, Tint => negb Archi.ptr64 + | Vptr _ _, Tlong => Archi.ptr64 + | (Vint _ | Vsingle _), Tany32 => true + | Vptr _ _, Tany32 => negb Archi.ptr64 + | _, Tany64 => true + | _, _ => false + end. + +Lemma has_type_b_correct: forall v t, + has_type_b v t = true <-> has_type v t. +Proof. + destruct v; destruct t; cbn; destruct Archi.ptr64; cbn; split; intros; auto; discriminate. +Qed. + Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop := match vl, tl with | nil, nil => True @@ -1471,6 +1493,60 @@ Proof. assert (32 < Int.max_unsigned) by reflexivity. lia. Qed. +Theorem shrx1_shr: + forall x z, + shrx x (Vint (Int.repr 1)) = Some z -> + z = shr (add x (shru x (Vint (Int.repr 31)))) (Vint (Int.repr 1)). +Proof. + intros. destruct x; simpl in H; try discriminate. + change (Int.ltu (Int.repr 1) (Int.repr 31)) with true in H; simpl in H. + inversion_clear H. + simpl. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true; simpl. + change (Int.ltu (Int.repr 1) Int.iwordsize) with true; simpl. + f_equal. + rewrite Int.shrx1_shr by reflexivity. + reflexivity. +Qed. + +Theorem shrx_shr_3: + forall n x z, + shrx x (Vint n) = Some z -> + z = (if Int.eq n Int.zero then x else + if Int.eq n Int.one + then shr (add x (shru x (Vint (Int.repr 31)))) (Vint Int.one) + else shr (add x (shru (shr x (Vint (Int.repr 31))) + (Vint (Int.sub (Int.repr 32) n)))) + (Vint n)). +Proof. + intros. destruct x; simpl in H; try discriminate. + destruct (Int.ltu n (Int.repr 31)) eqn:LT; inv H. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31; intros LT'. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. change (Int.signed Int.one) with 1. + rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. +- predSpec Int.eq Int.eq_spec n Int.one. + * subst n. simpl. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + change (Int.ltu Int.one Int.iwordsize) with true. simpl. + f_equal. + apply Int.shrx1_shr. + reflexivity. + * clear H0. + simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl. + replace (Int.ltu n Int.iwordsize) with true. + f_equal; apply Int.shrx_shr_2; assumption. + symmetry; apply zlt_true. change (Int.unsigned n < 32); lia. + symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32. + assert (Int.unsigned n <> 0). + { red; intros; elim H. + rewrite <- (Int.repr_unsigned n), H0. auto. } + rewrite Int.unsigned_repr. + change (Int.unsigned Int.iwordsize) with 32; lia. + assert (32 < Int.max_unsigned) by reflexivity. lia. +Qed. + Theorem or_rolm: forall x n m1 m2, or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2). @@ -1730,6 +1806,58 @@ Proof. assert (64 < Int.max_unsigned) by reflexivity. lia. Qed. +Theorem shrxl1_shrl: + forall x z, + shrxl x (Vint (Int.repr 1)) = Some z -> + z = shrl (addl x (shrlu x (Vint (Int.repr 63)))) (Vint (Int.repr 1)). +Proof. + intros. destruct x; simpl in H; try discriminate. + change (Int.ltu (Int.repr 1) (Int.repr 63)) with true in H; simpl in H. + inversion_clear H. + simpl. + change (Int.ltu (Int.repr 63) Int64.iwordsize') with true; simpl. + change (Int.ltu (Int.repr 1) Int64.iwordsize') with true; simpl. + f_equal. + rewrite Int64.shrx'1_shr' by reflexivity. + reflexivity. +Qed. + +Theorem shrxl_shrl_3: + forall n x z, + shrxl x (Vint n) = Some z -> + z = (if Int.eq n Int.zero then x else + if Int.eq n Int.one + then shrl (addl x (shrlu x (Vint (Int.repr 63)))) (Vint Int.one) + else shrl (addl x (shrlu (shrl x (Vint (Int.repr 63))) + (Vint (Int.sub (Int.repr 64) n)))) + (Vint n)). +Proof. + intros. destruct x; simpl in H; try discriminate. + destruct (Int.ltu n (Int.repr 63)) eqn:LT; inv H. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63; intros LT'. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. unfold Int64.shrx'. rewrite Int64.shl'_zero. unfold Int64.divs. change (Int64.signed Int64.one) with 1. + rewrite Z.quot_1_r. rewrite Int64.repr_signed; auto. +- predSpec Int.eq Int.eq_spec n Int.one. + * subst n. simpl. + change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. + change (Int.ltu Int.one Int64.iwordsize') with true. simpl. + f_equal. + apply Int64.shrx'1_shr'. + reflexivity. + * clear H0. +simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. + replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl. + replace (Int.ltu n Int64.iwordsize') with true. + f_equal; apply Int64.shrx'_shr_2; assumption. + symmetry; apply zlt_true. change (Int.unsigned n < 64); lia. + symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64. + assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } + rewrite Int.unsigned_repr. + change (Int.unsigned Int64.iwordsize') with 64; lia. + assert (64 < Int.max_unsigned) by reflexivity. lia. +Qed. + Theorem negate_cmp_bool: forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y). Proof. @@ -1888,6 +2016,20 @@ Proof. destruct (Float.cmp Cgt f f0); destruct (Float.cmp Ceq f f0); auto. Qed. +Theorem swap_cmpf_bool: + forall c x y, + Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x. +Proof. + destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto. +Qed. + +Theorem swap_cmpfs_bool: + forall c x y, + Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x. +Proof. + destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. +Qed. + Theorem cmp_ne_0_optbool: forall ob, cmp Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob. Proof. @@ -2508,6 +2650,55 @@ Qed. End VAL_INJ_OPS. +(* Specializations of cmpu_bool, cmpu, cmplu_bool, and cmplu for maximal pointer validity *) + +Definition mxcmpu_bool cmp v1 v2: option bool := + cmpu_bool (fun _ _ => true) cmp v1 v2. + +Lemma mxcmpu_bool_correct vptr (cmp: comparison) (v1 v2: val) b: + cmpu_bool vptr cmp v1 v2 = Some b + -> mxcmpu_bool cmp v1 v2 = Some b. +Proof. + intros; eapply cmpu_bool_lessdef; (econstructor 1 || eauto). +Qed. + +Definition mxcmpu cmp v1 v2 := of_optbool (mxcmpu_bool cmp v1 v2). + +Lemma mxcmpu_correct vptr (cmp: comparison) (v1 v2: val): + lessdef (cmpu vptr cmp v1 v2) (mxcmpu cmp v1 v2). +Proof. + unfold cmpu, mxcmpu. + remember (cmpu_bool _ cmp v1 v2) as ob. + destruct ob; simpl. + - erewrite mxcmpu_bool_correct; eauto. + econstructor. + - econstructor. +Qed. + +Definition mxcmplu_bool (cmp: comparison) (v1 v2: val) + := (cmplu_bool (fun _ _ => true) cmp v1 v2). + +Lemma mxcmplu_bool_correct vptr (cmp: comparison) (v1 v2: val) b: + (cmplu_bool vptr cmp v1 v2) = Some b + -> (mxcmplu_bool cmp v1 v2) = Some b. +Proof. + intros; eapply cmplu_bool_lessdef; (econstructor 1 || eauto). +Qed. + +Definition mxcmplu cmp v1 v2 := of_optbool (mxcmplu_bool cmp v1 v2). + +Lemma mxcmplu_correct vptr (cmp: comparison) (v1 v2: val): + lessdef (maketotal (cmplu vptr cmp v1 v2)) + (mxcmplu cmp v1 v2). +Proof. + unfold cmplu, mxcmplu. + remember (cmplu_bool _ cmp v1 v2) as ob. + destruct ob as [b|]; simpl. + - erewrite mxcmplu_bool_correct; eauto. + simpl. econstructor. + - econstructor. +Qed. + End Val. Notation meminj := Val.meminj. @@ -2601,3 +2792,24 @@ Proof. unfold compose_meminj; rewrite H1; rewrite H3; eauto. rewrite Ptrofs.add_assoc. decEq. unfold Ptrofs.add. apply Ptrofs.eqm_samerepr. auto with ints. Qed. + + +(** Particular cases of extensionality lemma *) + +Lemma cmpu_bool_valid_pointer_eq vptr1 vptr2 c v1 v2: + (forall (b : block) (z : Z), vptr1 b z = vptr2 b z) -> + Val.cmpu_bool vptr1 c v1 v2 = Val.cmpu_bool vptr2 c v1 v2. +Proof. + intros EQ; unfold Val.cmpu_bool; destruct v1; try congruence; + destruct v2; try congruence; + rewrite !EQ; auto. +Qed. + +Lemma cmplu_bool_valid_pointer_eq vptr1 vptr2 c v1 v2: + (forall (b : block) (z : Z), vptr1 b z = vptr2 b z) -> + Val.cmplu_bool vptr1 c v1 v2 = Val.cmplu_bool vptr2 c v1 v2. +Proof. + intros EQ; unfold Val.cmplu_bool; destruct v1; try congruence; + destruct v2; try congruence; + rewrite !EQ; auto. +Qed. |