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

trivial: autocorres: refactor symtab_merge

This commit is contained in:
Japheth Lim 2016-06-28 16:10:21 +10:00
parent 6ce286e3b6
commit 6c35cf176a
3 changed files with 14 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
tools/autocorres/tests/examples/type_strengthen_tricks.thy
View File

@ -59,10 +59,7 @@ let val filename = "type_strengthen.c";
val no_heap_abs = ["opt_j"];
val force_heap_abs = [];
(*
val hl_results = l2_results;
*)
val hl_results =
val hl_results = if false then l2_results else
HeapLift2.translate filename prog_info l2_results' HL_setup
(Symset.make no_heap_abs) (Symset.make force_heap_abs)
heap_abs_syntax keep_going
@ -70,10 +67,7 @@ let val filename = "type_strengthen.c";
val unsigned_abs = ["opt_a"];
val no_signed_abs = [];
(*
val wa_results = hl_results;
*)
val wa_results =
val wa_results = if false then hl_results else
WordAbstract2.translate filename prog_info hl_results
(Symset.make unsigned_abs) (Symset.make no_signed_abs) []
do_opt trace_opt (fn f => "wa_" ^ f ^ "'");
@ -83,11 +77,11 @@ let val filename = "type_strengthen.c";
TypeStrengthen2.translate ts_rules Symtab.empty filename prog_info
wa_results (fn f => f ^ "'") keep_going do_opt;
val l1_results' = FSeq.list_of l1_results |> map snd |> TypeStrengthen2.symtab_merge false;
val l2_results' = FSeq.list_of l2_results |> map snd |> TypeStrengthen2.symtab_merge false;
val hl_results' = FSeq.list_of hl_results |> map snd |> TypeStrengthen2.symtab_merge false;
val wa_results' = FSeq.list_of wa_results |> map snd |> TypeStrengthen2.symtab_merge false;
val ts_results' = FSeq.list_of ts_results |> map snd |> TypeStrengthen2.symtab_merge false;
val l1_results' = FSeq.list_of l1_results |> map snd |> Utils.symtab_merge false;
val l2_results' = FSeq.list_of l2_results |> map snd |> Utils.symtab_merge false;
val hl_results' = FSeq.list_of hl_results |> map snd |> Utils.symtab_merge false;
val wa_results' = FSeq.list_of wa_results |> map snd |> Utils.symtab_merge false;
val ts_results' = FSeq.list_of ts_results |> map snd |> Utils.symtab_merge false;
val _ = result_infos := FunctionInfo2.Phasetab.make
[(FunctionInfo2.CP, simpl_info),
(FunctionInfo2.L1, l1_results'),

7
tools/autocorres/type_strengthen2.ML
View File

@ -603,11 +603,6 @@ in
writeln ("Type Strengthening Statistics: \n" ^ data)
end
fun symtab_merge allow_dups tabs =
maps Symtab.dest tabs
|> (if allow_dups then sort_distinct (fast_string_ord o apply2 fst) else I)
|> Symtab.make;
(* Run through every function, attempting to strengthen its type.
* FIXME: this stage is currently completely sequential. Conversions
* that do not depend on each other should be in parallel;
@ -627,7 +622,7 @@ let
(* Wait for previous stage to finish first. *)
val l2_results = FSeq.list_of l2_results;
val lthy = List.last l2_results |> fst;
val l2_infos = symtab_merge false (map snd l2_results);
val l2_infos = Utils.symtab_merge false (map snd l2_results);
(* Prettify bound variable names in definitions. *)
val l2_infos = Symtab.map (fn f_name => fn info => let

6
tools/autocorres/utils.ML
View File

@ -1023,6 +1023,12 @@ val _ = assert (apply2 Substring.string (positionr "br" (Substring.full "abracad
val _ = assert (apply2 Substring.string (positionr "xx" (Substring.full "abracadabra"))
= ("abracadabra", "")) ""
(* Merge a list of Symtabs. *)
fun symtab_merge allow_dups tabs =
maps Symtab.dest tabs
|> (if allow_dups then sort_distinct (fast_string_ord o apply2 fst) else I)
|> Symtab.make;
end