From 3c30567c452f030267d0fb09465adf8d7b44a90d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 12:36:24 +0200 Subject: installed Profiling (not finished) --- extraction/extraction.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 9b568951..c2b5d83e 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -137,6 +137,8 @@ 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". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". @@ -147,9 +149,12 @@ 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 Profiling.function_id => "Profilingaux.function_id". +Extract Constant Profiling.branch_id => "Profilingaux.branch_id". + (* Cabs *) Extract Constant Cabs.loc => "{ lineno : int; -- cgit From d3a8a8870050810a7bc3fb5e004059197ec364f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 13:06:00 +0200 Subject: print hashes --- extraction/extraction.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index c2b5d83e..72c19385 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -152,6 +152,8 @@ 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". -- cgit From c3f5f3dbd088091e3fab9f357b01693932d148f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 17:02:45 +0200 Subject: reloading and exploiting seems to work --- extraction/extraction.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 72c19385..eb811f6c 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -138,7 +138,9 @@ Extract Constant Compopts.va_strict => Extract Constant Compopts.all_loads_nontrap => "fun _ -> !Clflags.option_all_loads_nontrap". Extract Constant Compopts.profile_arcs => - "fun _ -> !Clflags.option_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". @@ -156,6 +158,9 @@ 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 => -- cgit