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

autocorres-crefine: update CRefine demo to work after AutoCorres refactor 

Also fixes an AutoCorres bug that surfaced in the demo.
This commit is contained in:
Japheth Lim 2016-06-30 14:41:55 +10:00
parent 0afb748b1b
commit c31ee7a6a9
4 changed files with 75 additions and 85 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
lib/clib/AutoCorresModifiesProofs.thy
View File

@ -311,8 +311,10 @@ fun modifies_simp_term ctxt =
* Returns tuple of (state var, function arg vars, measure var, prop).
* The returned vars are Free in the prop; the measure var is NONE for non-recursive functions.
*)
fun gen_modifies_prop ctxt fn_info (prog_info: ProgramInfo.prog_info) f_name c_prop = let
val f_info = FunctionInfo.get_phase_info fn_info FunctionInfo.TS f_name;
fun gen_modifies_prop ctxt
(fn_info: FunctionInfo.function_info Symtab.table)
(prog_info: ProgramInfo.prog_info) f_name c_prop = let
val f_info = the (Symtab.lookup fn_info f_name);
val globals_type = #globals_type prog_info;
val globals_term = #globals_getter prog_info;
val ac_ret_type = #return_type f_info;
@ -325,7 +327,7 @@ fun gen_modifies_prop ctxt fn_info (prog_info: ProgramInfo.prog_info) f_name c_p
val modifies_postcond = Abs (Name.uu_, ac_ret_type, Abs ("s", globals_type, modifies_eqn))
|> modifies_simp_term ctxt;
val arg_vars = map Free (#args f_info);
val measure_var = if FunctionInfo.is_function_recursive fn_info f_name
val measure_var = if FunctionInfo.is_function_recursive f_info
(* will not clash with arg_vars as C identifiers do not contain primes *)
then SOME (Free ("measure'", @{typ nat})) else NONE;
val f_const = #const f_info
@ -442,7 +444,7 @@ fun do_modifies_one ctxt fn_info (prog_info: ProgramInfo.prog_info) callee_modif
val (state0_var, arg_vars, measure_var, ac_modifies_prop) =
gen_modifies_prop ctxt fn_info prog_info f_name c_modifies_prop;
val _ = if isSome measure_var then error ("do_modifies_one bug: got recursive function " ^ f_name) else ();
val f_def = FunctionInfo.get_phase_info fn_info FunctionInfo.TS f_name |> #definition;
val f_def = the (Symtab.lookup fn_info f_name) |> #definition;
fun leaf_tac ctxt n = FIRST [modifies_call_tac callee_modifies ctxt n, modifies_invariant_tac true ctxt n,
print_tac ctxt ("do_modifies_one failed (goal " ^ string_of_int n ^ ")")];
val thm = Goal.prove ctxt (map (fn (Free (v, _)) => v) (state0_var :: arg_vars)) [] ac_modifies_prop
@ -463,7 +465,7 @@ fun do_modifies_recursive ctxt fn_info (prog_info: ProgramInfo.prog_info) (calle
val c_modifies_props = map (fn f_name => Thm.prop_of (Proof_Context.get_thm ctxt (f_name ^ "_modifies"))) f_names;
val modifies_props =
map2 (gen_modifies_prop ctxt fn_info prog_info) f_names c_modifies_props;
val f_defs = map (fn f_name => FunctionInfo.get_phase_info fn_info FunctionInfo.TS f_name |> #definition) f_names;
val f_defs = map (fn f_name => the (Symtab.lookup fn_info f_name) |> #definition) f_names;
fun free_name (Free (v, _)) = v;
@ -593,7 +595,7 @@ fun do_modifies_recursive ctxt fn_info (prog_info: ProgramInfo.prog_info) (calle
(* Prove and store modifies rules for one function or recursive function group. *)
fun prove_modifies
(fn_info: FunctionInfo.fn_info)
(fn_info: FunctionInfo.function_info Symtab.table)
(prog_info: ProgramInfo.prog_info)
(callee_modifies: incr_net)
(results: thm Symtab.table)
@ -601,19 +603,19 @@ fun prove_modifies
(thm_names: string list)
ctxt
: (thm list * Proof.context) option = let
val f_infos = map (FunctionInfo.get_function_info fn_info) f_names;
val f_infos = map (the o Symtab.lookup fn_info) f_names;
val maybe_thms =
if length f_names = 1 andalso #is_simpl_wrapper (hd f_infos)
then let
val f_name = hd f_names;
val _ = tracing (f_name ^ " is un-translated; transferring C-parser's modifies rule directly")
val f_def = FunctionInfo.get_phase_info fn_info FunctionInfo.TS f_name |> #definition;
val _ = tracing (f_name ^ " is un-translated; transferring C-parser's modifies rule directly");
val f_def = the (Symtab.lookup fn_info f_name) |> #definition;
val orig_modifies = Proof_Context.get_thm ctxt (f_name ^ "_modifies");
val transfer_thm = @{thm autocorres_modifies_transfer};
val thm = transfer_thm OF [f_def, orig_modifies];
in SOME [modifies_simp ctxt thm] end
else let
val callees = map (Symset.make o FunctionInfo.get_function_callees fn_info) f_names
val callees = map (FunctionInfo.all_callees o the o Symtab.lookup fn_info) f_names
|> Symset.union_sets |> Symset.dest;
val missing_callees = callees |> filter_out (fn callee =>
Symtab.defined results callee orelse member op= f_names callee);
@ -652,23 +654,28 @@ fun define_modifies_group fn_info prog_info f_names (acc as (callee_modifies, re
* recently translated set of functions from a given C file.
*)
fun new_modifies_rules filename ctxt = let
val fn_info = Symtab.lookup (AutoCorresFunctionInfo.get (Proof_Context.theory_of ctxt)) filename |> the;
val all_fn_info = Symtab.lookup (AutoCorresFunctionInfo.get (Proof_Context.theory_of ctxt)) filename |> the;
val ts_info = FunctionInfo.Phasetab.lookup all_fn_info FunctionInfo.TS |> the;
val prog_info = ProgramInfo.get_prog_info ctxt filename;
(* Assume that the user has already generated and named modifies rules
* for previously-translated callees. *)
val existing_modifies =
Symtab.dest (FunctionInfo.get_all_functions fn_info)
Symtab.dest ts_info
|> List.mapPartial (fn (fn_name, fn_def) =>
try (fn _ => (fn_name, Proof_Context.get_thm ctxt (fn_name ^ "'_modifies"))) ())
|> Symtab.make;
val all_function_groups =
FunctionInfo.map_fn_info (fn info =>
if Symtab.defined existing_modifies (#name info) then NONE else SOME info) fn_info
|> FunctionInfo.get_topo_sorted_functions;
(* We will do modifies proofs for these functions *)
val pending_fn_info =
Symtab.dest ts_info
|> List.mapPartial (fn (f, info) =>
if Symtab.defined existing_modifies f then NONE else SOME (f, info))
|> Symtab.make;
val (call_graph, _) = FunctionInfo.calc_call_graph pending_fn_info;
val (callee_modifies, results, ctxt') =
fold (define_modifies_group fn_info prog_info)
all_function_groups (build_incr_net (Symtab.dest existing_modifies |> map snd),
existing_modifies, ctxt)
fold (define_modifies_group ts_info prog_info)
(#topo_sorted_functions call_graph |> map Symset.dest)
(build_incr_net (Symtab.dest existing_modifies |> map snd),
existing_modifies, ctxt)
in ctxt' end
end;

97
proof/crefine/AutoCorresTest.thy
View File

@ -377,79 +377,58 @@ lemma clzl'_ac_corres: "ac_corres globals ct \<Gamma> ret__long_' (\<lambda>s. x
end
text \<open>Add our manual translation of clzl into the AutoCorres function info.\<close>
ML \<open>
fun phasetab_merge_with merge (tab1, tab2) =
sort_distinct FunctionInfo.phase_ord
(FunctionInfo.Phasetab.keys tab1 @ FunctionInfo.Phasetab.keys tab2)
|> map (fn k => (k, case (FunctionInfo.Phasetab.lookup tab1 k, FunctionInfo.Phasetab.lookup tab2 k) of
(SOME x1, SOME x2) => merge (x1, x2)
| (SOME x1, NONE) => x1
| (NONE, SOME x2) => x2
(* (NONE, NONE) impossible *)))
|> FunctionInfo.Phasetab.make;
\<close>
setup {*
fn thy =>
let val clzl_cp = {
name = "clzl",
invented_body = false,
is_simpl_wrapper = false,
callees = Symset.empty,
rec_callees = Symset.empty,
phase = FunctionInfo.CP,
args = [("x", @{typ "32 word"})],
return_type = @{typ "32 signed word"},
const = @{term "clzl_'proc"},
raw_const = @{term "clzl_'proc"},
definition = @{thm kernel_all_substitute.clzl_body_def},
mono_thm = NONE
}: FunctionInfo.phase_info;
val clzl_l1 = {
phase = FunctionInfo.L1,
args = [("x", @{typ "32 word"})],
return_type = @{typ "32 signed word"},
const = @{term "kernel_all_substitute.l1_clzl'"},
raw_const = @{term "kernel_all_substitute.l1_clzl'"},
definition = @{thm kernel_all_substitute.l1_clzl'_def},
mono_thm = NONE
}: FunctionInfo.phase_info;
val clzl_l2 = {
phase = FunctionInfo.L2,
args = [("x", @{typ "32 word"})],
return_type = @{typ "32 signed word"},
const = @{term "kernel_all_substitute.l2_clzl'"},
raw_const = @{term "kernel_all_substitute.l2_clzl'"},
definition = @{thm kernel_all_substitute.l2_clzl'_def},
mono_thm = NONE
}: FunctionInfo.phase_info;
val clzl_ts = {
phase = FunctionInfo.TS,
args = [("x", @{typ "32 word"})],
return_type = @{typ "32 signed word"},
const = @{term "kernel_all_substitute.clzl'"},
raw_const = @{term "kernel_all_substitute.clzl'"},
definition = @{thm kernel_all_substitute.clzl'_def},
mono_thm = NONE
}: FunctionInfo.phase_info;
val clzl_info = {
name = "clzl",
invented_body = false,
is_simpl_wrapper = false,
phases = FunctionInfo.Phasetab.make
[(FunctionInfo.CP, clzl_cp),
(FunctionInfo.L1, clzl_l1),
(FunctionInfo.L2, clzl_l2),
(FunctionInfo.HL, FunctionInfo.phase_info_upd_phase FunctionInfo.HL clzl_l2),
(FunctionInfo.WA, FunctionInfo.phase_info_upd_phase FunctionInfo.WA clzl_l2),
(FunctionInfo.TS, clzl_ts)]
mono_thm = NONE,
corres_thm = @{thm TrueI}
}: FunctionInfo.function_info;
val clzl_l1 = clzl_cp
|> FunctionInfo.function_info_upd_phase FunctionInfo.L1
|> FunctionInfo.function_info_upd_const @{term "kernel_all_substitute.l1_clzl'"}
|> FunctionInfo.function_info_upd_definition @{thm kernel_all_substitute.l1_clzl'_def}
|> FunctionInfo.function_info_upd_corres_thm @{thm "kernel_all_substitute.l1_clzl'_corres"};
val clzl_l2 = clzl_l1
|> FunctionInfo.function_info_upd_phase FunctionInfo.L2
|> FunctionInfo.function_info_upd_const @{term "kernel_all_substitute.l2_clzl'"}
|> FunctionInfo.function_info_upd_definition @{thm kernel_all_substitute.l2_clzl'_def}
|> FunctionInfo.function_info_upd_corres_thm @{thm "kernel_all_substitute.l2_clzl'_corres"};
val clzl_ts = clzl_l2
|> FunctionInfo.function_info_upd_phase FunctionInfo.TS
|> FunctionInfo.function_info_upd_const @{term "kernel_all_substitute.clzl'"}
|> FunctionInfo.function_info_upd_definition @{thm kernel_all_substitute.clzl'_def}
|> FunctionInfo.function_info_upd_corres_thm @{thm "kernel_all_substitute.clzl'_TScorres"};
val clzl_info = FunctionInfo.Phasetab.make
(map (fn info => (#phase info, Symtab.make [("clzl", info)]))
[clzl_cp, clzl_l1, clzl_l2, clzl_ts]);
val file = "c/kernel_all.c_pp";
val fn_info = the (Symtab.lookup (AutoCorresFunctionInfo.get @{theory}) file);
(* hack to work around opacity of fn_info *)
fun add_fn_info fn_info new_infos = let
val fn_infos = FunctionInfo.get_all_functions fn_info;
val {base = locale_name,...} = OS.Path.splitBaseExt (OS.Path.file file);
val SOME ctxt = try (Named_Target.begin (locale_name, Position.none)) thy;
in FunctionInfo.init_fn_info ctxt file
|> FunctionInfo.map_fn_info (fn info =>
case Symtab.lookup new_infos (#name info) of
NONE => Symtab.lookup fn_infos (#name info)
| SOME ni => SOME ni) end;
val fn_info' = add_fn_info fn_info (Symtab.make [("clzl", clzl_info)]);
val fn_info = the (Symtab.lookup (AutoCorresFunctionInfo.get thy) file);
val fn_info' = phasetab_merge_with (Symtab.merge (K false)) (fn_info, clzl_info);
in
thy
|> AutoCorresFunctionInfo.map (Symtab.update (file, fn_info'))
|> AutoCorresData.add_def file "L1def" "clzl" @{thm kernel_all_substitute.l1_clzl'_def}
|> AutoCorresData.add_def file "L2def" "clzl" @{thm kernel_all_substitute.l2_clzl'_def}
|> AutoCorresData.add_def file "TSdef" "clzl" @{thm kernel_all_substitute.clzl'_def}
|> AutoCorresData.add_thm file "L1corres" "clzl" @{thm kernel_all_substitute.l1_clzl'_corres}
|> AutoCorresData.add_thm file "L2corres" "clzl" @{thm kernel_all_substitute.l2_clzl'_corres}
|> AutoCorresData.add_thm file "TScorres" "clzl" @{thm kernel_all_substitute.clzl'_TScorres}
end
*}

12
tools/autocorres/autocorres.ML
View File

@ -372,17 +372,13 @@ let
val _ = if not (isSome existing_phases) then () else
tracing ("Attempting to restart from previous translation of " ^ filename)
(* Fetch any existing translations, when being run in incremental mode. *)
fun get_existing_optional_phase phase =
case existing_phases of
NONE => SOME Symtab.empty
| SOME phases => FunctionInfo.Phasetab.lookup phases phase
fun get_existing_phase phase =
Option.getOpt (get_existing_optional_phase phase, Symtab.empty)
(* FIXME: if skip_heap_abs or skip_word_abs are used for some parts of
* an incremental translation, some functions will be missing.
* We ought to either handle this nicely (by carrying the
* L2/HL versions forward), or detect it early and
* produce an error report. *)
val [existing_simpl_info,
existing_l1_info,
existing_l2_info,
@ -396,6 +392,12 @@ let
FunctionInfo.HL,
FunctionInfo.WA,
FunctionInfo.TS]
(* HL and WA functions may be missing if skip_heap_abs and skip_word_abs
* are set. In that case, we carry forward the L2 or HL functions and
* cross our fingers. (Should work fine if skip_foo is used consistently
* for all functions, might not work if they are mixed.) *)
val existing_hl_info = Utils.symtab_merge_with snd (existing_l2_info, existing_hl_info);
val existing_wa_info = Utils.symtab_merge_with snd (existing_hl_info, existing_wa_info);
(* Skip functions that have already been translated. *)
val already_translated = Symset.make (Symtab.keys existing_ts_info)

6
tools/autocorres/type_strengthen.ML
View File

@ -308,8 +308,7 @@ let
let
(* Fix function parameters. *)
val fn_info = the (Symtab.lookup l2_infos fn_name)
(* Only produce measure parameters for recursive functions.
* FIXME: recalculate call graph prior to this *)
(* Only produce measure parameters for recursive functions. *)
val all_arg_names = (if is_recursive then ["rec_measure'"] else []) @
map fst (#args fn_info)
val all_arg_types = (if is_recursive then [AutoCorresUtil.measureT] else []) @
@ -362,6 +361,9 @@ let
(* NB: discard lthy because we don't want the placeholders to be fixed during define_functions *)
val (input_defs, _) = fold_map gen_fun_def_term (Utils.zip3 fn_names dicts thms) lthy
val (ts_defs, lthy) = Utils.define_functions input_defs false is_recursive lthy
(* TODO: we may want to cleanup callees and rec_callees here, like we do
* in other phases. It's not crucial, however, since this is the
* final phase. *)
(* Instantiate variables in our equivalence theorem to their newly-defined values. *)
fun do_inst_thm thm =