adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

WIP: autocorres: make trace results available again 

This changes the interface to access traces, making the underlying
symtabs explicit.
This commit is contained in:
Japheth Lim 2016-06-30 01:14:29 +10:00
parent cc1329c232
commit 6b72212597
10 changed files with 85 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
tools/autocorres/autocorres.ML
View File

@ -581,17 +581,27 @@ let
| SOME s => s
in fn f => prefix ^ f ^ suffix end
(* Initialise database for traces.
* Currently, this is implemented by mutating a global table.
* While slightly ugly, it does simplify adding more tracing to AutoCorres
* without cluttering the return types of existing code. *)
val trace_db: AutoCorresData.Trace Symtab.table (* type *) Symtab.table (* func *) Synchronized.var =
Synchronized.var "AutoCorres traces" Symtab.empty
fun add_trace f_name trace_name trace =
Synchronized.change trace_db
(Symtab.map_default (f_name, Symtab.empty) (Symtab.update_new (trace_name, trace)))
(* Do the translation. *)
val l1_results =
SimplConv2.translate
filename prog_info simpl_info existing_simpl_info existing_l1_info
(!(#no_c_termination opt) <> SOME true)
do_opt trace_opt (prefix "l1_" o make_function_name) lthy
do_opt trace_opt add_trace (prefix "l1_" o make_function_name) lthy
val l2_results =
LocalVarExtract2.translate
filename prog_info l1_results existing_l1_info existing_l2_info
do_opt trace_opt (prefix "l2_" o make_function_name)
do_opt trace_opt add_trace (prefix "l2_" o make_function_name)
val skip_heap_abs = !(#skip_heap_abs opt) = SOME true
val hl_results =
@ -606,7 +616,7 @@ let
filename prog_info l2_results' existing_l2_info existing_hl_info
HL_setup no_heap_abs force_heap_abs
heap_abs_syntax keep_going
(these (!(#trace_heap_lift opt))) do_opt trace_opt
(these (!(#trace_heap_lift opt))) do_opt trace_opt add_trace
(prefix "hl_" o make_function_name)
end
@ -616,14 +626,14 @@ let
else WordAbstract2.translate
filename prog_info hl_results existing_hl_info existing_wa_info
unsigned_word_abs no_signed_word_abs
(these (!(#trace_word_abs opt))) do_opt trace_opt
(these (!(#trace_word_abs opt))) do_opt trace_opt add_trace
(prefix "wa_" o make_function_name)
val ts_results =
TypeStrengthen2.translate
ts_rules ts_force filename prog_info
wa_results existing_wa_info existing_ts_info
make_function_name keep_going do_opt
make_function_name keep_going do_opt add_trace
(* Collect final translation results. *)
val l1_info = FSeq.list_of l1_results |> map snd |> Utils.symtab_merge false;
@ -708,6 +718,16 @@ let
val lthy = Local_Theory.background_theory (
AutoCorresFunctionInfo2.map (fn tbl =>
Symtab.update (filename, new_results) tbl)) lthy
(* All traces should be available at this point. Archive them. *)
val traces = Synchronized.value trace_db;
val _ = if Symtab.is_empty traces then () else
tracing "Saving translation traces to AutoCorresData.Traces."
val lthy = lthy |> Local_Theory.background_theory (
AutoCorresData.Traces.map
(Symtab.map_default (filename, Symtab.empty)
(fn old_traces => Utils.symtab_merge_with snd (old_traces, traces))));
in
(* Exit context. *)
Named_Target.exit lthy

19
tools/autocorres/autocorres_data.ML
View File

@ -22,6 +22,8 @@ sig
RuleTrace of thm AutoCorresTrace.RuleTrace
| SimpTrace of AutoCorresTrace.SimpTrace
structure Traces: THEORY_DATA
val add_trace: string -> string -> string -> Trace -> theory -> theory
val get_trace: theory -> string -> string -> string -> Trace option
@ -74,6 +76,19 @@ structure Terms = Theory_Data(
}
)
(* Function translation traces.
* These are for informational or debugging usage. *)
structure Traces = Theory_Data (
type T = Trace Symtab.table (* trace type *)
Symtab.table (* func name *)
Symtab.table (* file *);
val empty = Symtab.empty;
val extend = I;
(* We need a deep merge due to incremental translations (which can span
* multiple theories). snd is arbitrary. *)
val merge = Utils.symtab_merge_with (Utils.symtab_merge_with (Utils.symtab_merge_with snd));
)
(* Fetch a trace. *)
fun get_trace thy filename module fn_name =
Terms.get thy
@ -119,7 +134,6 @@ fun debug thy = Terms.get thy |> dest_ac_data |> (fn x => (Symtab3.dest (#proofs
end (* structure AutoCorresData *)
(* Function translation information.
* This is needed for resuming incremental translations. *)
structure AutoCorresFunctionInfo2 = Theory_Data(
@ -127,6 +141,5 @@ structure AutoCorresFunctionInfo2 = Theory_Data(
FunctionInfo2.Phasetab.table Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge (l, r) =
Symtab.merge (fn _ => true) (l, r);
val merge = Symtab.merge (K true);
)

5
tools/autocorres/autocorres_util2.ML
View File

@ -437,6 +437,8 @@ fun par_convert
(existing_infos: FunctionInfo2.function_info Symtab.table)
(* Functions from previous phase *)
(prev_results: FunctionInfo2.phase_results)
(* Add traces from the conversion result. *)
(add_trace: string -> string -> AutoCorresData.Trace -> unit)
(* Return converted functions in recursive groups.
* The groups are tagged with fn_infos from prev_results to identify them. *)
: (FunctionInfo2.function_info Symtab.table * convert_result Symtab.table) FSeq.fseq =
@ -453,6 +455,9 @@ fun par_convert
|> Par_List.map (fn (f, _) =>
(f, convert lthy fn_infos_accum f))
|> Symtab.make;
val _ = app (fn (f, result) => app (fn (typ, trace) =>
add_trace f typ trace) (#traces result))
(Symtab.dest conv_results);
in ((fn_infos, conv_results), fn_infos_accum) end)
existing_infos prev_results;

3
tools/autocorres/heap_lift2.ML
View File

@ -627,6 +627,7 @@ fun translate
(trace_funcs : string list)
(do_opt : bool)
(trace_opt : bool)
(add_trace: string -> string -> AutoCorresData.Trace -> unit)
(hl_function_name : string -> string)
: FunctionInfo2.phase_results =
if FSeq.null l2_results then FSeq.empty () else
@ -871,7 +872,7 @@ let
in (new_infos, lthy') end;
(* Do conversions in parallel. *)
val converted_groups = AutoCorresUtil2.par_convert convert existing_l2_infos l2_results;
val converted_groups = AutoCorresUtil2.par_convert convert existing_l2_infos l2_results add_trace;
(* Sequence of new function_infos and intermediate lthys *)
val def_results = FSeq.mk (fn _ =>

3
tools/autocorres/local_var_extract2.ML
View File

@ -1622,6 +1622,7 @@ fun translate
(existing_l2_infos: FunctionInfo2.function_info Symtab.table)
(do_opt: bool)
(trace_opt: bool)
(add_trace: string -> string -> AutoCorresData.Trace -> unit)
(l2_function_name: string -> string)
: FunctionInfo2.phase_results =
let;
@ -1629,7 +1630,7 @@ let;
val converted_groups =
AutoCorresUtil2.par_convert
(fn lthy => fn l1_infos => convert lthy prog_info l1_infos do_opt trace_opt l2_function_name)
existing_l1_infos l1_results;
existing_l1_infos l1_results add_trace;
(* Sequence of new function_infos and intermediate lthys *)
val def_results = FSeq.mk (fn _ =>

3
tools/autocorres/simpl_conv2.ML
View File

@ -561,6 +561,7 @@ fun translate
(check_termination: bool)
(do_opt: bool)
(trace_opt: bool)
(add_trace: string -> string -> AutoCorresData.Trace -> unit)
(l1_function_name: string -> string)
(lthy: local_theory)
: FunctionInfo2.phase_results =
@ -591,7 +592,7 @@ let
(fn lthy => fn simpl_infos =>
convert lthy prog_info simpl_infos const_to_function check_termination
do_opt trace_opt l1_function_name)
existing_simpl_infos initial_results;
existing_simpl_infos initial_results add_trace;
(* Sequence of new function_infos and intermediate lthys *)
val def_results = AutoCorresUtil2.define_funcs_sequence

35
tools/autocorres/tests/examples/TraceDemo.thy
View File

@ -25,26 +25,31 @@ autocorres [
* These tend to be very large and detailed.
*)
(* All traces are stored in the AutoCorresData.Traces theory data. *)
ML {*
val all_traces = the (Symtab.lookup (AutoCorresData.Traces.get @{theory}) "trace_demo.c")
*}
(* Heap lifting trace. *)
ML {*
AutoCorresData.get_trace @{theory} "trace_demo.c" "HL" "incr"
|> the |> (fn AutoCorresData.RuleTrace x => x)
the (Symtab.lookup (the (Symtab.lookup all_traces "incr")) "HL")
|> (fn AutoCorresData.RuleTrace x => x)
|> AutoCorresTrace.print_ac_trace
|> writeln
*}
(* Word abstraction trace. *)
ML {*
AutoCorresData.get_trace @{theory} "trace_demo.c" "WA" "incr"
|> the |> (fn AutoCorresData.RuleTrace x => x)
the (Symtab.lookup (the (Symtab.lookup all_traces "incr")) "WA")
|> (fn AutoCorresData.RuleTrace x => x)
|> AutoCorresTrace.print_ac_trace
|> writeln
*}
(* To navigate a trace in jEdit, write it to a file: *)
ML {*
AutoCorresData.get_trace @{theory} "trace_demo.c" "HL" "incr"
|> the |> (fn AutoCorresData.RuleTrace x => x)
the (Symtab.lookup (the (Symtab.lookup all_traces "incr")) "HL")
|> (fn AutoCorresData.RuleTrace x => x)
|> AutoCorresTrace.print_ac_trace
|> AutoCorresTrace.writeFile
(Path.append (Resources.master_directory @{theory}) (Path.make ["trace_demo_incr.trace"]) |> Path.implode)
@ -59,30 +64,30 @@ AutoCorresData.get_trace @{theory} "trace_demo.c" "HL" "incr"
(* Peephole optimisations (ie. rewrite rules). *)
ML {*
AutoCorresData.get_trace @{theory} "trace_demo.c" "L2 peephole opt" "incr"
|> the |> (fn AutoCorresData.SimpTrace x => x)
the (Symtab.lookup (the (Symtab.lookup all_traces "incr")) "L2 peephole opt")
|> (fn AutoCorresData.SimpTrace x => x)
*}
(* Flow-sensitive optimisations. If you use the no_opt option, they will be disabled and there will be no trace. *)
ML {*
AutoCorresData.get_trace @{theory} "trace_demo.c" "L2 flow opt" "incr"
Symtab.lookup (the (Symtab.lookup all_traces "incr")) "L2 flow opt"
|> Option.map (fn AutoCorresData.SimpTrace x => x)
*}
ML {*
AutoCorresData.get_trace @{theory} "trace_demo.c" "HL peephole opt" "incr"
|> the |> (fn AutoCorresData.SimpTrace x => x)
the (Symtab.lookup (the (Symtab.lookup all_traces "incr")) "HL peephole opt")
|> (fn AutoCorresData.SimpTrace x => x)
*}
ML {*
AutoCorresData.get_trace @{theory} "trace_demo.c" "HL flow opt" "incr"
Symtab.lookup (the (Symtab.lookup all_traces "incr")) "HL flow opt"
|> Option.map (fn AutoCorresData.SimpTrace x => x)
*}
ML {*
AutoCorresData.get_trace @{theory} "trace_demo.c" "WA peephole opt" "incr"
|> the |> (fn AutoCorresData.SimpTrace x => x)
the (Symtab.lookup (the (Symtab.lookup all_traces "incr")) "WA peephole opt")
|> (fn AutoCorresData.SimpTrace x => x)
*}
ML {*
AutoCorresData.get_trace @{theory} "trace_demo.c" "WA flow opt" "incr"
Symtab.lookup (the (Symtab.lookup all_traces "incr")) "WA flow opt"
|> Option.map (fn AutoCorresData.SimpTrace x => x)
*}

1
tools/autocorres/type_strengthen2.ML
View File

@ -577,6 +577,7 @@ fun translate
(make_function_name : string -> string)
(keep_going : bool)
(do_opt : bool)
(add_trace: string -> string -> AutoCorresData.Trace -> unit)
: FunctionInfo2.phase_results =
if FSeq.null l2_results then FSeq.empty () else
let

10
tools/autocorres/utils.ML
View File

@ -1029,6 +1029,16 @@ fun symtab_merge allow_dups tabs =
|> (if allow_dups then sort_distinct (fast_string_ord o apply2 fst) else I)
|> Symtab.make;
(* Merge with custom merge operation. *)
fun symtab_merge_with merge (tab1, tab2) =
sort_distinct fast_string_ord (Symtab.keys tab1 @ Symtab.keys tab2)
|> map (fn k => (k, case (Symtab.lookup tab1 k, Symtab.lookup tab2 k) of
(SOME x1, SOME x2) => merge (x1, x2)
| (SOME x1, NONE) => x1
| (NONE, SOME x2) => x2
(* (NONE, NONE) impossible *)))
|> Symtab.make
end

3
tools/autocorres/word_abstract2.ML
View File

@ -167,6 +167,7 @@ fun translate
(trace_funcs: string list)
(do_opt: bool)
(trace_opt: bool)
(add_trace: string -> string -> AutoCorresData.Trace -> unit)
(wa_function_name: string -> string)
: FunctionInfo2.phase_results =
if FSeq.null l2_results then FSeq.empty () else
@ -451,7 +452,7 @@ let
in (new_infos, lthy') end;
(* Do conversions in parallel. *)
val converted_groups = AutoCorresUtil2.par_convert convert existing_l2_infos l2_results;
val converted_groups = AutoCorresUtil2.par_convert convert existing_l2_infos l2_results add_trace;
(* Sequence of intermediate states: (lthy, new_defs) *)
val def_results = FSeq.mk (fn _ =>