450 lines
17 KiB
Standard ML
450 lines
17 KiB
Standard ML
(*
|
|
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
|
*
|
|
* SPDX-License-Identifier: BSD-2-Clause
|
|
*)
|
|
|
|
signature MODIFIES_PROOFS =
|
|
sig
|
|
|
|
type csenv = ProgramAnalysis.csenv
|
|
val gen_modify_body : theory -> typ -> term -> term ->
|
|
ProgramAnalysis.modify_var list -> term
|
|
(* [gen_modify_body thy ty s0 s vs]
|
|
ty is the Isabelle type of the state
|
|
s0 is an Isabelle var standing for the initial state
|
|
s is an Isabelle var standing for the final state
|
|
vs is the list of variables allowed to be modified.
|
|
|
|
The "global exception" variable will automatically be added to the
|
|
list of variables as something that can be modified.
|
|
*)
|
|
|
|
|
|
val gen_modify_goal : theory -> typ list -> term -> string ->
|
|
ProgramAnalysis.modify_var list -> term
|
|
(* [gen_modify_goal thy tys tm fname vs]
|
|
tys is the three types that are parameters to all HoarePackage constants
|
|
tm is the \<Gamma> that houses the lookup table from fn names to bodies
|
|
fname is the name of the function being called
|
|
vs is the list of variables allowed to be modified.
|
|
|
|
The "global exception" variable will automatically be added to the
|
|
goal as something that can be modified.
|
|
*)
|
|
|
|
val gen_modify_goalstring : csenv -> string -> string list -> string
|
|
|
|
val modifies_vcg_tactic : local_theory -> int -> tactic
|
|
val modifies_tactic : thm -> local_theory -> tactic
|
|
|
|
val prove_all_modifies_goals_local : csenv -> (string -> bool) -> typ list ->
|
|
local_theory -> local_theory
|
|
|
|
val prove_all_modifies_goals : theory -> csenv -> (string -> bool) ->
|
|
typ list -> string -> theory
|
|
(* string is the name of the locale where the theorems about Gamma live *)
|
|
|
|
val sorry_modifies_proofs : bool Config.T
|
|
val calculate_modifies_proofs : bool Config.T
|
|
end
|
|
|
|
structure Modifies_Proofs : MODIFIES_PROOFS =
|
|
struct
|
|
|
|
open TermsTypes
|
|
type csenv = ProgramAnalysis.csenv
|
|
|
|
(* Config item to determine if "modifies" thms should be generated. *)
|
|
val calculate_modifies_proofs =
|
|
Attrib.setup_config_bool @{binding calculate_modifies_proofs} (K true)
|
|
|
|
val sorry_modifies_proofs =
|
|
Attrib.setup_config_bool @{binding sorry_modifies_proofs} (K false);
|
|
|
|
fun put_conditional conf VAR ctxt =
|
|
let
|
|
val v = can getenv_strict VAR
|
|
val ctxt' = Config.put_generic conf v ctxt
|
|
in
|
|
Output.tracing ("Set " ^ Config.name_of conf ^ " to " ^ Config.print_value (Config.Bool v));
|
|
ctxt'
|
|
end
|
|
|
|
fun cond_sorry_modifies_proofs VAR ctxt =
|
|
let
|
|
val ctxt' = put_conditional sorry_modifies_proofs VAR ctxt
|
|
in
|
|
if Config.get_generic ctxt' sorry_modifies_proofs andalso
|
|
not (Config.get_generic ctxt' quick_and_dirty)
|
|
then warning "Setting sorry_modifies_proofs without quick_and_dirty."
|
|
else ();
|
|
ctxt'
|
|
end
|
|
|
|
fun gen_modify_goalstring csenv fname modstrings = let
|
|
fun foldthis (vname, vset) =
|
|
case MSymTab.lookup (ProgramAnalysis.get_addressed csenv) (MString.mk vname) of
|
|
NONE => Binaryset.add(vset, vname)
|
|
| SOME _ => Binaryset.add(vset, NameGeneration.global_heap)
|
|
val vset = List.foldl foldthis (Binaryset.empty String.compare) modstrings
|
|
in
|
|
"\<forall>\<sigma>. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call "^
|
|
fname ^ "_'proc " ^
|
|
"{t. t may_only_modify_globals \<sigma> in [" ^
|
|
commas (Binaryset.listItems vset) ^ "]}"
|
|
end
|
|
|
|
fun mvar_to_string mv = let
|
|
open ProgramAnalysis
|
|
in
|
|
case mv of
|
|
M vi => MString.dest (get_mname vi)
|
|
| TheHeap => NameGeneration.global_heap
|
|
| PhantomState => NameGeneration.phantom_state_name
|
|
| GhostState => NameGeneration.ghost_state_name
|
|
| AllGlobals => raise Match
|
|
|
|
end
|
|
|
|
fun gen_modify_body thy state_ty sigma t mvars = let
|
|
val vars = map mvar_to_string mvars
|
|
val vars = rev (sort_strings vars)
|
|
val glob_ty =
|
|
case state_ty of
|
|
Type(@{type_name "StateSpace.state.state_ext"}, [g, _]) => g
|
|
| _ => raise TYPE ("state_ty has unexpected form", [state_ty], [])
|
|
val globals_name = @{const_name "globals"}
|
|
val globals_t = Const(globals_name, state_ty --> glob_ty)
|
|
val base_t = globals_t $ sigma
|
|
fun gettypes v = let
|
|
val vn = HoarePackage.varname v
|
|
val qvn = "globals." ^ vn
|
|
val fullvar_name = Sign.intern_const thy qvn
|
|
val varaccessor_ty =
|
|
valOf (Sign.const_type thy fullvar_name)
|
|
handle Option => raise Fail ("Couldn't get type for constant "^
|
|
fullvar_name)
|
|
val (_, var_ty) = dom_rng varaccessor_ty
|
|
in
|
|
(vn, fullvar_name, var_ty)
|
|
end
|
|
val vartypes = map gettypes vars
|
|
fun mk_update((var_name, fullvarname, var_ty), acc) = let
|
|
val var_v = Free(var_name, var_ty)
|
|
val updfn = mk_abs(Free("_", var_ty), var_v)
|
|
val updator = Const(suffix Record.updateN fullvarname,
|
|
(var_ty --> var_ty) --> (glob_ty --> glob_ty))
|
|
in
|
|
updator $ updfn $ acc
|
|
end
|
|
val updated_t = List.foldr mk_update base_t vartypes
|
|
val globals_tt = globals_t $ t
|
|
val meq_t = Const(HoarePackage.modeqN, glob_ty --> glob_ty --> bool) $
|
|
globals_tt $ updated_t
|
|
fun mk_mex ((var_name, _, var_ty), base) = let
|
|
val abs_t = mk_abs(Free(var_name, var_ty), base)
|
|
in
|
|
Const(HoarePackage.modexN, (var_ty --> bool) --> bool) $
|
|
abs_t
|
|
end
|
|
in
|
|
List.foldl mk_mex meq_t vartypes
|
|
end
|
|
|
|
fun gen_modify_goal_pair thy tyargs gamma fname mvars = let
|
|
val state_ty = hd tyargs
|
|
val name_ty = List.nth(tyargs, 1)
|
|
val com_ty = mk_com_ty tyargs
|
|
val stateset_ty = mk_set_type state_ty
|
|
val error_ty = List.nth(tyargs, 2)
|
|
val sigma = Free("\<sigma>", state_ty)
|
|
val t = Free("t", state_ty)
|
|
|
|
val theta_element_ty =
|
|
list_mk_prod_ty [stateset_ty, name_ty, stateset_ty, stateset_ty]
|
|
val theta_ty = mk_set_type theta_element_ty
|
|
val hoarep_t =
|
|
Const(@{const_name "hoarep"},
|
|
(name_ty --> mk_option_ty com_ty) -->
|
|
theta_ty -->
|
|
mk_set_type error_ty -->
|
|
stateset_ty -->
|
|
com_ty -->
|
|
stateset_ty -->
|
|
stateset_ty -->
|
|
bool)
|
|
val theta_t = mk_empty theta_element_ty
|
|
val faults_t = mk_UNIV error_ty
|
|
val pre_t = list_mk_set state_ty [sigma]
|
|
val prog_t = Const(@{const_name "Language.com.Call"},
|
|
name_ty --> mk_com_ty tyargs) $
|
|
Const(Sign.intern_const
|
|
thy
|
|
(fname ^ HoarePackage.proc_deco),
|
|
name_ty)
|
|
(* post_t is the complicated Collect term *)
|
|
val post_t = let
|
|
val mexxed_t = gen_modify_body thy state_ty sigma t mvars
|
|
in
|
|
mk_collect_t state_ty $ mk_abs(t, mexxed_t)
|
|
end
|
|
val abr_t = mk_empty state_ty
|
|
val goal_t = hoarep_t $ gamma $ theta_t $ faults_t $ pre_t $ prog_t $ post_t $ abr_t
|
|
in
|
|
(mk_abs(sigma, post_t), mk_forall(sigma, goal_t))
|
|
end
|
|
|
|
fun gen_modify_goal thy tyargs gamma fname mvars = let
|
|
val (_, goal) = gen_modify_goal_pair thy tyargs gamma fname mvars
|
|
in
|
|
goal
|
|
end
|
|
|
|
fun munge_tactic ctxt goal msgf tac = let
|
|
fun tacticfn {prems = _,context} st =
|
|
if Config.get ctxt sorry_modifies_proofs then
|
|
if Config.get ctxt quick_and_dirty
|
|
then Skip_Proof.cheat_tac ctxt 1 st
|
|
else error "Can skip modifies-proofs only in quick-and-dirty mode."
|
|
else
|
|
tac context st
|
|
fun tacticmsg st t = case Seq.pull (tacticfn st t) of
|
|
NONE => Seq.empty
|
|
| SOME (t, _) => (msgf (); Seq.single t)
|
|
in
|
|
Goal.prove_future ctxt [] [] (TermsTypes.mk_prop goal) tacticmsg
|
|
end
|
|
|
|
fun modifies_vcg_tactic ctxt i t = let
|
|
val timer = Timer.startCPUTimer ()
|
|
val tac = HoarePackage.vcg_tac "_modifies" "false" [] ctxt i
|
|
val res = Seq.list_of (DETERM tac t)
|
|
val {usr, sys} = Timer.checkCPUTimer timer
|
|
in
|
|
Feedback.informStr (0, "modifies vcg-time:" ^ Time.fmt 2 (Time.+ (usr, sys)));
|
|
Seq.of_list res
|
|
end
|
|
|
|
fun seq_all_new i = let
|
|
fun before_all_new s t = t THEN_ALL_NEW s
|
|
in
|
|
fn (x::xs) => fold before_all_new xs x i
|
|
| [] => all_tac
|
|
end
|
|
|
|
fun modifies_tactic mod_inv_prop ctxt = let
|
|
val mip_intros = [mod_inv_prop] RL @{thms modifies_inv_intros}
|
|
val globals_equality = Proof_Context.get_thms ctxt "globals.equality"
|
|
fun asm_spec_tactic i =
|
|
seq_all_new i [
|
|
resolve_tac ctxt @{thms asm_spec_preserves},
|
|
asm_lr_simp_tac (ctxt addsimps @{thms mex_def meq_def})
|
|
]
|
|
in
|
|
seq_all_new 1 [
|
|
HoarePackage.hoare_rule_tac ctxt @{thms HoarePartial.ProcNoRec1},
|
|
REPEAT_ALL_NEW (resolve_tac ctxt (@{thms allI} @ mip_intros)),
|
|
asm_spec_tactic ORELSE' modifies_vcg_tactic ctxt,
|
|
TRY o clarsimp_tac ctxt,
|
|
TRY o REPEAT_ALL_NEW (resolve_tac ctxt [exI]),
|
|
resolve_tac ctxt globals_equality,
|
|
asm_lr_simp_tac ctxt,
|
|
resolve_tac ctxt @{thms surjective_pairing}
|
|
]
|
|
end
|
|
|
|
fun get_mod_inv_prop ctxt post_abs mod_inv_props = let
|
|
fun prove_mod_inv_prop () = let
|
|
val mi_prop_ty = fastype_of post_abs --> HOLogic.boolT
|
|
fun mi_goal prop = HOLogic.mk_Trueprop (Const (prop, mi_prop_ty) $ post_abs)
|
|
fun mi_prop_tac _ = let
|
|
val globals_equality = Proof_Context.get_thm ctxt "globals.equality"
|
|
fun mi_refl_tac _ =
|
|
simp_tac (clear_simpset ctxt addsimps @{thms modifies_inv_refl_def mex_def meq_def}) 1 THEN
|
|
resolve_tac ctxt @{thms allI} 1 THEN
|
|
resolve_tac ctxt @{thms CollectI} 1 THEN
|
|
TRY (REPEAT_ALL_NEW (resolve_tac ctxt @{thms exI}) 1) THEN
|
|
resolve_tac ctxt [globals_equality] 1 THEN
|
|
ALLGOALS (simp_tac (clear_simpset ctxt addsimprocs [Record.simproc]))
|
|
fun mi_incl_tac _ =
|
|
simp_tac (clear_simpset ctxt addsimps @{thms modifies_inv_incl_def mex_def meq_def}) 1 THEN
|
|
resolve_tac ctxt @{thms allI} 1 THEN
|
|
resolve_tac ctxt @{thms allI} 1 THEN
|
|
resolve_tac ctxt @{thms impI} 1 THEN
|
|
resolve_tac ctxt @{thms Collect_mono} 1 THEN
|
|
TRY (REPEAT_ALL_NEW (resolve_tac ctxt @{thms ex_mono}) 1) THEN
|
|
eresolve_tac ctxt @{thms CollectE} 1 THEN
|
|
TRY (REPEAT_ALL_NEW (eresolve_tac ctxt @{thms exE}) 1) THEN
|
|
clarsimp_tac ctxt 1
|
|
val mi_refl = Goal.prove ctxt [] [] (mi_goal @{const_name modifies_inv_refl}) mi_refl_tac
|
|
val mi_incl = Goal.prove ctxt [] [] (mi_goal @{const_name modifies_inv_incl}) mi_incl_tac
|
|
in
|
|
REPEAT_ALL_NEW (resolve_tac ctxt (mi_refl :: mi_incl :: @{thms modifies_inv_prop})) 1
|
|
end
|
|
val mi_prop = Goal.prove_future ctxt [] [] (mi_goal @{const_name modifies_inv_prop}) mi_prop_tac
|
|
in
|
|
(mi_prop, Termtab.update (post_abs, mi_prop) mod_inv_props)
|
|
end
|
|
in
|
|
case Termtab.lookup mod_inv_props post_abs of
|
|
SOME mi_prop => (mi_prop, mod_inv_props)
|
|
| NONE => prove_mod_inv_prop ()
|
|
end
|
|
|
|
fun prove_all_modifies_goals_local csenv includeP tyargs lthy = let
|
|
open ProgramAnalysis
|
|
val _ = Feedback.informStr (0, "Proving automatically calculated modifies proofs")
|
|
val globs_all_addressed = Config.get lthy CalculateState.globals_all_addressed
|
|
val _ = Feedback.informStr (0, "Globals_all_addressed mode = " ^ Bool.toString globs_all_addressed)
|
|
(* first enter the locale where \<Gamma> exists, and where all the
|
|
mappings from function name to function body exist *)
|
|
val lconsts = Proof_Context.consts_of lthy
|
|
val gamma_nm = Consts.intern lconsts "\<Gamma>"
|
|
val gamma_t = Syntax.check_term lthy (Const(gamma_nm, dummyT))
|
|
val {callgraph,callers} = compute_callgraphs csenv
|
|
|
|
fun do_one (fname, (failedsofar, mod_inv_props, lthy)) = let
|
|
val _ = Feedback.informStr (0, "Beginning modifies proof for singleton " ^ fname)
|
|
val timer = Timer.startCPUTimer ()
|
|
|
|
fun modifies_msg msg () = let
|
|
val {usr, sys} = Timer.checkCPUTimer timer
|
|
in
|
|
Feedback.informStr (0, "modifies:" ^ fname ^ ":" ^
|
|
Time.fmt 2 (Time.+ (usr, sys)) ^ "s:" ^ msg)
|
|
end;
|
|
in
|
|
case get_modifies csenv fname of
|
|
NONE => (modifies_msg "can't do modifies proof" ();
|
|
(Binaryset.add(failedsofar,fname), mod_inv_props, lthy))
|
|
| SOME mods => let
|
|
val mvlist = Binaryset.listItems mods
|
|
val mvlist =
|
|
(* map globals to "TheHeap" if globals_all_addressed is true*)
|
|
if globs_all_addressed then map (fn M _ => TheHeap | x => x) mvlist
|
|
else mvlist
|
|
val calls = case Symtab.lookup callgraph fname of
|
|
NONE => Binaryset.empty String.compare
|
|
| SOME s => s
|
|
val i = Binaryset.intersection(calls, failedsofar)
|
|
in
|
|
if Binaryset.isEmpty i then let
|
|
val thy = Proof_Context.theory_of lthy
|
|
val (post_abs, goal) = gen_modify_goal_pair thy tyargs gamma_t fname mvlist
|
|
val (mod_inv_prop, mod_inv_props') = get_mod_inv_prop lthy post_abs mod_inv_props
|
|
val th = munge_tactic lthy goal (modifies_msg "completed") (modifies_tactic mod_inv_prop)
|
|
val (_, lthy) = Local_Theory.note ((Binding.name (fname ^ "_modifies"), []), [th]) lthy
|
|
in
|
|
(failedsofar, mod_inv_props', lthy)
|
|
end
|
|
else let
|
|
val example = valOf (Binaryset.find (fn _ => true) i)
|
|
val _ = modifies_msg
|
|
("not attempted, as it calls a function ("
|
|
^ example ^ ") that has failed")
|
|
in
|
|
(Binaryset.add(failedsofar, fname), mod_inv_props, lthy)
|
|
end
|
|
end
|
|
end
|
|
exception NoMods of string Binaryset.set
|
|
fun do_recgroup (fnlist, (failedsofar, mod_inv_props, lthy)) = let
|
|
val n = length fnlist (* >= 1 *)
|
|
val rec_thm = HoarePackage.gen_proc_rec lthy HoarePackage.Partial n
|
|
val mods = valOf (get_modifies csenv (hd fnlist))
|
|
handle Option => (Feedback.informStr (0, "No modifies info for "^hd fnlist);
|
|
raise NoMods (Binaryset.addList(failedsofar, fnlist)))
|
|
val mvlist = Binaryset.listItems mods
|
|
fun gen_modgoal (fname : string) : term = let
|
|
val calls = case Symtab.lookup callgraph fname of
|
|
NONE => raise Fail (fname ^ " part of clique, but \
|
|
\doesn't call anything??")
|
|
| SOME s => s
|
|
val i = Binaryset.intersection(calls, failedsofar)
|
|
in
|
|
if Binaryset.isEmpty i then
|
|
gen_modify_goal (Proof_Context.theory_of lthy) tyargs
|
|
gamma_t fname mvlist
|
|
else let
|
|
val example = valOf (Binaryset.find (fn _ => true) i)
|
|
val _ = Feedback.informStr (0, "Not attempting modifies proof for "^fname^
|
|
" (or its recursive component) as it calls a\
|
|
\ function ("^example^") that has failed")
|
|
in
|
|
raise NoMods (Binaryset.addList(failedsofar, fnlist))
|
|
end
|
|
end
|
|
val nway_goal = list_mk_conj (map gen_modgoal fnlist)
|
|
fun tac ctxt =
|
|
HoarePackage.hoare_rule_tac ctxt [rec_thm] 1 THEN
|
|
ALLGOALS (HoarePackage.vcg_tac "_modifies" "false" [] ctxt)
|
|
in
|
|
let
|
|
val pnm = "Modifies proof for recursive clique " ^ commas fnlist
|
|
val _ = Feedback.informStr (0, pnm ^ " commencing.")
|
|
fun msg () = Feedback.informStr (0, pnm ^ " completed.")
|
|
val nway_thm = munge_tactic lthy nway_goal msg tac
|
|
val nway_thms = HOLogic.conj_elims lthy nway_thm
|
|
val _ = length nway_thms = length fnlist orelse
|
|
raise Fail "CONJUNCTS nway_thm and fnlist don't match up!"
|
|
fun note_it (nm, th, lthy) =
|
|
(Feedback.informStr (0, "Modifies rule for "^nm^" extracted");
|
|
#2 (Local_Theory.note ((Binding.name (nm ^ "_modifies"), []),
|
|
[th])
|
|
lthy))
|
|
val noted = ListPair.foldl note_it lthy (fnlist, nway_thms)
|
|
in
|
|
(failedsofar, mod_inv_props, noted)
|
|
end
|
|
end handle NoMods newset => (newset, mod_inv_props, lthy)
|
|
|
|
|
|
fun do_scc (args as (fnlist, acc)) =
|
|
case fnlist of
|
|
[fname] =>
|
|
if includeP fname then
|
|
if not (is_recursivefn csenv fname) then
|
|
do_one(fname, acc)
|
|
else do_recgroup args
|
|
else acc
|
|
| (fname::_) => if includeP fname then do_recgroup args
|
|
else acc
|
|
| _ => raise Fail "SCC with empty list!"
|
|
|
|
fun lift f fnm = case Symtab.lookup f fnm of
|
|
NONE => []
|
|
| SOME s => Binaryset.listItems s
|
|
val sorted_fnames =
|
|
Topo_Sort.topo_sort { cmp = String.compare,
|
|
graph = lift callgraph,
|
|
converse = lift callers}
|
|
(get_functions csenv)
|
|
val acc_init = (Binaryset.empty String.compare, Termtab.empty, lthy)
|
|
val (_, _, lthy) = List.foldl do_scc acc_init sorted_fnames
|
|
in
|
|
lthy
|
|
end
|
|
|
|
fun prove_all_modifies_goals thy csenv includeP tyargs globloc =
|
|
if Config.get_global thy calculate_modifies_proofs then
|
|
let
|
|
val lthy = Named_Target.init [] globloc thy
|
|
in
|
|
lthy
|
|
|> Local_Theory.begin_nested |> snd
|
|
|> prove_all_modifies_goals_local csenv includeP tyargs
|
|
|> Local_Theory.end_nested
|
|
|> Local_Theory.exit_global
|
|
end
|
|
else
|
|
thy
|
|
|
|
val _ =
|
|
Outer_Syntax.command
|
|
@{command_keyword "cond_sorry_modifies_proofs"}
|
|
"set sorry_modifies_proof option, conditional on env variable"
|
|
(Parse.text >> (Toplevel.generic_theory o cond_sorry_modifies_proofs))
|
|
|
|
end (* struct *)
|