1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11(* 12 * The top-level "autocorres" command. 13 *) 14structure AutoCorres = 15struct 16 17(* 18 * Option parsing for the autocorres command. 19 * These options are documented in the README.md. 20 *) 21 22(* 23 * Most fields are wrapped in option so that the parser can work out 24 * whether they have been specified already. 25 * 26 * Additionally, everything is a reference as a hack around the fact 27 * that SML doesn't have field-updater syntax. There are other ways to 28 * work around this, but this is a light-weight solution. 29 *) 30type autocorres_options = { 31 (* Do not lift heaps for these functions. *) 32 no_heap_abs : string list option ref, 33 34 (* Insist the the following functions should be lifted, even if our 35 * heuristics claim it won't succeed. *) 36 force_heap_abs : string list option ref, 37 38 (* Skip heap lifting for the whole program. *) 39 skip_heap_abs : bool option ref, 40 41 (* Enable unsigned word abstraction for these functions. *) 42 unsigned_word_abs : string list option ref, 43 44 (* Disable signed word abstraction for these functions. *) 45 no_signed_word_abs : string list option ref, 46 47 (* Skip word abstraction for the whole program. *) 48 skip_word_abs : bool option ref, 49 50 (* Only lift to these monads. *) 51 ts_rules : string list option ref, 52 53 (* Force functions to be lifted to certain monads. 54 The symtab is keyed on function name. *) 55 ts_force : string Symtab.table ref, 56 57 (* Create some funky syntax for heap operations. *) 58 heap_abs_syntax: bool option ref, 59 60 (* Only translate a subset of functions. *) 61 scope: string list option ref, 62 scope_depth: int option ref, 63 64 (* Do the translation in this locale (and use functions in this locale) *) 65 c_locale: string option ref, 66 67 (* Generate SIMPL wrappers that do not assert termination for the SIMPL. 68 * Also generates ac_corres proofs minus the termination flag. 69 * This option is for temporary CRefine compatibility. *) 70 no_c_termination: bool option ref, 71 72 (* Store detailed traces for conversions of the selected functions. *) 73 trace_heap_lift : string list option ref, 74 trace_word_abs : string list option ref, 75 76 (* Disable L1Peephole, L2Peephole and L2Opt rules. *) 77 no_opt : bool option ref, 78 79 (* Trace simplification rules. Note that some simplification is performed even with no_opt set. *) 80 trace_opt : bool option ref, 81 82 (* Define word{8,16,32,64} heaps even if the program does not use them. *) 83 gen_word_heaps : bool option ref, 84 85 keep_going : bool option ref, 86 87 (* Change generated names for lifted_globals fields *) 88 lifted_globals_field_prefix : string option ref, 89 lifted_globals_field_suffix : string option ref, 90 91 (* Change generated function names *) 92 function_name_prefix : string option ref, 93 function_name_suffix : string option ref 94} 95 96(* Get all that the given function depends on, up to "depth" functions deep. *) 97fun get_function_deps get_callees roots depth = 98let 99 fun get_calleess fns = Symset.union_sets (fns :: map get_callees (Symset.dest fns)) 100in 101 funpow depth get_calleess (Symset.make roots) 102end 103 104(* Convert the given reference from "NONE" to "SOME x", emitting an 105 * error if the value is already non-NONE. *) 106fun none_to_some ref_field new_value error_msg opt = 107 case !(ref_field opt) of 108 NONE => ((ref_field opt) := SOME new_value; opt) 109 | SOME _ => error error_msg 110 111(* Parsing expectations. *) 112fun expect x y = !! (K (K ("autocorres: expected " ^ y ^ " after " ^ x))) 113 114(* Generic parser for "NAME = THING" *) 115fun named_option parser name elem_desc= 116 Parse.reserved name |-- 117 expect (quote name) "\"=\"" (Parse.$$$ "=" |-- 118 expect "\"=\"" elem_desc parser) 119 120(* Generic parser for "NAME = STRING ..." *) 121val named_opt = named_option (Scan.repeat Parse.text) 122 123(* Generic parser for "NAME = <nat>" *) 124val nat_opt = named_option Parse.nat 125 126(* Valid options. *) 127val no_heap_abs_parser = 128 named_opt "no_heap_abs" "function names" >> 129 (fn funcs => none_to_some (#no_heap_abs) funcs "autocorres: no_heap_abs option specified multiple times") 130 131val force_heap_abs_parser = 132 named_opt "force_heap_abs" "function names" >> 133 (fn funcs => none_to_some (#force_heap_abs) funcs "autocorres: force_heap_abs option specified multiple times") 134 135val skip_heap_abs_parser = 136 Parse.reserved "skip_heap_abs" >> 137 (fn _ => none_to_some (#skip_heap_abs) true "autocorres: skip_heap_abs option specified multiple times") 138 139val ts_rules_parser = 140 named_opt "ts_rules" "rule names" >> 141 (fn rules => none_to_some (#ts_rules) rules "autocorres: ts_rules option specified multiple times") 142 143val scope_parser = 144 named_opt "scope" "function names" >> 145 (fn funcs => none_to_some (#scope) funcs "autocorres: scope option specified multiple times") 146 147val scope_depth_parser = 148 nat_opt "scope_depth" "integer" >> 149 (fn value => none_to_some (#scope_depth) value "autocorres: scope option specified multiple times") 150 151val c_locale_parser = 152 named_option Parse.text "c_locale" "locale name" >> 153 (fn funcs => none_to_some (#c_locale) funcs 154 "autocorres: c_locale option specified multiple times") 155 156val no_c_termination_parser = 157 Parse.reserved "no_c_termination" >> 158 (fn _ => none_to_some (#no_c_termination) true "autocorres: no_c_termination option specified multiple times") 159 160val ts_force_parser = 161 ((Parse.reserved "ts_force" |-- 162 expect "\"ts_force\"" "rule name" 163 (Parse.text :-- (fn name => expect name "\"=\"" (Parse.$$$ "="))) -- 164 Scan.repeat Parse.text)) >> 165 (fn ((rule, _), funcs) => fn opt => 166 let 167 val _ = 168 (#ts_force opt) := 169 (fold (fn func => (fn table => 170 Symtab.update_new (func, rule) table 171 handle Symtab.DUP _ => 172 error ("autocorres: function " ^ quote func 173 ^ " is already being forced to a particular type.") 174 )) funcs (!(#ts_force opt))) 175 in 176 opt 177 end) 178 179val unsigned_word_abs_parser = 180 named_opt "unsigned_word_abs" "function names" >> 181 (fn funcs => none_to_some (#unsigned_word_abs) funcs "autocorres: unsigned_word_abs option specified multiple times") 182 183val no_signed_word_abs_parser = 184 named_opt "no_signed_word_abs" "function names" >> 185 (fn funcs => none_to_some (#no_signed_word_abs) funcs "autocorres: no_signed_word_abs option specified multiple times") 186 187val skip_word_abs_parser = 188 Parse.reserved "skip_word_abs" >> 189 (fn _ => none_to_some (#skip_word_abs) true "autocorres: skip_word_abs option specified multiple times") 190 191val heap_abs_syntax_parser = 192 Parse.reserved "heap_abs_syntax" >> 193 (fn _ => none_to_some (#heap_abs_syntax) true "autocorres: heap_abs_syntax option specified multiple times") 194 195val trace_heap_lift_parser = 196 named_opt "trace_heap_lift" "function names" >> 197 (fn funcs => none_to_some (#trace_heap_lift) funcs "autocorres: trace_heap_lift option specified multiple times") 198 199val trace_word_abs_parser = 200 named_opt "trace_word_abs" "function names" >> 201 (fn funcs => none_to_some (#trace_word_abs) funcs "autocorres: trace_word_abs option specified multiple times") 202 203val no_opt_parser = 204 Parse.reserved "no_opt" >> 205 (fn _ => none_to_some (#no_opt) true "autocorres: no_opt option specified multiple times") 206 207val trace_opt_parser = 208 Parse.reserved "trace_opt" >> 209 (fn _ => none_to_some (#trace_opt) true "autocorres: trace_opt option specified multiple times") 210 211val gen_word_heaps_parser = 212 Parse.reserved "gen_word_heaps" >> 213 (fn _ => none_to_some (#gen_word_heaps) true "autocorres: gen_word_heaps option specified multiple times") 214 215val keep_going_parser = 216 Parse.reserved "keep_going" >> 217 (fn _ => none_to_some (#keep_going) true "autocorres: keep_going option specified multiple times") 218 219val lifted_globals_field_prefix_parser = 220 named_option Parse.text "lifted_globals_field_prefix" "string" >> 221 (fn funcs => none_to_some (#lifted_globals_field_prefix) funcs 222 "autocorres: lifted_globals_field_prefix option specified multiple times") 223 224val lifted_globals_field_suffix_parser = 225 named_option Parse.text "lifted_globals_field_suffix" "string" >> 226 (fn funcs => none_to_some (#lifted_globals_field_suffix) funcs 227 "autocorres: lifted_globals_field_suffix option specified multiple times") 228 229val function_name_prefix_parser = 230 named_option Parse.text "function_name_prefix" "string" >> 231 (fn funcs => none_to_some (#function_name_prefix) funcs 232 "autocorres: function_name_prefix option specified multiple times") 233 234val function_name_suffix_parser = 235 named_option Parse.text "function_name_suffix" "string" >> 236 (fn funcs => none_to_some (#function_name_suffix) funcs 237 "autocorres: function_name_suffix option specified multiple times") 238 239(* 240 * Blank set of options. 241 * 242 * Because we are using references, we need to construct a new set every 243 * time; hence the dummy parameter. 244 *) 245fun default_opts _ = { 246 no_heap_abs = ref NONE, 247 force_heap_abs = ref NONE, 248 skip_heap_abs = ref NONE, 249 unsigned_word_abs = ref NONE, 250 no_signed_word_abs = ref NONE, 251 skip_word_abs = ref NONE, 252 ts_rules = ref NONE, 253 ts_force = ref Symtab.empty, 254 heap_abs_syntax = ref NONE, 255 scope = ref NONE, 256 scope_depth = ref NONE, 257 c_locale = ref NONE, 258 no_c_termination = ref NONE, 259 trace_heap_lift = ref NONE, 260 trace_word_abs = ref NONE, 261 no_opt = ref NONE, 262 trace_opt = ref NONE, 263 gen_word_heaps = ref NONE, 264 keep_going = ref NONE, 265 lifted_globals_field_prefix = ref NONE, 266 lifted_globals_field_suffix = ref NONE, 267 function_name_prefix = ref NONE, 268 function_name_suffix = ref NONE 269 } : autocorres_options 270 271(* Combined parser. *) 272val autocorres_parser : (autocorres_options * string) parser = 273let 274 val option_parser = 275 (no_heap_abs_parser || 276 force_heap_abs_parser || 277 skip_heap_abs_parser || 278 ts_rules_parser || 279 ts_force_parser || 280 unsigned_word_abs_parser || 281 no_signed_word_abs_parser || 282 skip_word_abs_parser || 283 heap_abs_syntax_parser || 284 scope_parser || 285 scope_depth_parser || 286 c_locale_parser || 287 no_c_termination_parser || 288 trace_heap_lift_parser || 289 trace_word_abs_parser || 290 no_opt_parser || 291 trace_opt_parser || 292 gen_word_heaps_parser || 293 keep_going_parser || 294 lifted_globals_field_prefix_parser || 295 lifted_globals_field_suffix_parser || 296 function_name_prefix_parser || 297 function_name_suffix_parser) 298 |> !! (fn xs => K ("autocorres: unknown option " ^ quote (Parse.text (fst xs) |> #1))) 299 300 val options_parser = Parse.list option_parser >> (fn opt_fns => fold I opt_fns) 301in 302 (* Options *) 303 (Scan.optional (Parse.$$$ "[" |-- options_parser --| Parse.$$$ "]") I 304 >> (fn f => f (default_opts ()))) -- 305 (* Filename *) 306 Parse.text 307end 308 309 310 311(* 312 * Worker for the autocorres command. 313 *) 314fun do_autocorres (opt : autocorres_options) filename thy = 315let 316 (* Ensure that the filename has already been parsed by the C parser. *) 317 val csenv = case CalculateState.get_csenv thy filename of 318 NONE => error ("Filename '" ^ filename ^ "' has not been parsed by the C parser yet.") 319 | SOME x => x 320 321 (* Enter into the correct context. *) 322 val {base = locale_name,...} = OS.Path.splitBaseExt (OS.Path.file filename) 323 val locale_name = case !(#c_locale opt) of NONE => locale_name 324 | SOME l => l 325 val lthy = case try (Named_Target.begin (locale_name, Position.none)) thy of 326 SOME lthy => lthy 327 | NONE => error ("autocorres: no such locale: " ^ locale_name) 328 329 (* Fetch program information from the C-parser output. *) 330 val prog_info = ProgramInfo.get_prog_info lthy filename 331 val all_simpl_info = FunctionInfo.init_function_info lthy filename 332 val all_simpl_functions = Symset.make (Symtab.keys all_simpl_info) 333 334 (* Process autocorres options. *) 335 val keep_going = !(#keep_going opt) = SOME true 336 337 val _ = if not (!(#unsigned_word_abs opt) = NONE) andalso not (!(#skip_word_abs opt) = NONE) then 338 error "autocorres: unsigned_word_abs and skip_word_abs cannot be used together." 339 else if not (!(#no_signed_word_abs opt) = NONE) andalso not (!(#skip_word_abs opt) = NONE) then 340 error "autocorres: no_signed_word_abs and skip_word_abs cannot be used together." 341 else () 342 val skip_word_abs = !(#skip_word_abs opt) = SOME true 343 344 val _ = if not (!(#force_heap_abs opt) = NONE) andalso not (!(#skip_heap_abs opt) = NONE) then 345 error "autocorres: force_heap_abs and skip_heap_abs cannot be used together." 346 else if not (!(#no_heap_abs opt) = NONE) andalso not (!(#skip_heap_abs opt) = NONE) then 347 error "autocorres: no_heap_abs and skip_heap_abs cannot be used together." 348 else () 349 val no_heap_abs = these (!(#no_heap_abs opt)) 350 351 (* Resolve rule names for ts_rules and ts_force. *) 352 val ts_force = Symtab.map (K (fn name => Monad_Types.get_monad_type name (Context.Proof lthy) 353 |> the handle Option => Monad_Types.error_no_such_mt name)) 354 (!(#ts_force opt)) 355 val ts_rules = Monad_Types.get_ordered_rules (these (!(#ts_rules opt))) (Context.Proof lthy) 356 357 (* heap_abs_syntax defaults to off. *) 358 val heap_abs_syntax = !(#heap_abs_syntax opt) = SOME true 359 360 (* Ensure that we are not both forcing and preventing a function from being heap lifted. *) 361 val conflicting_heap_lift_fns = 362 Symset.inter (Symset.make (these (!(#no_heap_abs opt)))) (Symset.make (these (!(#force_heap_abs opt)))) 363 val _ = if not (Symset.is_empty conflicting_heap_lift_fns) then 364 error ("autocorres: Functions are declared as both 'no_heap_abs' and 'force_heap_abs': " 365 ^ commas (Symset.dest conflicting_heap_lift_fns)) 366 else 367 () 368 369 (* (Finished processing options.) *) 370 371 val existing_phases = Symtab.lookup (AutoCorresFunctionInfo.get thy) filename 372 val _ = if not (isSome existing_phases) then () else 373 tracing ("Attempting to restart from previous translation of " ^ filename) 374 375 (* Fetch any existing translations, when being run in incremental mode. *) 376 fun get_existing_optional_phase phase = 377 case existing_phases of 378 NONE => SOME Symtab.empty 379 | SOME phases => FunctionInfo.Phasetab.lookup phases phase 380 fun get_existing_phase phase = 381 Option.getOpt (get_existing_optional_phase phase, Symtab.empty) 382 val [existing_simpl_info, 383 existing_l1_info, 384 existing_l2_info, 385 existing_hl_info, 386 existing_wa_info, 387 existing_ts_info] = 388 map get_existing_phase 389 [FunctionInfo.CP, 390 FunctionInfo.L1, 391 FunctionInfo.L2, 392 FunctionInfo.HL, 393 FunctionInfo.WA, 394 FunctionInfo.TS] 395 (* HL and WA functions may be missing if skip_heap_abs and skip_word_abs 396 * are set. In that case, we carry forward the L2 or HL functions and 397 * cross our fingers. (Should work fine if skip_foo is used consistently 398 * for all functions, might not work if they are mixed.) *) 399 val existing_hl_info = Utils.symtab_merge_with snd (existing_l2_info, existing_hl_info); 400 val existing_wa_info = Utils.symtab_merge_with snd (existing_hl_info, existing_wa_info); 401 402 (* Skip functions that have already been translated. *) 403 val already_translated = Symset.make (Symtab.keys existing_ts_info) 404 405 (* Determine which functions should be translated. 406 * If "scope" is not specified, we translate all functions. 407 * Otherwise, we translate only "scope"d functions and their direct callees 408 * (which are translated using a trivial wrapper so that they can be called). *) 409 val (functions_to_translate, functions_to_wrap) = 410 case !(#scope opt) of 411 NONE => (all_simpl_functions, Symset.empty) 412 | SOME x => 413 let 414 val scope_depth = the_default 2 (!(#scope_depth opt)) 415 val get_deps = get_function_deps (fn f => 416 FunctionInfo.all_callees (the (Symtab.lookup all_simpl_info f))) 417 val funcs = get_deps x scope_depth 418 val _ = tracing ("autocorres scope: selected " ^ Int.toString (Symset.card funcs) ^ " function(s):") 419 val _ = app (fn f => tracing (" " ^ f)) (Symset.dest funcs) 420 val funcs_callees = 421 Symset.subtract (Symset.union already_translated funcs) (get_deps (Symset.dest funcs) 1) 422 val _ = if Symset.is_empty funcs_callees then () else 423 (tracing ("autocorres scope: wrapping " ^ 424 Int.toString (Symset.card funcs_callees) ^ " function(s):"); 425 app (fn f => tracing (" " ^ f)) (Symset.dest funcs_callees)) 426 in (funcs, funcs_callees) end 427 428 (* Functions that have already been translated cannot be translated again. *) 429 val already_translated = Symset.inter already_translated functions_to_translate 430 val _ = if Symset.is_empty already_translated then () else 431 error ("autocorres scope: these functions have already been translated: " ^ 432 commas (Symset.dest already_translated)) 433 434 (* If a function has no SIMPL body, we will not wrap its body; 435 * instead we create a dummy definition and translate it via the usual process. *) 436 val undefined_functions = 437 Symset.filter (fn f => #invented_body (the (Symtab.lookup all_simpl_info f))) functions_to_wrap 438 val functions_to_wrap = Symset.subtract undefined_functions functions_to_wrap 439 val functions_to_translate = Symset.union undefined_functions functions_to_translate 440 441 (* We will process these functions... *) 442 val functions_to_process = Symset.union functions_to_translate functions_to_wrap 443 (* ... and ignore these functions. *) 444 val functions_to_ignore = Symset.subtract functions_to_process all_simpl_functions 445 446 (* Disallow referring to functions that don't exist or are excluded from processing. *) 447 val funcs_in_options = 448 these (!(#no_heap_abs opt)) 449 @ these (!(#force_heap_abs opt)) 450 @ these (!(#unsigned_word_abs opt)) 451 @ these (!(#no_signed_word_abs opt)) 452 @ these (!(#scope opt)) 453 @ Symtab.keys (!(#ts_force opt)) 454 @ these (!(#trace_heap_lift opt)) 455 @ these (!(#trace_word_abs opt)) 456 |> Symset.make 457 val invalid_functions = 458 Symset.subtract all_simpl_functions funcs_in_options 459 val ignored_functions = 460 Symset.subtract (Symset.union invalid_functions functions_to_process) funcs_in_options 461 val _ = 462 if Symset.card invalid_functions > 0 then 463 error ("autocorres: no such function(s): " ^ commas (Symset.dest invalid_functions)) 464 else if Symset.card ignored_functions > 0 then 465 error ("autocorres: cannot configure translation for excluded function(s): " ^ 466 commas (Symset.dest ignored_functions)) 467 else 468 () 469 470 (* Only translate "scope" functions and their direct callees. *) 471 val simpl_info = 472 Symtab.dest all_simpl_info 473 |> List.mapPartial (fn (name, info) => 474 if Symset.contains functions_to_translate name then 475 SOME (name, FunctionInfo.function_info_upd_is_simpl_wrapper false info) 476 else if Symset.contains functions_to_wrap name then 477 SOME (name, FunctionInfo.function_info_upd_is_simpl_wrapper true info) 478 else 479 NONE) 480 |> Symtab.make 481 482 (* Recalculate callees after "scope" restriction. *) 483 val (simpl_call_graph, simpl_info) = FunctionInfo.calc_call_graph simpl_info 484 485 (* Check that recursive function groups are all lifted to the same monad. *) 486 val _ = #topo_sorted_functions simpl_call_graph 487 |> map (TypeStrengthen.compute_lift_rules ts_rules ts_force o Symset.dest) 488 489 (* Disable heap lifting for all un-translated functions. *) 490 val force_heap_abs = Symset.make (these (!(#force_heap_abs opt))) 491 val conflicting_heap_lift_fns = Symset.subtract functions_to_translate force_heap_abs 492 val _ = if not (Symset.is_empty conflicting_heap_lift_fns) then 493 error ("autocorres: Functions marked 'force_heap_abs' but excluded from 'scope': " 494 ^ commas (Symset.dest conflicting_heap_lift_fns)) 495 else 496 () 497 val no_heap_abs = Symset.union (Symset.make no_heap_abs) functions_to_wrap 498 499 (* Disable word abstraction for all un-translated functions. *) 500 val unsigned_word_abs = these (!(#unsigned_word_abs opt)) |> Symset.make 501 val no_signed_word_abs = these (!(#no_signed_word_abs opt)) |> Symset.make 502 val conflicting_unsigned_abs_fns = 503 Symset.subtract functions_to_translate unsigned_word_abs 504 val _ = if Symset.is_empty conflicting_unsigned_abs_fns then () else 505 error ("autocorres: Functions marked 'unsigned_word_abs' but excluded from 'scope': " 506 ^ commas (Symset.dest conflicting_unsigned_abs_fns)) 507 val no_signed_word_abs = Symset.union no_signed_word_abs functions_to_wrap 508 509 (* 510 * Sanity check the C parser's output. 511 * 512 * In the past, the C parser has defined terms that haven't type-checked due 513 * to sort constraints on constants. This doesn't violate the Isabelle 514 * kernel's soundness, but does wreck havoc on us. 515 *) 516 val sanity_errors = 517 Symtab.dest simpl_info 518 |> List.mapPartial (fn (fn_name, info) => 519 case Symtab.lookup existing_l1_info fn_name of 520 SOME _ => NONE (* already translated; ignore *) 521 | _ => let 522 val def = 523 info 524 |> #definition 525 |> Thm.prop_of 526 |> Utils.rhs_of 527 in 528 (Syntax.check_term lthy def; NONE) 529 handle (ERROR str) => SOME (fn_name, str) 530 end) 531 val _ = 532 if length sanity_errors > 0 then 533 error ("C parser failed sanity checks. Erroneous functions: " 534 ^ commas (map fst sanity_errors)) 535 else 536 () 537 538 val do_opt = !(#no_opt opt) <> SOME true 539 val trace_opt = !(#trace_opt opt) = SOME true 540 val gen_word_heaps = !(#gen_word_heaps opt) = SOME true 541 542 (* Any function that was declared in the C file (but never defined) should 543 * stay in the nondet-monad unless explicitly instructed by the user to be 544 * something else. *) 545 val ts_force = let 546 val invented_functions = 547 functions_to_process 548 (* Select functions with an invented body. *) 549 |> Symset.filter (Symtab.lookup simpl_info #> the #> #invented_body) 550 (* Ignore functions which already have a "ts_force" rule applied to them. *) 551 |> Symset.subtract (Symset.make (Symtab.keys ts_force)) 552 |> Symset.dest 553 in 554 (* Use the most general monadic type allowed by the user. *) 555 fold (fn n => Symtab.update_new (n, List.last ts_rules)) invented_functions ts_force 556 end 557 558 (* Prefixes/suffixes for generated names. *) 559 val make_lifted_globals_field_name = let 560 val prefix = case !(#lifted_globals_field_prefix opt) of 561 NONE => "" 562 | SOME p => p 563 val suffix = case !(#lifted_globals_field_suffix opt) of 564 NONE => "_''" 565 | SOME s => s 566 in fn f => prefix ^ f ^ suffix end 567 568 (* Prefixes/suffixes for generated names. *) 569 val make_function_name = let 570 val prefix = case !(#function_name_prefix opt) of 571 NONE => "" 572 | SOME p => p 573 val suffix = case !(#function_name_suffix opt) of 574 NONE => "'" 575 | SOME s => s 576 in fn f => prefix ^ f ^ suffix end 577 578 (* Initialise database for traces. 579 * Currently, this is implemented by mutating a global table. 580 * While slightly ugly, it does simplify adding more tracing to AutoCorres 581 * without cluttering the return types of existing code. *) 582 val trace_db: AutoCorresData.Trace Symtab.table (* type *) Symtab.table (* func *) Synchronized.var = 583 Synchronized.var "AutoCorres traces" Symtab.empty 584 fun add_trace f_name trace_name trace = 585 Synchronized.change trace_db 586 (Symtab.map_default (f_name, Symtab.empty) (Symtab.update_new (trace_name, trace))) 587 588 (* Do the translation. *) 589 val l1_results = 590 SimplConv.translate 591 filename prog_info simpl_info existing_simpl_info existing_l1_info 592 (!(#no_c_termination opt) <> SOME true) 593 do_opt trace_opt add_trace (prefix "l1_" o make_function_name) lthy 594 595 val l2_results = 596 LocalVarExtract.translate 597 filename prog_info l1_results existing_l1_info existing_l2_info 598 do_opt trace_opt add_trace (prefix "l2_" o make_function_name) 599 600 val skip_heap_abs = !(#skip_heap_abs opt) = SOME true 601 val hl_results = 602 if skip_heap_abs 603 then l2_results 604 else let 605 val (l2_results', HL_setup) = 606 HeapLift.prepare_heap_lift 607 filename prog_info l2_results lthy all_simpl_info 608 make_lifted_globals_field_name gen_word_heaps heap_abs_syntax; 609 in HeapLift.translate 610 filename prog_info l2_results' existing_l2_info existing_hl_info 611 HL_setup no_heap_abs force_heap_abs 612 heap_abs_syntax keep_going 613 (these (!(#trace_heap_lift opt))) do_opt trace_opt add_trace 614 (prefix "hl_" o make_function_name) 615 end 616 617 val wa_results = 618 if skip_word_abs 619 then hl_results 620 else WordAbstract.translate 621 filename prog_info hl_results existing_hl_info existing_wa_info 622 unsigned_word_abs no_signed_word_abs 623 (these (!(#trace_word_abs opt))) do_opt trace_opt add_trace 624 (prefix "wa_" o make_function_name) 625 626 val ts_results = 627 TypeStrengthen.translate 628 ts_rules ts_force filename prog_info 629 wa_results existing_wa_info existing_ts_info 630 make_function_name keep_going do_opt add_trace 631 632 (* Collect final translation results. *) 633 val l1_info = FSeq.list_of l1_results |> map snd |> Utils.symtab_merge false; 634 val l2_info = FSeq.list_of l2_results |> map snd |> Utils.symtab_merge false; 635 val hl_info = if skip_heap_abs then Symtab.empty else 636 FSeq.list_of hl_results |> map snd |> Utils.symtab_merge false; 637 val wa_info = if skip_word_abs then Symtab.empty else 638 FSeq.list_of wa_results |> map snd |> Utils.symtab_merge false; 639 val ts_results' = FSeq.list_of ts_results; 640 val ts_info = ts_results' |> map snd |> Utils.symtab_merge false; 641 642 val lthy = if null ts_results' then lthy else fst (List.last ts_results'); 643 644 (* Put together final ac_corres theorems. 645 * TODO: we should also store these as theory data. *) 646 fun prove_ac_corres fn_name = 647 let 648 val l1_thm = #corres_thm (the (Symtab.lookup l1_info fn_name)) 649 handle Option => raise SimplConv.FunctionNotFound fn_name 650 val l2_thm = #corres_thm (the (Symtab.lookup l2_info fn_name)) 651 handle Option => raise SimplConv.FunctionNotFound fn_name 652 val hl_thm = #corres_thm (the (Symtab.lookup hl_info fn_name)) 653 (* If heap lifting was disabled, we use a placeholder *) 654 handle Option => @{thm L2Tcorres_trivial_from_local_var_extract} OF [l2_thm] 655 val wa_thm = #corres_thm (the (Symtab.lookup wa_info fn_name)) 656 (* Placeholder for when word abstraction is disabled *) 657 handle Option => @{thm corresTA_trivial_from_heap_lift} OF [hl_thm] 658 val ts_thm = #corres_thm (the (Symtab.lookup ts_info fn_name)) 659 handle Option => raise SimplConv.FunctionNotFound fn_name 660 661 in let 662 val final_thm = @{thm ac_corres_chain} OF [l1_thm, l2_thm, hl_thm, wa_thm, ts_thm] 663 (* Remove fluff, like "f o id", that gets introduced by the HL and WA placeholders *) 664 val final_thm' = Simplifier.simplify (put_simpset AUTOCORRES_SIMPSET lthy) final_thm 665 in SOME final_thm' end 666 handle THM _ => 667 (Utils.THM_non_critical keep_going 668 ("autocorres: failed to prove ac_corres theorem for " ^ fn_name) 669 0 [l1_thm, l2_thm, hl_thm, wa_thm, ts_thm]; 670 NONE) 671 end 672 673 val ac_corres_thms = 674 Symtab.keys ts_info 675 |> Par_List.map (fn f => Option.map (pair f) (prove_ac_corres f)) 676 |> List.mapPartial I 677 678 val lthy = fold (fn (f, thm) => 679 Utils.define_lemma (make_function_name f ^ "_ac_corres") thm #> snd) 680 ac_corres_thms lthy 681 682 (* Name final mono theorems and add them to the simpset. *) 683 val lthy = 684 fold (fn (f, info) => fn lthy => 685 case #mono_thm info of 686 NONE => lthy 687 | SOME mono_thm => 688 Utils.define_lemma (make_function_name f ^ "_mono") mono_thm lthy |> snd 689 |> Utils.simp_add [mono_thm]) 690 (Symtab.dest ts_info) lthy 691 692 (* Save function info for future reference. *) 693 val simpl_info' = Symtab.merge (K false) (existing_simpl_info, simpl_info); 694 val l1_info' = Symtab.merge (K false) (existing_l1_info, l1_info); 695 val l2_info' = Symtab.merge (K false) (existing_l2_info, l2_info); 696 val hl_info' = Symtab.merge (K false) (existing_hl_info, hl_info); 697 val wa_info' = Symtab.merge (K false) (existing_wa_info, wa_info); 698 val ts_info' = Symtab.merge (K false) (existing_ts_info, ts_info); 699 val new_results = 700 FunctionInfo.Phasetab.make 701 ([(FunctionInfo.CP, simpl_info'), 702 (FunctionInfo.L1, l1_info'), 703 (FunctionInfo.L2, l2_info'), 704 (FunctionInfo.TS, ts_info')] 705 @ (if skip_heap_abs andalso Symtab.is_empty existing_hl_info 706 then [] else [(FunctionInfo.HL, hl_info')]) 707 @ (if skip_word_abs andalso Symtab.is_empty existing_wa_info 708 then [] else [(FunctionInfo.WA, wa_info')]) 709 ) 710 711 val _ = tracing "Saving function info to AutoCorresFunctionInfo." 712 val lthy = Local_Theory.background_theory ( 713 AutoCorresFunctionInfo.map (fn tbl => 714 Symtab.update (filename, new_results) tbl)) lthy 715 (* All traces should be available at this point. Archive them. *) 716 717 val traces = Synchronized.value trace_db; 718 val _ = if Symtab.is_empty traces then () else 719 tracing "Saving translation traces to AutoCorresData.Traces." 720 val lthy = lthy |> Local_Theory.background_theory ( 721 AutoCorresData.Traces.map 722 (Symtab.map_default (filename, Symtab.empty) 723 (fn old_traces => Utils.symtab_merge_with snd (old_traces, traces)))); 724 725in 726 (* Exit context. *) 727 Named_Target.exit lthy 728end 729 730end