Quelle  autocorres.ML

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(*
 * The top-level "autocorres" command.
 *)
structure AutoCorres =
struct


val verbose_msg = Utils.verbose_msg;

(* Get all that the given function depends on, up to "depth" functions deep. *)
fun get_function_deps get_callees roots depth =
let
  fun get_calleess fns = Symset.union_sets (fns :: map get_callees (Symset.dest fns))
in
  funpow depth get_calleess (Symset.make roots)
end

fun fixpoint eq iter x =
  let
    val y = iter x
  in
    if eq y x then y else fixpoint eq iter y
  end 

fun all_reachable finfos funs =
  let
    fun callees f =
      case Symtab.lookup finfos f of 
        NONE => Symset.empty
      | SOME info => FunctionInfo.all_callees info
    fun iter x = fold Symset.union (map callees (Symset.dest x)) x
    fun eq x y = (Symset.dest x = Symset.dest y)
  in
   funs |> Symset.make |> fixpoint eq iter |> Symset.dest
  end

(* Combined parser. *)
val autocorres_parser : (AutoCorres_Options.autocorres_options * string) parser =
  (* Options *)
   AutoCorres_Options.options_parser --
  (* Filename *)
  Parse.embedded

val init_autocorres_parser : (AutoCorres_Options.autocorres_options * string) parser =
  (* Options *)
  AutoCorres_Options.options_parser --
  (* Filename *)
  Parse.embedded

val final_autocorres_parser : (string) parser =
  (* Filename *)
  Parse.embedded


(* build_tasks calculates the "build-dependencies" of C-functions in the various phases of
 * autocorrres. To build a function in phase X it depends on all callees in the same phase and on
 * itsself in phase (X - 1). We identify a tasks by a string encoding: 
 *    <function_name>_<phase_name>_<cfile_name>
 *
 * The result is a list of tuples:
 *    (name, (imports, (scope, phase)))
 *  - name: string as described above
 *  - imports: list of names it depends on
 *  - (scope, phase) are the options for autocorres to build the function in a particular phase.
 *      (scope is a singleton list containing the function name)
 *  - an artificial final theory "autocorres_final_<cfile_name>" will be added to include all the
 *    root functions.
 * Note that the task list is complete and does not consider what might already be built. 
 *)
fun build_tasks finfos cfile skips max_phase =
  let

    fun get_rec_callees (finfos: FunctionInfo.function_info Symtab.table) f =
      let
        val info = case (Symtab.lookup finfos f) of SOME i => i | NONE => error ("function " ^ f ^ " undefined");
        val rec_callees =  Symset.dest (FunctionInfo.get_recursive_clique info);
      in rec_callees end

    fun get_callees (finfos: FunctionInfo.function_info Symtab.table) f =
      let
        val info = case (Symtab.lookup finfos f) of SOME i => i | NONE => error ("function " ^ f ^ " undefined");
        val callees =  Symset.dest 
             (Symset.subtract (FunctionInfo.get_recursive_clique info)
                (Symset.union_sets [FunctionInfo.get_callees info]));

      in callees end

    fun fixpoint_rec_callees  (finfos: FunctionInfo.function_info Symtab.table) fs =
      let 
        val fs' = union (op =) fs (map (get_rec_callees finfos) fs |> flat |> distinct (op =))
        val new = subtract (op =) fs fs'
      in 
        if null new then fs' else fixpoint_rec_callees finfos fs'
      end

    fun group (finfos: FunctionInfo.function_info Symtab.table) f =
      let
        val info = case (Symtab.lookup finfos f) of SOME i => i | NONE => error ("function " ^ f ^ " undefined");
        val rec_callees =  Symset.dest (FunctionInfo.get_recursive_clique info);
      in 
        if null rec_callees then [f] else fixpoint_rec_callees finfos (f::rec_callees) |> sort_strings
      end

    val group_name = space_implode "_";

    fun theory_name_group (finfos: FunctionInfo.function_info Symtab.table) cfile g phase =
          space_implode "_" [group_name g, FunctionInfo.string_of_phase phase, cfile]

    fun theory_name (finfos: FunctionInfo.function_info Symtab.table) cfile phase f = 
      theory_name_group finfos cfile (group finfos f) phase

    fun theory_content finfos cfile f phase =
      let
        val scope = group finfos f
        val callees = scope |> map (get_callees finfos) |> flat |> distinct (op =);
        val f_prev = if phase = FunctionInfo.L1 then "" else theory_name finfos cfile (FunctionInfo.prev_phase skips phase) f;
        val imports = (if f_prev = "" then [] else [f_prev]) @ map (theory_name finfos cfile phase) callees;

      in
        (theory_name finfos cfile phase f,
         (imports,
          (scope,
           phase)))
      end

    fun theory_final_name cfile = "autocorres_final_" ^ cfile 
    fun theory_final_content finfos cfile groups =
      let
        val name = theory_final_name cfile
        val imports = groups |> map (fn g => theory_name_group finfos cfile g max_phase) 

      in
        (name, (imports, ([], FunctionInfo.TS)))
      end

    fun mk_thys finfos cfile =
      let
        val groups = finfos |> Symtab.dest |> map (group finfos o fst) |> distinct (op =)
        val phases = FunctionInfo.phases |> drop 1 |> take (FunctionInfo.encode_phase max_phase)  
        fun mk phase = 
              groups 
              |> map (fn g =>  
                   (theory_content finfos cfile (hd g) phase))
        val final = (theory_final_content finfos cfile groups)
      in
        final::(phases |> map mk |> flat)
      end
  in
     mk_thys finfos cfile
  end

fun forall2 p [] = true
  | forall2 p [_] = true
  | forall2 p (x::y::xs) = p x y andalso forall2 p (y::xs);

fun existing_info lthy filename =
  let
    val existing_phases = Symtab.lookup (AutoCorresData.FunctionInfo.get (Context.Proof lthy)) filename

    val get_existing_optional_phase =
        case existing_phases of
            NONE => (fn phase => SOME Symtab.empty)
          | SOME phases => FunctionInfo.Phasetab.lookup phases 

    fun get_existing_phase phase =
         Option.getOpt (get_existing_optional_phase phase, Symtab.empty)

  in get_existing_phase end
     
fun compatible_options 
  (fun_opt: ProgramInfo.function_options) 
  ({param_kinds, might_exit,  ...}:FunctionInfo.in_out_fun_ptr_spec) =
  map (AutoCorresData.norm_kind {only_type=false} o snd) (ProgramInfo.get_in_out_parameters fun_opt) = 
  map (AutoCorresData.norm_kind {only_type=false} o fst) param_kinds andalso
  ProgramInfo.get_might_exit fun_opt = might_exit

 
fun complete_in_out_spec params in_out_spec =
  let
    val res = 
      params |> map (fn (n, cty) => 
        (n, the_default (fst (FunctionInfo.default_parameter_kind cty)) (AList.lookup (op =) in_out_spec n)))
  in res end

fun get_might_exit cse fname =
  let
    val fun_ptr_group = ProgramAnalysis.get_global_fun_ptr_group_with_same_type cse fname
    val _ = @{assert} (member (op =) fun_ptr_group fname)
  in
      exists (ProgramAnalysis.is_exit_reachable cse) fun_ptr_group
  end

fun check_might_exit cse opt fname =
  let
    val {skip_io_abs, ...} = AutoCorres_Options.get_skips opt
    val might_exit_group = get_might_exit cse fname
    val might_exit = ProgramAnalysis.is_exit_reachable cse fname
    val ts_force = AutoCorres_Options.get_ts_force opt
    val _ = if not skip_io_abs andalso not might_exit andalso might_exit_group andalso Symtab.lookup ts_force fname <> SOME "exit" then
            error ("IO option 'might_exit' is inferred for function: " ^ quote fname ^ " called via a function pointer.\n" ^
              "TS phase might fail for functions calling it via a function pointer unless you specify 'ts_force exit' for " ^ quote fname)   
            else ()
  in
    might_exit_group
  end
fun fun_options cse opt fname =
  let
    val params = these (ProgramAnalysis.get_params fname cse) |> map (fn vinfo => (ProgramAnalysis.srcname vinfo, ProgramAnalysis.get_vtype vinfo))
    val default_in_out_fun_ptr_params = params |> map_filter (fn (n, cty) => FunctionInfo.default_fun_ptr_params cty |> Option.map (pair n))

    val might_exit = check_might_exit cse opt fname
    val {skip_io_abs, skip_heap_abs, skip_word_abs} = AutoCorres_Options.get_skips opt
    val heap_abs = not (skip_heap_abs orelse member (op =) (these (AutoCorres_Options.get_no_heap_abs opt)) fname)
    val no_body = member (op =) (these (AutoCorres_Options.get_no_body opt)) fname
    val signed_abs = not (skip_word_abs orelse member (op =) (these (AutoCorres_Options.get_no_signed_word_abs opt)) fname)
    val unsigned_abs = (not skip_word_abs) andalso member (op =) (these (AutoCorres_Options.get_unsigned_word_abs opt)) fname
    val in_out_globals =  (not skip_io_abs) andalso member (op =) (these (AutoCorres_Options.get_in_out_globals opt)) fname
    val in_out_params = AList.lookup (op =) (these (AutoCorres_Options.get_in_out_parameters opt)) fname |> the_default ([], NONE, NONE)
    val in_out_params_opt = if skip_io_abs then NONE else SOME (complete_in_out_spec params (#1 in_out_params))
    val in_out_disjnt_opt = if skip_io_abs then NONE else (#2 in_out_params)
    val in_out_fun_ptr_params = if skip_io_abs then [] else these (#3 in_out_params)
    val overwrite_in_out_fun_ptr_params = default_in_out_fun_ptr_params 
      |> map (fn (n, x) => (n, the_default x (AList.lookup (op =) in_out_fun_ptr_params n))) 
    val skip_io_abs = skip_io_abs

  in
    ProgramInfo.make_function_options {heap_abs = heap_abs, no_body=no_body, signed_abs = signed_abs, unsigned_abs = unsigned_abs,
      skip_heap_abs = skip_heap_abs, skip_word_abs = skip_word_abs, skip_io_abs = skip_io_abs,
      in_out_parameters = in_out_params_opt, in_out_globals = in_out_globals, 
      in_out_disjoint_ptrs = in_out_disjnt_opt,
      in_out_fun_ptr_params = overwrite_in_out_fun_ptr_params, might_exit = might_exit}
  end

fun ensure_C_names [] = error ("ensure_C_names: expecting structure name and at least one field name")
  | ensure_C_names [x] = (x,[]) (* x must be a array type *)
  | ensure_C_names (x::xs) = 
      (NameGeneration.ensure_C_struct_name x,  map NameGeneration.ensure_C_field_name xs)

fun lookup_field (senv: ProgramAnalysis.senv) name (f::fs) = 
  case AList.lookup (op =) senv name of
    SOME (kind, fields, _ , _) => 
      (case AList.lookup RegionExtras.eq_wrap fields f of
        SOME (cty, _) => if null fs then cty else 
           (case cty of 
              CType.StructTy s => lookup_field senv s fs
            | CType.UnionTy s => lookup_field senv s fs
            | _ => error ("lookup_field: unexpected type: " ^ @{make_string} cty))
       | NONE => error ("lookup_field: unknown field " ^ quote f ^ " of structure " ^ quote name))
   | NONE => error ("lookup_field: unknown structure: " ^ quote name) 

fun check_fun_ptr_cty_spec {prefix, kind, elem} fname p cty (spec: ProgramInfo.in_out_fun_ptr_spec) =
  let
    val _ = if CType.fun_ptr_type cty then () else
        error (prefix ^ ": " ^ elem ^ " " ^ quote p ^ " in " ^ kind ^ ": " ^ 
          quote fname ^ "is not a function pointer: " ^ @{make_string} cty)
    val CType.Ptr (CType.Function (_, argTs)) = cty
    val _ = if length argTs = length (#param_kinds spec) then () else 
         error (prefix ^ ":function pointer spec of " ^ elem ^ " " ^ quote p ^ " in " ^ kind ^ ": " ^ 
          quote fname ^ "\nhas to specify in-out kinds for exactly " ^ @{make_string} (length argTs) ^ 
          " parameter(s). Got " ^ @{make_string} (length (#param_kinds spec)) ^ ".")
    fun check_arg_spec (argT, (kind', distinct)) = 
      let
        val _ = 
         if CType.ptr_type argT then () 
         else (case (kind', distinct) of 
             (FunctionInfo.Data, false) => ()
             | _ =>  error (prefix ^ ": function pointer spec of parameter " ^ quote p ^ " in " ^ kind ^ ": " ^ 
               quote fname ^ " unexpected specification for argument type " ^ @{make_string} (argT, (kind, distinct))))
      in () end
    val _ = map check_arg_spec (argTs ~~ #param_kinds spec)
   in () end

fun check_options thy cfilename opt =
  let
    val ctxt = Proof_Context.init_global thy
    val csenv = the (CalculateState.get_csenv thy cfilename)
    val all_functions = ProgramAnalysis.get_functions csenv
    val method_callers = ProgramAnalysis.method_callers csenv
    val in_out_globals = these (AutoCorres_Options.get_in_out_globals opt)
    val in_out_parameters = these (AutoCorres_Options.get_in_out_parameters opt)
    val skip_in_out_phase = null in_out_globals andalso null in_out_parameters
    val funs_with_fun_ptr_params = ProgramAnalysis.get_fun_ptr_params csenv
    val check_in_out_globals = Utils.timeit_msg 1 ctxt (fn _ => "check_in_out_globals") (fn _ => if skip_in_out_phase then () else
      let
        val in_out_globals = AutoCorres_Options.get_in_out_globals opt |> these |> sort fast_string_ord
        val unknown_functions = in_out_globals |> filter_out (member (op =) all_functions)
        val _ = if null unknown_functions then () else 
          warning ("unknown functions for option in_out_globals: " ^ @{make_string} unknown_functions)
        val known_in_out_globals = in_out_globals |> filter_out (member (op =) unknown_functions)
        val all_callers = maps (ProgramAnalysis.get_final_callers csenv o single) known_in_out_globals 
          |> sort_distinct fast_string_ord
        val missing_in_out_globals = all_callers |> filter_out (member (op =) known_in_out_globals)
        val _ = null missing_in_out_globals orelse
           error ("missing calling functions in in_out_globals: " ^ @{make_string} missing_in_out_globals) 
      in () end)
    val check_in_out_params = Utils.timeit_msg 1 ctxt (fn _ => "check_in_out_params") (fn _ => if skip_in_out_phase then () else
     let
       val in_out_params = these (AutoCorres_Options.get_in_out_parameters opt)
       val funs = map fst in_out_params
       val unknown_functions = funs |> filter_out (member (op =) all_functions)
       val _ = if null unknown_functions then () else  
          warning ("unknown functions for option in_out_params: " ^ @{make_string} unknown_functions)
       val known_in_out_params = in_out_params |> filter_out (member (fn (b, a) => fst b = a) unknown_functions) 
       fun check (fname, (in_outs, disjnts, fun_ptr_specs)) =  
         let
           val params = these (ProgramAnalysis.get_params fname csenv)
           fun get_info n = find_first (fn info => ProgramAnalysis.srcname info = n) params 
           val unknown_params = in_outs |> filter (is_none o get_info o fst)
           val _ = null unknown_params orelse
             error ("in_out_params: unknown parameters of function " ^ quote fname ^ ": " ^ @{make_string} unknown_params)
           fun is_ptr_type n = get_info n |> the |> ProgramAnalysis.get_vtype |> CType.ptr_type
           val non_ptr_params = in_outs |> filter_out (is_ptr_type o fst)
           val _ = null non_ptr_params orelse
             error ("in_out_params: not a pointer parameter of function " ^ quote fname ^ ": " ^ @{make_string} non_ptr_params)
           val disjnts' = these disjnts
           val unknown_disjnts = disjnts' |> filter (is_none o get_info)
           val _ = null unknown_disjnts orelse
             error ("in_out_params: unknown disjoint parameters of function " ^ quote fname ^ ": " ^ @{make_string} unknown_disjnts)       
           val non_ptr_disjnts = disjnts' |> filter_out (is_ptr_type)
           val _ = null non_ptr_disjnts orelse
             error ("in_out_params: not a pointer parameter of function " ^ quote fname ^ ": " ^ @{make_string} non_ptr_disjnts)
           val unknown_fun_ptr_params = these fun_ptr_specs |> filter (is_none o get_info o fst)
           val _ = null unknown_fun_ptr_params orelse
             error ("in_out_params: unknown function pointer parameters of function " ^ quote fname ^ ": " ^ @{make_string} unknown_fun_ptr_params)
           fun check_fun_ptr_spec (p, spec) =        
             let
               val info = the (get_info p)
               val cty = ProgramAnalysis.get_vtype info
             in check_fun_ptr_cty_spec {prefix = "in_out_params", kind="function", elem="parameter"} fname p cty spec end
           val _ = map check_fun_ptr_spec (these fun_ptr_specs)
         in () 
         end
       val _ = map check known_in_out_params
     in
       ()
     end)
     val check_method_known_functions = Utils.timeit_msg 1 ctxt (fn _ => "check_method_known_functions") (fn _ => if null method_callers then () else
       let
         val target_known_functions = the_default "exit" (AutoCorres_Options.get_ts_force_known_functions opt)
         val _ = writeln ("C-style method invocations detected in functions: " ^ @{make_string} method_callers)
         val _ = 
           if target_known_functions <> "exit" then 
             warning ("all potential function pointer instances for 'C-style object methods' must fit into (forced) target monad for known functions: " ^ 
               quote target_known_functions) 
           else ()
         val ts_force = AutoCorres_Options.get_ts_force opt
         fun ts fname = the_default "exit" (Symtab.lookup ts_force fname)
         val ts_rules = Monad_Types.get_ordered_rules [] (Context.Theory thy)
         fun ts_index rule_name = find_index (fn x => #name x = rule_name) ts_rules
         fun check_ts_fun fname = 
           let 
             val fi = ts_index (ts fname)
             val ki = ts_index target_known_functions
           in
             if fi < ki then
                error ("ts monad " ^ quote (ts fname) ^ " for function " ^ quote fname ^ 
                  " must be contained in monad " ^ quote target_known_functions ^ " for function pointers of known functions")
             else ()
           end
        val _ = map check_ts_fun method_callers
        val unsigned_word_abs = AutoCorres_Options.get_unsigned_word_abs opt
        val unsigned_word_abs_known_functions = AutoCorres_Options.get_unsigned_word_abs opt
        val no_signed_word_abs = AutoCorres_Options.get_no_signed_word_abs opt
        val no_signed_word_abs_known_functions = AutoCorres_Options.get_no_signed_word_abs opt
        val _ = 
          if is_none unsigned_word_abs andalso is_none unsigned_word_abs_known_functions andalso
             is_none no_signed_word_abs andalso is_none no_signed_word_abs_known_functions then () 
          else
            warning ("Make sure that word abstraction options for all functions that may be called via 'C-style object methods' must be" ^ 
                     "compatible with word abstraction options for known_functions!")
       in
        ()
       end)
     val check_funs_with_fun_ptr_params = Utils.timeit_msg 1 ctxt (fn _ => "check_funs_with_fun_ptr_params") (fn _ =>  if Symtab.is_empty funs_with_fun_ptr_params orelse skip_in_out_phase then () else
       let
         val funs = Symtab.dest funs_with_fun_ptr_params
         fun check_fun (fname, param_callees) =
           let
             val opts = fun_options csenv opt fname
             val params = the (Symtab.lookup (ProgramAnalysis.get_fninfo csenv) fname) |> #3 
               |> map ProgramAnalysis.srcname
             fun idx n = find_index (fn x => x = n) params
             val in_out_fun_ptr_params = ProgramInfo.get_in_out_fun_ptr_params opts
             fun check_param (p, in_out_spec) =
               let
                 val callees = nth (param_callees) (idx p) |> these
                   |> filter ProgramAnalysis.is_function |> map #1
                 fun check_callee c =
                   let
                     val callee_opts = fun_options csenv opt c
                     val arg_infos = the (Symtab.lookup (ProgramAnalysis.get_fninfo csenv) c) |> #3 
                     val callee_spec = ProgramInfo.in_out_fun_ptr_spec_of callee_opts arg_infos
                     val _ = if callee_spec = in_out_spec then () else 
                       error ("IO specification mismatch between callees of function pointer parameter " ^ 
                         quote p ^ " of function " ^ quote fname ^ ".\n" ^
                         "expected: " ^ @{make_string} in_out_spec ^ "\n" ^
                         "callee " ^ quote c ^ ": " ^ @{make_string} callee_spec)
                   in
                    ()
                   end
                 val _ = map check_callee callees
               in
                 ()
               end
             val _ = map check_param in_out_fun_ptr_params
           in
             ()
           end
         val _ = map check_fun funs
       in 
         ()
       end)
  in
    ()
  end


fun check_method_in_out_fun_ptr_specs thy cfilename opt =
  let
    val csenv = the (CalculateState.get_csenv thy cfilename)
    val senv = ProgramAnalysis.get_senv csenv
    val method_in_out_fun_ptr_specs = these (AutoCorres_Options.get_method_in_out_fun_ptr_specs opt)
    fun check_spec (path, spec) = 
      let 
         fun dest_ptr (CType.Ptr T) = CType.norm_enum T
         val (root, selectors) = ensure_C_names path
         val cty = lookup_field senv root selectors
         val _ = check_fun_ptr_cty_spec  {prefix = "method_in_out_fun_ptr_specs", kind="method", elem="field"} root (space_implode "." selectors) cty spec
      in (dest_ptr cty, (spec, (root, selectors))) end
    val cty_specs = map check_spec method_in_out_fun_ptr_specs 
     |> group_by ((op =) o apply2 fst)
    fun check_unique' [(cty, (spec, _))] = (cty, spec)
      | check_unique' xs = error ("check_method_in_out_fun_ptr_specs: all method pointers with same function type must " ^
         "have same in_out_fun_ptr_spec: " ^ @{make_string} xs)
    val check_unique = distinct ((op =) o apply2 (fst o snd)) #> check_unique'
    val cty_specs' = map check_unique cty_specs
  in cty_specs' end
fun finalise prog_info skips keep_going existing_ts (cliques, thy) =
  let
    val filename = ProgramInfo.get_prog_name prog_info
    val info_phase = FunctionInfo.info_phase skips
  in
    thy |> fold_join_thy (fn clique => fn thy =>
    let
      val loc = NameGeneration.intern_globals_locale_name thy filename

      val lthy = Named_Target.init [] loc thy
      val [simpl_info, l1_info, l2_info, io_info, hl_info, wa_info, ts_info] = 
        map (
             AutoCorresData.get_default_phase_info (Context.Proof lthy) filename o 
             info_phase)
         [FunctionInfo.CP, FunctionInfo.L1, FunctionInfo.L2, FunctionInfo.IO, FunctionInfo.HL, FunctionInfo.WA, FunctionInfo.TS]
    
      val ops = the (In_Out_Parameters.Data.get (NameGeneration.global_rcd_name) lthy)
      (* Put together final ac_corres theorems.
       * TODO: we should also store these as theory data. *) 
      fun prove_ac_corres fn_name =
      let
        fun get_corres_thm name (info:FunctionInfo.function_info Symtab.table) = 
          let
            val thm = FunctionInfo.get_corres_thm (the (Symtab.lookup info name))
              handle Option => raise SimplConv.FunctionNotFound name
          in Thm.transfer' lthy thm end;
    
        fun simplified ctxt thms = Simplifier.simplify ((Simplifier.clear_simpset ctxt) addsimps thms)
        val l1_thm = get_corres_thm fn_name l1_info
        val l2_thm = get_corres_thm fn_name l2_info |> CLocals.folded_with [filename, fn_name] lthy
                     (* If in-out lifting was disabled, we use a placeholder *)
        val io_thm = if #skip_io_abs skips then
                       @{thm IOcorres_trivial_from_local_var_extract} OF [l2_thm] 
                     else
                       get_corres_thm fn_name io_info |> #refines_to_IOcorres_conv ops lthy

                     (* If heap lifting was disabled, we use a placeholder *)
        val hl_thm = if #skip_heap_abs skips then @{thm L2Tcorres_trivial_from_in_out_parameters} OF [io_thm] 
                     else get_corres_thm fn_name hl_info 
    
                     (* Placeholder for when word abstraction is disabled *)
        val wa_thm = if #skip_word_abs skips then @{thm corresTA_trivial_from_heap_lift} OF [hl_thm]
                     else get_corres_thm fn_name wa_info
        val ts_thm = get_corres_thm fn_name ts_info
              |> simplified lthy @{thms refines_eq_convs}
                   
      in let
           fun inst_ac_rule rule = try (fn rule => rule OF [l1_thm, l2_thm, io_thm, hl_thm, wa_thm, ts_thm]) rule
           val final_thm = the (get_first inst_ac_rule @{thms ac_corres_chain_sims}) 
           (* Remove fluff, like "f o id", that gets introduced by the HL and WA placeholders *)
           val final_thm' = Simplifier.simplify (put_simpset AUTOCORRES_SIMPSET lthy) final_thm

         in SOME final_thm' end
         handle THM _ =>
             (Utils.THM_non_critical keep_going
                  ("autocorres: failed to prove ac_corres theorem for " ^ fn_name)
                  0 [l1_thm, l2_thm, io_thm, hl_thm, wa_thm, ts_thm];
              NONE) 
      end
    
      val ts_info_todos = Symtab.dest ts_info 
          |> filter_out (fn (k,p) => not (member (op =) clique k) orelse Symtab.defined existing_ts k)

      val _ = verbose_msg 0 lthy (fn _ => "Doing final autocorres proof for: " ^ commas (map fst ts_info_todos) ^ 
                " in locale " ^ loc)

      val ac_corres_thms = ts_info_todos
            |> map fst 
            |> Par_List.map (fn f => Option.map (pair f) (prove_ac_corres f))
            |> List.mapPartial I
      val ac_corres_attrib = map (Attrib.attribute lthy) @{attributes [ac_corres]}

      val lthy = lthy 
        |> fold (fn (f, thm) =>
             Utils.define_lemma (Binding.name (ProgramInfo.get_mk_fun_name prog_info FunctionInfo.TS "" f ^ "_ac_corres")) 
                ac_corres_attrib thm #> snd)
             ac_corres_thms 
        
    in Local_Theory.exit_global lthy end) cliques
  end

(*
 * Worker for the autocorres command. opt is already merged by parallel_autocorres.
 *)
fun do_autocorres parallel (opt : AutoCorres_Options.autocorres_options) filename prog_info HL_setup_opt thy = 
  AutoCorresUtil.timeit_msg 1 (Proof_Context.init_global thy) (fn _ => "autocorres") (fn () =>
let
  val lthy = Named_Target.theory_init thy
  val lthy = lthy |> AutoCorres_Options.Options_Proof.map (K opt)
  val all_simpl_info = AutoCorresData.get_phase_info (Context.Proof lthy) filename FunctionInfo.CP |> the

  (* Fetch program information from the C-parser output. *)
  val all_simpl_functions = Symset.make (Symtab.keys all_simpl_info)


  (* Process autocorres options. *)
  val keep_going = AutoCorres_Options.get_keep_going opt = SOME true

  val _ = if not (AutoCorres_Options.get_unsigned_word_abs opt = NONE) andalso not (AutoCorres_Options.get_skip_word_abs opt = NONE) then
              error "autocorres: unsigned_word_abs and skip_word_abs cannot be used together."
          else if not (AutoCorres_Options.get_no_signed_word_abs opt = NONE) andalso not (AutoCorres_Options.get_skip_word_abs opt = NONE) then
              error "autocorres: no_signed_word_abs and skip_word_abs cannot be used together."
          else ()

  val _ = if not (AutoCorres_Options.get_no_heap_abs opt = NONE) andalso not (AutoCorres_Options.get_skip_heap_abs opt = NONE) then
              error "autocorres: no_heap_abs and skip_heap_abs cannot be used together."
          else ()
  val no_heap_abs = these (AutoCorres_Options.get_no_heap_abs opt)

  val skips = AutoCorres_Options.get_skips opt
  (* 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))
                            (AutoCorres_Options.get_ts_force opt)
  val ts_rules = Monad_Types.get_ordered_rules (these (AutoCorres_Options.get_ts_rules opt)) (Context.Proof lthy)
  (* heap_abs_syntax defaults to off. *)
  val heap_abs_syntax = AutoCorres_Options.get_heap_abs_syntax opt = SOME true

  (* maximal phase to translate functions *)
  val max_phase = the_default FunctionInfo.TS (AutoCorres_Options.get_phase opt)

  (* (Finished processing options.) *)

  val prev_phase = FunctionInfo.prev_phase skips 

  val phases = FunctionInfo.phases
  val todo_phases = phases 
       |> take (FunctionInfo.encode_phase max_phase) 
       |> drop 1
       |> #skip_heap_abs skips ? filter_out (fn phase => phase = FunctionInfo.HL)
       |> #skip_word_abs skips ? filter_out (fn phase => phase = FunctionInfo.WA)
 
  val existing_infos = map (existing_info lthy filename) phases
  fun info infos phase = nth infos (FunctionInfo.encode_phase phase)
  val existing_info = info existing_infos

  fun keyset finfo = finfo |> Symtab.keys |> Symset.make
 
  fun verbose_phase_info str info = phases 
      |> map (fn phase => verbose_msg 1 lthy (fn _ => str ^ " " ^ FunctionInfo.string_of_phase phase ^ ": " ^
           @{make_string} (Symtab.keys (info phase))))

  val _ = verbose_phase_info "existing_info" existing_info;
  
  val _ = @{assert} (forall (fn p =>
      Symset.subset (keyset (existing_info p), keyset (existing_info (prev_phase p)))) todo_phases);


  (* Skip functions that have already been translated. *)
  val already_translated = Symset.make (Symtab.keys (existing_info max_phase))

  (* 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 = Symset.make (these (AutoCorres_Options.get_scope opt))

  (* 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 _ = verbose_msg 0 lthy (fn _ => "autocorres scope: selected " ^ Int.toString (Symset.card functions_to_translate) ^ " function(s): " ^ 
            commas (Symset.dest functions_to_translate));

  val nothing_todo =  Symset.is_empty (Symset.subtract already_translated functions_to_translate) 

  val _ = if nothing_todo then error ("All functions in scope are already translated (cf. option 'fresh').") 
   else ()
  (* We will process these functions... *)
  val functions_to_process = functions_to_translate
  (* ... and ignore these functions. *)
  val functions_to_ignore = Symset.subtract functions_to_process all_simpl_functions

  (* Disallow referring to functions that don't exist or are excluded from processing. *)
  val funcs_in_options =
        these (AutoCorres_Options.get_no_heap_abs opt)
        @ these (AutoCorres_Options.get_no_body opt)
        @ these (AutoCorres_Options.get_unsigned_word_abs opt)
        @ these (AutoCorres_Options.get_no_signed_word_abs opt)
        @ these (AutoCorres_Options.get_scope opt)
        @ Symtab.keys (AutoCorres_Options.get_ts_force 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 andalso not parallel then
      warning ("autocorres: cannot configure translation for excluded function(s): " ^
             commas (Symset.dest ignored_functions))
    else
      ()



  (* Only translate "scope" functions and their direct callees. *)
  val simpl_info =
        Symtab.dest all_simpl_info
        |> List.mapPartial (fn (name, info) =>
             if Symset.contains functions_to_translate name orelse Symset.contains already_translated name then
               (* we leave already translated function in, otherwise their callee information is stripped out
                * of the functions_to_translate *)
               SOME (name, FunctionInfo.map_is_simpl_wrapper (K false) info)
             else
               NONE)
        |> Symtab.make


  (* Recalculate callees after "scope" restriction. *)
  val (simpl_call_graph, simpl_info) = FunctionInfo.calc_call_graph simpl_info
  (* Check that recursive function groups are all lifted to the same monad. *)
  val _ = #topo_sorted_functions simpl_call_graph
          |> map (TypeStrengthen.compute_lift_rules ts_rules ts_force o Symset.dest)

  (* Disable heap lifting for all un-translated functions. *)
  val no_heap_abs = Symset.make no_heap_abs

  (* Disable word abstraction for all un-translated functions. *)
  val unsigned_word_abs = these (AutoCorres_Options.get_unsigned_word_abs opt) |> Symset.make
  val no_signed_word_abs = these (AutoCorres_Options.get_no_signed_word_abs opt) |> Symset.make
  val conflicting_unsigned_abs_fns =
        Symset.subtract functions_to_translate unsigned_word_abs

  val _ = if parallel orelse 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 do_polish = the_default true (AutoCorres_Options.get_do_polish opt)
  val L1_opt = the_default FunctionInfo.PEEP (AutoCorres_Options.get_L1_opt opt)
  val L2_opt = the_default FunctionInfo.PEEP (AutoCorres_Options.get_L2_opt opt)
  val HL_opt = the_default FunctionInfo.PEEP (AutoCorres_Options.get_HL_opt opt)
  val WA_opt = the_default FunctionInfo.PEEP (AutoCorres_Options.get_WA_opt opt)

  val trace_opt = AutoCorres_Options.get_trace_opt opt = SOME true
  val gen_word_heaps = AutoCorres_Options.get_gen_word_heaps opt = SOME true

  (* Prefixes/suffixes for generated names. *)
  val make_lifted_globals_field_name = let
    val prefix = case AutoCorres_Options.get_lifted_globals_field_prefix opt of
                     NONE => ""
                   | SOME p => p
    val suffix = case AutoCorres_Options.get_lifted_globals_field_suffix opt of
                     NONE => "_''"
                   | SOME s => s
  in fn f => prefix ^ f ^ suffix end

  fun do_phase' empty phase translate lthy = 
    if FunctionInfo.encode_phase phase <= FunctionInfo.encode_phase max_phase then
       (verbose_msg 1 lthy (fn _ => "Processing phase: " ^ FunctionInfo.string_of_phase phase); translate lthy)
    else (verbose_msg 1 lthy (fn _ => "Skipping phase: " ^ FunctionInfo.string_of_phase phase); empty lthy)

  val do_phase = do_phase' (fn lthy => ([], lthy))

  val base_locale_opt = AutoCorres_Options.get_base_locale opt
    |> Option.map (Locale.check_global thy)

  (* Do the translation. *)

  val cliques = [Symset.dest functions_to_process]
  val _ = verbose_msg 0 lthy (fn _ => "cliques: " ^ @{make_string} cliques)

  val (l1_cliques, lthy) = lthy |> do_phase FunctionInfo.L1 (
        SimplConv.translate
            skips
            base_locale_opt
            prog_info 
            (AutoCorres_Options.get_no_c_termination opt <> SOME true)
            L1_opt trace_opt parallel
            cliques);
  val (l2_cliques, lthy) = lthy |> do_phase FunctionInfo.L2 (
        LocalVarExtract.translate
            skips
            base_locale_opt
            prog_info  
            L2_opt trace_opt parallel 
            l1_cliques);
  (* When skip_io_abs / skip_heap_abs / skip_word_abs is set, we just pass the results from the previous
   * phase to the next phase. Function prove_ac_corres will then reflect these steps as 
   * identity transformations in the final proof. By passing the results to the final phase, 
   * we ensure that polishing
   * of the body and the final definition of the function is done.
   *)

  val (io_cliques, lthy) = lthy |> do_phase FunctionInfo.IO (fn lthy =>
    if #skip_io_abs skips
    then (l2_cliques, lthy)
    else lthy |>
      In_Out_Parameters.translate
        skips
        base_locale_opt
        prog_info
        parallel
        l2_cliques);

  val ((hl_cliques, maybe_heap_info), lthy) = 
    lthy |> do_phase' (fn lthy => (([], NONE), lthy)) FunctionInfo.HL (fn lthy =>
        if #skip_heap_abs skips
        then ((io_cliques, NONE), lthy)
        else 
          let
            val (hl_groups, lthy) = lthy |> HeapLift.translate
               skips
               base_locale_opt
               prog_info
               (the HL_setup_opt) no_heap_abs
               heap_abs_syntax keep_going
               HL_opt trace_opt parallel
               io_cliques

          in 
            ((hl_groups, SOME (#heap_info (the HL_setup_opt))), lthy)
          end);

  val (wa_cliques, lthy) = lthy |> do_phase FunctionInfo.WA  (fn lthy =>
        if #skip_word_abs skips
        then (hl_cliques, lthy) \<comment> \<open>c.f. previous comment on heap_lift phase\<close>  
        else lthy |> WordAbstract.translate skips base_locale_opt prog_info
               maybe_heap_info  
               unsigned_word_abs no_signed_word_abs
               WA_opt trace_opt parallel
               hl_cliques);

  val (ts_cliques, lthy) = lthy |> do_phase FunctionInfo.TS (
        TypeStrengthen.translate
            skips
            base_locale_opt
            ts_rules ts_force prog_info
            keep_going do_polish
            (wa_cliques))
  val thy = lthy |> Local_Theory.exit_global
    |> AutoCorresTrace.ProfileConv.transfer lthy
in
  (ts_cliques, thy)
end);

(* the final theory has no scope just combines everything *)
fun final_task (_, (_, (scope, _))) = null scope

fun sort_tasks tasks = 
  let
    val graph = Graph.make (map (fn (task as (name, (imports, (scope, phase)))) => ((name, task), imports)) tasks)
    val sorted = Graph.topological_order graph |> rev
  in 
    map (Graph.get_node graph) sorted
  end

fun spawn_autocorres parallel filename prog_info HL_setup opts tasks thy =
  let
     val ctxt = Proof_Context.init_global thy
     fun trace s = Utils.timing_msg 1 ctxt (fn () => "autocorres scheduler: " ^ s ()) 
 
     fun ac parallel (t as (name, (imports, (scope, phase)))) (cliques, thy)  =
       if final_task t then (cliques, thy)
       else
         let
           val opts' = AutoCorres_Options.upd_opts opts scope phase 
           val _ = trace (fn () => "doing autocorres for: " ^ name ^ ": " ^ @{make_string} (scope, phase))
         in do_autocorres parallel opts' filename prog_info HL_setup thy end
   in
     if parallel then
       let
         fun depends name = 
           case AList.lookup (op =) tasks name of
             NONE => []
           | SOME (imports, _) => imports
               
         fun join results = 
          let 
            val (cliquess, thys) = split_list results 
          in (flat cliquess |> distinct (op =), Context.join_thys thys) end
         
         val results = Utils.map_reduce trace I fst depends (ac true) join tasks ([], thy)
         
         val final_task_name = fst (hd (filter final_task tasks))
       in
         case AList.lookup (op =) results final_task_name of 
           SOME res => res
         | NONE => error ("parallel autocorres failed in building the theories")
       end  
    else
      let                                                                                      
        val sorted_tasks = sort_tasks tasks
        fun step task (cliques, thy) = 
          let val (cliques', thy') = ac false task (cliques, thy) in (cliques @ cliques' |> distinct (op =), thy') end
        val (cliques, thy') = ([], thy) 
          |> fold step sorted_tasks     
      in
        (cliques, thy')
      end
  end

fun is_initialized filename thy =
  Symtab.defined (AutoCorres_Options.Options_Theory.get thy) filename 


fun check_addressable_field thy xnames =
  let
    val ctxt = Proof_Context.init_global thy
    val (record_name, field_names) = ensure_C_names xnames


    val record_info = RecursiveRecordPackage.get_info thy
    fun select field (recordT, field_infos) =
      let
        val Type(record_name, _) = recordT     
      in
        case Symtab.lookup record_info record_name of
          SOME {fields,...} => (case find_first (fn (xn, T) => Long_Name.base_name xn = field) fields of 
                                  SOME (field_name, T) => (T, field_infos @ [(field_name, T)])
                                | NONE => error ("unknown field " ^ quote field ^ " for " ^ quote record_name))
        | NONE => error ("unknown struct type: " ^ quote record_name)
      end

    val T = \<^try>\<open>Proof_Context.read_typ ctxt record_name catch _ => error ("unknown struct type: " ^ quote record_name)\<close>
    val _ = if null field_names andalso not (TermsTypes.is_array_type T) then error ("not an array type: " ^ quote (Syntax.string_of_typ ctxt T))
            else ()
    val (_, fields) =  (T, []) |> fold select field_names  
  in
    (T, fields)
  end
    
fun check_addressable_fields ignore_addressable_fields_error thy prog_info xnames =
 let
   val ctxt = Proof_Context.init_global thy
   val record_info = RecursiveRecordPackage.get_info thy
   val union_variants = ProgramAnalysis.get_union_variants (ProgramInfo.get_csenv prog_info)

   fun resolve_variant (ty_name, variant_or_field_name) =
     case AList.lookup (op =) union_variants (Long_Name.base_name ty_name) of
       SOME variants => 
          (case get_first (fn (x, senv) => if x = variant_or_field_name then SOME (#1 (hd senv))  else NONE) variants of
             SOME (variant_name) => Long_Name.map_base_name (K variant_name) ty_name
          | _ => error ("resolve_variant: undefined union variant: " ^ @{make_string} (ty_name, variant_or_field_name)))
     | _ => ty_name

   fun merge_fields (fs as ((T, _)::_) ) = (T, distinct (op =) (map snd fs))  
   val singles = map (check_addressable_field thy) xnames |> group_by (fn ((T1, _), (T2, _)) => T1 = T2) 
     |> map merge_fields   

   fun all_fields (Type(record_name, _)) = Symtab.lookup record_info record_name |> the |> #fields

   fun suffixes sfxs field = 
     let
        val sfxs' = map_filter (fn (f::fs) => if f = field  then SOME fs else NONE | _ => NONE) sfxs
     in
       if null sfxs' then NONE else SOME (field, sfxs') 
     end

   fun expand_fields (prefix:(string*typ) list) (addressable_sfxs: (string*typ) list list) (T:typ): (string*typ) list list = 
     case addressable_sfxs of [[]] => [[]] | _ =>
     let
       val all = all_fields T
       val (addressable, not_addressable) = Utils.split_map_filter (suffixes addressable_sfxs) all
       val not_addressable' = map (fn (field as (_, fieldT), sfxs) => expand_fields (prefix @ [field]) sfxs fieldT) addressable
     in
       ( map (fn field => prefix @ [field]) not_addressable @  flat not_addressable')
     end 
   fun select_field (Type(record_name, _)) field = 
       let
         val record_name' = resolve_variant (record_name, field)
       in
         Symtab.lookup record_info record_name' |> the |> #fields 
         |> find_first (fn (long, ty) => Long_Name.base_name long = field)
         |> the
       end
   fun filter_intermediate_arrays [] = []
     | filter_intermediate_arrays [x] = [x]
     | filter_intermediate_arrays (x::xs) = x :: filter_out (fn (ty, fld) => fld = "") xs       

   fun expand_type ty [] = []
     | expand_type ty (x::xs) = 
          (case x of 
            Expr.Field f => 
              let val (long, ty') = select_field ty f in (ty, long)::expand_type ty' xs end
          | Expr.Index _ => 
              (case ty of
                 \<^Type>\<open>ptr ty'\<close> => expand_type ty' xs 
               | _ => let val ty' = TermsTypes.element_type ty in (ty, "")::expand_type ty' xs end))  

   val addressed_types = ProgramAnalysis.get_addressed_types (ProgramInfo.get_csenv prog_info) 
        |> Absyn.CTypeTab.dest
        |> map_filter (fn (cty, selectors) => 
            let
              val ty = CalculateState.ctype_to_typ_flexible_array {bitint_padding=true} ctxt cty
            in 
              if forall null selectors then 
                NONE
              else 
                SOME (map (filter_intermediate_arrays o expand_type ty) selectors)
            end) 
        |> flat |> flat

   val addressable_fields = singles |> map (fn (T, addressable) => 
        (T, 
         {not_addressable = expand_fields [] addressable T |> filter_out null, 
         addressable = addressable |> filter_out null}))
 
   fun find_addressable_field (ty, fld) = AList.lookup (op =) addressable_fields ty 
     |> Option.mapPartial (fn {addressable, ...} => 
          if null addressable andalso fld="" then 
            SOME ty 
          else
            get_first (fn flds => AList.lookup (op =) flds fld) addressable)

   val missing_fields = addressed_types |> filter_out (is_some o find_addressable_field)
   
   fun pretty (arr_ty, "") = Pretty.quote (Syntax.pretty_typ ctxt arr_ty)
     | pretty (struct_ty, fld) = 
         Pretty.block [
           Syntax.pretty_typ ctxt struct_ty, Pretty.str "." , 
           Pretty.str (Long_Name.base_name fld)]
  
   val trace = if ignore_addressable_fields_error then warning else error
   val _ = if null missing_fields then () else
       trace (Pretty.string_of (Pretty.big_list "These fields should be made addressable (for lifting into the split heap): " 
             (map pretty (missing_fields))))
 in
   addressable_fields
 end

fun frame_commute_lemmas thy =
  let
    val ctxt = Proof_Context.init_global thy
    val rec_name = NameGeneration.global_rcd_name
    val globalsT = Proof_Context.read_typ ctxt rec_name
    val fields = Record.get_extT_fields thy globalsT |> fst
    val fields_wo_heap = fields |> filter_out (fn (f, _) => Long_Name.base_name f = NameGeneration.global_heap_var)
    val field_funs = fields_wo_heap |> map (fn x as (f, T) =>
         (x, (Const (f, globalsT --> T),
          Const (f ^  Record.updateN, (T --> T) --> globalsT --> globalsT))))
    val frame =  Proof_Context.read_term_pattern ctxt (Long_Name.qualify NameGeneration.global_rcd_name "frame")
    val frame_def = Proof_Context.get_thm ctxt (Long_Name.qualify NameGeneration.global_rcd_name "frame_def")

    val ([A, g0, g], ctxt1) = Utils.fix_variant_frees [("A", \<^typ>\<open>addr set\<close>), ("g0", globalsT), ("g", globalsT)] ctxt

    fun sel_frame_prop sel = \<^infer_instantiate>\<open>A = A and g0 = g0 and g = g and sel = sel and frame=frame 
      in prop \<open>sel (frame A g0 g) = sel g\<close> \<close> ctxt1
    val sel_props = map sel_frame_prop (map (fst o snd) field_funs)
    fun prove (prop, ctxt')  = Goal.prove_future ctxt' [] [] prop (fn {context = ctxt, ...} =>
          Record.split_simp_tac ctxt [] (K ~1) 1 THEN
          asm_full_simp_tac (ctxt addsimps [frame_def]) 1) 
      |> singleton (Proof_Context.export ctxt' ctxt)
    fun prove1 prop = prove (prop, ctxt1) 
    val sel_thms = map prove1 sel_props
    fun upd_frame_prop ((_, T), (_, upd)) = 
      let
        val ([f], ctxt2) = Utils.fix_variant_frees [("f", T --> T)] ctxt1
        val prop = 
          \<^infer_instantiate>\<open>A = A and g0 = g0 and g = g and upd = upd and frame=frame and f = f
            in prop (schematic) \<open>frame A g0 (upd f g) = upd f (frame A g0 g)\<close>\<close> ctxt2
      in (prop, ctxt2) end
    val upd_props = map upd_frame_prop field_funs
    val upd_thms = map prove upd_props

  in
    {sel_thms = sel_thms, upd_thms = upd_thms}
  end

fun note_frame_commute_lemmas thy =
  let
    val {sel_thms, upd_thms} = frame_commute_lemmas thy
  in
    thy 
    |> Named_Target.theory_init
    |> Local_Theory.note ((Binding.make ("globals_sel_frame", \<^here>), @{attributes [sel_frame_thms, simp]}), sel_thms)
    ||>> Local_Theory.note ((Binding.make ("globals_upd_frame_commutes", \<^here>), @{attributes [upd_frame_commutes, simp]}), upd_thms)
    ||> Local_Theory.exit_global
  end

fun do_init_autocorres (opt : AutoCorres_Options.autocorres_options) cfilename store_opt thy =
  let
    val filename = cfilename |> Path.explode |> Path.drop_ext |> Path.file_name
  (* Ensure that the filename has already been parsed by the C parser. *)
    val csenv = case CalculateState.get_csenv thy cfilename of
          NONE => error ("Filename '" ^ cfilename ^ "' has not been parsed by the C parser yet.")
        | SOME x => x
    val globals_locale = NameGeneration.intern_globals_locale_name thy filename
  (* Prefixes/suffixes for generated names. *)
    fun gen_make_function_name phase ext = 
      let
        val phase_prefix = 
          case phase of 
               FunctionInfo.TS => "" 
             | FunctionInfo.CP => ""
             | _ => FunctionInfo.string_of_phase phase |> String.translate (str o Char.toLower) |> suffix "_"
        val prefix = 
          case phase of 
            FunctionInfo.CP => "" 
          | _ => (case AutoCorres_Options.get_function_name_prefix opt of
                         NONE => ""
                       | SOME p => p)
        val suffix =  
          case phase of 
            FunctionInfo.CP => "" 
          | _ => (case AutoCorres_Options.get_function_name_suffix opt of
                         NONE => "'"
                       | SOME s => s)
      in (fn name => phase_prefix ^ ext ^ prefix ^ name ^ suffix, 
          fn full_name => 
            let
            in
              full_name |> unsuffix suffix |> unprefix phase_prefix |> unprefix ext |> unprefix prefix
            end)
      end
    fun make_function_name phase ext name = fst (gen_make_function_name phase ext) name
    fun dest_function_name phase ext full_name = snd (gen_make_function_name phase ext) full_name

    val _ = check_options thy cfilename opt
  in
    if is_initialized filename thy 
    then 
      let
        val prog_info = AutoCorres_Options.get_prog_info thy filename
        val fun_opts = fun_options (ProgramInfo.get_csenv prog_info) opt
        val cty_specs = check_method_in_out_fun_ptr_specs thy cfilename opt
        val prog_info = prog_info 
          |> ProgramInfo.map_fun_options (K fun_opts)
          |> ProgramInfo.map_method_io_params (fn xs => AList.merge (op =) (op =) (xs, cty_specs))       
        val HL_setup_opt = Symtab.lookup (HeapLiftBase.HeapInfo.get thy) filename
        val prog_info = (case HL_setup_opt of 
            SOME HL_setup =>
              prog_info 
              |> ProgramInfo.map_lifted_globals_type (K (SOME (#globals_type (#heap_info HL_setup))))
              |> ProgramInfo.map_lift_global_heap (K ((#lift_fn_full (#heap_info HL_setup))))
                
          | NONE => prog_info)
      in
        ((prog_info, HL_setup_opt), thy)
      end
    else
      let 
        val thy = note_frame_commute_lemmas thy |> snd
        val ctxt0 = Proof_Context.init_global thy
        val cse = CalculateState.get_csenv thy cfilename |> the;
        val method_io_params = Utils.timeit_msg 1 ctxt0 (fn _ => "check_method_in_out_fun_ptr_specs") (fn _ => 
          check_method_in_out_fun_ptr_specs thy cfilename opt)
        val prog_info = Utils.timeit_msg 1 ctxt0 (fn _ => "get_prog_info") (fn _ => 
          ProgramInfo.get_prog_info thy (fun_options cse opt) method_io_params make_function_name dest_function_name cfilename)
        val skips = AutoCorres_Options.get_skips opt
        val (_, thy) = Utils.timeit_msg 1 ctxt0 (fn _ => "init_function_info") (fn _ => 
          thy |> AutoCorresData.init_function_info skips prog_info)
        val ctxt = Proof_Context.init_global thy

        val params = HP_TermsTypes.globals_stack_heap_raw_state_params HP_TermsTypes.State ctxt
        val [hrs, hrs_upd,  S] = map Utils.dummy_schematic 
               [#hrs params, #hrs_upd params, #S params] 
        val params_globals = HP_TermsTypes.globals_stack_heap_raw_state_params HP_TermsTypes.Globals ctxt
        val [hrs_globals, hrs_upd_globals] = map Utils.dummy_schematic
               [#hrs params_globals, #hrs_upd params_globals]       
        val expr = ([(@{locale L2_heap_raw_state}, ((NameGeneration.global_ext_type, false),
             (Expression.Positional (map SOME ([
               hrs_globals, hrs_upd_globals,
               hrs, hrs_upd, S, ProgramInfo.get_globals_getter prog_info])), [])))], []) 
     
        val thy = Utils.timeit_msg 1 ctxt0 (fn _ => "L2_heap_raw_state interpretation") (fn _ => 
          thy |> Named_Target.theory_init
          |> Interpretation.global_interpretation expr []
          |> Proof.global_terminal_proof ((Method.Basic (fn ctxt =>  SIMPLE_METHOD (
              (Locale.intro_locales_tac {strict = false, eager = true} ctxt [] THEN 
                 ALLGOALS (asm_full_simp_tac (ctxt addsimps 
                   @{thms hrs_mem_def hrs_mem_update_def hrs_htd_def hrs_htd_update_def case_prod_unfold}))))), 
              Position.no_range), NONE) 
          |> Local_Theory.exit_global)
   
        val max_arity = ProgramAnalysis.get_max_function_arity cse
        val lthy = Named_Target.theory_init thy
                   |> AutoCorres_Options.Options_Proof.map (K opt)
                   |> map_of_default_args.ensure_L2_call_map_of_default_commutes_upto max_arity
                   |> map_of_default_args.ensure_runs_to_partial_map_of_default_upto max_arity

        val all_simpl_infos = AutoCorresData.get_phase_info (Context.Proof lthy) filename FunctionInfo.CP |> the
        (* heap_abs_syntax defaults to off. *)
        val heap_abs_syntax = AutoCorres_Options.get_heap_abs_syntax opt = SOME true
     
        (* Prefixes/suffixes for generated names. *)
        val make_lifted_globals_field_name = 
          let
            val prefix = case AutoCorres_Options.get_lifted_globals_field_prefix opt of
                           NONE => ""
                         | SOME p => p
            val suffix = case AutoCorres_Options.get_lifted_globals_field_suffix opt of
                           NONE => "_''"
                         | SOME s => s
           in fn f => prefix ^ f ^ suffix end;

        val gen_word_heaps = AutoCorres_Options.get_gen_word_heaps opt = SOME true

        val (prog_info, HL_setup, lthy) = Utils.timeit_msg 1 ctxt0 (fn _ => "L2_heap_raw_state interpretation") (fn _ =>
          if AutoCorres_Options.get_skip_heap_abs opt = SOME true then (prog_info, NONE, lthy) 
          else
            let
              val ignore_addressable_fields_error = AutoCorres_Options.get_ignore_addressable_fields_error opt = SOME true
              val addressable_fields = AutoCorres_Options.get_addressable_fields opt |> these 
                |> check_addressable_fields ignore_addressable_fields_error thy prog_info

              val (HL_setup, lthy) = lthy |> HeapLiftBase.prepare_heap_lift filename prog_info addressable_fields 
                    all_simpl_infos make_lifted_globals_field_name gen_word_heaps heap_abs_syntax
              val prog_info = prog_info 
                |> ProgramInfo.map_lifted_globals_type (K (SOME (#globals_type (#heap_info HL_setup))))
                |> ProgramInfo.map_lift_global_heap (K ((#lift_fn_full (#heap_info HL_setup))))
            in (prog_info, SOME HL_setup, lthy) end)

        val opt' = if store_opt then opt else AutoCorres_Options.default_opts
        val _ = verbose_msg 0 (Proof_Context.init_global thy) (fn _ => "options: " ^ @{make_string} opt')
        val lthy = Utils.timeit_msg 1 ctxt0 (fn _ => "state_fold_congs") (fn _ =>
          let
            val state_fold_congs = ProgramInfo.get_state_fold_congs (Proof_Context.theory_of lthy) prog_info
            val [attr] = map (Attrib.attribute lthy) @{attributes [state_fold_congs]}
            (* FIXME: note instead of declaration should be sufficient *)
           in 
            lthy |> Local_Theory.declaration {pervasive = true, pos = \<^here>, syntax = false} (fn phi => 
                      fold (Thm.attribute_declaration attr o Morphism.thm phi) state_fold_congs)
           end)
        val thy = lthy 
          |> Local_Theory.exit_global
          |> AutoCorres_Options.Options_Theory.map (Symtab.update (filename, 
              {options=opt', prog_info = prog_info, state=AutoCorres_Options.Intermediate}))
      in ((prog_info, HL_setup), thy) end
  end  

fun is_finalised filename thy =
  let
    val state = Symtab.lookup (AutoCorres_Options.Options_Theory.get thy) filename 
      |> Option.map #state 
  in state = SOME (AutoCorres_Options.Final) end

fun final_autocorres skips prog_info funs thy =
  let
    val prog_name = ProgramInfo.get_prog_name prog_info
    val has_fun_pointers = ProgramAnalysis.program_has_fun_ptr_calls (ProgramInfo.get_csenv prog_info)
  in
    thy |> has_fun_pointers? ( 
      Named_Target.theory_init
      #> Function_Pointer.define_progenvs_and_rewrite_defs prog_name
      #> Local_Theory.exit_global
      #> AutoCorres_Options.Options_Theory.map (Symtab.map_entry prog_name 
           (fn  {options, prog_info, state} => {options = options, prog_info=prog_info, state=AutoCorres_Options.Final})))
  end

fun final_autocorres_cmd cfilename thy =
  let
    val start = Timing.start ();
    val filename = cfilename |> Path.explode |> Path.split_ext |> fst |> Path.file_name
    val (opt, prog_info) = 
      case Symtab.lookup (AutoCorres_Options.Options_Theory.get thy) filename of 
        SOME {options, ...}  => (options, #1 (#1 (do_init_autocorres options cfilename false thy)))
      | _ => error ("final_autocorres: autocorres not yet run on: " ^ quote cfilename)

   val all_functions = ProgramAnalysis.get_cliques (ProgramInfo.get_csenv prog_info) |> flat
   val _ = verbose_msg 0 (Proof_Context.init_global thy) (fn _ => "options: " ^ @{make_string} opt)

   val skips = AutoCorres_Options.get_skips opt
   val get_ts_def = AutoCorresData.get_function_info (Context.Theory thy) filename FunctionInfo.TS 
     #> Option.mapPartial FunctionInfo.get_proper_definition
   val translated_functions = all_functions |> filter (is_some o get_ts_def) 
   val thy = if not (is_finalised filename thy) 
     then final_autocorres skips prog_info translated_functions thy
     else error ("final_autocorres: autocorres already finalized for: " ^ quote cfilename)
  in
    thy
    before (Utils.timing_msg' 1 (Proof_Context.init_global thy) (fn _ => "final-autocorres") start)
  end

fun parallel_autocorres (opt : AutoCorres_Options.autocorres_options) cfilename thy =
  let
    val start = Timing.start ();

    val filename = cfilename |> Path.explode |> Path.split_ext |> fst |> Path.file_name
    val opt = case Symtab.lookup (AutoCorres_Options.Options_Theory.get thy) filename of

           NONE => opt
         | SOME {options=opt', ...} => AutoCorres_Options.merge_opt opt' opt;
    val ((prog_info, HL_setup), thy) = do_init_autocorres opt cfilename false thy
    val globals_locale = NameGeneration.intern_globals_locale_name thy filename  

    val _ = verbose_msg 0 (Proof_Context.init_global thy) (fn _ => "options: " ^ @{make_string} opt)
    val single_threaded = AutoCorres_Options.get_single_threaded opt = SOME true  (* single threaded defaults to off. *)

    val skips = AutoCorres_Options.get_skips opt
    val keep_going = AutoCorres_Options.get_keep_going opt = SOME true       
    val max_phase = the_default FunctionInfo.TS (AutoCorres_Options.get_phase opt)
    val existing_ts = existing_info (Proof_Context.init_global thy) filename FunctionInfo.TS

    val thy =
       ( let
            val lthy = Named_Target.init [] globals_locale thy
  
            val all_simpl_infos = AutoCorresData.get_phase_info (Context.Proof lthy) filename FunctionInfo.CP |> the
            val scope = these (AutoCorres_Options.get_scope opt)
            val reachable = if null scope then Symtab.keys all_simpl_infos  
              else all_reachable all_simpl_infos (these (AutoCorres_Options.get_scope opt))
 
            fun in_scope (t as (_, (_, (scope, _)))) = final_task t orelse subset (op =) (scope, reachable);
 
            val phase_info = existing_info lthy filename
 
            fun not_already_existing (t as (_, (_, (scope, phase)))) = final_task t orelse  
                  not (subset (op =) (scope, phase_info phase |> Symtab.keys))
   
            fun adjust_imports defined (name, (imports, (scope, phase))) = 
              let 
                val imports' = filter (member (op =) defined) imports
              in (name, (imports', (scope, phase))) end 
 
            val tasks = build_tasks all_simpl_infos filename skips max_phase 
                 |> filter in_scope
                 |> filter not_already_existing
                 |> (fn tasks => map (adjust_imports (map fst tasks)) tasks)
            val _ = verbose_msg 1 lthy (fn _=> "tasks: " ^ @{make_string} tasks)
            val _ = Utils.timing_msg 1 lthy (fn () => "tasks: " ^ @{make_string} tasks)
            val _ = @{assert} (final_task (hd tasks))
 
          in case tasks of
               (_::_) => spawn_autocorres (not single_threaded) filename prog_info HL_setup opt tasks thy 
             | _ => error ("All functions in scope are already translated (cf. option 'fresh').") 
               
          end)
       |> finalise prog_info skips keep_going existing_ts
 
   val all_functions = ProgramAnalysis.get_non_proto_and_body_spec_functions (ProgramInfo.get_csenv prog_info)
 
   val globloc = NameGeneration.intern_globals_locale_name thy filename
   val lthy = Named_Target.init [] globloc thy

   val TS_info = AutoCorresData.get_phase_info (Context.Proof lthy) filename FunctionInfo.TS
   val all_functions_translated = 
     case TS_info of NONE => false
     | SOME info => all_functions 
        |> forall (is_some o (Symtab.lookup info #> Option.mapPartial FunctionInfo.get_proper_corres_thm))

   val thy = 
     if all_functions_translated then 
        if is_finalised filename thy then
          (warning ("autocorres already finalised for: " ^ quote cfilename); thy) 
        else 
          final_autocorres skips prog_info all_functions thy
     else 
       thy
  in
    thy
    before (Utils.timing_msg' 1 (Proof_Context.init_global thy) (fn _ => "autocorres (parallel)") start)
  end
     
end