diff options
89 files changed, 2128 insertions, 215 deletions
@@ -80,6 +80,8 @@ BACKEND=\ RTLgen.v RTLgenspec.v RTLgenproof.v \ Tailcall.v Tailcallproof.v \ Inlining.v Inliningspec.v Inliningproof.v \ + Profiling.v Profilingproof.v \ + ProfilingExploit.v ProfilingExploitproof.v \ Renumber.v Renumberproof.v \ Duplicate.v Duplicateproof.v \ RTLtyping.v \ diff --git a/PROFILING.md b/PROFILING.md new file mode 100644 index 00000000..3f4cbc46 --- /dev/null +++ b/PROFILING.md @@ -0,0 +1,34 @@ +This version of CompCert includes a profiling system. It tells CompCert's optimization phases for each conditional branch instruction which of the two branches was more frequently taken. This system is not available for all combinations of target architecture and operating system; see below. + +For using this profiling system one has to +1. Compile a special version of the program that will count, for each branch, the number of times it was taken, and recording this information to a file. +2. Execute this special version on representative examples. It will record the frequencies of execution of branches to a log file. +3. Recompile the program, telling CompCert to use the information in the log file. + +This system does not use the same formats as gcc's gcov profiles, since it depends heavily on compiler internals. It seems however possible to profile and optimize programs consisting of modules compiled with gcc and CompCert by using both system simultaneously: compiler uses separate log files. + +To compile the special version that logs frequencies to files, use the option `-fprofile-arcs`. This option has to be specified at compile time but is not needed at link time (however, a reminder: if you link using another compiled than CompCert, you need to link against `libcompcert.a`). You may mix object files compiled with and without this option. + +This version may experience significant slowdown compared to normally compiled code, so do not use `-fprofile-arcs` for production code. + +At the end of execution of the program, frequency information will be logged to a file whose default name is `compcert_profiling.dat` (in the current directory). Another name may be used by specifying it using the `COMPCERT_PROFILING_DATA` environment variable. If this variable contains an empty string, no logging is done (but the slowdown still applies). + +Data are appended to the log file, never deleted, so it is safe to run the program several times on several test cases to accumulate data. + +Depending on the platform, this logging system is or is not thread-safe and is or is not compatible with position-independent code (PIC). In non thread-safe configurations, if two different execution threads execute code to be profiled, the profiling counters may end up with incorrect values. + +| Target platform | Available? | Thread-safe | PIC | +|-----------------|------------|-------------|-----| +| AArch64 | Yes | Yes | No | +| ARM | Yes | No | No | +| IA32 | Yes | No | No | +| K1c | Yes | Yes | No | +| PowerPC | No | | | +| PowerPC 64 | No | | | +| Risc-V 32 | No | | | +| Risc-V 64 | No | | | +| x86-64 | Yes | Yes | Yes | + +For recompiling the program using profiling information, use `-fprofile-use= compcert_profiling.dat -ftracelinearize` (substitute the appropriate filename for `compcert_profiling.dat` if needed). Experiments show performance improvement on K1c, not on other platforms. + +The same options (except for `-fprofile-use=` and `-fprofile-arcs`) should be used to compile the logging and optimized versions of the program: only functions that are exactly the same in the intermediate representation will be optimized according to profiling information. diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index 471ad501..b0787d0a 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -400,7 +400,7 @@ let expand_instruction instr = expand_annot_val kind txt targ args res | EF_memcpy(sz, al) -> expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args - | EF_annot _ | EF_debug _ | EF_inline_asm _ -> + | EF_annot _ | EF_debug _ | EF_inline_asm _ | EF_profiling _ -> emit instr | _ -> assert false diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v index b2a2308e..3d27f48f 100644 --- a/aarch64/Machregs.v +++ b/aarch64/Machregs.v @@ -158,6 +158,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_memcpy sz al => R15 :: R17 :: R29 :: nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob + | EF_profiling _ _ => R15 :: R17 :: nil | _ => nil end. diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index e54673dd..8d74daf4 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -133,7 +133,9 @@ module Target : TARGET = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" @@ -227,6 +229,28 @@ module Target : TARGET = | EOuxtw n -> fprintf oc ", uxtw #%a" coqint n | EOuxtx n -> fprintf oc ", uxtx #%a" coqint n + let next_profiling_label = + let atomic_incr_counter = ref 0 in + fun () -> + let r = sprintf ".Lcompcert_atomic_incr%d" !atomic_incr_counter in + incr atomic_incr_counter; r;; + + let print_profiling_logger oc id kind = + assert (kind >= 0); + assert (kind <= 1); + fprintf oc "%s begin profiling %a %d: atomic increment\n" comment + Profilingaux.pp_id id kind; + let ofs = profiling_offset id kind and lbl = next_profiling_label () in + fprintf oc " adrp x15, %s+%d\n" profiling_counter_table_name ofs; + fprintf oc " add x15, x15, :lo12:(%s+%d)\n" profiling_counter_table_name ofs; + fprintf oc "%s:\n" lbl; + fprintf oc " ldaxr x17, [x15]\n"; + fprintf oc " add x17, x17, 1\n"; + fprintf oc " stlxr w17, x17, [x15]\n"; + fprintf oc " cbnz w17, %s\n" lbl; + fprintf oc "%s end profiling %a %d\n" comment + Profilingaux.pp_id id kind;; + (* Printing of instructions *) let print_instruction oc = function (* Branches *) @@ -519,6 +543,8 @@ module Target : TARGET = fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment + | EF_profiling (id, coq_kind) -> + print_profiling_logger oc id (Z.to_int coq_kind) | _ -> assert false end @@ -575,7 +601,24 @@ module Target : TARGET = section oc Section_text; end + let aarch64_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name = + fprintf oc " adrp x2, %s\n" profiling_counter_table_name; + fprintf oc " adrp x1, %s\n" profiling_id_table_name; + fprintf oc " add x2, x2, :lo12:%s\n" profiling_counter_table_name; + fprintf oc " add x1, x1, :lo12:%s\n" profiling_id_table_name; + fprintf oc " mov w0, %d\n" nr_items; + fprintf oc " b %s\n" profiling_write_table_helper ;; + + let print_atexit oc to_be_called = + fprintf oc " adrp x0, %s\n" to_be_called; + fprintf oc " add x0, x0, :lo12:%s\n" to_be_called; + fprintf oc " b atexit\n";; + + let print_epilogue oc = + print_profiling_epilogue elf_text_print_fun_info (Init_atexit print_atexit) aarch64_profiling_stub oc; if !Clflags.option_g then begin Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index e850fed6..669d8c0c 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -177,6 +177,7 @@ let pp_instructions pp ic = | EF_annot_val _ | EF_builtin _ | EF_debug _ + | EF_profiling _ | EF_external _ | EF_free | EF_malloc diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 89aab5c7..6996c9bb 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -619,7 +619,7 @@ let expand_instruction instr = | EF_memcpy(sz, al) -> expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz)) (Int32.to_int (camlint_of_coqint al)) args - | EF_annot _ | EF_debug _ | EF_inline_asm _ -> + | EF_annot _ | EF_debug _ | EF_inline_asm _ | EF_profiling _ -> emit instr | _ -> assert false diff --git a/arm/Constantexpand.ml b/arm/Constantexpand.ml index 408b291e..8cc32c1f 100644 --- a/arm/Constantexpand.ml +++ b/arm/Constantexpand.ml @@ -106,6 +106,7 @@ let estimate_size = function | Pbuiltin (ef,_,_) -> begin match ef with | EF_inline_asm _ -> 256 + | EF_profiling _ -> 40 | _ -> 0 end | Pcfi_adjust _ | Pcfi_rel_offset _ diff --git a/arm/Machregs.v b/arm/Machregs.v index ae0ff6bf..1ec8f0a1 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -153,6 +153,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_memcpy sz al => R2 :: R3 :: R12 :: F7 :: nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob + | EF_profiling _ _ => R2 :: R3 :: R12 :: nil | _ => nil end. diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 03e06a65..839530c6 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -147,7 +147,9 @@ struct let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data(i) -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" @@ -202,6 +204,38 @@ struct | SOasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n | SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n + + let next_profiling_label = + let profiling_label_counter = ref 0 in + fun () -> + let r = sprintf ".Lprofiling_label%d" !profiling_label_counter in + incr profiling_label_counter; r;; + + let print_profiling_logger oc id kind = + assert (kind >= 0); + assert (kind <= 1); + let ofs = profiling_offset id kind and olbl = next_profiling_label () in + fprintf oc "%s begin profiling %a %d: non-atomic increment\n" comment + Profilingaux.pp_id id kind; + fprintf oc " ldr r2, %s\n" olbl; + fprintf oc " ldr r3, [r2, #%d]\n" + (if Configuration.is_big_endian then 8 else 0); + fprintf oc " ldr r12, [r2, #%d]\n" + (if Configuration.is_big_endian then 0 else 8); + fprintf oc " adds r3, r3, #1\n"; + fprintf oc " adc r12, r12, #0\n"; + fprintf oc " str r3, [r2, #%d]\n" + (if Configuration.is_big_endian then 8 else 0); + fprintf oc " str r12, [r2, #%d]\n" + (if Configuration.is_big_endian then 0 else 8); + let jlbl = next_profiling_label () in + fprintf oc " b %s\n" jlbl; + fprintf oc "%s:\n" olbl; + fprintf oc " .word %s + %d\n" profiling_counter_table_name ofs; + fprintf oc "%s:\n" jlbl; + fprintf oc "%s end profiling %a %d\n" comment + Profilingaux.pp_id id kind;; + let print_instruction oc = function (* Core instructions *) | Padc (r1,r2,so) -> @@ -482,6 +516,7 @@ struct fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment + | EF_profiling(id, coq_kind) -> print_profiling_logger oc id (Z.to_int coq_kind) | _ -> assert false end @@ -549,6 +584,11 @@ struct if !Clflags.option_mthumb then fprintf oc " .thumb_func\n" + + let text_print_fun_info oc name = + fprintf oc " .type %s, %%function\n" name; + fprintf oc " .size %s, . - %s\n" name name + let print_fun_info oc name = fprintf oc " .type %a, %%function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name @@ -596,9 +636,22 @@ struct if !Clflags.option_g then begin section oc Section_text; cfi_section oc - end + end + + let arm_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name = + fprintf oc " ldr r2, = %s\n" profiling_counter_table_name; + fprintf oc " ldr r1, = %s\n" profiling_id_table_name; + fprintf oc " mov r0, #%d\n" nr_items; + fprintf oc " b %s\n" profiling_write_table_helper;; + + let print_atexit oc to_be_called = + fprintf oc " ldr r0, = %s\n" to_be_called; + fprintf oc " b atexit\n";; let print_epilogue oc = + print_profiling_epilogue text_print_fun_info (Init_atexit print_atexit) arm_profiling_stub oc; if !Clflags.option_g then begin Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; diff --git a/backend/CSE.v b/backend/CSE.v index 1936d4e4..838d96a6 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -493,7 +493,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb | _ => empty_numbering end - | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ => + | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ | EF_profiling _ _ => set_res_unknown before res end | Icond cond args ifso ifnot _ => diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 5bbb7508..a7465cee 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1318,6 +1318,7 @@ Proof. + apply CASE2; inv H1; auto. + apply CASE1. + apply CASE2; inv H1; auto. + + apply CASE2; inv H1; auto. * apply set_res_lessdef; auto. - (* Icond *) diff --git a/backend/Cminor.v b/backend/Cminor.v index 91a4c104..dcebbb86 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -77,6 +77,7 @@ Inductive unary_operation : Type := | Osingleoflongu: unary_operation. (**r unsigned long to float32 *) Inductive binary_operation : Type := + | Oexpect: typ -> binary_operation (**r first value, second is expected*) | Oadd: binary_operation (**r integer addition *) | Osub: binary_operation (**r integer subtraction *) | Omul: binary_operation (**r integer multiplication *) @@ -301,6 +302,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := Definition eval_binop (op: binary_operation) (arg1 arg2: val) (m: mem): option val := match op with + | Oexpect ty => Some (Val.normalize arg1 ty) | Oadd => Some (Val.add arg1 arg2) | Osub => Some (Val.sub arg1 arg2) | Omul => Some (Val.mul arg1 arg2) diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 96cb8ae6..26f47e23 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -50,7 +50,7 @@ with exprlist : Type := | Econs: expr -> exprlist -> exprlist with condexpr : Type := - | CEcond : condition -> exprlist -> condexpr + | CEcond : condition -> option bool -> exprlist -> condexpr | CEcondition : condexpr -> condexpr -> condexpr -> condexpr | CElet: expr -> condexpr -> condexpr. @@ -207,10 +207,10 @@ with eval_exprlist: letenv -> exprlist -> list val -> Prop := eval_exprlist le (Econs a1 al) (v1 :: vl) with eval_condexpr: letenv -> condexpr -> bool -> Prop := - | eval_CEcond: forall le cond al vl vb, + | eval_CEcond: forall le cond expected al vl vb, eval_exprlist le al vl -> eval_condition cond vl m = Some vb -> - eval_condexpr le (CEcond cond al) vb + eval_condexpr le (CEcond cond expected al) vb | eval_CEcondition: forall le a b c va v, eval_condexpr le a va -> eval_condexpr le (if va then b else c) v -> @@ -495,7 +495,7 @@ with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist := with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr := match a with - | CEcond c al => CEcond c (lift_exprlist p al) + | CEcond c expected al => CEcond c expected (lift_exprlist p al) | CEcondition a b c => CEcondition (lift_condexpr p a) (lift_condexpr p b) (lift_condexpr p c) | CElet a b => CElet (lift_expr p a) (lift_condexpr (S p) b) end. diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v index 92ec45f2..8945cecf 100644 --- a/backend/Cminortyping.v +++ b/backend/Cminortyping.v @@ -64,6 +64,7 @@ Definition type_binop (op: binary_operation) : typ * typ * typ := | Ocmpf _ => (Tfloat, Tfloat, Tint) | Ocmpfs _ => (Tsingle, Tsingle, Tint) | Ocmpl _ | Ocmplu _ => (Tlong, Tlong, Tint) + | Oexpect ty => (ty, ty, ty) end. Module RTLtypes <: TYPE_ALGEBRA. diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml index 8905e252..c73bf30d 100644 --- a/backend/JsonAST.ml +++ b/backend/JsonAST.ml @@ -31,7 +31,7 @@ let pp_section pp sec = pp_jobject_end pp in match sec with | Section_text -> pp_simple "Text" - | Section_data init -> pp_complex "Data" init + | Section_data(init, thread_local) -> pp_complex "Data" init (* FIXME *) | Section_small_data init -> pp_complex "Small Data" init | Section_const init -> pp_complex "Const" init | Section_small_const init -> pp_complex "Small Const" init diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 155f5e55..0635e32d 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -121,7 +121,7 @@ module Printer(Target:TARGET) = let sec = match C2C.atom_sections name with | [s] -> s - | _ -> Section_data true + | _ -> Section_data (true, false) and align = match C2C.atom_alignof name with | Some a -> a diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index d82e6f84..7fa10aee 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -111,6 +111,10 @@ let elf_symbol_offset oc (symb, ofs) = if ofs <> 0L then fprintf oc " + %Ld" ofs (* Functions for fun and var info *) +let elf_text_print_fun_info oc name = + fprintf oc " .type %s, @function\n" name; + fprintf oc " .size %s, . - %s\n" name name + let elf_print_fun_info oc name = fprintf oc " .type %a, @function\n" elf_symbol name; fprintf oc " .size %a, . - %a\n" elf_symbol name elf_symbol name @@ -303,6 +307,7 @@ let print_version_and_options oc comment = fprintf oc " %s" Commandline.argv.(i) done; fprintf oc "\n" + (** Get the name of the common section if it is used otherwise the given section name, with bss as default *) @@ -310,4 +315,84 @@ let common_section ?(sec = ".bss") () = if !Clflags.option_fcommon then "COMM" else - sec + sec;; + +(* Profiling *) +let profiling_table : (Digest.t, int) Hashtbl.t = Hashtbl.create 1000;; +let next_profiling_position = ref 0;; +let profiling_position (x : Digest.t) : int = + match Hashtbl.find_opt profiling_table x with + | None -> let y = !next_profiling_position in + next_profiling_position := succ y; + Hashtbl.replace profiling_table x y; + y + | Some y -> y;; + +let profiling_ids () = + let nr_items = !next_profiling_position in + let ar = Array.make nr_items "" in + Hashtbl.iter + (fun x y -> ar.(y) <- x) + profiling_table; + ar;; + +let print_profiling_id oc id = + assert (String.length id = 16); + output_string oc " .byte"; + for i=0 to 15 do + fprintf oc " 0x%02x" (Char.code (String.get id i)); + if i < 15 then output_char oc ',' + done; + output_char oc '\n';; + +let profiling_counter_table_name = ".compcert_profiling_counters" +and profiling_id_table_name = ".compcert_profiling_ids" +and profiling_write_table = ".compcert_profiling_save_for_this_object" +and profiling_init = ".compcert_profiling_init" +and profiling_write_table_helper = "_compcert_write_profiling_table" +and dtor_section = ".dtors.65435,\"aw\",@progbits" +(* and fini_section = ".fini_array_00100,\"aw\"" *) +and init_section = ".init_array,\"aw\"";; + +type finalizer_call_method = + | Dtors + | Init_atexit of (out_channel -> string -> unit);; + +let write_symbol_pointer oc sym = + if Archi.ptr64 + then fprintf oc " .8byte %s\n" sym + else fprintf oc " .4byte %s\n" sym;; + +let print_profiling_epilogue declare_function finalizer_call_method print_profiling_stub oc = + if !Clflags.option_profile_arcs + then + let nr_items = !next_profiling_position in + if nr_items > 0 + then + begin + fprintf oc " .lcomm %s, %d\n" + profiling_counter_table_name (nr_items * 16); + fprintf oc " .section .rodata\n"; + fprintf oc "%s:\n" profiling_id_table_name; + Array.iter (print_profiling_id oc) (profiling_ids ()); + fprintf oc " .text\n"; + fprintf oc "%s:\n" profiling_write_table; + print_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name; + declare_function oc profiling_write_table; + match finalizer_call_method with + | Dtors -> + fprintf oc " .section %s\n" dtor_section; + write_symbol_pointer oc profiling_write_table + | Init_atexit(atexit_call) -> + fprintf oc " .section %s\n" init_section; + write_symbol_pointer oc profiling_init; + fprintf oc " .text\n"; + fprintf oc "%s:\n" profiling_init; + atexit_call oc profiling_write_table; + declare_function oc profiling_init + end;; + +let profiling_offset id kind = + ((profiling_position id)*2 + kind)*8;; diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index c9a6d399..051225a4 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -34,6 +34,7 @@ let precedence = function | Ebinop((Oadd|Osub|Oaddf|Osubf|Oaddfs|Osubfs|Oaddl|Osubl), _, _) -> (12, LtoR) | Ebinop((Oshl|Oshr|Oshru|Oshll|Oshrl|Oshrlu), _, _) -> (11, LtoR) | Ebinop((Ocmp _|Ocmpu _|Ocmpf _|Ocmpfs _|Ocmpl _|Ocmplu _), _, _) -> (10, LtoR) + | Ebinop((Oexpect _), _, _) -> (9, LtoR) | Ebinop((Oand|Oandl), _, _) -> (8, LtoR) | Ebinop((Oxor|Oxorl), _, _) -> (7, LtoR) | Ebinop((Oor|Oorl), _, _) -> (6, LtoR) @@ -89,6 +90,7 @@ let comparison_name = function | Cge -> ">=" let name_of_binop = function + | Oexpect _ -> "expect" | Oadd -> "+" | Osub -> "-" | Omul -> "*" diff --git a/backend/Profiling.v b/backend/Profiling.v new file mode 100644 index 00000000..4cba49ee --- /dev/null +++ b/backend/Profiling.v @@ -0,0 +1,65 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. + +Local Open Scope positive. + +Parameter function_id : function -> AST.profiling_id. +Parameter branch_id : AST.profiling_id -> node -> AST.profiling_id. + +Section PER_FUNCTION_ID. + Variable f_id : AST.profiling_id. + + Definition inject_profiling_call (prog : code) + (pc extra_pc ifso ifnot : node) : node * code := + let id := branch_id f_id pc in + let extra_pc' := Pos.succ extra_pc in + let prog' := PTree.set extra_pc + (Ibuiltin (EF_profiling id 0%Z) nil BR_none ifnot) prog in + let prog'':= PTree.set extra_pc' + (Ibuiltin (EF_profiling id 1%Z) nil BR_none ifso) prog' in + (Pos.succ extra_pc', prog''). + + Definition inject_at (prog : code) (pc extra_pc : node) : node * code := + match PTree.get pc prog with + | Some (Icond cond args ifso ifnot expected) => + inject_profiling_call + (PTree.set pc + (Icond cond args (Pos.succ extra_pc) extra_pc expected) prog) + pc extra_pc ifso ifnot + | _ => inject_profiling_call prog pc extra_pc 1 1 (* does not happen *) + end. + + Definition inject_at' (already : node * code) pc := + let (extra_pc, prog) := already in + inject_at prog pc extra_pc. + + Definition inject_l (prog : code) extra_pc injections := + List.fold_left (fun already (inject_pc : node) => + inject_at' already inject_pc) + injections + (extra_pc, prog). + + Definition gen_conditions (prog : code) := + List.map fst (PTree.elements (PTree.filter1 + (fun instr => + match instr with + | Icond cond args ifso ifnot expected => true + | _ => false + end) prog)). +End PER_FUNCTION_ID. + +Definition transf_function (f : function) : function := + let max_pc := max_pc_function f in + let conditions := gen_conditions (fn_code f) in + {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := snd (inject_l (function_id f) (fn_code f) (Pos.succ max_pc) conditions); + fn_entrypoint := f.(fn_entrypoint) |}. + +Definition transf_fundef (fd: fundef) : fundef := + AST.transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. diff --git a/backend/ProfilingExploit.v b/backend/ProfilingExploit.v new file mode 100644 index 00000000..cfca1a12 --- /dev/null +++ b/backend/ProfilingExploit.v @@ -0,0 +1,30 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. + +Local Open Scope positive. + +Parameter function_id : function -> AST.profiling_id. +Parameter branch_id : AST.profiling_id -> node -> AST.profiling_id. +Parameter condition_oracle : AST.profiling_id -> option bool. + +Definition transf_instr (f_id : AST.profiling_id) + (pc : node) (i : instruction) : instruction := + match i with + | Icond cond args ifso ifnot None => + Icond cond args ifso ifnot (condition_oracle (branch_id f_id pc)) + | _ => i + end. + +Definition transf_function (f : function) : function := + {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := PTree.map (transf_instr (function_id f)) f.(fn_code); + fn_entrypoint := f.(fn_entrypoint) |}. + +Definition transf_fundef (fd: fundef) : fundef := + AST.transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. diff --git a/backend/ProfilingExploitproof.v b/backend/ProfilingExploitproof.v new file mode 100644 index 00000000..bc68c38e --- /dev/null +++ b/backend/ProfilingExploitproof.v @@ -0,0 +1,224 @@ +Require Import FunInd. +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import ProfilingExploit. + + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof (Genv.find_funct_transf TRANSL). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + Genv.find_funct_ptr tge v = Some (transf_fundef f). +Proof (Genv.find_funct_ptr_transf TRANSL). + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (Genv.find_symbol_transf TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf TRANSL). + +Lemma sig_preserved: + forall f, funsig (transf_fundef f) = funsig f. +Proof. + destruct f; reflexivity. +Qed. + +Lemma find_function_translated: + forall ros rs fd, + find_function ge ros rs = Some fd -> + find_function tge ros rs = Some (transf_fundef fd). +Proof. + unfold find_function; intros. destruct ros as [r|id]. + eapply functions_translated; eauto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence. + eapply function_ptr_translated; eauto. +Qed. + +Lemma transf_function_at: + forall f pc i, + f.(fn_code)!pc = Some i -> + (transf_function f).(fn_code)!pc = Some(transf_instr (function_id f) pc i). +Proof. + intros until i. intro Hcode. + unfold transf_function; simpl. + rewrite PTree.gmap. + unfold option_map. + rewrite Hcode. + reflexivity. +Qed. + +Ltac TR_AT := + match goal with + | [ A: (fn_code _)!_ = Some _ |- _ ] => + generalize (transf_function_at _ _ _ A); intros + end. + + +Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := + | match_frames_intro: forall res f sp pc rs, + match_frames (Stackframe res f sp pc rs) + (Stackframe res (transf_function f) sp pc rs). + +Inductive match_states: RTL.state -> RTL.state -> Prop := + | match_regular_states: forall stk f sp pc rs m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (State stk f sp pc rs m) + (State stk' (transf_function f) sp pc rs m) + | match_callstates: forall stk f args m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Callstate stk f args m) + (Callstate stk' (transf_fundef f) args m) + | match_returnstates: forall stk v m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Returnstate stk v m) + (Returnstate stk' v m). + +Lemma step_simulation: + forall S1 t S2, RTL.step ge S1 t S2 -> + forall S1', match_states S1 S1' -> + exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. +Proof. + induction 1; intros S1' MS; inv MS; try TR_AT. +- (* nop *) + econstructor; split. eapply exec_Inop; eauto. + constructor; auto. +- (* op *) + econstructor; split. + eapply exec_Iop with (v := v); eauto. + rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. + constructor; auto. +(* load *) +- econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. + constructor; auto. +- (* load notrap1 *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = None). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap1; eauto. + constructor; auto. +- (* load notrap2 *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap2; eauto. + constructor; auto. +- (* store *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Istore; eauto. + constructor; auto. +(* call *) +- econstructor; split. + eapply exec_Icall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + constructor. constructor; auto. constructor. +(* tailcall *) +- econstructor; split. + eapply exec_Itailcall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + constructor. auto. +(* builtin *) +- econstructor; split. + eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. +(* cond *) +- destruct predb. + + econstructor; split. + eapply exec_Icond; eauto. + constructor; auto. + + simpl transf_instr in H1. + destruct condition_oracle in H1. + * econstructor; split. + eapply exec_Icond; eauto. + constructor; auto. + * econstructor; split. + eapply exec_Icond; eauto. + constructor; auto. +(* jumptbl *) +- econstructor; split. + eapply exec_Ijumptable; eauto. + constructor; auto. +(* return *) +- econstructor; split. + eapply exec_Ireturn; eauto. + constructor; auto. +(* internal function *) +- simpl. econstructor; split. + eapply exec_function_internal; eauto. + constructor; auto. +(* external function *) +- econstructor; split. + eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. +(* return *) +- inv STACKS. inv H1. + econstructor; split. + eapply exec_return; eauto. + constructor; auto. +Qed. + +Lemma transf_initial_states: + forall S1, RTL.initial_state prog S1 -> + exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. +Proof. + intros. inv H. econstructor; split. + econstructor. + eapply (Genv.init_mem_transf TRANSL); eauto. + rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto. + eapply function_ptr_translated; eauto. + rewrite <- H3; apply sig_preserved. + constructor. constructor. +Qed. + +Lemma transf_final_states: + forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). +Proof. + eapply forward_simulation_step. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + exact step_simulation. +Qed. + +End PRESERVATION. diff --git a/backend/Profilingaux.ml b/backend/Profilingaux.ml new file mode 100644 index 00000000..f8fc5d6b --- /dev/null +++ b/backend/Profilingaux.ml @@ -0,0 +1,71 @@ +open Camlcoq +open RTL +open Maps + +type identifier = Digest.t + +let pp_id channel (x : identifier) = + assert(String.length x = 16); + for i=0 to 15 do + Printf.fprintf channel "%02x" (Char.code (String.get x i)) + done + +let print_anonymous_function pp f = + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.fn_code)) in + PrintRTL.print_succ pp f.fn_entrypoint + (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1); + List.iter (PrintRTL.print_instruction pp) instrs; + Printf.fprintf pp "}\n\n" + +let function_id (f : coq_function) : identifier = + let digest = Digest.string (Marshal.to_string f []) in + Printf.fprintf stderr "FUNCTION hash = %a\n" pp_id digest; + print_anonymous_function stderr f; + digest + +let branch_id (f_id : identifier) (node : P.t) : identifier = + Digest.string (f_id ^ (Int64.to_string (P.to_int64 node)));; + +let profiling_counts : (identifier, (Int64.t*Int64.t)) Hashtbl.t = Hashtbl.create 1000;; + +let get_counts id = + match Hashtbl.find_opt profiling_counts id with + | Some x -> x + | None -> (0L, 0L);; + +let add_profiling_counts id counter0 counter1 = + let (old0, old1) = get_counts id in + Hashtbl.replace profiling_counts id (Int64.add old0 counter0, + Int64.add old1 counter1);; + +let input_counter (ic : in_channel) : Int64.t = + let r = ref Int64.zero in + for i=0 to 7 + do + r := Int64.add !r (Int64.shift_left (Int64.of_int (input_byte ic)) (8*i)) + done; + !r;; + +let load_profiling_info (filename : string) : unit = + let ic = open_in filename in + try + while true do + let id : identifier = really_input_string ic 16 in + let counter0 = input_counter ic in + let counter1 = input_counter ic in + (* Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id counter0 counter1 *) + add_profiling_counts id counter0 counter1 + done + with End_of_file -> close_in ic;; + +let condition_oracle (id : identifier) : bool option = + let (count0, count1) = get_counts id in + ( (* if count0 <> 0L || count1 <> 0L then *) + Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id count0 count1); + if count0 = count1 then None + else Some(count1 > count0);; diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v new file mode 100644 index 00000000..fc04c77e --- /dev/null +++ b/backend/Profilingproof.v @@ -0,0 +1,687 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import Profiling. +Require Import Lia. + +Local Open Scope positive. + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof (Genv.find_funct_transf TRANSL). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + Genv.find_funct_ptr tge v = Some (transf_fundef f). +Proof (Genv.find_funct_ptr_transf TRANSL). + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (Genv.find_symbol_transf TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf TRANSL). + +Lemma sig_preserved: + forall f, funsig (transf_fundef f) = funsig f. +Proof. + destruct f; reflexivity. +Qed. + +Lemma find_function_translated: + forall ros rs fd, + find_function ge ros rs = Some fd -> + find_function tge ros rs = Some (transf_fundef fd). +Proof. + unfold find_function; intros. destruct ros as [r|id]. + eapply functions_translated; eauto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence. + eapply function_ptr_translated; eauto. +Qed. + +Lemma pair_expand: + forall { A B : Type } (p : A*B), + p = ((fst p), (snd p)). +Proof. + destruct p; simpl; trivial. +Qed. + +Lemma inject_profiling_call_preserves: + forall id body pc extra_pc ifso ifnot pc0, + pc0 < extra_pc -> + PTree.get pc0 (snd (inject_profiling_call id body pc extra_pc ifso ifnot)) = PTree.get pc0 body. +Proof. + intros. simpl. + rewrite PTree.gso by lia. + apply PTree.gso. + lia. +Qed. + +Lemma inject_at_preserves : + forall id body pc extra_pc pc0, + pc0 < extra_pc -> + pc0 <> pc -> + PTree.get pc0 (snd (inject_at id body pc extra_pc)) = PTree.get pc0 body. +Proof. + intros. unfold inject_at. + destruct (PTree.get pc body) eqn:GET. + - destruct i. + all: try (rewrite inject_profiling_call_preserves; trivial; fail). + rewrite inject_profiling_call_preserves by trivial. + apply PTree.gso; lia. + - apply inject_profiling_call_preserves; trivial. +Qed. + +Lemma inject_profiling_call_increases: + forall id body pc extra_pc ifso ifnot, + fst (inject_profiling_call id body pc extra_pc ifso ifnot) = extra_pc + 2. +Proof. + intros. + simpl. + lia. +Qed. + +Lemma inject_at_increases: + forall id body pc extra_pc, + (fst (inject_at id body pc extra_pc)) = extra_pc + 2. +Proof. + intros. unfold inject_at. + destruct (PTree.get pc body). + - destruct i; apply inject_profiling_call_increases. + - apply inject_profiling_call_increases. +Qed. + +Lemma inject_l_preserves : + forall id injections body extra_pc pc0, + pc0 < extra_pc -> + List.forallb (fun injection => if peq injection pc0 then false else true) injections = true -> + PTree.get pc0 (snd (inject_l id body extra_pc injections)) = PTree.get pc0 body. +Proof. + induction injections; + intros until pc0; intros BEFORE ALL; simpl; trivial. + unfold inject_l. + simpl in ALL. + rewrite andb_true_iff in ALL. + destruct ALL as [NEQ ALL]. + simpl. + rewrite pair_expand with (p := inject_at id body a extra_pc). + progress fold (inject_l id (snd (inject_at id body a extra_pc)) + (fst (inject_at id body a extra_pc)) + injections). + rewrite IHinjections; trivial. + - apply inject_at_preserves; trivial. + destruct (peq a pc0); congruence. + - rewrite inject_at_increases. + lia. +Qed. + +Fixpoint inject_l_position extra_pc + (injections : list node) + (k : nat) {struct injections} : node := + match injections with + | nil => extra_pc + | pc::l' => + match k with + | O => extra_pc + | S k' => inject_l_position (extra_pc + 2) l' k' + end + end. + +Lemma inject_l_position_increases : forall injections pc k, + pc <= inject_l_position pc injections k. +Proof. + induction injections; simpl; intros. + lia. + destruct k. + lia. + specialize IHinjections with (pc := pc + 2) (k := k). + lia. +Qed. + +Lemma inject_l_injected_pc: + forall f_id injections cond args ifso ifnot expected body injnum pc extra_pc + (INSTR : body ! pc = Some (Icond cond args ifso ifnot expected)) + (BELOW : forallb (fun pc => pc <? extra_pc) injections = true) + (NOREPET : list_norepet injections) + (NUMBER : nth_error injections injnum = Some pc), + PTree.get pc (snd (inject_l f_id body extra_pc injections)) = + Some (Icond cond args + (Pos.succ (inject_l_position extra_pc injections injnum)) + (inject_l_position extra_pc injections injnum) expected). +Proof. + induction injections; simpl; intros. + { rewrite nth_error_nil in NUMBER. + discriminate NUMBER. } + simpl in BELOW. + rewrite andb_true_iff in BELOW. + destruct BELOW as [BELOW1 BELOW2]. + rewrite Pos.ltb_lt in BELOW1. + unfold inject_l. + simpl fold_left. + rewrite pair_expand with (p := inject_at f_id body a extra_pc). + progress fold (inject_l f_id (snd (inject_at f_id body a extra_pc)) + (fst (inject_at f_id body a extra_pc)) + injections). + destruct injnum as [ | injnum']; simpl in NUMBER. + { inv NUMBER. + rewrite inject_l_preserves; simpl. + - unfold inject_at. + rewrite INSTR. + unfold inject_profiling_call. simpl. + rewrite PTree.gso by lia. + rewrite PTree.gso by lia. + apply PTree.gss. + - rewrite inject_at_increases. + lia. + - inv NOREPET. + rewrite forallb_forall. + intros x IN. + destruct peq as [EQ | ]; trivial. + subst x. + contradiction. + } + simpl. + rewrite inject_at_increases. + apply IHinjections with (ifso := ifso) (ifnot := ifnot). + - rewrite inject_at_preserves; trivial. + + rewrite forallb_forall in BELOW2. + rewrite <- Pos.ltb_lt. + apply nth_error_In in NUMBER. + auto. + + inv NOREPET. + intro ZZZ. + subst a. + apply nth_error_In in NUMBER. + auto. + + - rewrite forallb_forall in BELOW2. + rewrite forallb_forall. + intros. + specialize BELOW2 with x. + rewrite Pos.ltb_lt in *. + intuition lia. + - inv NOREPET. trivial. + - trivial. +Qed. + +Lemma inject_l_injected0: + forall f_id cond args ifso ifnot expected injections body injnum pc extra_pc + (INSTR : body ! pc = Some (Icond cond args ifso ifnot expected)) + (BELOW : forallb (fun pc => pc <? extra_pc) injections = true) + (NOREPET : list_norepet injections) + (NUMBER : nth_error injections injnum = Some pc), + PTree.get (inject_l_position extra_pc injections injnum) + (snd (inject_l f_id body extra_pc injections)) = + Some (Ibuiltin (EF_profiling (branch_id f_id pc) 0%Z) nil BR_none ifnot). +Proof. + induction injections; intros. + { rewrite nth_error_nil in NUMBER. + discriminate NUMBER. } + simpl in BELOW. + rewrite andb_true_iff in BELOW. + destruct BELOW as [BELOW1 BELOW2]. + unfold inject_l. + simpl fold_left. + rewrite pair_expand with (p := inject_at f_id body a extra_pc). + progress fold (inject_l f_id (snd (inject_at f_id body a extra_pc)) + (fst (inject_at f_id body a extra_pc)) + injections). + destruct injnum as [ | injnum']; simpl in NUMBER. + { inv NUMBER. + rewrite inject_l_preserves; simpl. + - unfold inject_at. + rewrite INSTR. + unfold inject_profiling_call. simpl. + rewrite PTree.gso by lia. + apply PTree.gss. + - rewrite inject_at_increases. + lia. + - rewrite forallb_forall. + rewrite forallb_forall in BELOW2. + intros loc IN. + specialize BELOW2 with loc. + apply BELOW2 in IN. + destruct peq as [EQ | ]; trivial. + rewrite EQ in IN. + rewrite Pos.ltb_lt in IN. + lia. + } + simpl. + rewrite inject_at_increases. + + apply IHinjections. + - rewrite inject_at_preserves; trivial. + + rewrite forallb_forall in BELOW2. + rewrite <- Pos.ltb_lt. + apply nth_error_In in NUMBER. + auto. + + inv NOREPET. + intro ZZZ. + subst a. + apply nth_error_In in NUMBER. + auto. + + - rewrite forallb_forall in BELOW2. + rewrite forallb_forall. + intros. + specialize BELOW2 with x. + rewrite Pos.ltb_lt in *. + intuition lia. + - inv NOREPET. trivial. + - trivial. +Qed. + +Lemma inject_l_injected1: + forall f_id cond args ifso ifnot expected injections body injnum pc extra_pc + (INSTR : body ! pc = Some (Icond cond args ifso ifnot expected)) + (BELOW : forallb (fun pc => pc <? extra_pc) injections = true) + (NOREPET : list_norepet injections) + (NUMBER : nth_error injections injnum = Some pc), + PTree.get (Pos.succ (inject_l_position extra_pc injections injnum)) + (snd (inject_l f_id body extra_pc injections)) = + Some (Ibuiltin (EF_profiling (branch_id f_id pc) 1%Z) nil BR_none ifso). +Proof. + induction injections; intros. + { rewrite nth_error_nil in NUMBER. + discriminate NUMBER. } + simpl in BELOW. + rewrite andb_true_iff in BELOW. + destruct BELOW as [BELOW1 BELOW2]. + unfold inject_l. + simpl fold_left. + rewrite pair_expand with (p := inject_at f_id body a extra_pc). + progress fold (inject_l f_id (snd (inject_at f_id body a extra_pc)) + (fst (inject_at f_id body a extra_pc)) + injections). + destruct injnum as [ | injnum']; simpl in NUMBER. + { inv NUMBER. + rewrite inject_l_preserves; simpl. + - unfold inject_at. + rewrite INSTR. + unfold inject_profiling_call. simpl. + apply PTree.gss. + - rewrite inject_at_increases. + lia. + - rewrite forallb_forall. + rewrite forallb_forall in BELOW2. + intros loc IN. + specialize BELOW2 with loc. + apply BELOW2 in IN. + destruct peq as [EQ | ]; trivial. + rewrite EQ in IN. + rewrite Pos.ltb_lt in IN. + lia. + } + simpl. + rewrite inject_at_increases. + + apply IHinjections. + - rewrite inject_at_preserves; trivial. + + rewrite forallb_forall in BELOW2. + rewrite <- Pos.ltb_lt. + apply nth_error_In in NUMBER. + auto. + + inv NOREPET. + intro ZZZ. + subst a. + apply nth_error_In in NUMBER. + auto. + + - rewrite forallb_forall in BELOW2. + rewrite forallb_forall. + intros. + specialize BELOW2 with x. + rewrite Pos.ltb_lt in *. + intuition lia. + - inv NOREPET. trivial. + - trivial. +Qed. + +Lemma transf_function_at: + forall f pc i + (CODE : f.(fn_code)!pc = Some i) + (INSTR : match i with + | Icond _ _ _ _ _ => False + | _ => True + end), + (transf_function f).(fn_code)!pc = Some i. +Proof. + intros. + unfold transf_function; simpl. + rewrite inject_l_preserves. + assumption. + - pose proof (max_pc_function_sound f pc i CODE) as LE. + unfold Ple in LE. + lia. + - rewrite forallb_forall. + intros x IN. + destruct peq; trivial. + subst x. + unfold gen_conditions in IN. + rewrite in_map_iff in IN. + destruct IN as [[pc' i'] [EQ IN]]. + simpl in EQ. + subst pc'. + apply PTree.elements_complete in IN. + rewrite PTree.gfilter1 in IN. + rewrite CODE in IN. + destruct i; try discriminate; contradiction. +Qed. + +Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := +| match_frames_intro: forall res f sp pc rs, + match_frames (Stackframe res f sp pc rs) + (Stackframe res (transf_function f) sp pc rs). + +Inductive match_states: RTL.state -> RTL.state -> Prop := + | match_regular_states: forall stk f sp pc rs m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (State stk f sp pc rs m) + (State stk' (transf_function f) sp pc rs m) + | match_callstates: forall stk f args m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Callstate stk f args m) + (Callstate stk' (transf_fundef f) args m) + | match_returnstates: forall stk v m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Returnstate stk v m) + (Returnstate stk' v m). + +Lemma funsig_preserved: + forall fd, + funsig (transf_fundef fd) = funsig fd. +Proof. + destruct fd; simpl; trivial. +Qed. + +Lemma stacksize_preserved: + forall f, + fn_stacksize (transf_function f) = fn_stacksize f. +Proof. + destruct f; simpl; trivial. +Qed. + +Hint Resolve symbols_preserved funsig_preserved external_call_symbols_preserved senv_preserved stacksize_preserved : profiling. + +Lemma step_simulation: + forall s1 t s2 (STEP : step ge s1 t s2) + s1' (MS: match_states s1 s1'), + exists s2', plus step tge s1' t s2' /\ match_states s2 s2'. +Proof. + induction 1; intros; inv MS. + - econstructor; split. + + apply plus_one. apply exec_Inop. + erewrite transf_function_at; eauto. apply I. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_Iop with (op:=op) (args:=args). + * erewrite transf_function_at; eauto. apply I. + * rewrite eval_operation_preserved with (ge1:=ge); + eauto with profiling. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_Iload with (trap:=trap) (chunk:=chunk) + (addr:=addr) (args:=args) (a:=a). + erewrite transf_function_at; eauto. apply I. + rewrite eval_addressing_preserved with (ge1:=ge). + all: eauto with profiling. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_Iload_notrap1 with (chunk:=chunk) + (addr:=addr) (args:=args). + erewrite transf_function_at; eauto. apply I. + rewrite eval_addressing_preserved with (ge1:=ge). + all: eauto with profiling. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_Iload_notrap2 with (chunk:=chunk) + (addr:=addr) (args:=args) (a:=a). + erewrite transf_function_at; eauto. apply I. + rewrite eval_addressing_preserved with (ge1:=ge). + all: eauto with profiling. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_Istore with (chunk:=chunk) (src := src) + (addr:=addr) (args:=args) (a:=a). + erewrite transf_function_at; eauto. apply I. + rewrite eval_addressing_preserved with (ge1:=ge). + all: eauto with profiling. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_Icall with (sig:=(funsig fd)) (ros:=ros). + erewrite transf_function_at; eauto. apply I. + apply find_function_translated with (fd := fd). + all: eauto with profiling. + + constructor; auto. + constructor; auto. + constructor. + - econstructor; split. + + apply plus_one. apply exec_Itailcall with (sig:=(funsig fd)) (ros:=ros). + erewrite transf_function_at; eauto. apply I. + apply find_function_translated with (fd := fd). + all: eauto with profiling. + + constructor; auto. + - econstructor; split. + + apply plus_one. + apply exec_Ibuiltin with (ef:=ef) (args:=args) (vargs:=vargs). + erewrite transf_function_at; eauto. apply I. + apply eval_builtin_args_preserved with (ge1:=ge). + all: eauto with profiling. + + constructor; auto. + - destruct b. + + assert (In pc (gen_conditions (fn_code f))) as IN. + { unfold gen_conditions. + rewrite in_map_iff. + exists (pc, (Icond cond args ifso ifnot predb)). + split; simpl; trivial. + apply PTree.elements_correct. + rewrite PTree.gfilter1. + rewrite H. + reflexivity. + } + apply In_nth_error in IN. + destruct IN as [n IN]. + econstructor; split. + * eapply plus_two. + ++ eapply exec_Icond with (cond := cond) (args := args) (predb := predb) (b := true). + unfold transf_function. simpl. + erewrite inject_l_injected_pc with (cond := cond) (args := args). + ** reflexivity. + ** eassumption. + ** unfold gen_conditions. + rewrite forallb_forall. + intros x INx. + rewrite in_map_iff in INx. + destruct INx as [[x' i'] [EQ INx]]. + simpl in EQ. + subst x'. + apply PTree.elements_complete in INx. + rewrite PTree.gfilter1 in INx. + assert (x <= max_pc_function f) as MAX. + { destruct ((fn_code f) ! x) eqn:CODEx. + 2: discriminate. + apply max_pc_function_sound with (i:=i). + assumption. + } + rewrite Pos.ltb_lt. + lia. + ** unfold gen_conditions. + apply PTree.elements_keys_norepet. + ** exact IN. + ** assumption. + ** reflexivity. + ++ apply exec_Ibuiltin with (ef := (EF_profiling (branch_id (function_id f) pc) 1%Z)) (args := nil) (vargs := nil). + apply inject_l_injected1 with (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot) (expected := predb). + ** exact H. + ** unfold gen_conditions. + rewrite forallb_forall. + intros x INx. + rewrite in_map_iff in INx. + destruct INx as [[x' i'] [EQ INx]]. + simpl in EQ. + subst x'. + apply PTree.elements_complete in INx. + rewrite PTree.gfilter1 in INx. + assert (x <= max_pc_function f) as MAX. + { destruct ((fn_code f) ! x) eqn:CODEx. + 2: discriminate. + apply max_pc_function_sound with (i:=i). + assumption. + } + rewrite Pos.ltb_lt. + lia. + ** unfold gen_conditions. + apply PTree.elements_keys_norepet. + ** exact IN. + ** constructor. + ** constructor. + ++ reflexivity. + * simpl. constructor; auto. + + + assert (In pc (gen_conditions (fn_code f))) as IN. + { unfold gen_conditions. + rewrite in_map_iff. + exists (pc, (Icond cond args ifso ifnot predb)). + split; simpl; trivial. + apply PTree.elements_correct. + rewrite PTree.gfilter1. + rewrite H. + reflexivity. + } + apply In_nth_error in IN. + destruct IN as [n IN]. + econstructor; split. + * eapply plus_two. + ++ eapply exec_Icond with (cond := cond) (args := args) (predb := predb) (b := false). + unfold transf_function. simpl. + erewrite inject_l_injected_pc with (cond := cond) (args := args). + ** reflexivity. + ** eassumption. + ** unfold gen_conditions. + rewrite forallb_forall. + intros x INx. + rewrite in_map_iff in INx. + destruct INx as [[x' i'] [EQ INx]]. + simpl in EQ. + subst x'. + apply PTree.elements_complete in INx. + rewrite PTree.gfilter1 in INx. + assert (x <= max_pc_function f) as MAX. + { destruct ((fn_code f) ! x) eqn:CODEx. + 2: discriminate. + apply max_pc_function_sound with (i:=i). + assumption. + } + rewrite Pos.ltb_lt. + lia. + ** unfold gen_conditions. + apply PTree.elements_keys_norepet. + ** exact IN. + ** assumption. + ** reflexivity. + ++ apply exec_Ibuiltin with (ef := (EF_profiling (branch_id (function_id f) pc) 0%Z)) (args := nil) (vargs := nil). + apply inject_l_injected0 with (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot) (expected := predb). + ** exact H. + ** unfold gen_conditions. + rewrite forallb_forall. + intros x INx. + rewrite in_map_iff in INx. + destruct INx as [[x' i'] [EQ INx]]. + simpl in EQ. + subst x'. + apply PTree.elements_complete in INx. + rewrite PTree.gfilter1 in INx. + assert (x <= max_pc_function f) as MAX. + { destruct ((fn_code f) ! x) eqn:CODEx. + 2: discriminate. + apply max_pc_function_sound with (i:=i). + assumption. + } + rewrite Pos.ltb_lt. + lia. + ** unfold gen_conditions. + apply PTree.elements_keys_norepet. + ** exact IN. + ** constructor. + ** constructor. + ++ reflexivity. + * simpl. constructor; auto. + + - econstructor; split. + + apply plus_one. + apply exec_Ijumptable with (arg:=arg) (tbl:=tbl) (n:=n). + erewrite transf_function_at; eauto. apply I. + all: eauto with profiling. + + constructor; auto. + - econstructor; split. + + apply plus_one. + apply exec_Ireturn. + erewrite transf_function_at; eauto. apply I. + rewrite stacksize_preserved. eassumption. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_function_internal. + rewrite stacksize_preserved. eassumption. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_function_external. + eauto with profiling. + + constructor; auto. + - inv STACKS. inv H1. + econstructor; split. + + apply plus_one. apply exec_return. + + constructor; auto. +Qed. + +Lemma transf_initial_states: + forall S1, RTL.initial_state prog S1 -> + exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. +Proof. + intros. inv H. econstructor; split. + econstructor. + eapply (Genv.init_mem_transf TRANSL); eauto. + rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto. + eapply function_ptr_translated; eauto. + rewrite <- H3; apply sig_preserved. + constructor. constructor. +Qed. + +Lemma transf_final_states: + forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). +Proof. + eapply forward_simulation_plus. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + exact step_simulation. +Qed. + +End PRESERVATION. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index ac98f3a1..243d7b7c 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -477,9 +477,9 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) {struct a} : mon node := match a with - | CEcond c al => + | CEcond c expected al => do rl <- alloc_regs map al; - do nt <- add_instr (Icond c rl ntrue nfalse None); + do nt <- add_instr (Icond c rl ntrue nfalse expected); transl_exprlist map al rl nt | CEcondition a b c => do nc <- transl_condexpr map c ntrue nfalse; diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index e39d3b56..26688e23 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -41,7 +41,7 @@ and size_exprs = function | Econs(e1, el) -> size_expr e1 + size_exprs el and size_condexpr = function - | CEcond(c, args) -> size_exprs args + | CEcond(c, expected, args) -> size_exprs args | CEcondition(c1, c2, c3) -> 1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3 | CElet(a, c) -> diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index b94ec22f..e62aff22 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -799,11 +799,11 @@ Proof. Qed. Lemma transl_condexpr_CEcond_correct: - forall le cond al vl vb, + forall le cond expected al vl vb, eval_exprlist ge sp e m le al vl -> transl_exprlist_prop le al vl -> eval_condition cond vl m = Some vb -> - transl_condexpr_prop le (CEcond cond al) vb. + transl_condexpr_prop le (CEcond cond expected al) vb. Proof. intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 30ad7d82..36b8409d 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -744,10 +744,10 @@ Inductive tr_expr (c: code): with tr_condition (c: code): mapping -> list reg -> condexpr -> node -> node -> node -> Prop := - | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl i, + | tr_CEcond: forall map pr cond expected bl ns ntrue nfalse n1 rl i, tr_exprlist c map pr bl ns n1 rl -> c!n1 = Some (Icond cond rl ntrue nfalse i) -> - tr_condition c map pr (CEcond cond bl) ns ntrue nfalse + tr_condition c map pr (CEcond cond expected bl) ns ntrue nfalse | tr_CEcondition: forall map pr a1 a2 a3 ns ntrue nfalse n2 n3, tr_condition c map pr a1 ns n2 n3 -> tr_condition c map pr a2 n2 ntrue nfalse -> diff --git a/backend/Selection.v b/backend/Selection.v index 4ab3331e..342bd8ca 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -35,12 +35,13 @@ Local Open Scope error_monad_scope. (** Conversion of conditions *) -Function condexpr_of_expr (e: expr) : condexpr := +Function condexpr_of_expr (e: expr) (expected : option bool) : condexpr := match e with - | Eop (Ocmp c) el => CEcond c el - | Econdition a b c => CEcondition a (condexpr_of_expr b) (condexpr_of_expr c) - | Elet a b => CElet a (condexpr_of_expr b) - | _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil) + | Eop (Ocmp c) el => CEcond c expected el + | Econdition a b c => CEcondition a (condexpr_of_expr b expected) + (condexpr_of_expr c expected) + | Elet a b => CElet a (condexpr_of_expr b expected) + | _ => CEcond (Ccompuimm Cne Int.zero) expected (e ::: Enil) end. Function condition_of_expr (e: expr) : condition * exprlist := @@ -120,6 +121,7 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := match op with + | Cminor.Oexpect ty => arg1 | Cminor.Oadd => add arg1 arg2 | Cminor.Osub => sub arg1 arg2 | Cminor.Omul => mul arg1 arg2 @@ -166,7 +168,7 @@ Definition sel_select (ty: typ) (cnd ifso ifnot: expr) : expr := let (cond, args) := condition_of_expr cnd in match SelectOp.select ty cond args ifso ifnot with | Some a => a - | None => Econdition (condexpr_of_expr cnd) ifso ifnot + | None => Econdition (condexpr_of_expr cnd None) ifso ifnot end. (** Conversion from Cminor expression to Cminorsel expressions *) @@ -243,7 +245,8 @@ Definition sel_builtin_res (optid: option ident) : builtin_res ident := Function sel_known_builtin (bf: builtin_function) (args: exprlist) := match bf, args with | BI_platform b, _ => - SelectOp.platform_builtin b args + SelectOp.platform_builtin b args +(* | BI_standard BI_expect, a1 ::: a2 ::: Enil => Some a1 *) | BI_standard (BI_select ty), a1 ::: a2 ::: a3 ::: Enil => Some (sel_select ty a1 a2 a3) | BI_standard BI_fabs, a1 ::: Enil => @@ -291,16 +294,16 @@ Fixpoint sel_switch (arg: nat) (t: comptree): exitexpr := | CTaction act => XEexit act | CTifeq key act t' => - XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key)) + XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key) None) (XEexit act) (sel_switch arg t') | CTiflt key t1 t2 => - XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key)) + XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key) None) (sel_switch arg t1) (sel_switch arg t2) | CTjumptable ofs sz tbl t' => XElet (make_sub (Eletvar arg) ofs) - (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz)) + (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz) None) (XEjumptable (make_to_int (Eletvar O)) tbl) (sel_switch (S arg) t')) end. @@ -375,6 +378,22 @@ Definition if_conversion | _, _ => None end. +Definition extract_expect1 (e : Cminor.expr) : option bool := + match e with + | Cminor.Ebinop (Cminor.Oexpect ty) e1 (Cminor.Econst (Cminor.Ointconst c)) => + Some (if Int.eq_dec c Int.zero then false else true) + | Cminor.Ebinop (Cminor.Oexpect ty) e1 (Cminor.Econst (Cminor.Olongconst c)) => + Some (if Int64.eq_dec c Int64.zero then false else true) + | _ => None + end. + +Definition extract_expect (e : Cminor.expr) : option bool := + match e with + | Cminor.Ebinop (Cminor.Ocmpu Cne) e1 (Cminor.Econst (Cminor.Ointconst c)) => + if Int.eq_dec c Int.zero then extract_expect1 e1 else None + | _ => extract_expect1 e + end. + (** Conversion from Cminor statements to Cminorsel statements. *) Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt := @@ -402,8 +421,10 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt : match if_conversion ki env e ifso ifnot with | Some s => OK s | None => - do ifso' <- sel_stmt ki env ifso; do ifnot' <- sel_stmt ki env ifnot; - OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot') + do ifso' <- sel_stmt ki env ifso; + do ifnot' <- sel_stmt ki env ifnot; + OK (Sifthenelse (condexpr_of_expr (sel_expr e) + (extract_expect e)) ifso' ifnot') end | Cminor.Sloop body => do body' <- sel_stmt ki env body; OK (Sloop body') diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml index 26a79fd7..5a8bde8c 100644 --- a/backend/Selectionaux.ml +++ b/backend/Selectionaux.ml @@ -39,6 +39,7 @@ let cost_unop = function | Osingleoflong | Osingleoflongu -> assert false let cost_binop = function + | Oexpect _ -> 0 | Oadd | Osub -> 1 | Omul -> 2 | Odiv | Odivu | Omod | Omodu -> assert false diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index aa53c9cb..955c45a4 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -196,12 +196,12 @@ Variable e: env. Variable m: mem. Lemma eval_condexpr_of_expr: - forall a le v b, + forall expected a le v b, eval_expr tge sp e m le a v -> Val.bool_of_val v b -> - eval_condexpr tge sp e m le (condexpr_of_expr a) b. + eval_condexpr tge sp e m le (condexpr_of_expr a expected) b. Proof. - intros until a. functional induction (condexpr_of_expr a); intros. + intros until a. functional induction (condexpr_of_expr a expected); intros. (* compare *) inv H. econstructor; eauto. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto. @@ -310,46 +310,47 @@ Lemma eval_sel_binop: exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. - apply eval_add; auto. - apply eval_sub; auto. - apply eval_mul; auto. - eapply eval_divs; eauto. - eapply eval_divu; eauto. - eapply eval_mods; eauto. - eapply eval_modu; eauto. - apply eval_and; auto. - apply eval_or; auto. - apply eval_xor; auto. - apply eval_shl; auto. - apply eval_shr; auto. - apply eval_shru; auto. - apply eval_addf; auto. - apply eval_subf; auto. - apply eval_mulf; auto. - apply eval_divf; auto. - apply eval_addfs; auto. - apply eval_subfs; auto. - apply eval_mulfs; auto. - apply eval_divfs; auto. - eapply eval_addl; eauto. - eapply eval_subl; eauto. - eapply eval_mull; eauto. - eapply eval_divls; eauto. - eapply eval_divlu; eauto. - eapply eval_modls; eauto. - eapply eval_modlu; eauto. - eapply eval_andl; eauto. - eapply eval_orl; eauto. - eapply eval_xorl; eauto. - eapply eval_shll; eauto. - eapply eval_shrl; eauto. - eapply eval_shrlu; eauto. - apply eval_comp; auto. - apply eval_compu; auto. - apply eval_compf; auto. - apply eval_compfs; auto. - exists v; split; auto. eapply eval_cmpl; eauto. - exists v; split; auto. eapply eval_cmplu; eauto. + - exists v1; split; trivial. apply Val.lessdef_normalize. + - apply eval_add; auto. + - apply eval_sub; auto. + - apply eval_mul; auto. + - eapply eval_divs; eauto. + - eapply eval_divu; eauto. + - eapply eval_mods; eauto. + - eapply eval_modu; eauto. + - apply eval_and; auto. + - apply eval_or; auto. + - apply eval_xor; auto. + - apply eval_shl; auto. + - apply eval_shr; auto. + - apply eval_shru; auto. + - apply eval_addf; auto. + - apply eval_subf; auto. + - apply eval_mulf; auto. + - apply eval_divf; auto. + - apply eval_addfs; auto. + - apply eval_subfs; auto. + - apply eval_mulfs; auto. + - apply eval_divfs; auto. + - eapply eval_addl; eauto. + - eapply eval_subl; eauto. + - eapply eval_mull; eauto. + - eapply eval_divls; eauto. + - eapply eval_divlu; eauto. + - eapply eval_modls; eauto. + - eapply eval_modlu; eauto. + - eapply eval_andl; eauto. + - eapply eval_orl; eauto. + - eapply eval_xorl; eauto. + - eapply eval_shll; eauto. + - eapply eval_shrl; eauto. + - eapply eval_shrlu; eauto. + - apply eval_comp; auto. + - apply eval_compu; auto. + - apply eval_compf; auto. + - apply eval_compfs; auto. + - exists v; split; auto. eapply eval_cmpl; eauto. + - exists v; split; auto. eapply eval_cmplu; eauto. Qed. Lemma eval_sel_select: @@ -395,6 +396,13 @@ Proof. inv ARGS; try discriminate. inv H0; try discriminate. inv SEL. simpl in SEM; inv SEM. apply eval_absf; auto. + (* + (* expect *) + inv ARGS; try discriminate. + inv H0; try discriminate. + inv H2; try discriminate. + simpl in SEM. inv SEM. inv SEL. + destruct v1; destruct v0. + all: econstructor; split; eauto. *) - eapply eval_platform_builtin; eauto. Qed. diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index dfe42df0..0f240602 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +(* FIXME: expected branching information not propagated *) (** Instruction selection for 64-bit integer operations *) Require String. @@ -256,7 +257,7 @@ Definition cmpl_ne_zero (e: expr) := Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil)) (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))). @@ -278,7 +279,7 @@ Definition cmplu (c: comparison) (e1 e2: expr) := Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil)) (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))). diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bc5173ca..75f5eb3e 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -46,16 +46,29 @@ let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103 let atom_is_static a = try - (Hashtbl.find decl_atom a).a_storage = C.Storage_static + match (Hashtbl.find decl_atom a).a_storage with + | C.Storage_static | C.Storage_thread_local_static -> true + | _ -> false with Not_found -> false let atom_is_extern a = try - (Hashtbl.find decl_atom a).a_storage = C.Storage_extern + match (Hashtbl.find decl_atom a).a_storage with + | C.Storage_extern| C.Storage_thread_local_extern -> true + | _ -> false with Not_found -> false +let atom_is_thread_local a = + try + match (Hashtbl.find decl_atom a).a_storage with + | C.Storage_thread_local_extern| C.Storage_thread_local_static + | C.Storage_thread_local -> true + | _ -> false + with Not_found -> + false + let atom_alignof a = try (Hashtbl.find decl_atom a).a_alignment @@ -168,9 +181,10 @@ let ais_annot_functions = let builtins_generic = { builtin_typedefs = []; builtin_functions = - ais_annot_functions - @ + ais_annot_functions @ [ + "__builtin_expect", + (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false); (* Integer arithmetic *) "__builtin_bswap64", (TInt(IULongLong, []), [TInt(IULongLong, [])], false); @@ -899,6 +913,14 @@ let rec convertExpr env e = | C.ECompound(ty1, ie) -> unsupported "compound literals"; ezero + | C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, args) -> + (match args with + | [e1; e2] -> + ewrap (Ctyping.ebinop Cop.Oexpect (convertExpr env e1) (convertExpr env e2)) + | _ -> + error "__builtin_expect wants two arguments"; + ezero) + | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) when List.length args < 2 -> error "too few arguments to function call, expected at least 2, have 0"; ezero @@ -1236,7 +1258,8 @@ let convertFundef loc env fd = let vars = List.map (fun (sto, id, ty, init) -> - if sto = Storage_extern || sto = Storage_static then + if sto = Storage_extern || sto = Storage_thread_local_extern + || sto = Storage_static || sto = Storage_thread_local_static then unsupported "'static' or 'extern' local variable"; if init <> None then unsupported "initialized local variable"; @@ -1339,15 +1362,21 @@ let convertGlobvar loc env (sto, id, ty, optinit) = let init' = match optinit with | None -> - if sto = C.Storage_extern then [] else [AST.Init_space sz] + if sto = C.Storage_extern || sto = C.Storage_thread_local_extern + then [] else [AST.Init_space sz] | Some i -> convertInitializer env ty i in let (section, access) = - Sections.for_variable env loc id' ty (optinit <> None) in + Sections.for_variable env loc id' ty (optinit <> None) + (match sto with + | Storage_thread_local | Storage_thread_local_extern + | Storage_thread_local_static -> true + | _ -> false) in if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then error "'%s' is too big (%s bytes)" id.name (Z.to_string sz); - if sto <> C.Storage_extern && Cutil.incomplete_type env ty then + if sto <> C.Storage_extern && sto <> C.Storage_thread_local_extern + && Cutil.incomplete_type env ty then error "'%s' has incomplete type" id.name; Hashtbl.add decl_atom id' { a_storage = sto; @@ -1446,7 +1475,7 @@ let cleanupGlobals p = if IdentSet.mem fd.fd_name !strong then error "multiple definitions of %s" fd.fd_name.name; strong := IdentSet.add fd.fd_name !strong - | C.Gdecl(Storage_extern, id, ty, init) -> + | C.Gdecl((Storage_extern|Storage_thread_local_extern), id, ty, init) -> extern := IdentSet.add id !extern | C.Gdecl(sto, id, ty, Some i) -> if IdentSet.mem id !strong then @@ -1465,7 +1494,7 @@ let cleanupGlobals p = match g.gdesc with | C.Gdecl(sto, id, ty, init) -> let better_def_exists = - if sto = Storage_extern then + if sto = Storage_extern || sto = Storage_thread_local_extern then IdentSet.mem id !strong || IdentSet.mem id !weak else if init = None then IdentSet.mem id !strong diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index b08c3ad7..fbf9bbeb 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -509,6 +509,10 @@ Definition do_ef_debug (kind: positive) (text: ident) (targs: list typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := Some(w, E0, Vundef, m). +Definition do_ef_profiling (id : profiling_id) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + Some(w, E0, Vundef, m). + Definition do_builtin_or_external (name: string) (sg: signature) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match lookup_builtin_function name sg with @@ -531,6 +535,7 @@ Definition do_external (ef: external_function): | EF_annot_val kind text targ => do_ef_annot_val text targ | EF_inline_asm text sg clob => do_inline_assembly text sg ge | EF_debug kind text targs => do_ef_debug kind text targs + | EF_profiling id kind => do_ef_profiling id end. Lemma do_ef_external_sound: @@ -598,6 +603,8 @@ Proof with try congruence. eapply do_inline_assembly_sound; eauto. - (* EF_debug *) unfold do_ef_debug. mydestr. split; constructor. +- (* EF_profiling *) + unfold do_ef_profiling. mydestr. split; constructor. Qed. Lemma do_ef_external_complete: @@ -652,6 +659,8 @@ Proof. eapply do_inline_assembly_complete; eauto. - (* EF_debug *) inv H. inv H0. reflexivity. +- (* EF_profiling *) + inv H. inv H0. reflexivity. Qed. (** * Reduction of expressions *) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 5acb996d..744df818 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1335,6 +1335,7 @@ Lemma eval_binop_compat: /\ Val.inject f v tv. Proof. destruct op; simpl; intros; inv H. +- TrivialExists. apply Val.normalize_inject; auto. - TrivialExists. apply Val.add_inject; auto. - TrivialExists. apply Val.sub_inject; auto. - TrivialExists. inv H0; inv H1; constructor. diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 143e87a3..47a02851 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -33,6 +33,7 @@ Inductive unary_operation : Type := | Oabsfloat : unary_operation. (**r floating-point absolute value *) Inductive binary_operation : Type := + | Oexpect : binary_operation (**r return first argument *) | Oadd : binary_operation (**r addition (binary [+]) *) | Osub : binary_operation (**r subtraction (binary [-]) *) | Omul : binary_operation (**r multiplication (binary [*]) *) @@ -763,6 +764,14 @@ Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val : (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2))) v1 t1 v2 t2 m. +Definition sem_expect (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint n1)) + (fun sg n1 n2 => Some(Vlong n1)) + (fun n1 n2 => Some(Vfloat n1)) + (fun n1 n2 => Some(Vsingle n1)) + v1 t1 v2 t2 m. + Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => @@ -1050,6 +1059,7 @@ Definition sem_binary_operation (v1: val) (t1: type) (v2: val) (t2:type) (m: mem): option val := match op with + | Oexpect => sem_expect v1 t1 v2 t2 m | Oadd => sem_add cenv v1 t1 v2 t2 m | Osub => sem_sub cenv v1 t1 v2 t2 m | Omul => sem_mul v1 t1 v2 t2 m @@ -1290,6 +1300,9 @@ Lemma sem_binary_operation_inj: 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. +- (* expect *) + unfold sem_expect in *. + eapply sem_binarith_inject; eauto; intros; exact I. - (* add *) assert (A: forall cenv ty si v1' v2' tv1' tv2', Val.inject f v1' tv1' -> Val.inject f v2' tv2' -> diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 5bd12d00..f78b52ae 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -259,6 +259,11 @@ Definition make_add_ptr_long (ce: composite_env) (ty: type) (e1 e2: expr) := let n := make_intconst (Int.repr sz) in OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))). +Definition make_expect (e1: expr) (ty1: type) (e2: expr) (ty2: type) := + make_binarith (Oexpect AST.Tint) (Oexpect AST.Tint) + (Oexpect AST.Tfloat) (Oexpect AST.Tsingle) + (Oexpect AST.Tlong) (Oexpect AST.Tlong) e1 ty1 e2 ty2. + Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with | add_case_pi ty si => make_add_ptr_int ce ty si e1 e2 @@ -421,6 +426,7 @@ Definition transl_binop (ce: composite_env) (a: expr) (ta: type) (b: expr) (tb: type) : res expr := match op with + | Cop.Oexpect => make_expect a ta b tb | Cop.Oadd => make_add ce a ta b tb | Cop.Osub => make_sub ce a ta b tb | Cop.Omul => make_mul a ta b tb diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 1ceb8e4d..c5ba19d5 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -619,6 +619,11 @@ End MAKE_BIN. Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm. +Lemma make_expect_correct: binary_constructor_correct make_expect sem_expect. +Proof. + apply make_binarith_correct; intros; auto. +Qed. + Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)). Proof. assert (A: forall ty si a b c e le m va vb v, @@ -922,22 +927,23 @@ Lemma transl_binop_correct: eval_expr ge e le m c v. Proof. intros. destruct op; simpl in *. - eapply make_add_correct; eauto. - eapply make_sub_correct; eauto. - eapply make_mul_correct; eauto. - eapply make_div_correct; eauto. - eapply make_mod_correct; eauto. - eapply make_and_correct; eauto. - eapply make_or_correct; eauto. - eapply make_xor_correct; eauto. - eapply make_shl_correct; eauto. - eapply make_shr_correct; eauto. - eapply make_cmp_correct; eauto. - eapply make_cmp_correct; eauto. - eapply make_cmp_correct; eauto. - eapply make_cmp_correct; eauto. - eapply make_cmp_correct; eauto. - eapply make_cmp_correct; eauto. +- eapply make_expect_correct; eauto. +- eapply make_add_correct; eauto. +- eapply make_sub_correct; eauto. +- eapply make_mul_correct; eauto. +- eapply make_div_correct; eauto. +- eapply make_mod_correct; eauto. +- eapply make_and_correct; eauto. +- eapply make_or_correct; eauto. +- eapply make_xor_correct; eauto. +- eapply make_shl_correct; eauto. +- eapply make_shr_correct; eauto. +- eapply make_cmp_correct; eauto. +- eapply make_cmp_correct; eauto. +- eapply make_cmp_correct; eauto. +- eapply make_cmp_correct; eauto. +- eapply make_cmp_correct; eauto. +- eapply make_cmp_correct; eauto. Qed. Lemma make_load_correct: diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 00fcf8ab..bde4001f 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -111,6 +111,7 @@ Definition comparison_type (ty1 ty2: type) (m: string): res type := Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type := match op with + | Oexpect => binarith_type ty1 ty2 "__builtin_expect" | Oadd => match classify_add ty1 ty2 with | add_case_pi ty _ | add_case_ip _ ty @@ -1546,6 +1547,8 @@ Lemma pres_sem_binop: Proof. intros until m; intros TY SEM WT1 WT2. destruct op; simpl in TY; simpl in SEM. +- (* expect *) + unfold sem_expect in SEM. eapply pres_sem_binarith; eauto; intros; exact I. - (* add *) unfold sem_add, sem_add_ptr_int, sem_add_ptr_long in SEM; DestructCases; auto with ty. eapply pres_sem_binarith; eauto; intros; exact I. diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 0e735d2d..0aefde31 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -62,6 +62,7 @@ let precedence = function | Ebinop(Oand, _, _, _) -> (8, LtoR) | Ebinop(Oxor, _, _, _) -> (7, LtoR) | Ebinop(Oor, _, _, _) -> (6, LtoR) + | Ebinop(Oexpect, _, _, _) -> (5, LtoR) (* Expressions *) diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 03dc5837..beca056f 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -30,6 +30,7 @@ let name_unop = function | Oabsfloat -> "__builtin_fabs" let name_binop = function + | Oexpect -> "expect" | Oadd -> "+" | Osub -> "-" | Omul -> "*" @@ -158,6 +159,7 @@ let rec precedence = function | Ebinop(Oand, _, _, _) -> (8, LtoR) | Ebinop(Oxor, _, _, _) -> (7, LtoR) | Ebinop(Oor, _, _, _) -> (6, LtoR) + | Ebinop(Oexpect, _, _, _) -> (5, LtoR) (* fixme *) | Eseqand _ -> (5, LtoR) | Eseqor _ -> (4, LtoR) | Econdition _ -> (3, RtoL) diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index e7d57a1c..95e3957c 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -770,53 +770,53 @@ Proof. (* val *) simpl in H. destruct v; monadInv H; exists (@nil ident); split; auto with gensym. Opaque makeif. - intros. destruct dst; simpl in *; inv H2. +- intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. - intros. destruct dst; simpl in *; inv H2. +- intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. - intros. destruct dst; simpl in *; inv H2. +- intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. - intros. destruct dst; simpl in *; inv H2. +- intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. (* var *) - monadInv H; econstructor; split; auto with gensym. UseFinish. constructor. +- monadInv H; econstructor; split; auto with gensym. UseFinish. constructor. (* field *) - monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish. +- monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* valof *) - monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. (* deref *) - monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. +- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* addrof *) - monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. +- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. econstructor; eauto. (* unop *) - monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. +- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* binop *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. (* cast *) - monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. +- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* seqand *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. @@ -840,7 +840,7 @@ Opaque makeif. apply list_disjoint_cons_r; eauto with gensym. apply contained_app; eauto with gensym. (* seqor *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. @@ -864,7 +864,7 @@ Opaque makeif. apply list_disjoint_cons_r; eauto with gensym. apply contained_app; eauto with gensym. (* condition *) - monadInv H2. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H2. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. @@ -896,13 +896,13 @@ Opaque makeif. apply contained_app; eauto with gensym. apply contained_app; eauto with gensym. (* sizeof *) - monadInv H. UseFinish. +- monadInv H. UseFinish. exists (@nil ident); split; auto with gensym. constructor. (* alignof *) - monadInv H. UseFinish. +- monadInv H. UseFinish. exists (@nil ident); split; auto with gensym. constructor. (* assign *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. destruct dst; monadInv EQ2; simpl add_dest in *. (* for value *) @@ -921,7 +921,7 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* assignop *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]]. destruct dst; monadInv EQ3; simpl add_dest in *. @@ -941,7 +941,7 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* postincr *) - monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0; simpl add_dest in *. (* for value *) exists (x0 :: tmp1); split. @@ -958,7 +958,7 @@ Opaque makeif. econstructor; eauto with gensym. apply contained_cons; eauto with gensym. (* comma *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. @@ -968,7 +968,7 @@ Opaque makeif. destruct dst; simpl; auto with gensym. apply contained_app; eauto with gensym. (* call *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. destruct dst; monadInv EQ2; simpl add_dest in *. (* for value *) @@ -986,7 +986,7 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* builtin *) - monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0; simpl add_dest in *. (* for value *) exists (x0 :: tmp1); split. @@ -1001,13 +1001,13 @@ Opaque makeif. repeat rewrite app_ass. econstructor; eauto with gensym. congruence. apply contained_cons; eauto with gensym. (* loc *) - monadInv H. +- monadInv H. (* paren *) - monadInv H0. +- monadInv H0. (* nil *) - monadInv H; exists (@nil ident); split; auto with gensym. constructor. +- monadInv H; exists (@nil ident); split; auto with gensym. constructor. (* cons *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. diff --git a/common/AST.v b/common/AST.v index eb34d675..268e13d5 100644 --- a/common/AST.v +++ b/common/AST.v @@ -464,6 +464,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 @@ -514,10 +519,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. *) @@ -535,6 +543,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. *) @@ -553,6 +562,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. *) @@ -568,7 +578,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. diff --git a/common/Events.v b/common/Events.v index 28bb992a..033e2e03 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1378,6 +1378,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 @@ -1412,6 +1417,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; omega. +(* 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 @@ -1530,6 +1569,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: @@ -1537,18 +1577,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/PrintAST.ml b/common/PrintAST.ml index 3f718428..38bbfa47 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -47,6 +47,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) @@ -61,7 +68,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 diff --git a/common/Sections.ml b/common/Sections.ml index 839128a5..ea0b6dbc 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -17,7 +17,8 @@ type section_name = | Section_text - | Section_data of bool (* true = init data, false = uninit data *) + | Section_data of bool (* true = init data, false = uninit data *) + * bool (* thread local? *) | Section_small_data of bool | Section_const of bool | Section_small_const of bool @@ -47,8 +48,8 @@ type section_info = { } let default_section_info = { - sec_name_init = Section_data true; - sec_name_uninit = Section_data false; + sec_name_init = Section_data (true, false); + sec_name_uninit = Section_data (false, false); sec_writable = true; sec_executable = false; sec_access = Access_default @@ -63,8 +64,13 @@ let builtin_sections = [ sec_writable = false; sec_executable = true; sec_access = Access_default}; "DATA", - {sec_name_init = Section_data true; - sec_name_uninit = Section_data false; + {sec_name_init = Section_data (true, false); + sec_name_uninit = Section_data (false, false); + sec_writable = true; sec_executable = false; + sec_access = Access_default}; + "TDATA", + {sec_name_init = Section_data (true, true); + sec_name_uninit = Section_data (false, true); sec_writable = true; sec_executable = false; sec_access = Access_default}; "SDATA", @@ -175,7 +181,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 = @@ -194,7 +200,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 d9fd9239..00c06c20 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -18,7 +18,8 @@ type section_name = | Section_text - | Section_data of bool (* true = init data, false = uninit data *) + | Section_data of bool (* true = init data, false = uninit data *) + * bool (* thread local? *) | Section_small_data of bool | Section_const of bool | Section_small_const of bool @@ -46,7 +47,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 -> bool -> +val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> bool -> 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/cparser/C.mli b/cparser/C.mli index 15717565..3c271f3f 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -86,8 +86,11 @@ type attributes = attribute list type storage = | Storage_default (* used for toplevel names without explicit storage *) + | Storage_thread_local | Storage_extern | Storage_static + | Storage_thread_local_extern + | Storage_thread_local_static | Storage_auto (* used for block-scoped names without explicit storage *) | Storage_register diff --git a/cparser/Cabs.v b/cparser/Cabs.v index 5f12e8a1..2dae061a 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -54,7 +54,7 @@ Inductive typeSpecifier := (* Merge all specifiers into one type *) | Tenum : option string -> option (list (string * option expression * loc)) -> list attribute -> typeSpecifier with storage := - AUTO | STATIC | EXTERN | REGISTER | TYPEDEF + AUTO | STATIC | EXTERN | REGISTER | TYPEDEF | THREAD_LOCAL with cvspec := | CV_CONST | CV_VOLATILE | CV_RESTRICT diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index ecf83779..7bae2fe2 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -354,7 +354,9 @@ and is_constant_lval env e = begin match Env.find_ident env id with | Env.II_ident(sto, _) -> begin match sto with - | Storage_default | Storage_extern | Storage_static -> true + | Storage_default | Storage_extern | Storage_static + | Storage_thread_local | Storage_thread_local_extern | Storage_thread_local_static + -> true | Storage_auto | Storage_register -> false end | Env.II_enum _ -> false (* should not happen *) diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml index 63ac8ac1..9f19395a 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -126,14 +126,14 @@ let add_enum e = *) let visible_decl (sto, id, ty, init) = - sto = Storage_default && + (sto = Storage_default || sto = Storage_thread_local) && match ty with TFun _ -> false | _ -> true let visible_fundef f = match f.fd_storage with - | Storage_default -> not f.fd_inline - | Storage_extern -> true - | Storage_static -> false + | Storage_default | Storage_thread_local -> not f.fd_inline + | Storage_extern | Storage_thread_local_extern -> true + | Storage_static | Storage_thread_local_static -> false | Storage_auto | Storage_register -> assert false let rec add_init_globdecls accu = function diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 9aeec421..78970990 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -361,6 +361,9 @@ let storage pp = function | Storage_default -> () | Storage_extern -> fprintf pp "extern " | Storage_static -> fprintf pp "static " + | Storage_thread_local -> fprintf pp "_Thread_local" + | Storage_thread_local_extern -> fprintf pp "extern _Thread_local" + | Storage_thread_local_static -> fprintf pp "static _Thread_local" | Storage_auto -> () (* used only in blocks, where it can be omitted *) | Storage_register -> fprintf pp "register " diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 9e17cb7e..0504ad0b 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -152,6 +152,9 @@ let name_of_storage_class = function | Storage_default -> "<default>" | Storage_extern -> "'extern'" | Storage_static -> "'static'" + | Storage_thread_local -> "'_Thread_local'" + | Storage_thread_local_extern -> "'_Thread_local extern'" + | Storage_thread_local_static -> "'_Thread_local static'" | Storage_auto -> "'auto'" | Storage_register -> "'register'" @@ -177,15 +180,29 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = | Storage_static,Storage_static | Storage_extern,Storage_extern | Storage_default,Storage_default -> sto - | _,Storage_static -> + | Storage_thread_local_static,Storage_thread_local_static + | Storage_thread_local_extern,Storage_thread_local_extern + | Storage_thread_local,Storage_thread_local -> sto + | _,Storage_static | _,Storage_thread_local_static -> error loc "static declaration of '%s' follows non-static declaration" s; sto | Storage_static,_ -> Storage_static (* Static stays static *) - | Storage_extern,_ -> if is_function_type env new_ty then Storage_extern else sto + | Storage_thread_local_static,_ -> Storage_thread_local_static (* Thread-local static stays static *) + | (Storage_extern|Storage_thread_local_extern),_ -> if is_function_type env new_ty then Storage_extern else sto | Storage_default,Storage_extern -> if is_global_defined s && is_function_type env ty then warning loc Extern_after_definition "this extern declaration follows a non-extern definition and is ignored"; Storage_extern + | Storage_thread_local,Storage_thread_local_extern -> + if is_global_defined s && is_function_type env ty then + warning loc Extern_after_definition "this extern declaration follows a non-extern definition and is ignored"; + Storage_extern + | Storage_thread_local, Storage_default -> + error loc "Non thread-local declaration follows thread-local"; + sto + | Storage_default, (Storage_thread_local|Storage_thread_local_extern) -> + error loc "Thread-local declaration follows non thread-local"; + sto | _,Storage_extern -> old_sto (* "auto" and "register" don't appear in toplevel definitions. Normally this was checked earlier. Generate error message @@ -639,13 +656,26 @@ let rec elab_specifier ?(only = false) loc env specifier = restrict := cv = CV_RESTRICT; attr := add_attributes (elab_cvspec env cv) !attr | SpecStorage st -> - if !sto <> Storage_default && st <> TYPEDEF then + if !sto <> Storage_default && st <> TYPEDEF && st <> THREAD_LOCAL then error loc "multiple storage classes in declaration specifier"; begin match st with | AUTO -> sto := Storage_auto | STATIC -> sto := Storage_static | EXTERN -> sto := Storage_extern | REGISTER -> sto := Storage_register + | THREAD_LOCAL -> + sto := (match !sto with + | Storage_static | Storage_thread_local_static -> + Storage_thread_local_static + | Storage_extern | Storage_thread_local_extern -> + Storage_thread_local_extern + | Storage_default | Storage_thread_local -> + Storage_thread_local + | Storage_auto|Storage_register -> + error loc "_Thread_local on auto or register variable"; + !sto + ) + | TYPEDEF -> if !typedef then error loc "multiple uses of 'typedef'"; diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index e44a330f..b36b3e81 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -72,6 +72,7 @@ let () = ("goto", fun loc -> GOTO loc); ("if", fun loc -> IF loc); ("inline", fun loc -> INLINE loc); + ("_Thread_local", fun loc -> THREAD_LOCAL loc); ("_Noreturn", fun loc -> NORETURN loc); ("int", fun loc -> INT loc); ("long", fun loc -> LONG loc); @@ -542,6 +543,7 @@ and singleline_comment = parse | Pre_parser.IF loc -> loop (Parser.IF_ loc) | Pre_parser.INC loc -> loop (Parser.INC loc) | Pre_parser.INLINE loc -> loop (Parser.INLINE loc) + | Pre_parser.THREAD_LOCAL loc -> loop (Parser.THREAD_LOCAL loc) | Pre_parser.INT loc -> loop (Parser.INT loc) | Pre_parser.LBRACE loc -> loop (Parser.LBRACE loc) | Pre_parser.LBRACK loc -> loop (Parser.LBRACK loc) diff --git a/cparser/Parser.vy b/cparser/Parser.vy index 03bfa590..4f3b9789 100644 --- a/cparser/Parser.vy +++ b/cparser/Parser.vy @@ -32,7 +32,7 @@ Require Cabs. LEFT_ASSIGN RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN %token<Cabs.loc> LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA - SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE + SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE THREAD_LOCAL NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE CONST VOLATILE VOID STRUCT UNION ENUM UNDERSCORE_BOOL PACKED ALIGNAS ATTRIBUTE ASM @@ -397,6 +397,8 @@ storage_class_specifier: { (Cabs.AUTO, loc) } | loc = REGISTER { (Cabs.REGISTER, loc) } +| loc = THREAD_LOCAL + { (Cabs.THREAD_LOCAL, loc) } (* 6.7.2 *) type_specifier: diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 64412194..aeeb9326 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -257,13 +257,16 @@ let rec reserve_public env = function match dcl.gdesc with | Gdecl(sto, id, _, _) -> begin match sto with - | Storage_default | Storage_extern -> enter_public env id + | Storage_default | Storage_thread_local + | Storage_extern | Storage_thread_local_extern -> + enter_public env id | Storage_static -> env | _ -> assert false end | Gfundef f -> begin match f.fd_storage with - | Storage_default | Storage_extern -> enter_public env f.fd_name + | Storage_default | Storage_extern + -> enter_public env f.fd_name | Storage_static -> env | _ -> assert false end diff --git a/cparser/deLexer.ml b/cparser/deLexer.ml index de0e9b6e..43c1a679 100644 --- a/cparser/deLexer.ml +++ b/cparser/deLexer.ml @@ -30,6 +30,7 @@ let delex (symbol : string) : string = | "BUILTIN_VA_ARG" -> "__builtin_va_arg" | "CONST" -> "const" | "INLINE" -> "inline" + | "THREAD_LOCAL" -> "_Thread_local" | "PACKED" -> "__packed__" | "RESTRICT" -> "restrict" | "SIGNED" -> "signed" diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly index 669ecf5e..e21a3519 100644 --- a/cparser/pre_parser.mly +++ b/cparser/pre_parser.mly @@ -54,7 +54,7 @@ COLON AND MUL_ASSIGN DIV_ASSIGN MOD_ASSIGN ADD_ASSIGN SUB_ASSIGN LEFT_ASSIGN RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT - AUTO REGISTER INLINE NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE + AUTO REGISTER INLINE THREAD_LOCAL NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE UNDERSCORE_BOOL CONST VOLATILE VOID STRUCT UNION ENUM CASE DEFAULT IF ELSE SWITCH WHILE DO FOR GOTO CONTINUE BREAK RETURN BUILTIN_VA_ARG ALIGNOF ATTRIBUTE ALIGNAS PACKED ASM BUILTIN_OFFSETOF @@ -430,6 +430,7 @@ storage_class_specifier_no_typedef: | STATIC | AUTO | REGISTER +| THREAD_LOCAL {} (* [declaration_specifier_no_type] matches declaration specifiers diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 8e3305ef..fd9603ee 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -87,3 +87,6 @@ let option_fmove_loop_invariants = ref true let option_fnontrap_loads = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 + +let option_profile_arcs = ref false +let option_fbranch_probabilities = ref true diff --git a/driver/Compiler.v b/driver/Compiler.v index e6d39152..69041ab0 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -37,6 +37,8 @@ Require Selection. Require RTLgen. Require Tailcall. Require Inlining. +Require Profiling. +Require ProfilingExploit. Require FirstNop. Require Renumber. Require Duplicate. @@ -65,6 +67,8 @@ Require Selectionproof. Require RTLgenproof. Require Tailcallproof. Require Inliningproof. +Require Profilingproof. +Require ProfilingExploitproof. Require FirstNopproof. Require Renumberproof. Require Duplicateproof. @@ -138,34 +142,38 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 1) @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) - @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program) + @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program) @@ print (print_RTL 3) - @@ time "Renumbering" Renumber.transf_program + @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program) @@ print (print_RTL 4) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) + @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program) @@ print (print_RTL 5) - @@ time "Renumbering pre constprop" Renumber.transf_program + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 6) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 7) - @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) + @@ time "Renumbering pre constprop" Renumber.transf_program @@ print (print_RTL 8) - @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) @@ print (print_RTL 10) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program) @@ print (print_RTL 11) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 12) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 13) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 14) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 15) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 16) + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ print (print_RTL 17) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 18) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -267,6 +275,8 @@ Definition CompCert's_passes := ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog + ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) + ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog) ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) @@ -318,7 +328,9 @@ Proof. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. - set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) in *. + set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. + set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. + set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *. set (p9bis := Renumber.transf_program p9) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := Renumber.transf_program p10) in *. @@ -347,6 +359,8 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. + exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. + exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. exists p9bis; split. apply Renumberproof.transf_program_match. exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. @@ -418,7 +432,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p29)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p31)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -437,6 +451,10 @@ Ltac DestructM := eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. + eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index 5acd2640..58ac62b7 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -87,6 +87,12 @@ Parameter all_loads_nontrap: unit -> bool. (** Flag -fforward-moves. Forward moves after CSE. *) Parameter optim_forward_moves: unit -> bool. +(** Flag -fprofile-arcs. Add profiling logger. *) +Parameter profile_arcs : unit -> bool. + +(** Flag -fbranch_probabilities. Use profiling information if available *) +Parameter branch_probabilities : unit -> bool. + (* TODO is there a more appropriate place? *) Require Import Coqlib. Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. diff --git a/driver/Driver.ml b/driver/Driver.ml index 6a9e9b92..3fae2a7d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -225,7 +225,10 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -falign-functions <n> Set alignment (in bytes) of function entry points -falign-branch-targets <n> Set alignment (in bytes) of branch targets -falign-cond-branches <n> Set alignment (in bytes) of conditional branches - -fcommon Put uninitialized globals in the common section [on]. + -fcommon Put uninitialized globals in the common section [on] + -fprofile-arcs Profile branches [off]. + -fprofile-use= filename Use profiling information in filename + -fbranch-probabilities Use profiling information (if available) for branches [on] |} ^ target_help ^ toolchain_help ^ @@ -330,6 +333,7 @@ let cmdline_actions = _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-Obranchless", Set option_Obranchless; + Exact "-fprofile-use=", String (fun s -> Profilingaux.load_profiling_info s); Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n); Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); @@ -420,7 +424,9 @@ let cmdline_actions = @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap @ f_opt "forward-moves" option_fforward_moves -(* Code generation options *) + (* Code generation options *) + @ f_opt "profile-arcs" option_profile_arcs + @ f_opt "branch-probabilities" option_fbranch_probabilities @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) @ [ diff --git a/extraction/extraction.v b/extraction/extraction.v index b6aa3409..9070e26d 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -152,6 +152,10 @@ Extract Constant Compopts.va_strict => "fun _ -> false". Extract Constant Compopts.all_loads_nontrap => "fun _ -> !Clflags.option_all_loads_nontrap". +Extract Constant Compopts.profile_arcs => +"fun _ -> !Clflags.option_profile_arcs". +Extract Constant Compopts.branch_probabilities => + "fun _ -> !Clflags.option_fbranch_probabilities". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". @@ -162,9 +166,17 @@ Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". Extract Constant Compiler.time => "Timing.time_coq". Extract Constant Compopts.time => "Timing.time_coq". - (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) +(* Profiling *) +Extract Constant AST.profiling_id => "Digest.t". +Extract Constant AST.profiling_id_eq => "Digest.equal". +Extract Constant Profiling.function_id => "Profilingaux.function_id". +Extract Constant Profiling.branch_id => "Profilingaux.branch_id". +Extract Constant ProfilingExploit.function_id => "Profilingaux.function_id". +Extract Constant ProfilingExploit.branch_id => "Profilingaux.branch_id". +Extract Constant ProfilingExploit.condition_oracle => "Profilingaux.condition_oracle". + (* Cabs *) Extract Constant Cabs.loc => "{ lineno : int; diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index 8ab10bc5..e388d2aa 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -591,6 +591,7 @@ let expand_instruction instr = | EF_external _ -> failwith "asmexpand: external" | EF_inline_asm _ -> emit instr | EF_runtime _ -> failwith "asmexpand: runtime" + | EF_profiling _ -> emit instr end | _ -> emit instr diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 8098b5d1..cff1164c 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -171,6 +171,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := if Z.leb sz 15 then R62 :: R63 :: R61 :: nil else R62 :: R63 :: R61 :: R60 :: nil + | EF_profiling _ _ => R62 :: R63 ::nil | _ => nil end. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 930b1c51..43177019 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -157,8 +157,12 @@ module Target (*: TARGET*) = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else "COMM" + | Section_data(true, true) -> + ".section .tdata,\"awT\",@progbits" + | Section_data(false, true) -> + ".section .tbss,\"awT\",@nobits" + | Section_data(i, false) | Section_small_data(i) -> + (if i then ".data" else "COMM") | Section_const i | Section_small_const i -> if i then ".section .rodata" else "COMM" | Section_string -> ".section .rodata" @@ -211,14 +215,20 @@ module Target (*: TARGET*) = (* Generate code to load the address of id + ofs in register r *) -(* FIXME DMonniaux ugly ugly hack to get at standard __thread data *) let loadsymbol oc r id ofs = if Archi.pic_code () then begin assert (ofs = Integers.Ptrofs.zero); - fprintf oc " make %a = %s\n" ireg r (extern_atom id) - end else begin - if (extern_atom id) = "_impure_thread_data" then begin - fprintf oc " addd %a = $r13, @tprel(%a)\n" ireg r symbol_offset (id, ofs) + if C2C.atom_is_thread_local id then begin + (* fprintf oc " addd %a = $r13, @tprel(%s)\n" ireg r (extern_atom id) *) + fprintf oc " addd %a = $r13, @tlsle(%s)\n" ireg r (extern_atom id) + end else begin + fprintf oc " make %a = %s\n" ireg r (extern_atom id) + end + end else + begin + if C2C.atom_is_thread_local id then begin + (* fprintf oc " addd %a = $r13, @tprel(%a)\n" ireg r symbol_offset (id, ofs) *) + fprintf oc " addd %a = $r13, @tlsle(%a)\n" ireg r symbol_offset (id, ofs) end else begin fprintf oc " make %a = %a\n" ireg r symbol_offset (id, ofs) end @@ -239,7 +249,20 @@ module Target (*: TARGET*) = (*let w oc = if Archi.ptr64 then output_string oc "w" *) -(* Offset part of a load or store *) + + (* Profiling *) + + + let k1c_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name = + fprintf oc " make $r0 = %d\n" nr_items; + fprintf oc " make $r1 = %s\n" profiling_id_table_name; + fprintf oc " make $r2 = %s\n" profiling_counter_table_name; + fprintf oc " goto %s\n" profiling_write_table_helper; + fprintf oc " ;;\n";; + + (* Offset part of a load or store *) let offset oc n = ptrofs oc n @@ -328,6 +351,18 @@ module Target (*: TARGET*) = fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment + | EF_profiling(id, coq_kind) -> + let kind = Z.to_int coq_kind in + assert (kind >= 0); + assert (kind <= 1); + fprintf oc "%s profiling %a %d\n" comment + Profilingaux.pp_id id kind; + fprintf oc " make $r63 = %s\n" profiling_counter_table_name; + fprintf oc " make $r62 = 1\n"; + fprintf oc " ;;\n"; + fprintf oc " afaddd %d[$r63] = $r62\n" + (profiling_offset id kind); + fprintf oc " ;;\n" | _ -> assert false end @@ -789,8 +824,9 @@ module Target (*: TARGET*) = if !Clflags.option_g then begin section oc Section_text; end - + let print_epilogue oc = + print_profiling_epilogue elf_text_print_fun_info Dtors k1c_profiling_stub oc; if !Clflags.option_g then begin Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index f4d4285a..38f4bc75 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -365,6 +365,7 @@ let pp_instructions pp ic = | EF_annot_val _ | EF_builtin _ | EF_debug _ + | EF_profiling _ | EF_external _ | EF_free | EF_malloc diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 50b1bdd6..52f4f855 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -472,7 +472,7 @@ Definition intuoffloat (e: expr) := else Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (CEcond (Ccompf Clt) None (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 0f608d25..3ea03786 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -117,7 +117,9 @@ module Linux_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) -> if i then ".data" else @@ -218,7 +220,9 @@ module Diab_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i -> if i then ".data" else common_section () + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data (i, false) -> if i then ".data" else common_section () | Section_small_data i -> if i then ".sdata" else ".sbss" | Section_const _ -> ".text" | Section_small_const _ -> ".sdata2" diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 64bcea4c..1f02ca71 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -107,7 +107,9 @@ module Target : TARGET = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" diff --git a/runtime/Makefile b/runtime/Makefile index 3b1cabc4..bf979d5f 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -38,6 +38,8 @@ OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \ vararg.o endif +OBJS+=write_profiling_table.o + LIB=libcompcert.a INCLUDES=include/float.h include/stdarg.h include/stdbool.h \ @@ -71,7 +73,7 @@ $(LIB): $(OBJS) # generated assembly %.o: c/%.c c/i64.h ../ccomp - ../ccomp -O2 -S -o $*.s -I./c c/$*.c + ../ccomp -g -O2 -S -o $*.s -I./c c/$*.c sed -i -e 's/i64_/__compcert_i64_/g' $*.s $(CASMRUNTIME) -o $*.o $*.s @rm $*.s diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c new file mode 100644 index 00000000..0ce7a948 --- /dev/null +++ b/runtime/c/write_profiling_table.c @@ -0,0 +1,58 @@ +#include <stdint.h> +#include <stdio.h> +#include <stdlib.h> +#include <errno.h> + +typedef uint8_t md5_hash[16]; +typedef uint64_t condition_counters[2]; + +static void write_id(FILE *fp, md5_hash *hash) { + fwrite(hash, 16, 1, fp); +} + +#define BYTE(counter, i) ((counter >> (8*i)) & 0xFF) +static void write_counter(FILE *fp, uint64_t counter) { + putc(BYTE(counter, 0), fp); + putc(BYTE(counter, 1), fp); + putc(BYTE(counter, 2), fp); + putc(BYTE(counter, 3), fp); + putc(BYTE(counter, 4), fp); + putc(BYTE(counter, 5), fp); + putc(BYTE(counter, 6), fp); + putc(BYTE(counter, 7), fp); +} + +void _compcert_write_profiling_table(unsigned int nr_items, + md5_hash id_table[], + condition_counters counter_table[]) { + errno = 0; + + const char *filename = getenv("COMPCERT_PROFILING_DATA"); + if (filename) { + if (!*filename) return; + } else { + filename = "compcert_profiling.dat"; + } + + FILE *fp = fopen(filename, "a"); + //fprintf(stderr, "successfully opened profiling file\n"); + if (fp == NULL) { + perror("open CompCert profiling data for writing"); + return; + } + + for(unsigned int i=0; i<nr_items; i++) { + write_id(fp, &id_table[i]); + write_counter(fp, counter_table[i][0]); + write_counter(fp, counter_table[i][1]); + } + //fprintf(stderr, "successfully written profiling file\n"); + + fclose(fp); + //fprintf(stderr, "successfully closed profiling file\n"); + if (errno != 0) { + perror("write CompCert profiling data"); + return; + } + // fprintf(stderr, "write CompCert profiling data: no error\n"); +} diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h index 718ac3e5..7f111742 100644 --- a/runtime/include/ccomp_k1c_fixes.h +++ b/runtime/include/ccomp_k1c_fixes.h @@ -6,7 +6,7 @@ #endif #undef __GNUC__ -#define __thread +#define __thread _Thread_local struct __int128_ccomp { long __int128_ccomp_low; long __int128_ccomp_high; }; @@ -25,6 +25,6 @@ extern long long __compcert_afaddd(void *address, unsigned long long incr); extern int __compcert_afaddw(void *address, unsigned int incr); #endif -#define __builtin_expect(x, y) (x) +/* #define __builtin_expect(x, y) (x) */ #define __builtin_ctz(x) __builtin_k1_ctzw(x) #define __builtin_clz(x) __builtin_k1_clzw(x) diff --git a/test/monniaux/cycles.h b/test/monniaux/cycles.h index c7dc582b..5011b18c 100644 --- a/test/monniaux/cycles.h +++ b/test/monniaux/cycles.h @@ -45,11 +45,16 @@ static inline cycle_t get_cycle(void) { return cycles; } -#elif defined (__ARM_ARCH) && (__ARM_ARCH >= 6) +#elif defined (__ARM_ARCH) // && (__ARM_ARCH >= 6) #if (__ARM_ARCH < 8) typedef uint32_t cycle_t; #define PRcycle PRId32 +#ifdef ARM_NO_PRIVILEGE +static inline cycle_t get_cycle(void) { + return 0; +} +#else /* need this kernel module https://github.com/zertyz/MTL/tree/master/cpp/time/kernel/arm */ static inline cycle_t get_cycle(void) { @@ -57,14 +62,20 @@ static inline cycle_t get_cycle(void) { __asm__ volatile ("mrc p15, 0, %0, c9, c13, 0":"=r" (cycles)); return cycles; } +#endif #else #define PRcycle PRId64 typedef uint64_t cycle_t; + +#ifdef ARM_NO_PRIVILEGE +static inline cycle_t get_cycle(void) { + return 0; +} +#else /* need this kernel module: https://github.com/jerinjacobk/armv8_pmu_cycle_counter_el0 on 5+ kernels, remove first argument of access_ok macro */ - static inline cycle_t get_cycle(void) { uint64_t val; @@ -72,6 +83,7 @@ static inline cycle_t get_cycle(void) return val; } #endif +#endif #else #define PRcycle PRId32 diff --git a/test/monniaux/expect/expect.c b/test/monniaux/expect/expect.c new file mode 100644 index 00000000..30e0742a --- /dev/null +++ b/test/monniaux/expect/expect.c @@ -0,0 +1,7 @@ +#ifndef PREDICTED +#define PREDICTED 0 +#endif + +int expect(int x, int *y, int *z) { + return __builtin_expect(x, PREDICTED) ? *y : *z; +} diff --git a/test/monniaux/minisat/Makefile.on_marte b/test/monniaux/minisat/Makefile.on_marte new file mode 100644 index 00000000..af7b9145 --- /dev/null +++ b/test/monniaux/minisat/Makefile.on_marte @@ -0,0 +1,16 @@ +EXE=minisat.ccomp.exe minisat.ccomp.trace-linearize.exe \ + minisat.gcc-O3.exe \ + minisat.ccomp.profiled.exe minisat.gcc-O3.profiled.exe + +LOG=$(EXE:.exe=.dat) + +all: $(LOG) + +%.log : %.exe + rm -f $@ + for i in `seq 1 1000` ; do ./$< sudoku.sat >> $@; done + +%.dat : %.log + grep 'time cycles: ' $< | sed -e 's/time cycles: //' | awk '{ total += $$1; count++ } END { print total/count }' > $@ + +.SECONDARY: diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled new file mode 100644 index 00000000..77ba8b43 --- /dev/null +++ b/test/monniaux/minisat/Makefile.profiled @@ -0,0 +1,64 @@ +# -*- mode: makefile; -*- + +CFILES=main.c solver.c clock.c +CCOMP=../../../ccomp + +#GCC=aarch64-linux-gnu-gcc +GCC=k1-cos-gcc +#EXECUTE=qemu-aarch64 +#EXECUTE=qemu-arm +#EXECUTE=k1-cluster -- +#EXECUTE_CYCLES=k1-cluster --cycle-based -- + +LIBS=-lm +PROFILING_DAT=compcert_profiling.dat +EXAMPLE=sudoku.sat +CCOMPFLAGS=-static -finline-asm -finline-auto-threshold 50 +GCCFLAGS=-static +ALL=minisat.ccomp.log minisat.ccomp.trace-linearize.log minisat.ccomp.profiled.log minisat.gcc-O3.log minisat.gcc-O3.profiled.log + +all: $(ALL) +exe: $(ALL:.log=.exe) + +minisat.ccomp.exe: $(CFILES) + $(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ $(LIBS) + +minisat.ccomp.profile-arcs.exe: $(CFILES) + $(CCOMP) -DARM_NO_PRIVILEGE $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS) + +minisat.gcc-O3.exe: $(CFILES) + $(GCC) $(GCCFLAGS) -O3 $(CFILES) -o $@ $(LIBS) + +clock.gcc-O3.noprofile.o : clock.c + $(GCC) -DARM_NO_PRIVILEGE $(GCCFLAGS) -O3 -c $< -o @ + +minisat.gcc-O3.profile-arcs.exe: main.c solver.c clock.gcc-O3.noprofile.o + $(GCC) -DARM_NO_PRIVILEGE $(GCCFLAGS) -fprofile-arcs -O3 $+ -o $@ $(LIBS) + +gcda: minisat.gcc-O3.profile-arcs.exe + $(EXECUTE) ./$< $(EXAMPLE) + +main.gcda solver.gcda: gcda + +minisat.gcc-O3.profiled.exe: $(CFILES) $(GCDAFILES) + $(GCC) $(GCCFLAGS) -O3 -fprofile-use $(CFILES) -o $@ $(LIBS) + +minisat.ccomp.trace-linearize.exe: $(CFILES) + $(CCOMP) $(CCOMPFLAGS) -fduplicate 0 -ftracelinearize $(CFILES) -o $@ $(LIBS) + +$(PROFILING_DAT): minisat.ccomp.profile-arcs.exe + -rm -f $(PROFILING_DAT) + $(EXECUTE) ./$< $(EXAMPLE) + +minisat.ccomp.profiled.exe: $(CFILES) $(PROFILING_DAT) + $(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -ftracelinearize $(CFILES) -o $@ $(LIBS) + +%.log : %.exe + $(EXECUTE_CYCLES) $< $(EXAMPLE) 2>&1 | tee $@ + +clean: + -rm -f *.log *.exe $(PROFILING_DAT) $(GCDAFILES) + +.PHONY: clean gcda exe all + +.SECONDARY: diff --git a/test/monniaux/minisat/clock.c b/test/monniaux/minisat/clock.c new file mode 120000 index 00000000..d6bade99 --- /dev/null +++ b/test/monniaux/minisat/clock.c @@ -0,0 +1 @@ +../clock.c
\ No newline at end of file diff --git a/test/monniaux/minisat/cycles.h b/test/monniaux/minisat/cycles.h new file mode 120000 index 00000000..84e54d21 --- /dev/null +++ b/test/monniaux/minisat/cycles.h @@ -0,0 +1 @@ +../cycles.h
\ No newline at end of file diff --git a/test/monniaux/minisat/k1c.inline_50.log b/test/monniaux/minisat/k1c.inline_50.log new file mode 100644 index 00000000..438a06b4 --- /dev/null +++ b/test/monniaux/minisat/k1c.inline_50.log @@ -0,0 +1,14 @@ +==> minisat.ccomp.log <== +time cycles: 3252345 + +==> minisat.ccomp.profiled.log <== +time cycles: 3150170 + +==> minisat.ccomp.trace-linearize.log <== +time cycles: 3192299 + +==> minisat.gcc-O3.log <== +time cycles: 2780324 + +==> minisat.gcc-O3.profiled.log <== +time cycles: 2487533 diff --git a/test/monniaux/minisat/solver.h b/test/monniaux/minisat/solver.h index c9ce0219..4b96b017 100644 --- a/test/monniaux/minisat/solver.h +++ b/test/monniaux/minisat/solver.h @@ -19,6 +19,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA **************************************************************************************************/ // Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko +#include <stdint.h> + #ifndef solver_h #define solver_h @@ -39,11 +41,14 @@ static const bool false = 0; typedef int lit; typedef char lbool; +#if 0 #ifdef _WIN32 typedef signed __int64 uint64; // compatible with MS VS 6.0 #else typedef unsigned long long uint64; #endif +#endif +typedef uint64_t uint64; static const int var_Undef = -1; static const lit lit_Undef = -2; diff --git a/test/monniaux/profiling/profiling_call.c b/test/monniaux/profiling/profiling_call.c new file mode 100644 index 00000000..ce20241d --- /dev/null +++ b/test/monniaux/profiling/profiling_call.c @@ -0,0 +1,27 @@ +/* +For knowing how to write assembly profiling stubs. + */ + +#include <stdint.h> +#include <stdio.h> +#include <errno.h> + +typedef uint8_t md5_hash[16]; +typedef uint64_t condition_counters[2]; + +void _compcert_write_profiling_table(unsigned int nr_items, + md5_hash id_table[], + condition_counters counter_table[]); + +static md5_hash id_table[42] = {{1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16}}; +static condition_counters counter_table[42]; + +void write_profile(void) { + _compcert_write_profiling_table(42, id_table, counter_table); +} + +static _Atomic uint64_t counter; + +void incr_counter(void) { + counter++; +} diff --git a/test/monniaux/thread_local/thread_local.c b/test/monniaux/thread_local/thread_local.c new file mode 100644 index 00000000..7a50db0a --- /dev/null +++ b/test/monniaux/thread_local/thread_local.c @@ -0,0 +1,13 @@ +#include <stdio.h> + +_Thread_local int toto; +_Thread_local int toto2 = 45; + +int foobar(void) { + return toto; +} + +int main() { + printf("%d %d\n", toto, toto2); + return 0; +} diff --git a/test/monniaux/thread_local/thread_local2.c b/test/monniaux/thread_local/thread_local2.c new file mode 100644 index 00000000..ba244ac6 --- /dev/null +++ b/test/monniaux/thread_local/thread_local2.c @@ -0,0 +1,18 @@ +#include <stdio.h> +#include <pthread.h> + +_Thread_local int toto; +_Thread_local int toto2 = 45; + +void* poulet(void * dummy) { + printf("%p %p\n", &toto, &toto2); + return NULL; +} + +int main() { + pthread_t thr; + poulet(NULL); + pthread_create(&thr, NULL, poulet, NULL); + pthread_join(thr, NULL); + return 0; +} diff --git a/test/mppa/hardcheck.sh b/test/mppa/hardcheck.sh index 82b63182..b6538f0e 100755 --- a/test/mppa/hardcheck.sh +++ b/test/mppa/hardcheck.sh @@ -3,4 +3,4 @@ source do_test.sh -do_test hardcheck +do_test hardcheck 1 diff --git a/test/mppa/hardtest.sh b/test/mppa/hardtest.sh index 09511da6..6321bc7d 100755 --- a/test/mppa/hardtest.sh +++ b/test/mppa/hardtest.sh @@ -3,4 +3,4 @@ source do_test.sh -do_test hardtest +do_test hardtest 1 diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index b8353046..ad667e3d 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -552,7 +552,7 @@ let expand_instruction instr = expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args | EF_annot_val(kind,txt, targ) -> expand_annot_val kind txt targ args res - | EF_annot _ | EF_debug _ | EF_inline_asm _ -> + | EF_annot _ | EF_debug _ | EF_inline_asm _ | EF_profiling _ -> emit instr | _ -> assert false diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index a23c37d5..2a09207b 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -503,7 +503,7 @@ Definition intuoffloat (e: expr) := if Archi.splitlong then Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (CEcond (Ccompf Clt) None (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat else @@ -516,7 +516,7 @@ Nondetfunction floatofintu (e: expr) := if Archi.splitlong then let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in Elet e - (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) + (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) None (Eletvar O ::: Enil)) (floatofint (Eletvar O)) (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)) else diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 6159437e..38eff731 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -133,7 +133,9 @@ module ELF_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" @@ -165,7 +167,44 @@ module ELF_System : SYSTEM = let print_var_info = elf_print_var_info - let print_epilogue _ = () + let print_atexit oc to_be_called = + if Archi.ptr64 + then + begin + fprintf oc " leaq %s(%%rip), %%rdi\n" to_be_called; + fprintf oc " jmp atexit\n" + end + else + begin + fprintf oc " pushl $%s\n" to_be_called; + fprintf oc " call atexit\n"; + fprintf oc " addl $4, %%esp\n"; + fprintf oc " ret\n" + end + + let x86_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name = + if Archi.ptr64 + then + begin + fprintf oc " leaq %s(%%rip), %%rdx\n" profiling_counter_table_name; + fprintf oc " leaq %s(%%rip), %%rsi\n" profiling_id_table_name; + fprintf oc " movl $%d, %%edi\n" nr_items; + fprintf oc " jmp %s\n" profiling_write_table_helper + end + else + begin + fprintf oc " pushl $%s\n" profiling_counter_table_name; + fprintf oc " pushl $%s\n" profiling_id_table_name; + fprintf oc " pushl $%d\n" nr_items; + fprintf oc " call %s\n" profiling_write_table_helper ; + fprintf oc " addl $12, %%esp\n"; + fprintf oc " ret\n" + end;; + + let print_epilogue oc = + print_profiling_epilogue elf_text_print_fun_info (Init_atexit print_atexit) x86_profiling_stub oc;; let print_comm_decl oc name sz al = fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al @@ -191,7 +230,9 @@ module MacOS_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i || (not !Clflags.option_fcommon) then ".data" else "COMM" | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".const" else "COMM" @@ -268,7 +309,9 @@ module Cygwin_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rdata,\"dr\"" else "COMM" @@ -395,8 +438,28 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%a(%%rip)" label lbl end - - + let print_profiling_logger oc id kind = + assert (kind >= 0); + assert (kind <= 1); + let ofs = profiling_offset id kind in + if Archi.ptr64 + then + begin + fprintf oc "%s profiling %a %d: atomic increment\n" comment + Profilingaux.pp_id id kind; + fprintf oc " lock addq $1, %s+%d(%%rip)\n" + profiling_counter_table_name ofs + end + else + begin + fprintf oc "%s begin profiling %a %d: increment\n" comment + Profilingaux.pp_id id kind; + fprintf oc " addl $1, %s+%d\n" profiling_counter_table_name ofs; + fprintf oc " adcl $1, %s+%d\n" profiling_counter_table_name (ofs+4); + fprintf oc "%s end profiling %a %d: increment\n" comment + Profilingaux.pp_id id kind; + end + (* Printing of instructions *) (* Reminder on X86 assembly syntaxes: @@ -834,6 +897,8 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment + | EF_profiling(id, coq_kind) -> + print_profiling_logger oc id (Z.to_int coq_kind) | _ -> assert false end |