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

autocorres: use c-parser name demangler 

The C parser tracks what short names a given long name corresponds to.
Change AutoCorres to use that information, instead of trying to demangle
the names 'manually'.
This commit is contained in:
Edward Pierzchalski 2019-03-06 16:43:13 +11:00
parent 7ec43436ba
commit caf2d2cfef
2 changed files with 25 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
tools/autocorres/local_var_extract.ML
View File

@ -39,10 +39,10 @@ fun setup_l2_ss ctxt = put_simpset AUTOCORRES_SIMPSET ctxt
addsimps [@{thm ucast_id}, @{thm pred_conj_def}]
(* Convert a set of variable names into an Isabelle list of strings. *)
fun var_set_to_isa_list s =
fun var_set_to_isa_list prog_info s =
dest_set s
|> map fst
|> map ProgramInfo.demangle_name
|> map (ProgramInfo.demangle_name prog_info)
|> map Utils.encode_isa_string
|> Utils.encode_isa_list @{typ string}
@ -738,7 +738,7 @@ fun inject_return_vals ctxt prog_info name_map needed_returns allow_excess throw
val injected_return =
mk_l2monad prog_info @{const_name L2_gets} needed_returns throw_vars
[absdummy (#globals_type prog_info) (HOLogic.mk_tuple (dest_set needed_returns |> map name_map)),
var_set_to_isa_list needed_returns]
var_set_to_isa_list prog_info needed_returns]
|> abs_over_tuple_vars name_map vars_returned
(* Append the return statement to the input term. *)
@ -839,7 +839,7 @@ in
| Modify (_, (SOME expr, _, _), NONE) =>
let
val generated_term = mk_monad @{const_name L2_gets}
empty_set throw_vars [expr, var_set_to_isa_list empty_set]
empty_set throw_vars [expr, var_set_to_isa_list prog_info empty_set]
val thm = mkthm empty_set empty_set generated_term @{thm L2corres_gets_skip}
in
inject (empty_set, empty_set, generated_term, thm)
@ -868,7 +868,7 @@ in
| Modify (_, (SOME expr, read_vars, _), SOME output_var) =>
let
val generated_term = mk_monad @{const_name L2_gets}
(make_set [output_var]) throw_vars [expr, var_set_to_isa_list (make_set [output_var])]
(make_set [output_var]) throw_vars [expr, var_set_to_isa_list prog_info (make_set [output_var])]
val thm = mkthm read_vars (make_set [output_var]) generated_term @{thm L2corres_modify_gets}
in
inject (read_vars, make_set [output_var], generated_term, thm)
@ -878,7 +878,7 @@ in
let
val generated_term = mk_monad @{const_name L2_throw} needed_vars throw_vars
[HOLogic.mk_tuple (dest_set throw_vars |> map name_map),
var_set_to_isa_list throw_vars]
var_set_to_isa_list prog_info throw_vars]
val thm = mkthm throw_vars needed_vars generated_term @{thm L2corres_throw}
in
(throw_vars, needed_vars, generated_term, thm)
@ -1057,7 +1057,7 @@ in
abs_over_tuple_vars name_map loop_iterators expr,
new_body,
HOLogic.mk_tuple (dest_set loop_iterators |> map name_map),
var_set_to_isa_list loop_iterators]
var_set_to_isa_list prog_info loop_iterators]
(* Generate a proof. *)
val thm =
@ -1227,7 +1227,7 @@ fun get_expected_l2_fn_args lthy prog_info l1_infos fn_name =
let
val fn_def = the (Symtab.lookup l1_infos fn_name)
in
map (apfst (ProgramInfo.demangle_name)) (#args fn_def)
map (apfst (ProgramInfo.demangle_name prog_info)) (#args fn_def)
end
fun get_expected_l2_fn_thm prog_info l1_infos ctxt fn_name fn_free fn_args _ measure_var =
@ -1533,7 +1533,7 @@ fun convert
* We do this after fixing the callees, because there is still some broken code
* (e.g. in define_funcs) that requires callee var to exactly match the
* names generated by l2_function_name. *)
val f_args = map (apfst ProgramInfo.demangle_name) (#args f_info);
val f_args = map (apfst (ProgramInfo.demangle_name prog_info)) (#args f_info);
val (arg_names, lthy''') = Variable.variant_fixes (map fst f_args) lthy'';
val arg_frees = arg_names ~~ map snd f_args;
@ -1601,7 +1601,7 @@ fun define
|> FunctionInfo.function_info_upd_mono_thm NONE (* added later *)
(* Update arg names to match our newly converted functions *)
|> FunctionInfo.function_info_upd_args
(map (apfst (ProgramInfo.demangle_name)) (#args old_info))
(map (apfst (ProgramInfo.demangle_name prog_info)) (#args old_info))
end) new_thms;
in (new_infos, lthy') end;

33
tools/autocorres/program_info.ML
View File

@ -118,24 +118,21 @@ end
(*
* Demangle a name mangled by the C parser.
*)
fun demangle_name m =
if NameGeneration.rmUScoreSafety m <> m
then (* ignore the "StrictC'" prefix when decoding, but we need to re-mangle it in
* so that the resulting name is legal in Isabelle *)
NameGeneration.mkIdentUScoreSafe (demangle_name (NameGeneration.rmUScoreSafety m))
else case NameGeneration.dest_embret (MString.mk m) of
(* Return variable for function f *)
SOME (_, n) => "ret" ^ (if n > 1 then string_of_int n else "")
(* Ordinary variable. Split the type suffix off if there is one. *)
| NONE => let
val delim = "___" (* NameGeneration.tag_name_with_type *)
val (prefix, _) = apply2 Substring.string (Utils.positionr delim (Substring.full m))
in prefix end
val _ = assert (demangle_name "c___ret_int" = "c") ""
val _ = assert (demangle_name "ret_eret_2" = "ret2") ""
val _ = assert (demangle_name "StrictC'__reserved___int" = "StrictC'__reserved") ""
fun demangle_name (prog_info: prog_info) m =
case m |> NameGeneration.rmUScoreSafety |> MString.mk |> NameGeneration.dest_embret of
(* Return variable for function f *)
SOME (_, n) => "ret" ^ (if n > 1 then string_of_int n else "")
(* Ordinary variable. Look up the original name in csenv. *)
| NONE =>
let
fun lookup k v = Symtab.lookup v k
in
(* Don't bother checking if we're asked to demangle an unmangled name
(e.g. a global), just default to the input. *)
ProgramAnalysis.get_mangled_vars (#csenv prog_info)
|> lookup m |> Option.map (hd #> ProgramAnalysis.srcname)
|> the_default m
end
(*
* Extract details from the c-parser about the given program.