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 11signature ISAR_INSTALL = 12sig 13 14 type additional_options 15 val GhostState : string -> additional_options 16 val get_Csyntax : theory -> string -> Absyn.ext_decl list 17 val gen_umm_types_file : string -> string -> theory -> theory 18 val do_cpp : {error_detail : int, cpp_path : string option} -> 19 {includes : string list, filename : string} -> string 20 val install_C_file : (((bool option * bool option) * bool option) * string) * 21 additional_options list option -> 22 theory -> theory 23 val interactive_install : string -> theory -> theory 24 val mk_thy_relative : theory -> string -> string 25 26 val extra_trace_filename : string Config.T 27 28 val installed_C_files : theory 29 -> {c_filename : string, locale_names : string list, 30 options: (bool * bool * bool), 31 additional_options: additional_options list} list 32end 33 34structure IsarInstall : ISAR_INSTALL = 35struct 36 37type 'a wrap = 'a Region.Wrap.t 38val bogus = SourcePos.bogus 39 40fun setup_feedback extra_output_filename = let 41 val trace_extra = case extra_output_filename of 42 NONE => K () 43 | SOME f => let 44 val out = TextIO.openOut f 45 in fn s => (TextIO.output (out, s); TextIO.flushOut out) end 46 val add_extra = case extra_output_filename of 47 NONE => (fn pfx => fn f => f) 48 | SOME _ => (fn pfx => fn f => fn s => (trace_extra (pfx ^ s); f s)) 49 in 50 Feedback.errorf := add_extra "ERROR: " (ignore o error); 51 Feedback.warnf := add_extra "" warning; 52 Feedback.informf := add_extra "" (Output.tracing o Feedback.timestamp) 53 end 54 55val extra_trace_filename = let 56 val (config, setup) = 57 Attrib.config_string @{binding "CParser_extra_trace_file"} (K "") 58in 59 Context.>>(Context.map_theory setup); 60 config 61end 62 63fun setup_feedback_thy thy = let 64 val str = Config.get_global thy extra_trace_filename 65 in setup_feedback (if str = "" then NONE else SOME str) end 66 67val _ = setup_feedback NONE 68 69structure C_Includes = Theory_Data 70(struct 71 type T = string list 72 val empty = [] 73 val extend = I 74 val merge = Library.merge (op =) 75end); 76 77datatype additional_options = MachineState of string | GhostState of string | CRoots of string list 78 79type install_data = {c_filename : string, locale_names : string list, 80 options: (bool * bool * bool), 81 additional_options: additional_options list} 82structure C_Installs = Theory_Data 83(struct 84 type T = install_data list 85 val empty = [] 86 val extend = I 87 val merge = Library.merge (op =) 88end); 89val installed_C_files = C_Installs.get 90 91structure IsaPath = Path 92 93val get_Cdir = Resources.master_directory 94 95fun mk_thy_relative thy s = 96 if OS.Path.isRelative s then OS.Path.concat(Path.implode (get_Cdir thy), s) 97 else s 98 99val cpp_path = let 100 val (cpp_path_config, cpp_path_setup) = 101 Attrib.config_string (Binding.name "cpp_path") (K "/usr/bin/cpp") 102in 103 Context.>>(Context.map_theory cpp_path_setup); 104 cpp_path_config 105end 106 107val munge_info_fname = let 108 val (mifname_config, mifname_setup) = 109 Attrib.config_string (Binding.name "munge_info_fname") (K "") 110in 111 Context.>>(Context.map_theory mifname_setup); 112 mifname_config 113end 114 115val report_cpp_errors = let 116 val (report_cpp_errors_config, report_cpp_errors_setup) = 117 Attrib.config_int (Binding.name "report_cpp_errors") (K 10) 118in 119 Context.>>(Context.map_theory report_cpp_errors_setup); 120 report_cpp_errors_config 121end 122 123fun do_cpp {error_detail, cpp_path} {includes, filename} = 124 case cpp_path of 125 NONE => filename 126 | SOME p => 127 let 128 open OS.FileSys OS.Process 129 val tmpname = tmpName() 130 val err_tmpname = tmpName() 131 val includes_string = String.concat (map (fn s => "-I\""^s^"\" ") includes) 132 fun plural 1 = "" | plural _ = "s" 133 val cmdline = 134 p ^ " " ^ includes_string ^ " -CC \"" ^ filename ^ "\" > " ^ tmpname ^ " 2> " ^ err_tmpname 135 in 136 if isSuccess (system cmdline) then (OS.FileSys.remove err_tmpname; tmpname) 137 else let val _ = OS.FileSys.remove tmpname 138 val (msg, rest) = File.read_lines (Path.explode err_tmpname) |> chop error_detail 139 val _ = OS.FileSys.remove err_tmpname 140 val _ = warning ("cpp failed on " ^ filename ^ "\nCommand: " ^ cmdline ^ 141 "\n\nOutput:\n" ^ 142 cat_lines (msg @ (if null rest then [] else 143 ["(... " ^ string_of_int (length rest) ^ 144 " more line" ^ plural (length rest) ^ ")"]))) 145 in raise Feedback.WantToExit ("cpp failed on " ^ filename) end 146 end 147 148fun get_Csyntax thy s = let 149 val _ = setup_feedback_thy thy 150 val cpp_option = 151 case Config.get_global thy cpp_path of 152 "" => NONE 153 | s => SOME s 154 val cpp_error_count = Config.get_global thy report_cpp_errors 155 val (ast0, _) = 156 StrictCParser.parse 157 (do_cpp {error_detail = cpp_error_count, cpp_path = cpp_option}) 158 15 159 (C_Includes.get thy) 160 (mk_thy_relative thy s) 161 handle IO.Io {name, ...} => error ("I/O error on "^name) 162in 163 ast0 |> SyntaxTransforms.remove_anonstructs |> SyntaxTransforms.remove_typedefs 164end 165 166fun define_naming_scheme [] _ = I 167 | define_naming_scheme fninfo nmdefs = let 168 fun name_term fni = SOME (HOLogic.mk_string (#fname fni)) 169 fun name_name fni = #fname fni ^ "_name" 170 171 in StaticFun.define_tree_and_thms_with_defs 172 (Binding.name NameGeneration.naming_scheme_name) 173 (map name_name fninfo) nmdefs 174 (map name_term fninfo) @{term "id :: int => int"} 175 #> snd end 176 177fun define_function_names fninfo thy = let 178 open Feedback 179 fun decl1 (fni, (n, defs, lthy)) = let 180 open TermsTypes 181 val cname = suffix HoarePackage.proc_deco (#fname fni) 182 val _ = informStr (4, "Adding ("^cname^" :: int) = "^Int.toString n) 183 val b = Binding.name cname 184 val ((_, (_, th)), lthy) = 185 Local_Theory.define ((b, NoSyn), 186 ((Thm.def_binding b, []), mk_int_numeral n)) 187 lthy 188 val lthy' = Local_Theory.reset lthy 189 val morph = Proof_Context.export_morphism lthy lthy' 190 val th' = Morphism.thm morph th 191 192 in 193 (n + 1, th' :: defs, lthy') 194 end 195 val (_, defs, lthy) = 196 List.foldl decl1 (1, [], Named_Target.theory_init thy) fninfo 197 val lthy' = define_naming_scheme fninfo (List.rev defs) lthy 198in 199 (defs, Local_Theory.exit_global lthy') 200end 201 202 203fun print_addressed_vars cse = let 204 open ProgramAnalysis Feedback 205 val globs = get_globals cse 206 val _ = informStr (0, "There are "^Int.toString (length globs)^" globals: "^ 207 commas_quote (map srcname globs)) 208 val addressed = get_addressed cse 209 val addr_vars = map MString.dest (MSymTab.keys addressed) 210 val _ = informStr (0, "There are "^Int.toString (length addr_vars)^ 211 " addressed variables: "^ commas_quote addr_vars) 212in 213 () 214end 215 216fun define_global_initializers globloc msgpfx name_munger mungedb cse globs thy = let 217 open ProgramAnalysis Absyn 218 val lthy = Named_Target.init globloc thy 219 val globinits = let 220 val inittab = get_globinits cse 221 fun foldthis (gnm : MString.t, gty) defs = let 222 val rhs_opt = MSymTab.lookup inittab gnm 223 val rhs_t = 224 case rhs_opt of 225 NONE => ExpressionTranslation.zero_term thy (get_senv cse) gty 226 | SOME rhs => let 227 open ExpressionTranslation 228 fun error _ = (Feedback.errorStr'(eleft rhs, eright rhs, 229 "Illegal form in initialisor for\ 230 \ global"); 231 raise Fail "Bad global initialisation") 232 val fakeTB = TermsTypes.TB {var_updator = error, var_accessor = error, 233 rcd_updator = error, rcd_accessor = error} 234 fun varinfo s = stmt_translation.state_varlookup "" s mungedb 235 val ei = expr_term lthy cse fakeTB varinfo rhs 236 val ei = case gty of 237 Array _ => ei 238 | _ => typecast(thy,gty,ei) 239 in 240 rval_of ei (Free("x", TermsTypes.bool)) 241 (* the Free("x",bool) is arbitrary as the constant 242 expression should be ignoring the state argument *) 243 end 244 in 245 (gnm, gty, rhs_t) :: defs 246 end 247 in 248 MSymTab.fold foldthis globs [] 249 end 250 fun define1 ((nm, ty, value), lthy) = let 251 open Feedback 252 val _ = informStr(2, 253 msgpfx ^ MString.dest nm ^ " (of C type "^ 254 Absyn.tyname ty ^") to have value "^ 255 Syntax.string_of_term lthy value) 256 val b = Binding.name (MString.dest (name_munger nm)) 257 val (_, lthy) = 258 Local_Theory.define 259 ((b, NoSyn), ((Thm.def_binding b, []), value)) 260 lthy 261 in 262 lthy 263 end 264in 265 List.foldl define1 lthy globinits 266 |> Local_Theory.exit_global 267end 268 269val use_anon_vars = let 270 val (uavconfig, uavsetup) = Attrib.config_bool (Binding.name "use_anonymous_local_variables") (K false) 271in 272 Context.>>(Context.map_theory uavsetup); 273 uavconfig 274end 275 276val allow_underscore_idents = let 277 val (auiconfig, auisetup) = Attrib.config_bool (Binding.name "allow_underscore_idents") (K false) 278in 279 Context.>>(Context.map_theory auisetup); 280 auiconfig 281end 282 283fun get_callees cse slist = let 284 val {callgraph = cg,...} = ProgramAnalysis.compute_callgraphs cse 285 fun recurse acc worklist = 286 case worklist of 287 [] => acc 288 | fnname :: rest => 289 if Binaryset.member(acc, fnname) then recurse acc rest 290 else 291 case Symtab.lookup cg fnname of 292 NONE => recurse (Binaryset.add(acc, fnname)) rest 293 | SOME set => recurse (Binaryset.add(acc, fnname)) 294 (Binaryset.listItems set @ rest) 295in 296 recurse (Binaryset.empty String.compare) slist 297end 298 299fun install_C_file0 (((((memsafe),ctyps),cdefs),s),statetylist_opt) thy = let 300 val _ = setup_feedback_thy thy 301 val {base = localename,...} = OS.Path.splitBaseExt (OS.Path.file s) 302 val _ = not (Long_Name.is_qualified localename) orelse 303 raise Fail ("Base of filename looks like qualified Isabelle ID: "^ 304 localename) 305 val _ = localename <> "" orelse 306 raise Fail ("Filename (>'" ^ s ^ 307 "'<) gives \"\" as locale name, which is illegal") 308 val statetylist = case statetylist_opt of NONE => [] | SOME l => List.rev l 309 val mstate_ty = 310 case get_first (fn (MachineState s) => SOME s | _ => NONE) statetylist of 311 NONE => TermsTypes.nat 312 | SOME s => Syntax.read_typ_global thy s 313 val roots_opt = 314 get_first (fn CRoots slist => SOME slist | _ => NONE) statetylist 315 val gstate_ty = 316 case get_first (fn (GhostState s) => SOME s | _ => NONE) statetylist of 317 NONE => TermsTypes.unit 318 | SOME s => Syntax.read_typ_global thy s 319 val thy = Config.put_global CalculateState.current_C_filename s thy 320 val thy = CalculateState.store_ghostty (s, gstate_ty) thy 321 val anon_vars = Config.get_global thy use_anon_vars 322 val uscore_idents = Config.get_global thy allow_underscore_idents 323 324 val o2b = isSome 325 val install_typs = not (o2b cdefs) orelse (o2b ctyps) 326 val install_defs = not (o2b ctyps) orelse (o2b cdefs) 327 val ms = o2b memsafe 328 val ast = get_Csyntax thy s 329 open ProgramAnalysis CalculateState Feedback 330 val owners = 331 (* non-null if there are any globals that have owned_by annotations *) 332 let 333 open StmtDecl RegionExtras 334 fun getowner d = 335 case d of 336 Decl d => 337 (case node d of 338 VarDecl (_, _, _, _, attrs) => get_owned_by attrs 339 | _ => NONE) 340 | _ => NONE 341 in 342 List.mapPartial getowner ast 343 end 344 val mifname = case Config.get_global thy munge_info_fname of 345 "" => NONE 346 | s => SOME s 347 348 val ((ast, _ (* init_stmts *)), cse) = 349 process_decls {anon_vars=anon_vars,owners = owners, 350 allow_underscore_idents = uscore_idents, 351 munge_info_fname = mifname} 352 ast 353 val () = export_mungedb cse 354 val thy = store_csenv (s, cse) thy 355 356 val _ = print_addressed_vars cse 357 val ecenv = cse2ecenv cse 358 val thy = define_enum_consts ecenv thy 359 val state = create_state cse 360 val (thy, rcdinfo) = mk_thy_types cse install_typs thy 361 val ast = SyntaxTransforms.remove_embedded_fncalls cse ast 362in 363 if install_defs then let 364 val (thy, vdecls, globs) = 365 mk_thy_decls 366 state {owners=owners,gstate_ty=gstate_ty,mstate_ty=mstate_ty} thy 367 val loc_b = Binding.name (suffix HPInter.globalsN localename) 368 val (globloc, ctxt) = 369 Expression.add_locale loc_b loc_b ([], []) globs thy 370 val thy = Local_Theory.exit_global ctxt 371 val _ = Output.state ("Created locale for globals (" ^ Binding.print loc_b ^ 372 ")- with " ^ Int.toString (length globs) ^ 373 " globals elements") 374 val _ = app (fn e => Output.state ("-- " ^ HPInter.asm_to_string (Syntax.string_of_term ctxt) e)) 375 globs 376 val mungedb = mk_mungedb vdecls 377 val thy = CalculateState.store_mungedb (s, mungedb) thy 378 val thy = 379 define_global_initializers globloc "Defining untouched global constant " 380 NameGeneration.untouched_global_name 381 mungedb 382 cse 383 (calc_untouched_globals cse) 384 thy 385 val thy = 386 if Config.get_global thy CalculateState.record_globinits then let 387 val globs0 = get_globals cse 388 val globs_types = map (fn vi => (get_mname vi, get_vi_type vi)) globs0 389 val glob_table = MSymTab.make globs_types 390 in 391 define_global_initializers 392 globloc "Defining initializers for all globals " 393 NameGeneration.global_initializer_name 394 mungedb 395 cse 396 glob_table 397 thy 398 end 399 else (Feedback.informStr (0, 400 "Ignoring initialisations of modified globals (if any)"); 401 thy) 402 open TermsTypes 403 val (globty, styargs) = let 404 val globty0 = Type(Sign.intern_type thy 405 NameGeneration.global_rcd_name, []) 406 val globty = expand_tyabbrevs (thy2ctxt thy) globty0 407 val statetype0 = 408 Type(Sign.intern_type thy NameGeneration.local_rcd_name, [globty]) 409 val statetype = expand_tyabbrevs (thy2ctxt thy) statetype0 410 (* only happens if no local variables, = no functions declared, 411 = pretty bogus 412 (decl_only and bigstruct test cases are like this though) *) 413 handle TYPE _ => alpha 414 in 415 (globty, [statetype, int, StrictC_errortype_ty]) 416 end 417 val toTranslate = Option.map (get_callees cse) roots_opt 418 val toTranslate_s = 419 case toTranslate of 420 NONE => "all functions" 421 | SOME set => "functions " ^ 422 String.concatWith ", " (Binaryset.listItems set) ^ 423 " (derived from "^ 424 String.concatWith ", " (valOf roots_opt) ^ ")" 425 val _ = 426 Feedback.informStr (0, "Beginning function translation for " ^ 427 toTranslate_s) 428 val toTranslateP = 429 case toTranslate of 430 NONE => (fn _ => true) 431 | SOME set => (fn s => Binaryset.member(set,s)) 432 val fninfo : HPInter.fninfo list = HPInter.mk_fninfo thy cse toTranslateP ast 433 val (nmdefs, thy) = define_function_names fninfo thy 434 val compile_bodies = 435 stmt_translation.define_functions (globty, styargs) 436 mungedb 437 cse 438 fninfo 439 rcdinfo 440 ms 441 val (loc2, thy) = 442 HPInter.make_function_definitions localename 443 cse 444 styargs 445 (List.rev nmdefs) 446 fninfo 447 compile_bodies 448 globloc 449 globs 450 thy 451 val thy = 452 if not (Symtab.is_empty (get_defined_functions cse)) then 453 Modifies_Proofs.prove_all_modifies_goals thy cse toTranslateP styargs loc2 454 else thy (* like this is ever going to happen *) 455 in 456 C_Installs.map (fn ss => 457 {c_filename = s, locale_names = [globloc, loc2], 458 options = (ms, install_typs, install_defs), 459 additional_options = statetylist} :: ss) thy 460 end 461 else 462 C_Installs.map (fn ss => 463 {c_filename = s, locale_names = [], 464 options = (ms, install_typs, install_defs), 465 additional_options = statetylist} :: ss) thy 466end handle e as TYPE (s,tys,tms) => 467 (Feedback.informStr (0, s ^ "\n" ^ 468 Int.toString (length tms) ^ " term(s): " ^ 469 String.concatWith 470 ", " 471 (map (Syntax.string_of_term @{context}) tms) ^ "\n" ^ 472 Int.toString (length tys) ^ " type(s): "^ 473 String.concatWith 474 ", " 475 (map (Syntax.string_of_typ @{context}) tys)); 476 raise e) 477 478fun install_C_file args thy = 479 thy |> install_C_file0 args 480 |> Config.put_global CalculateState.current_C_filename "" 481 482(* for interactive debugging/testing *) 483fun interactive_install s thy = 484 install_C_file ((((NONE, NONE), NONE), s), NONE) thy 485 handle TYPE (s,tys,tms) => 486 (Feedback.informStr (0, s ^ "\n" ^ 487 Int.toString (length tms) ^ " term(s): " ^ 488 String.concatWith 489 ", " 490 (map (Syntax.string_of_term @{context}) tms) ^ "\n" ^ 491 Int.toString (length tys) ^ " type(s): "^ 492 String.concatWith 493 ", " 494 (map (Syntax.string_of_typ @{context}) tys)); 495 thy); 496 497 498fun install_C_types s thy = let 499 open CalculateState ProgramAnalysis 500 val ast = get_Csyntax thy s 501 val (_, cse) = 502 process_decls { 503 anon_vars = Config.get_global thy use_anon_vars, 504 allow_underscore_idents = Config.get_global thy allow_underscore_idents, 505 munge_info_fname = NONE, 506 owners = []} ast 507 val (thy, _) = mk_thy_types cse true thy 508in 509 thy 510end 511 512fun gen_umm_types_file inputfile outputfile thy = let 513 open ProgramAnalysis 514 val ast = get_Csyntax thy inputfile 515 val (_, cse) = 516 process_decls { 517 anon_vars = Config.get_global thy use_anon_vars, 518 allow_underscore_idents = Config.get_global thy allow_underscore_idents, 519 munge_info_fname = NONE, 520 owners = []} ast 521 val _ = CalculateState.gen_umm_types_file cse outputfile 522in 523 thy 524end 525 526val memsafeN = "memsafe" 527val typesN = "c_types" 528val defsN = "c_defs" 529val mtypN = "machinety" 530val ghosttypN = "ghostty" 531val rootsN = "roots" 532 533local 534 structure P = Parse 535 structure K = Keyword 536in 537fun new_include s thy = C_Includes.map (fn sl => mk_thy_relative thy s::sl) thy 538 539val _ = Outer_Syntax.command @{command_keyword "new_C_include_dir"} 540 "add a directory to the include path" 541 (P.text >> (Toplevel.theory o new_include)) 542 543val file_inclusion = let 544 val typoptions = 545 P.reserved mtypN |-- (P.$$$ "=" |-- P.text >> MachineState) || 546 P.reserved ghosttypN |-- (P.$$$ "=" |-- P.text >> GhostState) || 547 P.reserved rootsN |-- (P.$$$ "=" |-- (P.$$$ "[" |-- P.enum1 "," P.text --| P.$$$ "]") >> CRoots) 548in 549 ((Scan.option (P.$$$ memsafeN)) -- 550 (Scan.option (P.$$$ typesN)) -- 551 (Scan.option (P.$$$ defsN)) -- P.text -- 552 (Scan.option 553 (P.$$$ "[" |-- P.enum1 "," typoptions --| P.$$$ "]"))) >> 554 (Toplevel.theory o install_C_file) 555end 556 557val _ = 558 Outer_Syntax.command 559 @{command_keyword "install_C_file"} 560 "import a C file" 561 file_inclusion 562 563val _ = 564 Outer_Syntax.command 565 @{command_keyword "install_C_types"} 566 "install types from a C file" 567 (P.text >> (Toplevel.theory o install_C_types)) 568 569end 570 571end; (* struct *) 572