WIP: autocorres: hacky proof of concept for incremental translation.
Demo in tests/examples/Incremental. Note that changing autocorres options between invocations will probably just fail ungracefully. Meant for issue VER-518 but not yet tested on CKernel.
This commit is contained in:
Japheth Lim
parent
a6f8332d60
commit
7f97e0b34a
|
|
@ -296,7 +296,7 @@ fun default_opts _ = {
|
|||
lifted_globals_field_suffix = ref NONE,
|
||||
function_name_prefix = ref NONE,
|
||||
function_name_suffix = ref NONE
|
||||
}
|
||||
} : autocorres_options
|
||||
|
||||
(* Combined parser. *)
|
||||
val autocorres_parser : (autocorres_options * string) parser =
|
||||
|
|
@ -358,8 +358,8 @@ let
|
|||
|
||||
(* Fetch basic program information. *)
|
||||
val prog_info = ProgramInfo.get_prog_info lthy filename
|
||||
val fn_info = FunctionInfo.init_fn_info lthy filename
|
||||
val all_simpl_functions = Symset.make (Symtab.keys (FunctionInfo.get_functions fn_info))
|
||||
val basic_fn_info = FunctionInfo.init_fn_info lthy filename
|
||||
val all_simpl_functions = Symset.make (Symtab.keys (FunctionInfo.get_functions basic_fn_info))
|
||||
|
||||
(* Process autocorres options. *)
|
||||
val keep_going = !(#keep_going opt) = SOME true
|
||||
|
|
@ -378,23 +378,6 @@ let
|
|||
else ()
|
||||
val no_heap_abs = these (!(#no_heap_abs opt))
|
||||
|
||||
(* Disallow referring to functions that don't exist. *)
|
||||
val funcs_in_options =
|
||||
these (!(#no_heap_abs opt))
|
||||
@ these (!(#force_heap_abs opt))
|
||||
@ these (!(#unsigned_word_abs opt))
|
||||
@ these (!(#no_signed_word_abs opt))
|
||||
@ these (!(#scope opt))
|
||||
@ Symtab.keys (!(#ts_force opt))
|
||||
@ these (!(#trace_heap_lift opt))
|
||||
@ these (!(#trace_word_abs opt))
|
||||
val invalid_functions =
|
||||
Symset.subtract all_simpl_functions (Symset.make funcs_in_options)
|
||||
val _ =
|
||||
if Symset.card invalid_functions > 0 then
|
||||
error ("autocorres: no such function(s): " ^ commas (Symset.dest invalid_functions))
|
||||
else ()
|
||||
|
||||
(* Resolve rule names for ts_rules and ts_force. *)
|
||||
val ts_force = Symtab.map (K (fn name => Monad_Types.get_monad_type name (Context.Proof lthy)
|
||||
|> the handle Option => Monad_Types.error_no_such_mt name))
|
||||
|
|
@ -413,59 +396,115 @@ let
|
|||
else
|
||||
()
|
||||
|
||||
(* (Finished processing options.) *)
|
||||
|
||||
val old_fn_info = Symtab.lookup (AutoCorresFunctionInfo.get thy) filename
|
||||
val _ = if not (isSome old_fn_info) then () else
|
||||
tracing ("Attempting to restart from previous translation of " ^ filename)
|
||||
|
||||
(* Skip functions that have already been translated. *)
|
||||
val old_translations = Option.getOpt (Option.map FunctionInfo.get_functions old_fn_info, Symtab.empty)
|
||||
|> Symtab.dest |> map fst |> Symset.make
|
||||
|
||||
(* Determine which functions should be translated.
|
||||
* If "scope" is not specified, we translate all functions.
|
||||
* Otherwise, we translate only "scope"d functions and their direct callees
|
||||
* (which are translated using a trivial wrapper so that they can be called). *)
|
||||
val (functions_to_translate, functions_to_wrap) =
|
||||
case !(#scope opt) of
|
||||
NONE => (all_simpl_functions, Symset.empty)
|
||||
| SOME x =>
|
||||
let
|
||||
val scope_depth = the_default 2 (!(#scope_depth opt))
|
||||
val get_deps = get_function_deps (FunctionInfo.get_function_callees basic_fn_info)
|
||||
val funcs = get_deps x scope_depth
|
||||
val _ = tracing ("autocorres scope: selected " ^ Int.toString (Symset.card funcs) ^ " function(s):")
|
||||
val _ = app (fn f => tracing (" " ^ f)) (Symset.dest funcs)
|
||||
val funcs_callees =
|
||||
Symset.subtract (Symset.union old_translations funcs) (get_deps (Symset.dest funcs) 1)
|
||||
val _ = if Symset.is_empty funcs_callees then () else
|
||||
(tracing ("autocorres scope: wrapping " ^
|
||||
Int.toString (Symset.card funcs_callees) ^ " function(s):");
|
||||
app (fn f => tracing (" " ^ f)) (Symset.dest funcs_callees))
|
||||
in (funcs, funcs_callees) end
|
||||
|
||||
(* Functions that have already been translated cannot be translated again. *)
|
||||
val already_translated = Symset.inter old_translations functions_to_translate
|
||||
val _ = if Symset.is_empty already_translated then () else
|
||||
error ("autocorres scope: these functions have already been translated: " ^
|
||||
commas (Symset.dest already_translated))
|
||||
|
||||
(* If a function has no SIMPL body, we will not wrap its body;
|
||||
* instead we create a dummy definition and translate it via the usual process. *)
|
||||
val undefined_functions =
|
||||
Symset.filter (fn f => #invented_body (FunctionInfo.get_function_def basic_fn_info f)) functions_to_wrap
|
||||
val functions_to_wrap = Symset.subtract undefined_functions functions_to_wrap
|
||||
val functions_to_translate = Symset.union undefined_functions functions_to_translate
|
||||
|
||||
(* We will process these functions... *)
|
||||
val functions_to_process = Symset.union functions_to_translate functions_to_wrap
|
||||
(* ... and ignore these functions. *)
|
||||
val functions_to_ignore = Symset.subtract functions_to_process all_simpl_functions
|
||||
|
||||
(* Only translate "scope" functions and their direct callees. *)
|
||||
val fn_info = FunctionInfo.map_fn_info (fn def =>
|
||||
if Symset.contains functions_to_translate (#name def) then
|
||||
SOME (FunctionInfo.fn_def_update_is_simpl_wrapper false def)
|
||||
else if Symset.contains functions_to_wrap (#name def) then
|
||||
SOME (FunctionInfo.fn_def_update_is_simpl_wrapper true def)
|
||||
else
|
||||
NONE) basic_fn_info
|
||||
|
||||
(* Don't consider function calls in un-translated functions in our call graph. *)
|
||||
val fn_info = FunctionInfo.set_autocorres_scope fn_info functions_to_process
|
||||
|
||||
(* Disallow referring to functions that don't exist or are excluded from processing. *)
|
||||
val funcs_in_options =
|
||||
these (!(#no_heap_abs opt))
|
||||
@ these (!(#force_heap_abs opt))
|
||||
@ these (!(#unsigned_word_abs opt))
|
||||
@ these (!(#no_signed_word_abs opt))
|
||||
@ these (!(#scope opt))
|
||||
@ Symtab.keys (!(#ts_force opt))
|
||||
@ these (!(#trace_heap_lift opt))
|
||||
@ these (!(#trace_word_abs opt))
|
||||
|> Symset.make
|
||||
val invalid_functions =
|
||||
Symset.subtract all_simpl_functions funcs_in_options
|
||||
val ignored_functions =
|
||||
Symset.subtract (Symset.union invalid_functions functions_to_process) funcs_in_options
|
||||
val _ =
|
||||
if Symset.card invalid_functions > 0 then
|
||||
error ("autocorres: no such function(s): " ^ commas (Symset.dest invalid_functions))
|
||||
else if Symset.card ignored_functions > 0 then
|
||||
error ("autocorres: cannot configure translation for excluded function(s): " ^
|
||||
commas (Symset.dest ignored_functions))
|
||||
else
|
||||
()
|
||||
|
||||
(* Check that recursive function groups are all lifted to the same monad. *)
|
||||
val _ = FunctionInfo.get_topo_sorted_functions fn_info
|
||||
|> map (TypeStrengthen.compute_lift_rules ts_rules ts_force)
|
||||
|
||||
(* (Finished processing options.) *)
|
||||
|
||||
(* Determine which functions should be translated. *)
|
||||
val all_functions =
|
||||
case !(#scope opt) of
|
||||
NONE => all_simpl_functions
|
||||
| SOME x =>
|
||||
let
|
||||
val scope_depth = the_default 2 (!(#scope_depth opt))
|
||||
val funcs = get_function_deps (FunctionInfo.get_function_callees fn_info) x scope_depth
|
||||
val _ = tracing ("autocorres scope: selected " ^ Int.toString (Symset.card funcs) ^ " function(s):")
|
||||
val _ = app (fn f => tracing (" " ^ f)) (Symset.dest funcs)
|
||||
in funcs end
|
||||
|
||||
(* Mark functions that shouldn't be processed.
|
||||
* We will generate wrappers to call them (L1_call_simpl ... AC_call_simpl). *)
|
||||
val undefined_functions =
|
||||
Symset.filter (fn f => #invented_body (FunctionInfo.get_function_def fn_info f)) all_simpl_functions
|
||||
val all_functions = Symset.union all_functions undefined_functions
|
||||
val untranslated_functions =
|
||||
Symset.subtract (Symset.union all_functions undefined_functions) all_simpl_functions
|
||||
|
||||
val fn_info = FunctionInfo.map_fn_info (fn def =>
|
||||
SOME (if Symset.contains all_functions (#name def) then def
|
||||
else FunctionInfo.fn_def_update_is_simpl_wrapper true def)) fn_info
|
||||
|
||||
(* Don't consider function calls in un-translated functions. *)
|
||||
val fn_info = FunctionInfo.set_autocorres_scope fn_info all_functions
|
||||
|
||||
(* Disable heap lifting for all un-translated functions. *)
|
||||
val conflicting_heap_lift_fns =
|
||||
Symset.inter untranslated_functions (Symset.make (these (!(#force_heap_abs opt))))
|
||||
val force_heap_abs = Symset.make (these (!(#force_heap_abs opt)))
|
||||
val conflicting_heap_lift_fns = Symset.subtract functions_to_translate force_heap_abs
|
||||
val _ = if not (Symset.is_empty conflicting_heap_lift_fns) then
|
||||
error ("autocorres: Functions marked 'force_heap_abs' but excluded from 'scope': "
|
||||
^ commas (Symset.dest conflicting_heap_lift_fns))
|
||||
else
|
||||
()
|
||||
|
||||
val no_heap_abs = Symset.union (Symset.make no_heap_abs) untranslated_functions
|
||||
val no_heap_abs = Symset.union (Symset.make no_heap_abs) functions_to_wrap
|
||||
|
||||
(* Disable word abstraction for all un-translated functions. *)
|
||||
val unsigned_word_abs = these (!(#unsigned_word_abs opt)) |> Symset.make
|
||||
val no_signed_word_abs = these (!(#no_signed_word_abs opt)) |> Symset.make
|
||||
val conflicting_unsigned_abs_fns =
|
||||
Symset.inter untranslated_functions unsigned_word_abs
|
||||
Symset.subtract functions_to_translate unsigned_word_abs
|
||||
val _ = if Symset.is_empty conflicting_unsigned_abs_fns then () else
|
||||
error ("autocorres: Functions marked 'unsigned_word_abs' but excluded from 'scope': "
|
||||
^ commas (Symset.dest conflicting_unsigned_abs_fns))
|
||||
val no_signed_word_abs = Symset.union no_signed_word_abs untranslated_functions
|
||||
val no_signed_word_abs = Symset.union no_signed_word_abs functions_to_wrap
|
||||
|
||||
(*
|
||||
* Sanity check the C parser's output.
|
||||
|
|
@ -476,14 +515,17 @@ let
|
|||
*)
|
||||
val sanity_errors = AutoCorresUtil.map_all lthy fn_info (fn fn_name =>
|
||||
let
|
||||
val info = FunctionInfo.get_function_def fn_info fn_name
|
||||
val def =
|
||||
FunctionInfo.get_function_def fn_info fn_name
|
||||
info
|
||||
|> #definition
|
||||
|> Thm.prop_of
|
||||
|> Utils.rhs_of
|
||||
in
|
||||
(Syntax.check_term lthy def; NONE)
|
||||
handle (ERROR str) => SOME (fn_name, str)
|
||||
(* Exclude already-translated functions *)
|
||||
if #finished info then NONE (* ignore *) else
|
||||
((Syntax.check_term lthy def; NONE)
|
||||
handle (ERROR str) => SOME (fn_name, str))
|
||||
end)
|
||||
|> map_filter I
|
||||
val _ =
|
||||
|
|
@ -502,7 +544,7 @@ let
|
|||
* something else. *)
|
||||
val ts_force = let
|
||||
val invented_functions =
|
||||
all_functions
|
||||
functions_to_process
|
||||
(* Select functions with an invented body. *)
|
||||
|> Symset.filter (fn n => FunctionInfo.get_function_def fn_info n |> #invented_body)
|
||||
(* Ignore functions which already have a "ts_force" rule applied to them. *)
|
||||
|
|
@ -533,24 +575,128 @@ let
|
|||
| SOME s => s
|
||||
in fn f => prefix ^ f ^ suffix end
|
||||
|
||||
(* For resuming a translation, we resurrect intermediate data for
|
||||
* previously-translated callees and shove it into fn_info. *)
|
||||
fun resurrect_fn_def phase fn_name =
|
||||
if phase = "CP"
|
||||
then FunctionInfo.get_function_def basic_fn_info fn_name
|
||||
|> FunctionInfo.fn_def_update_finished true
|
||||
else let
|
||||
val fn_def = Utils.the' ("Failed to retrieve definition for " ^ fn_name ^ " (" ^ phase ^ ")")
|
||||
(AutoCorresData.get_def thy filename (phase ^ "def") fn_name)
|
||||
val mono_thm = @{thm TrueI} (* FIXME: oops, we didn't actually store these anywhere *)
|
||||
val (raw_const, raw_args) = strip_comb (Utils.lhs_of_eq (Thm.prop_of fn_def))
|
||||
val (locale_args, call_args) = take_prefix is_Free raw_args
|
||||
val fn_const = betapplys (raw_const, locale_args)
|
||||
val call_args = map (fn Var ((n, _), T) => (n, T)) call_args
|
||||
val (measure_arg, fn_args) = case call_args of
|
||||
(m as ("rec_measure'", @{typ nat})) :: args => (SOME m, args)
|
||||
| _ => (NONE, call_args)
|
||||
val basic_info = FunctionInfo.get_function_def basic_fn_info fn_name
|
||||
val fn_args = if phase = "L1" then #args basic_info else fn_args (* L1 doesn't have lifted args yet *)
|
||||
val info = {
|
||||
name = fn_name,
|
||||
args = fn_args,
|
||||
return_type = #return_type basic_info, (* FIXME: won't work with word abs *)
|
||||
const = fn_const,
|
||||
raw_const = raw_const,
|
||||
definition = fn_def,
|
||||
mono_thm = mono_thm,
|
||||
invented_body = #invented_body basic_info,
|
||||
is_simpl_wrapper = #is_simpl_wrapper basic_info,
|
||||
finished = true
|
||||
} : FunctionInfo.function_def
|
||||
in info end
|
||||
|
||||
fun munge_old_funcs phase (FunctionInfo.FunctionInfo {
|
||||
function_info, function_callees, const_to_function,
|
||||
topo_sorted_functions, recursive_functions }) = let
|
||||
(* HACK: AutoCorresUtil uses topo_sorted_functions to decide which functions
|
||||
* to translate. So we simply add the old function info to fn_info
|
||||
* but leave topo_sorted_functions unchanged. *)
|
||||
val old_function_info =
|
||||
Option.getOpt (Option.map FunctionInfo.get_functions old_fn_info, Symtab.empty)
|
||||
|> Symtab.dest
|
||||
|> List.mapPartial (try (fn (f_name, _) => (f_name, resurrect_fn_def phase f_name)))
|
||||
|> Symtab.make
|
||||
val old_const_to_function =
|
||||
Symtab.dest old_function_info
|
||||
|> map (fn (_, fn_def) => (#raw_const fn_def, #name fn_def))
|
||||
|> Termtab.make
|
||||
(* add dependencies from functions_to_translate to already-translated functions *)
|
||||
val new_function_callees = case basic_fn_info of FunctionInfo.FunctionInfo x =>
|
||||
Symtab.dest (#function_callees x)
|
||||
|> filter (fn (fn_name, _) => Symset.contains functions_to_process fn_name)
|
||||
|> map (apsnd (filter (Symtab.defined old_function_info)))
|
||||
val function_callees' =
|
||||
fold (fn (fn_name, callees) =>
|
||||
Symtab.map_default (fn_name, callees) (fn callees' =>
|
||||
Symset.dest (Symset.union (Symset.make callees) (Symset.make callees'))))
|
||||
new_function_callees function_callees
|
||||
val old_recursive_functions = case old_fn_info of
|
||||
NONE => Symtab.empty
|
||||
| SOME (FunctionInfo.FunctionInfo x) => #recursive_functions x
|
||||
in FunctionInfo.FunctionInfo {
|
||||
(* fn_info may contain previously-munged info, so we overwrite that by
|
||||
* passing its components as the second argument to Table.merge *)
|
||||
function_info = Symtab.merge (K true) (old_function_info, function_info),
|
||||
function_callees = function_callees',
|
||||
const_to_function = Termtab.merge (K true) (old_const_to_function, const_to_function),
|
||||
topo_sorted_functions = topo_sorted_functions,
|
||||
recursive_functions = Symtab.merge (K true) (old_recursive_functions, recursive_functions) } end
|
||||
|
||||
(* Do the translation. *)
|
||||
val _ = @{trace} ("debug: initial fn_info", FunctionInfo.get_functions fn_info |> Symtab.dest)
|
||||
val fn_info = if not (isSome old_fn_info) then fn_info else
|
||||
munge_old_funcs "CP" fn_info |> tap (fn fn_info =>
|
||||
@{trace} ("debug: initial fn_info, munged", FunctionInfo.get_functions fn_info |> Symtab.dest,
|
||||
case fn_info of FunctionInfo.FunctionInfo x => Symtab.dest (#function_callees x)))
|
||||
val (lthy, fn_info) =
|
||||
SimplConv.translate_simpl
|
||||
filename prog_info fn_info
|
||||
do_opt trace_opt (prefix "l1_" o make_function_name) lthy
|
||||
|
||||
val _ = @{trace} ("debug: L1 fn_info", FunctionInfo.get_functions fn_info |> Symtab.dest)
|
||||
val fn_info = if not (isSome old_fn_info) then fn_info else
|
||||
munge_old_funcs "L1" fn_info |> tap (fn fn_info =>
|
||||
@{trace} ("debug: L1 fn_info, munged", FunctionInfo.get_functions fn_info |> Symtab.dest,
|
||||
case fn_info of FunctionInfo.FunctionInfo x => Symtab.dest (#function_callees x)))
|
||||
val (lthy, fn_info) =
|
||||
LocalVarExtract.translate_l2 filename prog_info fn_info do_opt trace_opt (prefix "l2_" o make_function_name) lthy
|
||||
|
||||
val force_heap_abs = Symset.make (these (!(#force_heap_abs opt)))
|
||||
val (lthy, fn_info) =
|
||||
if !(#skip_heap_abs opt) = SOME true then (lthy, fn_info) else
|
||||
HeapLift.system_heap_lift filename prog_info fn_info
|
||||
no_heap_abs force_heap_abs
|
||||
make_lifted_globals_field_name heap_abs_syntax keep_going
|
||||
(these (!(#trace_heap_lift opt))) do_opt trace_opt
|
||||
(prefix "hl_" o make_function_name) gen_word_heaps lthy
|
||||
val _ = @{trace} ("debug: L2 fn_info", FunctionInfo.get_functions fn_info |> Symtab.dest)
|
||||
val fn_info = if not (isSome old_fn_info) then fn_info else
|
||||
munge_old_funcs "L2" fn_info |> tap (fn fn_info =>
|
||||
@{trace} ("debug: L2 fn_info, munged", FunctionInfo.get_functions fn_info |> Symtab.dest,
|
||||
case fn_info of FunctionInfo.FunctionInfo x => Symtab.dest (#function_callees x)))
|
||||
|
||||
val (lthy, fn_info) =
|
||||
if !(#skip_heap_abs opt) = SOME true then (lthy, fn_info) else let
|
||||
(* Create base definitions for the new program, including a new
|
||||
* "globals" record with a lifted heap. *)
|
||||
val (heap_info, lthy) = case Symtab.lookup (HeapInfo.get thy) filename of
|
||||
(* Use basic_fn_info so that our generated heap will work for all functions,
|
||||
* even if the user selected a subset for this run *)
|
||||
NONE => let val (heap_info, lthy) =
|
||||
HeapLiftBase.setup prog_info basic_fn_info
|
||||
make_lifted_globals_field_name gen_word_heaps lthy
|
||||
(* Save the heap info to the theory data. *)
|
||||
val lthy = Local_Theory.background_theory (
|
||||
HeapInfo.map (fn tbl =>
|
||||
Symtab.update (filename, heap_info) tbl)) lthy
|
||||
in (heap_info, lthy) end
|
||||
| SOME heap_info => (heap_info, lthy)
|
||||
in HeapLift.system_heap_lift filename prog_info fn_info heap_info
|
||||
no_heap_abs force_heap_abs
|
||||
heap_abs_syntax keep_going
|
||||
(these (!(#trace_heap_lift opt))) do_opt trace_opt
|
||||
(prefix "hl_" o make_function_name) lthy end
|
||||
|
||||
val _ = @{trace} ("debug: HL fn_info", FunctionInfo.get_functions fn_info |> Symtab.dest)
|
||||
val fn_info = if not (isSome old_fn_info) then fn_info else
|
||||
munge_old_funcs "HL" fn_info |> tap (fn fn_info =>
|
||||
@{trace} ("debug: HL fn_info, munged", FunctionInfo.get_functions fn_info |> Symtab.dest,
|
||||
case fn_info of FunctionInfo.FunctionInfo x => Symtab.dest (#function_callees x)))
|
||||
val (lthy, fn_info) =
|
||||
if skip_word_abs then (lthy, fn_info) else
|
||||
WordAbstract.word_abstract
|
||||
|
|
@ -559,6 +705,11 @@ let
|
|||
(these (!(#trace_word_abs opt))) do_opt trace_opt
|
||||
(prefix "wa_" o make_function_name) lthy
|
||||
|
||||
val _ = @{trace} ("debug: WA fn_info", FunctionInfo.get_functions fn_info |> Symtab.dest)
|
||||
val fn_info = if not (isSome old_fn_info) then fn_info else
|
||||
munge_old_funcs "WA" fn_info |> tap (fn fn_info =>
|
||||
@{trace} ("debug: WA fn_info, munged", FunctionInfo.get_functions fn_info |> Symtab.dest,
|
||||
case fn_info of FunctionInfo.FunctionInfo x => Symtab.dest (#function_callees x)))
|
||||
val (lthy, fn_info) =
|
||||
TypeStrengthen.type_strengthen
|
||||
ts_rules ts_force filename prog_info fn_info make_function_name
|
||||
|
|
@ -566,6 +717,10 @@ let
|
|||
|
||||
(* Save fn_info for future reference. *)
|
||||
val _ = tracing "Saving function info to AutoCorresFunctionInfo."
|
||||
val fn_info = if not (isSome old_fn_info) then fn_info else
|
||||
munge_old_funcs "TS" fn_info |> tap (fn fn_info =>
|
||||
@{trace} ("debug: TS fn_info, munged", FunctionInfo.get_functions fn_info |> Symtab.dest,
|
||||
case fn_info of FunctionInfo.FunctionInfo x => Symtab.dest (#function_callees x)))
|
||||
val lthy = Local_Theory.background_theory (
|
||||
AutoCorresFunctionInfo.map (fn tbl =>
|
||||
Symtab.update (filename, fn_info) tbl)) lthy
|
||||
|
|
|
|||
|
|
@ -16,6 +16,7 @@ sig
|
|||
val translate :
|
||||
local_theory
|
||||
-> FunctionInfo.fn_info
|
||||
-> 'b Symtab.table
|
||||
-> (local_theory -> string -> 'a)
|
||||
-> (local_theory -> 'b Symtab.table -> 'c -> (string * 'a) list -> ('b list * 'c * local_theory))
|
||||
-> (FunctionInfo.function_def list -> local_theory -> thm list)
|
||||
|
|
@ -142,7 +143,7 @@ fun has_simpl_body_def lthy name =
|
|||
* "define" is handed a list of functions which must all be defined in one
|
||||
* step.
|
||||
*)
|
||||
fun translate lthy fn_info convert define prove_mono fn_def_translate v =
|
||||
fun translate lthy fn_info initial_callees convert define prove_mono fn_def_translate v =
|
||||
let
|
||||
(* Get list of functions we need to translate. *)
|
||||
val function_groups = FunctionInfo.get_topo_sorted_functions fn_info
|
||||
|
|
@ -179,7 +180,7 @@ fun translate lthy fn_info convert define prove_mono fn_def_translate v =
|
|||
end
|
||||
|
||||
val (proof_table, new_fn_defs, v, lthy)
|
||||
= fold translate function_groups (Symtab.empty, Symtab.empty, v, lthy)
|
||||
= fold translate function_groups (initial_callees, Symtab.empty, v, lthy)
|
||||
|
||||
val mono_thms =
|
||||
function_groups
|
||||
|
|
@ -635,9 +636,16 @@ let
|
|||
val do_define_funcs =
|
||||
define_funcs phase filename fn_info get_const_name get_fn_type
|
||||
get_fn_assumption get_fn_args rec_base_case
|
||||
val initial_callees = Symtab.dest (FunctionInfo.get_functions fn_info)
|
||||
|> List.mapPartial (fn (fn_name, fn_def) =>
|
||||
if not (#finished fn_def) then NONE else
|
||||
AutoCorresData.get_thm (Proof_Context.theory_of ctxt)
|
||||
filename (phase ^ "corres") fn_name
|
||||
|> Option.map (fn thm => (fn_name, thm)))
|
||||
|> Symtab.make
|
||||
|
||||
(* Do the translation. *)
|
||||
val (ctxt', new_fn_info, _) = translate ctxt fn_info do_gen_corres do_define_funcs prove_mono
|
||||
val (ctxt', new_fn_info, _) = translate ctxt fn_info initial_callees do_gen_corres do_define_funcs prove_mono
|
||||
(fn lthy => K (update_fn_info lthy)) ()
|
||||
|
||||
(* Map function information. *)
|
||||
|
|
|
|||
|
|
@ -14,7 +14,6 @@
|
|||
*)
|
||||
signature FUNCTION_INFO =
|
||||
sig
|
||||
type fn_info;
|
||||
|
||||
type function_def = {
|
||||
name : string,
|
||||
|
|
@ -25,7 +24,25 @@ sig
|
|||
definition : thm,
|
||||
mono_thm : thm,
|
||||
invented_body : bool,
|
||||
is_simpl_wrapper : bool
|
||||
is_simpl_wrapper : bool,
|
||||
finished : bool
|
||||
};
|
||||
|
||||
datatype fn_info = FunctionInfo of {
|
||||
(* Database of "function_info" records. *)
|
||||
function_info : function_def Symtab.table,
|
||||
|
||||
(* Functions directly called by a particular function. *)
|
||||
function_callees : string list Symtab.table,
|
||||
|
||||
(* Mapping from "const" back to the function name. (cache) *)
|
||||
const_to_function : string Termtab.table,
|
||||
|
||||
(* Topologically sorted functions, based on call graph. (cache) *)
|
||||
topo_sorted_functions : string list list,
|
||||
|
||||
(* List of recursive calls a function makes. (cache) *)
|
||||
recursive_functions : string list Symtab.table
|
||||
};
|
||||
|
||||
val init_fn_info : Proof.context -> string -> fn_info;
|
||||
|
|
@ -49,6 +66,7 @@ sig
|
|||
val fn_def_update_mono_thm : thm -> function_def -> function_def;
|
||||
val fn_def_update_invented_body : bool -> function_def -> function_def;
|
||||
val fn_def_update_is_simpl_wrapper : bool -> function_def -> function_def;
|
||||
val fn_def_update_finished : bool -> function_def -> function_def;
|
||||
|
||||
val is_function_recursive : fn_info -> string -> bool;
|
||||
val get_recursive_group : fn_info -> string -> string list;
|
||||
|
|
@ -89,7 +107,11 @@ type function_def = {
|
|||
|
||||
(* Is this just a wrapper around a SIMPL procedure?
|
||||
* True if function is excluded from translation "scope". *)
|
||||
is_simpl_wrapper : bool
|
||||
is_simpl_wrapper : bool,
|
||||
|
||||
(* Remember whether we have already translated this function,
|
||||
* and should skip it on later runs. *)
|
||||
finished : bool
|
||||
};
|
||||
|
||||
datatype fn_info = FunctionInfo of {
|
||||
|
|
@ -241,7 +263,8 @@ let
|
|||
definition = hd definition,
|
||||
mono_thm = @{thm TrueI}, (* placeholder *)
|
||||
invented_body = invented,
|
||||
is_simpl_wrapper = false
|
||||
is_simpl_wrapper = false,
|
||||
finished = false
|
||||
}
|
||||
end
|
||||
in
|
||||
|
|
@ -325,34 +348,38 @@ fun get_topo_sorted_functions (FunctionInfo functions) =
|
|||
(* SML record update insanity. *)
|
||||
fun fn_def_update_name new_val old
|
||||
= { name = new_val,
|
||||
args = #args old, return_type = #return_type old, const = #const old, raw_const = #raw_const old, definition = #definition old, mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old }
|
||||
args = #args old, return_type = #return_type old, const = #const old, raw_const = #raw_const old, definition = #definition old, mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old, finished = #finished old }
|
||||
fun fn_def_update_args new_val old
|
||||
= { name = #name old,
|
||||
args = new_val,
|
||||
return_type = #return_type old, const = #const old, raw_const = #raw_const old, definition = #definition old, mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old }
|
||||
return_type = #return_type old, const = #const old, raw_const = #raw_const old, definition = #definition old, mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old, finished = #finished old }
|
||||
fun fn_def_update_const new_val old
|
||||
= { name = #name old, args = #args old, return_type = #return_type old,
|
||||
const = new_val, raw_const = head_of new_val,
|
||||
definition = #definition old, mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old }
|
||||
definition = #definition old, mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old, finished = #finished old }
|
||||
fun fn_def_update_definition new_val old
|
||||
= { name = #name old, args = #args old, return_type = #return_type old, const = #const old, raw_const = #raw_const old,
|
||||
definition = new_val,
|
||||
mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old }
|
||||
mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old, finished = #finished old }
|
||||
fun fn_def_update_return_type new_val old
|
||||
= { name = #name old, args = #args old,
|
||||
return_type = new_val,
|
||||
const = #const old, raw_const = #raw_const old, definition = #definition old, mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old }
|
||||
const = #const old, raw_const = #raw_const old, definition = #definition old, mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old, finished = #finished old }
|
||||
fun fn_def_update_mono_thm new_val old
|
||||
= { name = #name old, args = #args old, return_type = #return_type old, const = #const old, raw_const = #raw_const old, definition = #definition old,
|
||||
mono_thm = new_val,
|
||||
invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old }
|
||||
invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old, finished = #finished old }
|
||||
fun fn_def_update_invented_body new_val old
|
||||
= { name = #name old, args = #args old, return_type = #return_type old, const = #const old, raw_const = #raw_const old, definition = #definition old, mono_thm = #mono_thm old,
|
||||
invented_body = new_val,
|
||||
is_simpl_wrapper = #is_simpl_wrapper old }
|
||||
is_simpl_wrapper = #is_simpl_wrapper old, finished = #finished old }
|
||||
fun fn_def_update_is_simpl_wrapper new_val old
|
||||
= { name = #name old, args = #args old, return_type = #return_type old, const = #const old, raw_const = #raw_const old, definition = #definition old, mono_thm = #mono_thm old, invented_body = #invented_body old,
|
||||
is_simpl_wrapper = new_val }
|
||||
is_simpl_wrapper = new_val,
|
||||
finished = #finished old }
|
||||
fun fn_def_update_finished new_val old
|
||||
= { name = #name old, args = #args old, return_type = #return_type old, const = #const old, raw_const = #raw_const old, definition = #definition old, mono_thm = #mono_thm old, invented_body = #invented_body old, is_simpl_wrapper = #is_simpl_wrapper old,
|
||||
finished = new_val }
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -375,22 +375,17 @@ fun system_heap_lift
|
|||
(filename : string)
|
||||
(prog_info : ProgramInfo.prog_info)
|
||||
(fn_info : FunctionInfo.fn_info)
|
||||
(heap_info : HeapLiftBase.heap_info)
|
||||
(no_heap_abs : Symset.key Symset.set)
|
||||
(force_heap_abs : Symset.key Symset.set)
|
||||
(make_lifted_globals_field_name : string -> string)
|
||||
(heap_abs_syntax : bool)
|
||||
(keep_going : bool)
|
||||
(trace_funcs : string list)
|
||||
(do_opt : bool)
|
||||
(trace_opt : bool)
|
||||
(hl_function_name : string -> string)
|
||||
(gen_word_heaps : bool)
|
||||
lthy =
|
||||
let
|
||||
(* Create base definitions for the new program, including a new
|
||||
* "globals" record with a lifted heap. *)
|
||||
val (heap_info, lthy) = HeapLiftBase.setup prog_info fn_info make_lifted_globals_field_name gen_word_heaps lthy
|
||||
|
||||
(* Do some extra lifting and create syntax (see field_syntax comment). *)
|
||||
val (syntax_lift_rules, lthy) =
|
||||
if not heap_abs_syntax then
|
||||
|
|
@ -748,11 +743,6 @@ let
|
|||
(if member (op =) trace_funcs fn_name then [("HL", AutoCorresData.RuleTrace trace)] else []) @ opt_traces)
|
||||
end
|
||||
|
||||
(* Save the heap info to the theory data. *)
|
||||
val lthy = Local_Theory.background_theory (
|
||||
HeapInfo.map (fn tbl =>
|
||||
Symtab.update (filename, heap_info) tbl)) lthy
|
||||
|
||||
(* Update function information. *)
|
||||
fun update_function_defs lthy fn_def =
|
||||
FunctionInfo.fn_def_update_const (Utils.get_term lthy (hl_function_name (#name fn_def))) fn_def
|
||||
|
|
|
|||
|
|
@ -0,0 +1,76 @@
|
|||
(*
|
||||
* Copyright 2016, NICTA
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(NICTA_BSD)
|
||||
*)
|
||||
|
||||
(*
|
||||
* AutoCorres has experimental support for incremental translation.
|
||||
* To use it, simply run the autocorres command with the "scope" option
|
||||
* to select different functions for each run.
|
||||
*)
|
||||
theory Incremental imports
|
||||
"../../AutoCorres"
|
||||
begin
|
||||
|
||||
install_C_file "type_strengthen.c"
|
||||
|
||||
(* Translate only opt_j *)
|
||||
autocorres [
|
||||
ts_rules = nondet,
|
||||
scope_depth = 0,
|
||||
scope = opt_j
|
||||
] "type_strengthen.c"
|
||||
|
||||
thm type_strengthen.opt_j'_def
|
||||
|
||||
(* Translate st_i, which calls opt_j. Calls to opt_j are translated correctly. *)
|
||||
autocorres [
|
||||
ts_rules = nondet,
|
||||
no_heap_abs = st_i,
|
||||
scope_depth = 0,
|
||||
scope = st_i
|
||||
] "type_strengthen.c"
|
||||
|
||||
thm type_strengthen.st_i'.simps
|
||||
|
||||
(* st_h calls st_g, which we did not select.
|
||||
* So this translates st_g by generating a wrapper for its SIMPL code. *)
|
||||
autocorres [
|
||||
ts_rules = nondet,
|
||||
no_signed_word_abs = st_h,
|
||||
scope_depth = 0,
|
||||
scope = st_h
|
||||
] "type_strengthen.c"
|
||||
|
||||
thm type_strengthen.st_h'_def
|
||||
type_strengthen.st_g'_def
|
||||
|
||||
(* Translate the remaining functions. *)
|
||||
autocorres [
|
||||
ts_rules = pure option nondet,
|
||||
ts_force option = pure_f,
|
||||
scope_depth = 0,
|
||||
scope = pure_f pure_f2 pure_g pure_h pure_i pure_j pure_k pure_div_roundup
|
||||
gets_f gets_g opt_f opt_g opt_h (* opt_j *) opt_i opt_none opt_l opt_a hax
|
||||
st_f (* st_g st_h st_i *) exc_f
|
||||
] "type_strengthen.c"
|
||||
|
||||
context type_strengthen begin
|
||||
(* All function defs. *)
|
||||
thm pure_f'_def pure_f2'_def
|
||||
thm pure_g'_def pure_h'_def
|
||||
pure_i'_def pure_j'_def pure_k'_def pure_div_roundup'_def
|
||||
thm gets_f'_def gets_g'_def
|
||||
thm opt_f'_def opt_g'_def opt_h'.simps opt_i'_def
|
||||
opt_j'_def opt_a'.simps
|
||||
thm opt_l'_def
|
||||
thm st_f'_def st_g'_def st_h'_def st_i'.simps hax'_def
|
||||
thm exc_f'_def
|
||||
end
|
||||
|
||||
end
|
||||
|
|
@ -638,12 +638,19 @@ let
|
|||
(the (AutoCorresData.get_def (Proof_Context.theory_of lthy)
|
||||
filename "TSdef" (#name fn_def))))
|
||||
|
||||
val initial_callees = Symtab.dest (FunctionInfo.get_functions fn_info)
|
||||
|> List.mapPartial (fn (fn_name, fn_def) =>
|
||||
if not (#finished fn_def) then NONE else
|
||||
AutoCorresData.get_thm (Proof_Context.theory_of lthy)
|
||||
filename ("TScorres") fn_name
|
||||
|> Option.map (fn thm => (fn_name, thm)))
|
||||
|> Symtab.make
|
||||
val (lthy, fn_info, (_, results)) =
|
||||
AutoCorresUtil.translate
|
||||
lthy fn_info convert define
|
||||
lthy fn_info Symtab.empty convert define
|
||||
(fn defs => fn lthy => map (retrieve_mono_thm lthy) defs)
|
||||
update_function_def
|
||||
(Symtab.empty, [])
|
||||
(initial_callees, [])
|
||||
|
||||
(* Print some statistics for curiosity's sake. *)
|
||||
(*
|
||||
|
|
|
|||
Loading…
Reference in New Issue