File ‹name_generation.ML›
signature NAME_GENERATION =
sig
val globalsN : string
val locals_stackN: string
val bytesN : string
val initialisation_function : string
val return_var_name : MString.t
val tmp_var_name : string * int -> MString.t
val dest_tmp : MString.t -> (string * int) option
val is_return_or_tmp: MString.t -> bool
val fun_ptr_name: string -> string
val C_global_var : MString.t -> MString.t
val global_var : string -> string
val global_addr : string -> string
val fake_param : string -> int -> string
val stack_addrs : string
val global_addrs : string
val known_function: string
datatype var_kind = In of int | Out | Loc
val var_kind_ord : (var_kind * var_kind) -> order
type var_sort = {kind: var_kind, addressable: bool}
datatype local_ref = Positional of (int * typ) | Named of string
val map_local_ref : ((int * typ) -> (int * typ)) -> (string -> string) -> local_ref -> local_ref
val map_positional: ((int * typ) -> (int * typ)) -> local_ref -> local_ref
val map_named : (string -> string) -> local_ref -> local_ref
val the_named: local_ref -> string
val the_positional: local_ref -> (int * typ)
val positional_name : bool -> string -> int -> int CTypeDatatype.ctype -> string
val dest_positional_name : string -> (var_kind * string) option
val ensure_varname : string -> string
val un_varname : string -> string
val canonical_name : (string * (var_kind * typ * int CTypeDatatype.ctype)) -> string
val tag_name_with_type : {name: string, typname:string} -> string
val adglob_rcd_tyname : string
val adglob_struct_var : string
val naming_scheme_name : string
val exitN : string
val exit_status_parN : string
val enum_const_name : string -> string
val enum_const_summary_lemma_sfx : string
val untouched_global_name : MString.t -> MString.t
val global_initializer_name : MString.t -> MString.t
val global_data_name : string -> string
val state_rcd_name : string
val global_rcd_name : string
val global_ext_type : string
val global_exn_var_name : string
val global_exn_var : string
val global_heap : string
val global_heap_var : string
val C_struct_name : string -> string
val unC_struct_name : string -> string
val ensure_C_struct_name : string -> string
val C_field_name : string -> string
val unC_field_name : string -> string
val ensure_C_field_name : string -> string
val internalAnonStructPfx : string
val mkAnonStructName : {union:bool} -> int -> string
val mkIdentUScoreSafe : string -> string
val rmUScoreSafety : string -> string
val apt_string : string -> string
val numCopyN : string
val phantom_state_name : string
val ghost_state_name : string
val owned_by_fn_name : string
val mk_localstatic : {fname : string, vname : string } -> MString.t
val globals_locale_name: string -> string
val variables_bundle_name: string -> string
val impl_clique_locale_name: string list -> string
val impl_locale_name: string -> string
val simpl_locale_name: string -> string
val intern_locale: theory -> xstring -> string
val maybe_intern_locale: theory -> xstring -> string
val intern_bundle: theory -> xstring -> string
val intern_globals_locale_name: theory -> string -> string
val intern_variables_bundle_name: theory -> string -> string
val intern_impl_clique_locale_name: theory -> string list -> string
val intern_impl_locale_name: theory -> string -> string
val intern_simpl_locale_name: theory -> string -> string
end;
structure NameGeneration :> NAME_GENERATION =
struct
datatype local_ref = Positional of (int * typ) | Named of string
fun map_local_ref f g l =
case l of
Positional p => Positional (f p)
| Named n => Named (g n)
fun map_positional f = map_local_ref f I
fun map_named g = map_local_ref I g
fun the_named (Named s) = s
fun the_positional (Positional p) = p
val globalsN = "_global_addresses"
val locals_stackN = "locals_stack"
val exitN = "exit"
val exit_status_parN = "status"
val initialisation_function = "___special___init"
val bytesN = "bytes'"
val return_var_name = MString.mk "ret'";
fun tmp_var_name (f,i) =
MString.mk ("ret'" ^ f ^ "'" ^ Int.toString i)
fun dest_tmp s0 =
let
val s = MString.dest s0
open Substring
val (pfx, digsfx) = splitr Char.isDigit (full s)
in
if isEmpty digsfx then NONE
else if isSuffix "'" pfx andalso isPrefix "ret'" pfx then
SOME (string (triml 4 (trimr 1 pfx)), the (Int.fromString (string digsfx)))
else
NONE
end
fun is_return_or_tmp s =
MString.dest s = MString.dest return_var_name orelse is_some (dest_tmp s)
datatype var_kind = In of int | Out | Loc
fun var_kind_ord (In i1, In i2) = int_ord (i1, i2)
| var_kind_ord (In _ , Out ) = LESS
| var_kind_ord (In _ , Loc ) = LESS
| var_kind_ord (Out , In _ ) = GREATER
| var_kind_ord (Out , Out ) = EQUAL
| var_kind_ord (Out , Loc ) = LESS
| var_kind_ord (Loc , In _ ) = GREATER
| var_kind_ord (Loc , Out ) = GREATER
| var_kind_ord (Loc , Loc ) = EQUAL
type var_sort = {kind: var_kind, addressable: bool}
fun un_varname name =
perhaps (try (unsuffix HoarePackage.deco)) name
fun ensure_varname name =
case try (unsuffix HoarePackage.deco) name of
SOME _ => name
| _ => suffix HoarePackage.deco name
fun gen_positional_name sfx kind i cty = suffix sfx (space_implode "'" [kind, string_of_int i, Absyn.tyname cty])
fun positional_name deco = gen_positional_name (if deco then HoarePackage.deco else "")
fun dest_positional_name n =
case space_explode "'" (un_varname n) of
("in":: pos::(tynames as _::_)) => SOME (In (fst (read_int (Symbol.explode pos))), space_implode "'" tynames)
| _ => NONE
fun canonical_name (name, (kind, ty, cty)) =
(case kind of
In i => positional_name false "in" i cty
| _ => name)
fun tag_name_with_type {name: string, typname:string} = name ^ "'" ^ typname
fun fake_param f i = f ^ "_param_" ^ Int.toString i
fun ext_type t = t ^ "_ext"
fun enum_const_name s = s
val enum_const_summary_lemma_sfx = "_defs"
fun fix_underscore s = if String.isPrefix "_" s
then "underscore" ^ s else s
fun untouched_global_name s =
s |> MString.dest |> fix_underscore |> MString.mk
fun global_initializer_name s =
fix_underscore (MString.dest s) ^ "_global_initializer" |> MString.mk
fun global_data_name s = fix_underscore s ^ "_global_data"
val state_rcd_name = "state"
val global_rcd_name = "globals"
val global_ext_type = ext_type global_rcd_name
val global_exn_var_name = "global_exn_var'"
val global_exn_var = global_exn_var_name ^ "_'"
fun C_global_var s = s
fun global_var s = Hoare.varname s
fun global_addr s = s ^"_addr"
fun global_upd s = global_var s ^ "_upd"
val global_heap = "t_hrs"
val global_heap_var = global_var global_heap
val stack_addrs = "𝒮"
val global_addrs = "𝒢"
val known_function = "known_function"
fun apt_string s = "[.[" ^ s ^ "].]"
val numCopyN = "tyCopy"
fun C_struct_name s = s ^ "_C"
fun unC_struct_name s =
if String.isSuffix "_C" s then
String.extract(s,0,SOME(size s - 2))
else s
val C_field_name = CType.C_field_name
val unC_field_name = CType.unC_field_name
fun ensure make dest s = make (dest s)
val ensure_C_struct_name = ensure C_struct_name unC_struct_name
val ensure_C_field_name = ensure C_field_name unC_field_name
val adglob_rcd_tyname = "adglobs_struct"
val adglob_struct_var = "adglobs"
val phantom_state_name = "phantom_machine_state"
val ghost_state_name = "ghost'state"
val naming_scheme_name = "\\" ^ "<Gamma>_naming"
val owned_by_fn_name = "owner'ship"
val internalAnonStructPfx = "ISA_anon_struct_"
fun mkAnonStructName {union=false} i = "AnonStruct" ^ Int.toString i ^ "'"
| mkAnonStructName {union=true} i = "AnonUnion" ^ Int.toString i ^ "'"
val ussafe_pfx = "StrictC'"
fun mkIdentUScoreSafe s =
if String.sub(s, 0) = #"_" then ussafe_pfx^s
else s
fun rmUScoreSafety s =
if String.isPrefix ussafe_pfx s then
String.extract(s, String.size ussafe_pfx, NONE)
else s
fun mk_localstatic {fname, vname} =
MString.mk (fname ^ "'" ^ vname)
fun fun_ptr_name fname =
if Name.is_internal fname then suffix Hoare.proc_deco fname else fname
fun intern_locale thy name =
let
val loc = Locale.intern thy name |> perhaps Long_Name.dest_hidden
in
if Locale.defined thy loc then loc else error ("intern_locale: undefined locale: " ^ name)
end
fun maybe_intern_locale thy name =
case try (intern_locale thy) name of SOME n => n | NONE => name
fun intern_bundle thy name =
let
val ctxt = Proof_Context.init_global thy
val loc = Bundle.check ctxt (name, Position.none)
in
loc
end
fun globals_locale_name filename = suffix globalsN filename
fun intern_globals_locale_name thy filename =
intern_locale thy (globals_locale_name filename);
fun variables_bundle_name fname = suffix "_variables" fname;
fun intern_variables_bundle_name thy fname =
intern_bundle thy (variables_bundle_name fname);
fun impl_clique_locale_name clique = suffix "_impl" (space_implode "_" (sort_strings clique));
fun impl_locale_name fname = impl_clique_locale_name [fname]
fun intern_impl_clique_locale_name thy clique =
intern_locale thy (impl_clique_locale_name clique);
fun intern_impl_locale_name thy fname = intern_impl_clique_locale_name thy [fname]
fun simpl_locale_name prog_name = suffix "_simpl" prog_name;
fun intern_simpl_locale_name thy prog_name = intern_locale thy prog_name
end;