diff --git a/lib/clib/AutoCorresModifiesProofs.thy b/lib/clib/AutoCorresModifiesProofs.thy index 743b8952d..8578cfa75 100644 --- a/lib/clib/AutoCorresModifiesProofs.thy +++ b/lib/clib/AutoCorresModifiesProofs.thy @@ -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; diff --git a/proof/crefine/AutoCorresTest.thy b/proof/crefine/AutoCorresTest.thy index 21f4227fa..d11f9d3b2 100644 --- a/proof/crefine/AutoCorresTest.thy +++ b/proof/crefine/AutoCorresTest.thy @@ -377,79 +377,58 @@ lemma clzl'_ac_corres: "ac_corres globals ct \ ret__long_' (\s. x end text \Add our manual translation of clzl into the AutoCorres function info.\ +ML \ +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; +\ 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 *} diff --git a/tools/autocorres/autocorres.ML b/tools/autocorres/autocorres.ML index 19b56b017..8ece6f147 100644 --- a/tools/autocorres/autocorres.ML +++ b/tools/autocorres/autocorres.ML @@ -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) diff --git a/tools/autocorres/type_strengthen.ML b/tools/autocorres/type_strengthen.ML index ed078da1b..01e9b2c17 100644 --- a/tools/autocorres/type_strengthen.ML +++ b/tools/autocorres/type_strengthen.ML @@ -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 =