1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory SimplExport 8 9imports GraphLang CommonOpsLemmas GlobalsSwap ExtraSpecs 10 11begin 12 13lemma field_lvalue_offset_eq: 14 "field_lookup (typ_info_t TYPE('a :: c_type)) f 0 = Some v 15 \<Longrightarrow> field_lvalue (ptr :: 'a ptr) f = ptr_val ptr + of_nat (snd v)" 16 apply (cases v, simp, drule field_lookup_offset_eq) 17 apply (simp add: field_lvalue_def) 18 done 19 20ML \<open> 21fun dest_binT (Type (@{type_name signed}, [t])) = Word_Lib.dest_binT t 22 | dest_binT t = Word_Lib.dest_binT t 23 24fun dest_array_type (Type (@{type_name array}, [T, n])) = let 25 val (s, _) = dest_Type n 26 val s = Long_Name.base_name s 27 in if String.isPrefix "tyCopy" s 28 then (T, fst (read_int (raw_explode (unprefix "tyCopy" s)))) 29 else (T, dest_binT n) 30 end 31 | dest_array_type typ = raise TYPE ("dest_array_type", [typ], []) 32 33fun dest_array_init (Const (@{const_name fupdate}, _) $ n $ f $ arr) = let 34 val xs = dest_array_init arr 35 val n = HOLogic.dest_number n |> snd 36 in nth_map n (curry betapply f) xs end 37 | dest_array_init (Const (@{const_name FCP}, T) $ f) = let 38 val (_, width) = dest_array_type (range_type T) 39 in map (curry betapply f) (map (HOLogic.mk_number @{typ nat}) 40 (0 upto width - 1)) 41 end 42 | dest_array_init t = raise TERM ("dest_array_init", [t]) 43 44val ops = Symtab.make [ 45 (@{const_name "plus"}, ("Plus", true)), 46 (@{const_name "minus"}, ("Minus", true)), 47 (@{const_name "times"}, ("Times", true)), 48 (@{const_name "modulo_class.modulo"}, ("Modulus", true)), 49 (@{const_name "divide_class.divide"}, ("DividedBy", true)), 50 (@{const_name "bitAND"}, ("BWAnd", true)), 51 (@{const_name "bitOR"}, ("BWOr", true)), 52 (@{const_name "bitXOR"}, ("BWXOR", true)), 53 (@{const_name "conj"}, ("And", true)), 54 (@{const_name "disj"}, ("Or", true)), 55 (@{const_name "implies"}, ("Implies", true)), 56 (@{const_name "HOL.eq"}, ("Equals", false)), 57 (@{const_name "less"}, ("Less", false)), 58 (@{const_name "less_eq"}, ("LessEquals", false)), 59 (@{const_name "ptr_less"}, ("Less", false)), 60 (@{const_name "ptr_le"}, ("LessEquals", false)), 61 (@{const_name "word_sless"}, ("SignedLess", false)), 62 (@{const_name "word_sle"}, ("SignedLessEquals", false)), 63 (@{const_name "Not"}, ("Not", true)), 64 (@{const_name "bitNOT"}, ("BWNot", true)), 65 (@{const_name "ucast"}, ("WordCast", false)), 66 (@{const_name "scast"}, ("WordCastSigned", false)), 67 (@{const_name "True"}, ("True", true)), 68 (@{const_name "False"}, ("False", true)), 69 (@{const_name "If"}, ("IfThenElse", false)), 70 (@{const_name "Set.member"}, ("MemDom", false)), 71 (@{const_name "shiftl"}, ("ShiftLeft", false)), 72 (@{const_name "shiftr"}, ("ShiftRight", false)), 73 (@{const_name "sshiftr"}, ("SignedShiftRight", false)), 74 (@{const_name "bv_clz"}, ("CountLeadingZeroes", true)), 75 (@{const_name "bv_ctz"}, ("CountTrailingZeroes", true)), 76 (@{const_name "all_htd_updates"}, ("HTDUpdate", false)) 77 ] |> Symtab.lookup 78 79fun locals ctxt = Syntax.read_typ ctxt "'a myvars" 80 |> Record.get_recT_fields (Proof_Context.theory_of ctxt) 81 |> fst 82 |> filter_out (fn (s, _) => s = @{const_name "globals"}) 83 |> Symtab.make |> Symtab.defined 84 85fun local_upds ctxt = Syntax.read_typ ctxt "'a myvars" 86 |> Record.get_recT_fields (Proof_Context.theory_of ctxt) 87 |> fst 88 |> filter_out (fn (s, _) => s = @{const_name "globals"}) 89 |> map (apfst (suffix Record.updateN)) 90 |> Symtab.make |> Symtab.defined 91 92fun get_field ctxt s = let 93 val xs = space_explode "." s 94 val fld = List.last xs 95 val tp = rev xs |> tl |> rev |> space_implode "." 96 val is_upd = String.isSuffix "_update" fld 97 val fld = if is_upd then unsuffix "_update" fld else fld 98 val _ = Proof_Context.get_thm ctxt 99 (tp ^ "_" ^ fld ^ "_fl_Some") 100 in SOME (tp, fld, is_upd) end 101 handle ERROR _ => NONE 102 | Bind => NONE 103 104val read_const = Proof_Context.read_const {proper = true, strict = true} 105 106fun process_struct ctxt csenv (nm, flds) = let 107 val offs = map (ProgramAnalysis.offset csenv (map snd flds)) 108 (0 upto (length flds - 1)) 109 val cons = read_const ctxt (nm ^ "." ^ nm) 110 val typ = dest_Const cons |> snd |> strip_type |> snd 111 val sz = ProgramAnalysis.sizeof csenv (Absyn.StructTy nm) 112 val algn = ProgramAnalysis.alignof csenv (Absyn.StructTy nm) 113 val accs = map (fst #> prefix (nm ^ ".") 114 #> read_const ctxt) flds 115 in (nm, (cons, typ, sz, algn, map fst flds ~~ (accs ~~ offs))) end 116 117fun structs ctxt csenv = ProgramAnalysis.get_senv csenv 118 |> map (process_struct ctxt csenv) 119 |> Symtab.make 120 121fun structs_by_typ ctxt csenv = Symtab.dest (structs ctxt csenv) 122 |> map (fn (nm, (cons, typ, sz, algn, flds)) => (fst (dest_Type typ), (nm, cons, sz, algn, flds))) 123 |> Symtab.make |> Symtab.lookup 124 125fun cons_fields ctxt csenv = structs ctxt csenv |> Symtab.dest 126 |> map (fn (_, (cons, typ, _, _, flds)) 127 => (fst (dest_Const cons), (fst (dest_Type typ), 128 map (snd #> fst #> dest_Const #> fst) flds))) 129 |> Symtab.make |> Symtab.lookup 130 131fun enums ctxt csenv = let 132 val Absyn.CE ecenv = ProgramAnalysis.cse2ecenv csenv 133 in 134 #enumenv ecenv |> Symtab.dest 135 |> map (fn (s, (n, _)) => 136 (read_const ctxt s 137 |> dest_Const |> fst, n)) 138 |> Symtab.make |> Symtab.lookup 139 end 140 141fun thm_to_rew thm 142 = ((Thm.concl_of thm |> HOLogic.dest_Trueprop |> HOLogic.dest_eq) 143 handle TERM _ => (Thm.concl_of thm |> Logic.dest_equals)) 144 handle TERM _ => (Thm.concl_of thm |> HOLogic.dest_Trueprop |> HOLogic.dest_imp) 145 146fun cons_field_upds ctxt csenv = let 147 val simps = ProgramAnalysis.get_senv csenv 148 |> maps (fn (tp, vs) => map (pair tp o fst) vs) 149 |> maps (fn (tp, fld) => [Proof_Context.get_thm ctxt 150 (tp ^ "." ^ fld ^ ".simps"), 151 Proof_Context.get_thm ctxt 152 (tp ^ "." ^ fld ^ Record.updateN ^ ".simps")]) 153 val accups = ProgramAnalysis.get_senv csenv 154 |> map (fn (tp, _) => (tp, Proof_Context.get_thms ctxt 155 (tp ^ "_accupd_same"))) 156 |> maps (fn (_, [t]) => [t] 157 | (tp, ts) => ts @ Proof_Context.get_thms ctxt 158 (tp ^ "_accupd_diff")) 159 val rews = map thm_to_rew (simps @ accups) 160 in Pattern.rewrite_term (Proof_Context.theory_of ctxt) rews [] end 161 162type export_params = {cons_field_upds: term -> term, 163 cons_fields: string -> (string * string list) option, 164 const_globals: Termtab.key -> string option, 165 enums: string -> int option, 166 local_upds: string -> bool, 167 locals: string -> bool, 168 rw_global_accs: string -> string option, 169 rw_global_upds: string -> string option, 170 rw_globals_tab: (term * term) Symtab.table, 171 structs_by_typ: 172 string -> (string * term * int * int * (string * (term * int)) list) option} 173 174fun get_all_export_params ctxt csenv : export_params = let 175 (* assuming DefineGlobalsList has already run *) 176 val defs = if (can (Proof_Context.get_thms ctxt) "no_global_data_defs") 177 then [] else Proof_Context.get_thms ctxt "global_data_defs" 178 val rhss = map (Thm.concl_of #> Logic.dest_equals #> snd) defs 179 val const_globals = map_filter 180 (fn (Const (@{const_name const_global_data}, _) $ nm $ v) 181 => SOME (HOLogic.dest_string nm, v) 182 | _ => NONE) rhss |> map swap |> Termtab.make |> Termtab.lookup 183 val rw_globals = map_filter (fn (Const (@{const_name global_data}, _) $ nm $ get $ set) 184 => SOME (HOLogic.dest_string nm, get, set) | _ => NONE) rhss 185 val rw_globals_tab = Symtab.make (map (fn x => (#1 x, (#2 x, #3 x))) rw_globals) 186 val rw_global_accs = map (fn (nm, c, _) => (fst (dest_Const c), nm)) rw_globals 187 |> Symtab.make |> Symtab.lookup 188 val rw_global_upds = map (fn (nm, _, c) => (fst (dest_Const c), nm)) rw_globals 189 |> Symtab.make |> Symtab.lookup 190 in {const_globals = const_globals, rw_globals_tab = rw_globals_tab, 191 rw_global_accs = rw_global_accs, 192 rw_global_upds = rw_global_upds, 193 cons_field_upds = cons_field_upds ctxt csenv, 194 enums = enums ctxt csenv, 195 cons_fields = cons_fields ctxt csenv, 196 structs_by_typ = structs_by_typ ctxt csenv, 197 locals = locals ctxt, 198 local_upds = local_upds ctxt} end 199\<close> 200 201ML \<open> 202 203val machine_word = case @{typ machine_word} of 204 @{typ word32} => "Word 32" 205 | @{typ word64} => "Word 64" 206 207fun convert_type _ _ @{typ bool} = "Bool" 208 | convert_type _ _ (Type (@{type_name word}, [n])) 209 = "Word " ^ signed_string_of_int (dest_binT n) 210 | convert_type abs ctxt (Type (@{type_name array}, [t, n])) 211 = "Array " ^ convert_type abs ctxt t ^ " " ^ (string_of_int (dest_binT n) 212 handle TYPE _ => (case n of Type (s, []) => (unprefix "tyCopy" (Long_Name.base_name s) 213 handle Fail _ => raise TYPE ("convert_type", [t, n], [])) 214 | _ => raise TYPE ("convert_type", [t, n], []))) 215 | convert_type true ctxt (Type (@{type_name ptr}, [T])) = "Ptr " ^ convert_type true ctxt T 216 | convert_type false _ (Type (@{type_name ptr}, _)) = machine_word 217 | convert_type _ _ @{typ "machine_word \<Rightarrow> word8"} = "Mem" 218 | convert_type _ _ @{typ "machine_word \<Rightarrow> bool"} = "Dom" 219 | convert_type _ _ @{typ "machine_word set"} = "Dom" 220 | convert_type _ _ @{typ heap_typ_desc} = "HTD" 221 222 | convert_type _ _ @{typ nat} = raise TYPE ("convert_type: nat", [], []) 223 | convert_type _ _ @{typ unit} = "UNIT" 224 | convert_type _ _ (Type ("fun", [Type (@{type_name word}, [i]), Type (@{type_name word}, [j])])) 225 = "WordArray " ^ signed_string_of_int (dest_binT i) ^ " " ^ signed_string_of_int (dest_binT j) 226 | convert_type _ _ (Type (@{type_name itself}, _)) = "Type" 227 | convert_type _ _ @{typ int} = raise TYPE ("convert_type: int", [], []) 228 | convert_type _ ctxt (Type (s, [])) = if Long_Name.base_name s = "machine_state" then "PMS" 229 else (Proof_Context.get_thm ctxt 230 (Long_Name.base_name s ^ "_td_names"); "Struct " ^ s) 231 | convert_type _ _ T = raise TYPE ("convert_type", [T], []) 232\<close> 233 234consts 235 pseudo_acc :: "'a \<Rightarrow> 'a" 236 237text \<open> 238 239Phase 1 of the conversion, converts accs and upds on SIMPL 240state (a record) to accs of named vars, using the pseudo_acc 241constant above to guard the accesses and lists of upds with strings. 242\<close> 243 244ML \<open> 245 246fun naming localname = Long_Name.base_name localname 247 |> unsuffix "_'" |> suffix "#v" 248 249fun mk_pseudo_acc s T = Const (@{const_name pseudo_acc}, T --> T) 250 $ Free (s, T) 251 252fun dest_global_mem_acc_addr (params : export_params) t = let 253 val acc = case head_of t of Const (c, _) => #rw_global_accs params c 254 | _ => NONE 255 val const = #const_globals params t 256 val T = fastype_of t 257 in case (const, acc) of 258 (SOME _, _) => NONE 259 | (NONE, SOME nm) => SOME (TermsTypes.mk_global_addr_ptr (nm, T)) 260 | (NONE, NONE) => NONE 261 end 262 263fun dest_ptr_type (Type (@{type_name ptr}, [a])) = a 264 | dest_ptr_type T = raise TYPE ("dest_ptr_type", [T], []) 265 266fun mk_memacc p = let 267 val T = fastype_of p 268 in Const (@{const_name h_val}, @{typ heap_mem} --> T --> dest_ptr_type T) 269 $ mk_pseudo_acc "Mem" @{typ heap_mem} $ p end 270 271fun mk_fun_app f x = let 272 val fT = fastype_of f 273 in Const (@{const_name "fun_app"}, fT --> fastype_of x --> range_type fT) $ f $ x end 274 275val ghost_assns = mk_pseudo_acc "GhostAssertions" @{typ "ghost_assertions"} 276 277val int_to_ghost_key = @{term "word_of_int :: int \<Rightarrow> 50 word"} 278 279fun convert_fetch_phase1 _ (@{term hrs_mem} $ _) = mk_pseudo_acc "Mem" @{typ heap_mem} 280 | convert_fetch_phase1 _ (@{term hrs_htd} $ _) = mk_pseudo_acc "HTD" @{typ heap_typ_desc} 281 | convert_fetch_phase1 _ (Const (@{const_name ghost_assertion_data_get}, _) $ k $ _ $ _) 282 = mk_fun_app ghost_assns (int_to_ghost_key $ k) 283 | convert_fetch_phase1 params (Abs (s, T, t)) 284 = Abs (s, T, convert_fetch_phase1 params t) 285 | convert_fetch_phase1 params t = if not (is_Const (head_of t)) then t 286 else let 287 val (f, xs) = strip_comb t 288 val (c, _) = dest_Const f 289 val T = fastype_of t 290 in case (#locals params c, dest_global_mem_acc_addr params t, #enums params c) of 291 (true, _, _) => (case xs of [Free ("s", _)] => mk_pseudo_acc (naming c) T 292 | [Free ("rv", _)] => mk_pseudo_acc ("rv#space#" ^ naming c) T 293 | _ => raise TERM ("convert_fetch_phase1: acc?", [t]) 294 ) 295 | (_, SOME p, _) => mk_memacc p 296 | (_, _, SOME n) => HOLogic.mk_number T n 297 | _ => list_comb (f, map (convert_fetch_phase1 params) xs) 298 end 299 300fun mk_memupd1 ptr v m = if dest_ptr_type (fastype_of ptr) = fastype_of v 301 then Const (@{const_name heap_update}, fastype_of ptr --> fastype_of v 302 --> @{typ "heap_mem \<Rightarrow> heap_mem"}) 303 $ ptr $ v $ m 304 else raise TERM ("mk_memupd1: types disagree", [ptr, v]) 305 306fun mk_memupd2 ptr v = mk_memupd1 ptr v (mk_pseudo_acc "Mem" @{typ heap_mem}) 307 308fun mk_fun_upd f x v = Const (@{const_name fun_upd}, 309 fastype_of f --> fastype_of x --> fastype_of v --> fastype_of f) $ f $ x $ v 310 311fun convert_upd_phase1 ctxt params (t as (Const (@{const_name globals_update}, _) 312 $ (Const (c, _) $ f) $ s)) = (case (Envir.beta_eta_contract f, 313 String.isPrefix NameGeneration.ghost_state_name 314 (Long_Name.base_name c), #rw_global_upds params c) of 315 (Const (@{const_name hrs_mem_update}, _) 316 $ (Const (@{const_name heap_update}, _) $ p $ v), _, _) 317 => [("Mem", convert_fetch_phase1 params (mk_memupd2 p v))] 318 | (Const (@{const_name hrs_htd_update}, _) $ g, _, _) 319 => [("HTD", (convert_fetch_phase1 params 320 (betapply (g, mk_pseudo_acc "HTD" @{typ heap_typ_desc}))))] 321 | (Const (@{const_name ghost_assertion_data_set}, _) $ k $ v $ _, _, _) 322 => [("GhostAssertions", mk_fun_upd ghost_assns (int_to_ghost_key $ k) 323 (convert_fetch_phase1 params v))] 324 | (_, true, _) => ((Syntax.pretty_term ctxt f |> Pretty.writeln); []) 325 | (_, _, SOME nm) => let 326 val acc = the (Symtab.lookup (#rw_globals_tab params) nm) |> fst 327 val v = convert_fetch_phase1 params (betapply (f, acc $ s)) 328 val ptr = TermsTypes.mk_global_addr_ptr (nm, fastype_of v) 329 in [("Mem", mk_memupd2 ptr v)] end 330 | _ => raise TERM ("convert_upd", [t])) 331 | convert_upd_phase1 _ params (t as (Const (c, _) $ f $ s)) = let 332 val c' = unsuffix Record.updateN c 333 val cT' = fastype_of s --> fastype_of (f $ s) 334 val _ = (#local_upds params c) orelse raise TERM ("convert_upd_phase1: nonlocal", [t]) 335 val v = betapply (f, Const (c', cT') $ s) 336 in [(naming c', convert_fetch_phase1 params v)] end 337 | convert_upd_phase1 _ _ t = raise TERM ("convert_upd_phase1", [t]) 338\<close> 339 340text \<open>Phase 2 eliminates compound types, so we access and 341update only words from memory and local values.\<close> 342 343ML \<open> 344fun ptr_simp ctxt = ctxt addsimps @{thms CTypesDefs.ptr_add_def size_of_def size_td_array 345 field_lvalue_offset_eq align_td_array' word_of_int scast_def[symmetric] 346 ucast_def[symmetric] 347 sint_sbintrunc' word_smod_numerals word_sdiv_numerals sdiv_int_def smod_int_def} 348 |> Simplifier.rewrite 349 350val trace_ptr_simp = false 351 352fun ptr_simp_term ctxt s pat t = let 353 val rew_thm = pat |> Thm.cterm_of ctxt |> ptr_simp ctxt 354 val rew = rew_thm |> Thm.concl_of |> Logic.varify_global |> Logic.dest_equals 355 val _ = (not (fst rew aconv snd rew)) 356 orelse raise TERM ("ptr_simp_term: " ^ s, [fst rew]) 357 val _ = if not trace_ptr_simp then () else 358 (Thm.pretty_thm ctxt rew_thm |> Pretty.writeln; 359 Syntax.pretty_term ctxt t |> Pretty.writeln) 360 in Pattern.rewrite_term (Proof_Context.theory_of ctxt) [rew] [] t end 361 362fun convert_ghost_key ctxt k = let 363 val procs = Term.add_const_names k [] 364 |> filter (String.isSuffix HoarePackage.proc_deco) 365 val proc_defs = map (suffix "_def" #> Proof_Context.get_thm ctxt) procs 366 val conv = Simplifier.rewrite (ctxt addsimps proc_defs) 367 (Thm.cterm_of ctxt k) 368 369 val n = Thm.rhs_of conv |> Thm.term_of 370 val _ = HOLogic.dest_number n 371 372 in n end 373 374fun dest_arrayT (Type (@{type_name array}, [elT, nT])) = let 375 in (elT, dest_binT nT) end 376 | dest_arrayT T = raise TYPE ("dest_arrayT", [T], []) 377 378fun dest_nat (@{term Suc} $ n) = dest_nat n + 1 379 | dest_nat (@{term "0 :: nat"}) = 0 380 | dest_nat n = HOLogic.dest_number n |> snd 381 382fun get_c_type_size ctxt T = let 383 val TT = Logic.mk_type T 384 val size_of = Const (@{const_name size_of}, type_of TT --> @{typ nat}) $ TT 385 in (ptr_simp_term ctxt "c_type_size" size_of size_of |> dest_nat) end 386 387val ptr_to_typ = Logic.mk_type o dest_ptr_type o fastype_of 388 389fun mk_arr_idx arr i = let 390 val arrT = fastype_of arr 391 val elT = case arrT of Type (@{type_name "array"}, [elT, _]) 392 => elT | _ => raise TYPE ("mk_arr_idx", [arrT], [arr]) 393 in Const (@{const_name "Arrays.index"}, arrT --> @{typ nat} --> elT) 394 $ arr $ i 395 end 396 397fun get_ptr_val (Const (@{const_name "Ptr"}, _) $ x) = x 398 | get_ptr_val p = Const (@{const_name ptr_val}, 399 fastype_of p --> @{typ machine_word}) $ p 400 401fun mk_ptr_offs opt_T p offs = let 402 val pT = fastype_of p 403 val T = case opt_T of NONE => pT 404 | SOME T => Type (@{type_name ptr}, [T]) 405 in Const (@{const_name Ptr}, @{typ machine_word} --> T) 406 $ (@{term "(+) :: machine_word \<Rightarrow> _"} 407 $ get_ptr_val p $ offs) 408 end 409 410fun get_acc_type [] T = T 411 | get_acc_type accs _ = (List.last accs $ @{term x}) 412 |> fastype_of 413 414val normalise_ring_ops = let 415 fun gather_plus (Const (@{const_name "plus"}, _) $ a $ b) 416 = gather_plus a @ gather_plus b 417 | gather_plus x = [x] 418 fun gather_times (Const (@{const_name "times"}, _) $ a $ b) 419 = gather_times a @ gather_times b 420 | gather_times x = [x] 421 fun fold_op _ [x] = x 422 | fold_op oper (x :: xs) = oper $ x $ (fold_op oper xs) 423 | fold_op _ [] = error "fold_op: shouldn't get empty list" 424 fun inner (x as (Const (@{const_name "plus"}, _) $ _ $ _)) 425 = gather_plus x |> map inner 426 |> sort Term_Ord.fast_term_ord 427 |> fold_op (head_of x) 428 | inner (x as (Const (@{const_name "times"}, _) $ _ $ _)) 429 = gather_times x |> map inner 430 |> sort Term_Ord.fast_term_ord 431 |> fold_op (head_of x) 432 | inner (f $ x) = inner f $ inner x 433 | inner x = x 434 in inner end 435 436fun dest_mem_acc_addr (Const (@{const_name h_val}, _) $ _ $ p) 437 = SOME p 438 | dest_mem_acc_addr _ = NONE 439 440fun narrow_mem_upd ctxt (params : export_params) p v = let 441 val T = fastype_of v 442 fun mk_offs T = mk_ptr_offs (SOME T) p 443 fun mk_offs2 T = mk_offs T o HOLogic.mk_number @{typ machine_word} 444 val sterm = Syntax.pretty_term ctxt #> Pretty.string_of 445 val styp = Syntax.pretty_typ ctxt #> Pretty.string_of 446 in if (dest_mem_acc_addr v = SOME p) then [] 447 else if #structs_by_typ params (fst (dest_Type T)) <> NONE 448 then let 449 val (_, _, _, _, flds) = the (#structs_by_typ params (fst (dest_Type T))) 450 val fld_writes = map (fn (_, (acc, offs)) 451 => (mk_offs2 (fastype_of (acc $ v)) offs, 452 #cons_field_upds params (acc $ v))) flds 453 in maps (uncurry (narrow_mem_upd ctxt params)) fld_writes end 454 else if fst (dest_Type T) = @{type_name array} 455 then let 456 val (elT, n) = dest_arrayT T 457 val elT_size = get_c_type_size ctxt elT 458 in case v of (Const (@{const_name Arrays.update}, _) $ arr $ i $ x) 459 => narrow_mem_upd ctxt params (mk_offs elT (@{term "(*) :: machine_word => _"} 460 $ HOLogic.mk_number @{typ machine_word} elT_size 461 $ (@{term "of_nat :: nat \<Rightarrow> machine_word"} $ i))) 462 x @ narrow_mem_upd ctxt params p arr 463 | _ => let 464 val addrs = map (fn i => (mk_offs2 elT (i * elT_size))) 465 (0 upto (n - 1)) 466 val elems = dest_array_init v 467 handle TERM _ => map 468 (fn i => mk_arr_idx v (HOLogic.mk_number @{typ nat} i)) 469 (0 upto (n - 1)) 470 val _ = (if n < 16 then () else 471 warning ("expanding " ^ string_of_int n ^ ": " 472 ^ sterm p ^ styp (fastype_of p) ^ ": " ^ sterm v)) 473 in maps (uncurry (narrow_mem_upd ctxt params)) (addrs ~~ elems) end 474 end 475 else if fst (dest_Type T) <> @{type_name word} 476 andalso fst (dest_Type T) <> @{type_name ptr} 477 then raise TERM ("narrow_mem_upd failed to narrow:", [p, v]) 478 else [(p, v)] 479 end 480 481fun triv_mem_upd ctxt p v = case dest_mem_acc_addr v of 482 NONE => false 483 | SOME p' => p aconv p' orelse let 484 val t = @{term "(-) :: machine_word \<Rightarrow> _"} $ get_ptr_val p $ get_ptr_val p' 485 val thm = ptr_simp ctxt (Thm.cterm_of ctxt t) 486 val t' = Thm.rhs_of thm |> Thm.term_of 487 in t' = @{term "0 :: machine_word"} 488 orelse (Thm.pretty_thm ctxt thm |> Pretty.writeln; false) 489 end 490 491fun narrow_mem_acc _ _ [] p = p 492 | narrow_mem_acc ctxt params accs p = let 493 fun get_offs (Const (@{const_name Arrays.index}, idxT) $ i) = let 494 val (elT, _) = dest_arrayT (domain_type idxT) 495 val elT_size = get_c_type_size ctxt elT 496 in @{term "(*) :: machine_word \<Rightarrow> _"} $ HOLogic.mk_number @{typ machine_word} elT_size 497 $ (@{term "of_nat :: nat \<Rightarrow> machine_word"} $ i) end 498 | get_offs (Const (s, T)) = let 499 val struct_typ = domain_type T |> dest_Type |> fst 500 val (_, _, _, _, flds) = the (#structs_by_typ params struct_typ) 501 val matches = filter (fn (_, (c, _)) => c = Const (s, T)) flds 502 val _ = (length matches = 1) 503 orelse raise TERM ("narrow_mem_acc: get_offs: ", [Const (s, T)]) 504 val offs = snd (snd (hd matches)) 505 in HOLogic.mk_number @{typ machine_word} offs end 506 | get_offs t = raise TERM ("narrow_mem_acc: get_offs: ", [t]) 507 val T' = get_acc_type accs (@{typ nat} (* doesn't matter *)) 508 val offs = foldr1 (fn (x, y) => @{term "(+) :: machine_word \<Rightarrow> _"} $ x $ y) 509 (map get_offs accs) 510 in mk_ptr_offs (SOME T') p offs end 511 512fun try_norm_index ctxt i = let 513 val i' = ptr_simp_term ctxt "idx_simp" i i 514 in dest_nat i'; i' end handle TERM _ => i 515 516fun mk_acc_array i xs = let 517 val n = length xs 518 val _ = warning ("expanding acc array, width " ^ string_of_int n) 519 val i = @{term "of_nat :: nat \<Rightarrow> machine_word"} $ i 520 fun inner [(x, _)] = x 521 | inner ((x, j) :: xs) = let 522 val y = inner xs 523 val T = fastype_of x 524 in Const (@{const_name "If"}, HOLogic.boolT --> T --> T --> T) 525 $ HOLogic.mk_eq (i, HOLogic.mk_number @{typ machine_word} j) $ x $ y end 526 | inner [] = error "mk_acc_array: empty" 527 in inner (xs ~~ (0 upto (n - 1))) end 528 529fun phase2_convert_global ctxt params accs 530 ((idx as Const (@{const_name Arrays.index}, _)) $ i $ t) 531 = phase2_convert_global ctxt params ((idx $ try_norm_index ctxt i) :: accs) t 532 | phase2_convert_global ctxt params accs (Const acc $ t) 533 = phase2_convert_global ctxt params (Const acc :: accs) t 534 | phase2_convert_global ctxt params accs t = case #const_globals params t 535 of SOME nm => let 536 val known_offs = forall (fn Const (@{const_name Arrays.index}, _) $ i 537 => (try dest_nat i) <> NONE 538 | _ => true) accs 539 val (c, _) = dest_Const t 540 val c_def = Proof_Context.get_thm ctxt (c ^ "_def") 541 val def_body = safe_mk_meta_eq c_def |> Thm.rhs_of |> Thm.term_of 542 |> Envir.beta_eta_contract 543 val p = TermsTypes.mk_global_addr_ptr (nm, fastype_of t) 544 val t' = if known_offs then def_body else mk_memacc p 545 val t_thm = if known_offs then SOME c_def else NONE 546 in SOME (t', t_thm) end 547 | _ => NONE 548 549fun convert_fetch_ph2 ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs) 550 (t as (Const (@{const_name fupdate}, _) $ _ $ _ $ _)) = let 551 val xs = dest_array_init (#cons_field_upds (params : export_params) t) 552 in case (try dest_nat i) of 553 SOME i => convert_fetch_ph2 ctxt params accs (nth xs i) 554 | NONE => mk_acc_array (convert_fetch_ph2 ctxt params [] i) 555 (map (convert_fetch_ph2 ctxt params accs) xs) 556 end 557 | convert_fetch_ph2 ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs) 558 (t as (Const (@{const_name FCP}, _) $ _)) = let 559 val xs = dest_array_init (#cons_field_upds params t) 560 in case (try dest_nat i) of 561 SOME i => convert_fetch_ph2 ctxt params accs (nth xs i) 562 | NONE => mk_acc_array (convert_fetch_ph2 ctxt params [] i) 563 (map (convert_fetch_ph2 ctxt params accs) xs) 564 end 565 | convert_fetch_ph2 ctxt params accs ((idx as Const (@{const_name Arrays.index}, _)) $ arr $ i) = let 566 val i' = convert_fetch_ph2 ctxt params accs i 567 val i'' = try_norm_index ctxt i' 568 in convert_fetch_ph2 ctxt params (idx $ i'' :: accs) arr end 569 | convert_fetch_ph2 ctxt params ((idx as Const (@{const_name Arrays.index}, _)) $ i :: accs) 570 (Const (@{const_name Arrays.update}, _) $ arr' $ i' $ v) 571 = let 572 val eq = HOLogic.mk_eq (i, i') 573 val eq = ptr_simp_term ctxt "idx_eq_simp" eq eq handle TERM _ => eq 574 val x = convert_fetch_ph2 ctxt params accs v 575 val y = convert_fetch_ph2 ctxt params (idx $ i :: accs) arr' 576 val T = fastype_of x 577 in case eq of @{term True} => x | @{term False} => y 578 | _ => Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) 579 $ convert_fetch_ph2 ctxt params [] eq $ x $ y end 580 | convert_fetch_ph2 ctxt params accs (Const (@{const_name h_val}, _) $ _ $ p) 581 = let 582 val p = convert_fetch_ph2 ctxt params [] p 583 val p = narrow_mem_acc ctxt params accs p 584 in mk_memacc p end 585 | convert_fetch_ph2 ctxt params [] (Const (@{const_name heap_update}, _) $ p $ v $ m) 586 = let 587 val xs = narrow_mem_upd ctxt params p v 588 |> map (apply2 (convert_fetch_ph2 ctxt params [])) 589 |> filter_out (uncurry (triv_mem_upd ctxt)) 590 val m = convert_fetch_ph2 ctxt params [] m 591 in fold (uncurry mk_memupd1) xs m end 592 | convert_fetch_ph2 _ _ [] (t as (Const (@{const_name pseudo_acc}, _) $ _)) = t 593 | convert_fetch_ph2 ctxt params accs (Const (@{const_name pseudo_acc}, _) $ Free (s, T)) = let 594 val T = get_acc_type accs T 595 fun canon s [] = mk_pseudo_acc s T 596 | canon s (Const (@{const_name Arrays.index}, idxT) $ i :: accs) = (case 597 (try dest_nat i) 598 of SOME i => canon (s ^ "." ^ string_of_int i) accs 599 | NONE => let val (_, n) = dest_arrayT (domain_type idxT) 600 in mk_acc_array (convert_fetch_ph2 ctxt params [] i) 601 (map (fn j => canon (s ^ "." ^ string_of_int j) accs) 602 (0 upto (n - 1))) end) 603 | canon s (Const (acc_nm, _) :: accs) 604 = canon (s ^ "." ^ Long_Name.base_name acc_nm) accs 605 | canon _ (t :: _) = raise TERM ("convert_fetch_ph2: canon: ", [t]) 606 in canon s accs end 607 | convert_fetch_ph2 _ _ [] (t as (Free ("symbol_table", _) $ _)) 608 = t 609 | convert_fetch_ph2 _ _ [] (t as Free ("domain", _)) 610 = t 611 | convert_fetch_ph2 ctxt params accs t = let 612 val (f, xs) = strip_comb t 613 val (c, _) = dest_Const f 614 val cnv = phase2_convert_global ctxt params accs f 615 |> Option.map (fst #> convert_fetch_phase1 params) 616 in if (get_field ctxt c |> Option.map #3) = SOME false 617 then case xs of [x] => convert_fetch_ph2 ctxt params (f :: accs) x 618 | _ => raise TERM ("convert_fetch_ph2: expected single", f :: xs) 619 else if cnv <> NONE then convert_fetch_ph2 ctxt params accs (the cnv) 620 else if (get_field ctxt c <> NONE orelse #cons_fields params c <> NONE) 621 then let 622 val _ = (accs <> []) orelse raise TERM ("convert_fetch_ph2: no accs", [t]) 623 val t' = hd accs $ t 624 val t'' = #cons_field_upds params t' 625 in if t'' aconv t' then raise TERM ("convert_fetch_ph2: irreducible upd:", [t']) 626 else convert_fetch_ph2 ctxt params (tl accs) t'' end 627 else list_comb (f, map (convert_fetch_ph2 ctxt params []) xs) end 628 629fun convert_upd_ph2_worker ctxt params s v T accs = 630 if #structs_by_typ params (fst (dest_Type T)) <> NONE 631 then let 632 val (_, _, _, _, flds) = the (#structs_by_typ params (fst (dest_Type T))) 633 in maps (fn (fld_nm, (acc, _)) => convert_upd_ph2_worker ctxt params (s ^ "." ^ fld_nm) 634 v (range_type (fastype_of acc)) (accs @ [acc])) flds end 635 else if fst (dest_Type T) = @{type_name array} 636 then let 637 val (elT, n) = dest_arrayT T 638 in maps (fn i => convert_upd_ph2_worker ctxt params (s ^ "." ^ string_of_int i) 639 v elT (accs @ [Const (@{const_name Arrays.index}, T --> @{typ nat} --> elT) 640 $ HOLogic.mk_number @{typ nat} i])) (0 upto (n - 1)) 641 end 642 else [(s, convert_fetch_ph2 ctxt params accs v)] 643 644fun convert_upd_ph2 ctxt params (s, v) 645 = convert_upd_ph2_worker ctxt params s v (fastype_of v) [] 646(* |> tap (map (snd #> Syntax.pretty_term ctxt #> Pretty.writeln)) *) 647\<close> 648 649text \<open>The final conversion reduces Isabelle terms to strings\<close> 650 651ML \<open> 652val space_pad = space_implode " " 653 654fun space_pad_list xs = space_pad (string_of_int (length xs) :: xs) 655 656fun s_st ctxt = Syntax.read_term ctxt "s :: globals myvars" 657fun rv_st ctxt = Syntax.read_term ctxt "rv :: globals myvars" 658 659fun convert_op ctxt params nm tp xs = "Op " ^ nm ^ " " ^ tp 660 ^ " " ^ space_pad_list (map (convert_ph3 ctxt params) xs) 661 662and convert_ph3 ctxt params (Const (@{const_name Collect}, _) $ S $ x) 663 = convert_ph3 ctxt params (betapply (S, x)) 664 | convert_ph3 ctxt params (Const (@{const_name Lattices.inf}, _) $ S $ T $ x) 665 = convert_op ctxt params "And" "Bool" [betapply (S, x), betapply (T, x)] 666 | convert_ph3 ctxt params (Const (@{const_name Ptr}, _) $ p) = convert_ph3 ctxt params p 667 | convert_ph3 ctxt params (Const (@{const_name ptr_val}, _) $ p) = convert_ph3 ctxt params p 668 | convert_ph3 ctxt params (t as (Const (@{const_name CTypesDefs.ptr_add}, T) $ _ $ _)) 669 = convert_ph3 ctxt params (ptr_simp_term ctxt "ptr_add" 670 (head_of t $ Free ("p", domain_type T) $ Free ("n", @{typ int})) t) 671 | convert_ph3 ctxt params (t as (Const (@{const_name field_lvalue}, T) $ _ $ s)) 672 = convert_ph3 ctxt params (ptr_simp_term ctxt "field_lvalue" 673 (head_of t $ Free ("p", domain_type T) $ s) t) 674 | convert_ph3 ctxt params (Const (@{const_name store_word64}, _) $ p $ w $ m) 675 = convert_op ctxt params "MemUpdate" "Mem" [m, p, w] 676 | convert_ph3 ctxt params (Const (@{const_name store_word32}, _) $ p $ w $ m) 677 = convert_op ctxt params "MemUpdate" "Mem" [m, p, w] 678 | convert_ph3 ctxt params (Const (@{const_name store_word8}, _) $ p $ w $ m) 679 = convert_op ctxt params "MemUpdate" "Mem" [m, p, w] 680 | convert_ph3 ctxt params (Const (@{const_name heap_update}, _) $ p $ v $ m) 681 = convert_op ctxt params "MemUpdate" "Mem" [m, p, v] 682 | convert_ph3 ctxt params (t as (Const (@{const_name h_val}, _) $ m $ p)) 683 = convert_op ctxt params "MemAcc" (convert_type false ctxt (fastype_of t)) [m, p] 684 | convert_ph3 ctxt params (Const (@{const_name load_word64}, _) $ p $ m) 685 = convert_op ctxt params "MemAcc" "Word 64" [m, p] 686 | convert_ph3 ctxt params (Const (@{const_name load_word32}, _) $ p $ m) 687 = convert_op ctxt params "MemAcc" "Word 32" [m, p] 688 | convert_ph3 ctxt params (Const (@{const_name load_word8}, _) $ p $ m) 689 = convert_op ctxt params "MemAcc" "Word 8" [m, p] 690 | convert_ph3 ctxt params (Const (@{const_name fun_upd}, _) $ f $ x $ v) 691 = convert_op ctxt params "WordArrayUpdate" 692 (convert_type false ctxt (fastype_of f)) [f, x, v] 693 | convert_ph3 ctxt params (Const (@{const_name fun_app}, _) $ f $ x) 694 = convert_op ctxt params "WordArrayAccess" 695 (convert_type false ctxt (fastype_of (f $ x))) [f, x] 696 | convert_ph3 ctxt params ((le as Const (@{const_name less_eq}, _)) 697 $ (Const (@{const_name insert}, _) $ p $ S) $ D) 698 = convert_op ctxt params "And" "Bool" [HOLogic.mk_mem (p, D), le $ S $ D] 699 | convert_ph3 ctxt params (Const (@{const_name less_eq}, _) 700 $ Const (@{const_name bot_class.bot}, _) $ _) = convert_ph3 ctxt params @{term True} 701 | convert_ph3 ctxt params (Const (@{const_name htd_safe}, _) $ _ $ _) 702 = convert_ph3 ctxt params @{term True} 703 | convert_ph3 ctxt params (Const (@{const_name uminus}, T) $ v) 704 = let val T = domain_type T 705 in convert_ph3 ctxt params (Const (@{const_name minus}, T --> T --> T) 706 $ Const (@{const_name zero_class.zero}, T) $ v) end 707 | convert_ph3 ctxt params (Const (@{const_name h_t_valid}, _) $ htd 708 $ Const (@{const_name c_guard}, _) $ p) 709 = convert_op ctxt params "PValid" "Bool" [htd, ptr_to_typ p, p] 710 | convert_ph3 ctxt params (Const (@{const_name array_assertion}, _) $ p $ n $ htd) 711 = convert_op ctxt params "PArrayValid" "Bool" 712 [htd, ptr_to_typ p, p, @{term "of_nat :: nat => machine_word"} $ n] 713 | convert_ph3 ctxt params (Const (@{const_name ptr_add_assertion'}, assT) 714 $ p $ n $ str $ htd) 715 = convert_ph3 ctxt params let val T = dest_ptr_type (fastype_of p) 716 val ass' = (Const (@{const_name ptr_add_assertion}, assT)) $ p $ n $ str $ htd 717 val ass'' = Pattern.rewrite_term (Proof_Context.theory_of ctxt) 718 (map thm_to_rew @{thms ptr_add_assertion_uintD ptr_add_assertion_sintD 719 if_True if_False}) [] ass' 720 in if T = @{typ unit} orelse T = @{typ word8} 721 then @{term True} else ass'' end 722 | convert_ph3 ctxt params (Const (@{const_name ptr_inverse_safe}, _) $ p $ htd) 723 = convert_op ctxt params "PGlobalValid" "Bool" [htd, ptr_to_typ p, p] 724 | convert_ph3 ctxt params (Const (@{const_name ptr_safe}, _) $ p $ htd) 725 = convert_op ctxt params "PWeakValid" "Bool" [htd, ptr_to_typ p, p] 726 | convert_ph3 ctxt params (Const (@{const_name globals_list_distinct}, _) $ 727 (Const (@{const_name image}, _) $ Const (@{const_name fst}, _) 728 $ (Const (@{const_name s_footprint}, _) $ _)) $ _ $ _) 729 = convert_ph3 ctxt params @{term True} 730 | convert_ph3 ctxt params (Const (@{const_name c_guard}, _) $ p) 731 = convert_op ctxt params "PAlignValid" "Bool" [ptr_to_typ p, p] 732 | convert_ph3 ctxt params (Const (@{const_name bot}, _) $ _) 733 = convert_ph3 ctxt params @{term False} 734 | convert_ph3 ctxt params (Const (@{const_name top_class.top}, _) $ _) 735 = convert_ph3 ctxt params @{term True} 736 | convert_ph3 ctxt params (Const (@{const_name insert}, _) $ v $ S $ x) 737 = convert_op ctxt params "Or" "Bool" [HOLogic.mk_eq (v, x), betapply (S, x)] 738 | convert_ph3 _ _ (Free ("symbol_table", _) $ s) 739 = "Symbol " ^ HOLogic.dest_string s ^ " " ^ machine_word 740 | convert_ph3 ctxt params (Const (@{const_name of_nat}, T) $ (Const (@{const_name unat}, _) $ x)) 741 = let 742 val t1 = fastype_of x 743 val t2 = range_type T 744 in if t1 = t2 then convert_ph3 ctxt params x 745 else convert_ph3 ctxt params (Const (@{const_name ucast}, t1 --> t2) $ x) 746 end 747 | convert_ph3 ctxt params (t as (Const (@{const_name of_nat}, _) $ _)) 748 = convert_ph3 ctxt params (ptr_simp_term ctxt "of_nat" t t) 749 | convert_ph3 ctxt params (t as (Const (@{const_name power}, _) $ x $ y)) 750 = (case try HOLogic.dest_number x of 751 SOME ((typ as Type (@{type_name word}, _)), 2) => convert_ph3 ctxt params 752 (Const (@{const_name shiftl}, typ --> @{typ nat} --> typ) 753 $ HOLogic.mk_number typ 1 $ y) 754 | _ => convert_ph3 ctxt params (ptr_simp_term ctxt "power" t t)) 755 | convert_ph3 ctxt params (Const (@{const_name ptr_coerce}, _) $ p) 756 = convert_ph3 ctxt params p 757 | convert_ph3 ctxt params (t as (Const (@{const_name word_of_int}, _) $ _)) 758 = if head_of t = int_to_ghost_key then convert_ph3 ctxt params (convert_ghost_key ctxt t) 759 else let 760 val thy = Proof_Context.theory_of ctxt 761 val t' = Pattern.rewrite_term thy (map (Thm.concl_of #> HOLogic.dest_Trueprop 762 #> HOLogic.dest_eq) @{thms word_uint.Rep_inverse word_sint.Rep_inverse}) [] t 763 in if t' aconv t then convert_ph3 ctxt params (ptr_simp_term ctxt "word_of_int" t t) 764 else convert_ph3 ctxt params t' end 765 | convert_ph3 ctxt params (t as (Const (@{const_name sdiv}, _) $ _ $ _)) 766 = convert_ph3 ctxt params (ptr_simp_term ctxt "sdiv" t t) 767 | convert_ph3 ctxt _ (t as (Const (@{const_name numeral}, _) $ _)) 768 = let 769 val n = HOLogic.dest_number t |> snd 770 handle TERM _ => raise TERM ("convert_ph3", [t]) 771 val _ = (fastype_of t <> @{typ int}) orelse raise TERM ("convert_ph3: int", [t]) 772 in "Num " ^ signed_string_of_int n ^ " " ^ convert_type false ctxt (fastype_of t) end 773 | convert_ph3 ctxt _ (Const (@{const_name Pure.type}, Type (_, [T]))) 774 = "Type " ^ convert_type true ctxt T 775 | convert_ph3 ctxt _ (Const (@{const_name pseudo_acc}, _) $ Free (s, T)) 776 = "Var " ^ s ^ " " ^ convert_type false ctxt T 777 | convert_ph3 ctxt params t = let 778 val (f, xs) = strip_comb t 779 val (c, _) = dest_Const f 780 val xs = if member (op =) [@{const_name shiftl}, 781 @{const_name shiftr}, @{const_name sshiftr}] c 782 then case xs of 783 [x, y] => [x, Const (@{const_name of_nat}, @{typ nat} --> fastype_of x) $ y] 784 | _ => raise TERM ("convert_ph3: shift", [t]) 785 else xs 786 in case ops c of 787 (SOME (nm, _)) => convert_op ctxt params nm (convert_type false ctxt (fastype_of t)) xs 788 | NONE => ("Num " ^ signed_string_of_int (snd (HOLogic.dest_number t)) 789 ^ " " ^ convert_type false ctxt (fastype_of t) 790 handle TERM _ => raise TERM ("convert_ph3", [t])) 791 end 792 793fun htd_simp ctxt = ctxt addsimps @{thms fold_all_htd_updates 794 unat_less_2p_word_bits[simplified word_bits_conv]} 795 |> Simplifier.add_cong @{thm if_cong} |> Simplifier.rewrite 796 797fun simp_htd ctxt t = let 798 val rew_thm = Thm.cterm_of ctxt t |> htd_simp ctxt 799 in Thm.term_of (Thm.rhs_of rew_thm) end 800 801fun convert_upd_ph3 ctxt params (s, v) = 802 let 803 val nm = if s = "HTD" then "HTD HTD" 804 else s ^ " " ^ convert_type false ctxt (fastype_of v) 805 val v = if s = "HTD" then simp_htd ctxt v else v 806 val v = convert_ph3 ctxt params v 807 in (nm, v) end 808 handle TERM (s, ts) => raise TERM ("convert_upd_ph3: " ^ s, v :: ts) 809\<close> 810 811ML \<open> 812fun convert_fetch ctxt params t = 813 Envir.beta_eta_contract t 814 |> convert_fetch_phase1 params 815 |> convert_fetch_ph2 ctxt params [] 816 |> convert_ph3 ctxt params 817 818fun tracet (s, t) = ((Syntax.pretty_term @{context} t |> Pretty.writeln); (s, t)) 819 820fun convert_param_upds ctxt params (t as (Const (c, _) $ _ $ s)) 821 = if #local_upds params c orelse c = @{const_name globals_update} 822 then convert_param_upds ctxt params s 823 @ (Envir.beta_eta_contract t 824(* |> tap (Syntax.pretty_term ctxt #> Pretty.writeln) *) 825 |> convert_upd_phase1 ctxt params 826(* |> map tracet *) 827(* |> map (apsnd (Syntax.check_term ctxt)) *) 828 |> maps (convert_upd_ph2 ctxt params) 829(* |> map (apsnd (Syntax.check_term ctxt)) *) 830 |> map (convert_upd_ph3 ctxt params) 831 ) 832 else raise TERM ("convert_param_upds", [t]) 833 | convert_param_upds ctxt _ t = (if t = s_st ctxt then [] 834 else raise TERM ("convert_param_upds", [t])) 835 836\<close> 837 838ML \<open> 839 840val all_c_params = ["Mem Mem", "HTD HTD", "PMS PMS", 841 "GhostAssertions WordArray 50 " ^ ParseGraph.ptr_size_str] 842val all_c_in_params = map (prefix "Var ") all_c_params 843val all_asm_params = ["Mem Mem", "PMS PMS"] 844val all_asm_in_params = map (prefix "Var ") all_asm_params 845 846fun asm_spec_name_to_fn_name _ specname = let 847 val name = space_implode "_" (space_explode " " specname) 848 in "asm_instruction'" ^ name end 849 850fun mk_safe f ctxt params s = ( 851 Proof_Context.get_thm ctxt (s ^ "_body_def"); 852 Proof_Context.get_thm ctxt (s ^ "_impl"); 853 f ctxt params s) handle ERROR _ => false 854 855fun mk_set_int s t = let 856 val T = fastype_of s 857 in Const (@{const_name Lattices.inf}, T --> T --> T) $ s $ t end 858 859val reduce_set_mem_eqs = @{thms mem_Collect_eq Int_iff Un_iff empty_iff iffI[OF TrueI UNIV_I]} 860 |> map (mk_meta_eq #> Thm.concl_of #> Logic.dest_equals) 861 862fun reduce_set_mem ctxt x S = let 863 val t = HOLogic.mk_mem (x, S) 864 val t' = Pattern.rewrite_term (Proof_Context.theory_of ctxt) 865 reduce_set_mem_eqs [] t 866 in if t aconv t' then Pretty.writeln (Syntax.pretty_term ctxt (HOLogic.mk_prod (t, t'))) 867 else (); t' 868 end 869 870 871fun is_spec_body_const @{const_name Spec} = true 872 | is_spec_body_const @{const_name guarded_spec_body} = true 873 | is_spec_body_const _ = false 874 875fun has_reads body = exists_Const (fn (s, T) => 876 snd (strip_type T) = @{typ heap_raw_state} 877 orelse is_spec_body_const s) body 878 879fun has_reads_globals (params : export_params) body = exists_Const (fn (s, T) => 880 snd (strip_type T) = @{typ heap_raw_state} 881 orelse is_spec_body_const s 882 orelse #rw_global_accs params s <> NONE 883 orelse #const_globals params (Const (s, T)) <> NONE 884 ) body 885 886fun get_reads_calls ctxt params globals name = let 887 val thm = Proof_Context.get_thm ctxt (name ^ "_body_def") 888 |> simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms call_def block_def}) 889 fun calls (Const (@{const_name com.Call}, _) $ proc) = [proc] 890 | calls (f $ x) = calls f @ calls x 891 | calls (Abs (_, _, t)) = calls t 892 | calls _ = [] 893 val reads = (if globals then has_reads_globals params else has_reads) 894 (Thm.concl_of thm) 895 val call_to_name = dest_Const #> fst #> Long_Name.base_name 896 #> unsuffix "_'proc" 897 in (reads, calls (Thm.concl_of thm) |> map call_to_name) end 898 899fun is_no_read ctxt params globals s = let 900 fun inner stack s = if member (op =) stack s then true else let 901 val (reads, calls) = get_reads_calls ctxt params globals s 902 in not reads andalso forall I (map (inner (s :: stack)) calls) end 903 in inner [] s end 904 905fun is_no_write ctxt s = let 906 val thm = Proof_Context.get_thm ctxt (s ^ "_modifies") 907 val mex = exists_Const (fn (s, _) => s = @{const_name mex}) (Thm.concl_of thm) 908 in not mex end 909 910fun synthetic_updates ctxt params pref (Const (c, T)) = let 911 val s = s_st ctxt 912 val sT = fastype_of s 913 val xT = range_type T 914 val upd = Const (suffix Record.updateN c, (xT --> xT) --> sT --> sT) 915 $ Abs ("v", xT, Bound 0) $ s 916 |> Syntax.check_term ctxt 917 val upds = convert_param_upds ctxt params upd 918 in map (apfst (prefix pref)) upds end 919 | synthetic_updates _ _ _ t = raise TERM ("synthetic_updates", [t]) 920 921fun is_no_read_globals ctxt params = is_no_read ctxt params true 922 923fun get_global_valid_assertion ctxt (params : export_params) t = let 924 val tnames = Term.add_const_names t [] 925 val globs = map_filter (#rw_global_accs params) tnames 926 @ map_filter (#rw_global_upds params) tnames 927 fun assert nm = let 928 val T = Symtab.lookup (#rw_globals_tab params) nm 929 |> the |> fst |> fastype_of |> range_type 930 val p = TermsTypes.mk_global_addr_ptr (nm, T) 931 in convert_op ctxt params "PGlobalValid" "Bool" 932 [mk_pseudo_acc "HTD" @{typ heap_typ_desc}, ptr_to_typ p, p] 933 end 934 val globs = sort_distinct fast_string_ord globs 935 |> map assert 936 fun conj (x, y) = "Op And Bool 2 " ^ x ^ " " ^ y 937 in case globs of [] => NONE 938 | _ => SOME (foldr1 conj globs) 939 end 940 941fun emit outfile s = TextIO.output (outfile, s ^ "\n") 942 943fun add_global_valid_assertion outfile ctxt params t n = 944 case get_global_valid_assertion ctxt params t of NONE => 945 (n + 1, string_of_int n) 946 | SOME ass => (emit outfile (string_of_int (n + 1) ^ " Cond " ^ string_of_int n ^ " Err " ^ ass); 947 (n + 2, string_of_int (n + 1))) 948 949fun emit_body ctxt outfile params (Const (@{const_name Seq}, _) $ a $ b) n c e = let 950 val (n, nm) = emit_body ctxt outfile params b n c e 951 handle TERM (s, ts) => raise TERM (s, b :: ts) 952 | Empty => raise TERM ("emit_body: got Empty", [b]) 953 val (n, nm) = emit_body ctxt outfile params a n nm e 954 handle TERM (s, ts) => raise TERM (s, a :: ts) 955 | Empty => raise TERM ("emit_body: got Empty", [a]) 956 in (n, nm) end 957 | emit_body ctxt outfile params (Const (@{const_name Catch}, _) $ a $ b) n c e = (case b of 958 Const (@{const_name com.Skip}, _) => emit_body ctxt outfile params a n c (c, c) 959 | Const (@{const_name ccatchbrk}, _) $ _ => emit_body ctxt outfile params a n c (fst e, c) 960 | t => raise TERM ("emit_body ctxt params (Catch)", [t]) 961 ) 962 | emit_body ctxt outfile params (Const (@{const_name creturn}, _) $ _ $ upd $ f) n _ (r, b) = 963 emit_body ctxt outfile params (@{term com.Basic} $ Abs ("s", dummyT, betapplys (upd, 964 [Abs ("_", dummyT, betapply (f, Bound 1)), Bound 0]))) n r (r, b) 965 | emit_body _ _ _ (Const (@{const_name creturn_void}, _) $ _) n _ (r, _) = (n, r) 966 | emit_body _ _ _ (Const (@{const_name cbreak}, _) $ _) n _ (_, b) = (n, b) 967 | emit_body _ _ _ (Const (@{const_name com.Skip}, _)) n c _ = (n, c) 968 | emit_body ctxt outfile params (Const (@{const_name com.Cond}, _) $ S $ a $ b) n c e = let 969 val (n, nm_a) = emit_body ctxt outfile params a n c e 970 val (n, nm_b) = emit_body ctxt outfile params b n c e 971 val s = convert_fetch ctxt params (reduce_set_mem ctxt (s_st ctxt) S) 972 in 973 emit outfile (string_of_int n ^ " Cond " ^ nm_a ^ " " ^ nm_b ^ " " ^ s); 974 add_global_valid_assertion outfile ctxt params S n 975 end 976 | emit_body ctxt outfile params (Const (@{const_name Guard}, T) $ F $ G $ 977 (Const (@{const_name Guard}, _) $ _ $ G' $ a)) n c e 978 = emit_body ctxt outfile params (Const (@{const_name Guard}, T) $ F 979 $ (mk_set_int G G') $ a) n c e 980 | emit_body ctxt outfile params (Const (@{const_name Guard}, _) $ _ $ G $ a) n c e = let 981 val (n, nm) = emit_body ctxt outfile params a n c e 982 val thy = Proof_Context.theory_of ctxt 983 val G = Pattern.rewrite_term thy 984 (@{thms guard_arith_simps meta_eq_to_obj_eq[OF ptr_arr_retyps_def]} 985 |> map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)) [] G 986 val s = convert_fetch ctxt params (reduce_set_mem ctxt (s_st ctxt) G) 987 in 988 emit outfile (string_of_int n ^ " Cond " ^ nm ^ " Err " ^ s); 989 add_global_valid_assertion outfile ctxt params G n 990 end 991 | emit_body _ _ _ (Const (@{const_name com.Basic}, _) $ Abs (_, _, Bound 0)) n c _ 992 = (n, c) 993 | emit_body ctxt outfile params (Const (@{const_name com.Basic}, _) $ f) n c _ = let 994 val upds = convert_param_upds ctxt params (betapply (f, s_st ctxt)) 995 |> filter_out (fn (s, v) => v = "Var " ^ s) 996 |> map (fn (s, v) => s ^ " " ^ v) 997 998 in 999 emit outfile (string_of_int n ^ " Basic " ^ c ^ " " ^ space_pad_list upds); 1000 add_global_valid_assertion outfile ctxt params f n 1001 end 1002 | emit_body ctxt outfile params (Const (@{const_name Spec}, _) 1003 $ (Const (@{const_name asm_spec}, _) $ _ $ _ $ vol $ spec $ lhs $ vs)) 1004 n c _ = let 1005 val spec = HOLogic.dest_string spec 1006 val lhss = convert_param_upds ctxt params 1007 (betapplys (lhs, [@{term "0 :: machine_word"}, s_st ctxt])) 1008 val args = HOLogic.dest_list (betapply (vs, s_st ctxt)) 1009 |> map (convert_fetch ctxt params) 1010 val args = args @ all_asm_in_params 1011 val outs = map fst lhss @ all_asm_params 1012 val _ = HOLogic.mk_prod 1013 in emit outfile (string_of_int n ^ " Call " ^ c ^ " " ^ asm_spec_name_to_fn_name vol spec 1014 ^ " " ^ space_pad_list args ^ " " ^ space_pad_list outs); 1015 add_global_valid_assertion outfile ctxt params (HOLogic.mk_prod (lhs, vs)) n 1016 end 1017 | emit_body ctxt outfile params (Const (@{const_name call}, _) $ f $ Const (p, _) 1018 $ _ $ r2) n c e = let 1019 val proc_info = Hoare.get_data ctxt |> #proc_info 1020 val ret_vals = Symtab.lookup proc_info (Long_Name.base_name p) 1021 |> the |> #params 1022 |> filter (fn (v, _) => v = HoarePackage.Out) 1023 |> maps (snd #> read_const ctxt 1024 #> synthetic_updates ctxt params "rv#space#") 1025 |> map fst 1026 1027 val p_short = unsuffix "_'proc" (Long_Name.base_name p) 1028 val no_read = mk_safe is_no_read_globals ctxt params p_short 1029 val no_write = mk_safe (K o is_no_write) ctxt params p_short 1030 (* writes implicitly require reads, really *) 1031 val no_read = no_read andalso no_write 1032 1033 val args = ((convert_param_upds ctxt params (betapply (f, s_st ctxt)) 1034 |> map snd (* discard the local names of the updated variables *)) 1035 @ (if no_read then [] else all_c_in_params)) 1036 handle TERM (s, ts) => raise TERM ("emit_body call: " ^ s, f :: ts) 1037 1038 val out = ret_vals @ (if no_write then [] else all_c_params) 1039 1040 val (n, nm_save) = emit_body ctxt outfile params (betapplys (r2, [@{term i}, rv_st ctxt])) n c e 1041 1042 in emit outfile (string_of_int n ^ " Call " ^ nm_save ^ " " ^ (unsuffix "_'proc" p) 1043 ^ " " ^ space_pad_list args ^ " " ^ space_pad_list out); 1044 add_global_valid_assertion outfile ctxt params f n 1045 end 1046 | emit_body _ _ _ (Const (@{const_name lvar_nondet_init}, _) $ _ $ _) n c _ 1047 = (n, c) 1048 | emit_body ctxt outfile params (Const (@{const_name whileAnno}, _) $ C $ _ $ _ $ bd) n c e = let 1049 fun sn i = string_of_int (n + i) 1050 val lc = "loop#" ^ sn 0 ^ "#count" ^ " " ^ machine_word 1051 val (n', nm) = emit_body ctxt outfile params bd (n + 4) (sn 0) e 1052 val cond = convert_fetch ctxt params (reduce_set_mem ctxt (s_st ctxt) C) 1053 val err_cond = case get_global_valid_assertion ctxt params C 1054 of NONE => "Op True Bool 0" 1055 | SOME s => s 1056 in emit outfile (sn 0 ^ " Basic " ^ sn 1 ^ " 1 " ^ lc 1057 ^ " Op Plus " ^ machine_word ^ " 2 Var " ^ lc ^ " Num 1 " ^ machine_word); 1058 emit outfile (sn 1 ^ " Cond " ^ sn 2 ^ " Err " ^ err_cond); 1059 emit outfile (sn 2 ^ " Cond " ^ nm ^ " " ^ c ^ " " ^ cond); 1060 emit outfile (sn 3 ^ " Basic " ^ sn 1 ^ " 1 " ^ lc ^ " Num 0 " ^ machine_word); 1061 (n', sn 3) 1062 end 1063 | emit_body _ _ _ t _ _ _ = raise TERM ("emit_body", [t]) 1064 1065fun emit_func_body ctxt outfile eparams name = let 1066 val proc_info = Hoare.get_data ctxt |> #proc_info 1067 val params = Symtab.lookup proc_info (name ^ "_'proc") 1068 |> the |> #params 1069 |> map (apsnd (read_const ctxt 1070 #> synthetic_updates ctxt eparams "" 1071 #> map fst)) 1072 1073 val no_read = mk_safe is_no_read_globals ctxt eparams name 1074 val no_write = mk_safe (K o is_no_write) ctxt eparams name 1075 (* writes implicitly require reads, really *) 1076 val no_read = no_read andalso no_write 1077 1078 val inputs = (filter (fn p => fst p = HoarePackage.In) params 1079 |> maps snd) @ (if no_read then [] else all_c_params) 1080 1081 val outputs = (filter (fn p => fst p = HoarePackage.Out) params 1082 |> maps snd) @ (if no_write then [] else all_c_params) 1083 1084 val body = Get_Body_Refines.get ctxt name 1085 |> simplify (put_simpset HOL_basic_ss ctxt 1086 addsimps @{thms switch.simps fst_conv snd_conv 1087 insert_iff empty_iff 1088 ptr_add_assertion_def if_True if_False 1089 bv_clz_def[symmetric] bv_ctz_def[symmetric] 1090 }) 1091 |> Thm.concl_of |> HOLogic.dest_Trueprop 1092 |> (fn t => (case t of Const (@{const_name simple_simpl_refines}, _) $ _ $ lhs $ _ => lhs 1093 | _ => raise Option)) 1094 handle Option => @{term "Spec S"} 1095 | THM _ => @{term "Spec S"} 1096 1097 val full_nm = read_const ctxt (name ^ "_'proc") 1098 |> dest_Const |> fst |> unsuffix "_'proc" 1099 in emit outfile ""; 1100 emit outfile ("Function " ^ full_nm ^ " " ^ space_pad_list inputs 1101 ^ " " ^ space_pad_list outputs); 1102 if (try (head_of #> dest_Const #> fst #> is_spec_body_const) body) 1103 = SOME true 1104 then () 1105 else (emit outfile ("1 Basic Ret 0"); 1106 emit_body ctxt outfile eparams body 2 "1" ("ErrExc", "ErrExc") 1107 |> snd |> prefix "EntryPoint " |> emit outfile 1108 handle TERM (s, ts) => raise TERM ("emit_func_body: " ^ name ^ ": " ^ s, body :: @{term True} :: ts) 1109 | TYPE (s, Ts, ts) => raise TYPE ("emit_func_body: " ^ name ^ ": " ^ s, Ts, body :: @{term True} :: ts) 1110 | Empty => raise TERM ("emit_func_body: Empty", [body])) 1111 end 1112 1113fun emit_struct ctxt outfile csenv (nm, flds) = let 1114 val offs = map (ProgramAnalysis.offset csenv (map snd flds)) 1115 (0 upto (length flds - 1)) 1116 val full_nm = read_const ctxt (nm ^ "." ^ nm) 1117 |> dest_Const |> snd |> strip_type |> snd |> dest_Type |> fst 1118 val thy = Proof_Context.theory_of ctxt 1119 val sz = ProgramAnalysis.sizeof csenv (Absyn.StructTy nm) 1120 val algn = ProgramAnalysis.alignof csenv (Absyn.StructTy nm) 1121 fun emit_fld ((fld_nm, fld_ty), offs) = emit outfile (space_pad 1122 ["StructField", fld_nm, convert_type false ctxt 1123 (CalculateState.ctype_to_typ (thy, fld_ty)), string_of_int offs]) 1124 in emit outfile (space_pad ["Struct", full_nm, string_of_int sz, 1125 string_of_int algn]); app emit_fld (flds ~~ offs) end 1126 1127fun scan_func_body_asm_instructions ctxt name = let 1128 val body = Proof_Context.get_thm ctxt (name ^ "_body_def") 1129 fun has_lhs lhs = betapplys (lhs, [Bound 0, Bound 1]) <> Bound 1 1130 fun nm_args vs = betapply (vs, s_st ctxt) |> HOLogic.dest_list |> length 1131 fun gather (Const (@{const_name asm_spec}, _) $ _ $ _ $ vol $ nm $ lhs $ vs) xs 1132 = (asm_spec_name_to_fn_name vol (HOLogic.dest_string nm), 1133 has_lhs lhs, nm_args vs) :: xs 1134 | gather (f $ x) xs = gather f (gather x xs) 1135 | gather _ xs = xs 1136 in gather (Thm.concl_of body) [] end 1137 handle ERROR _ => [] 1138 1139fun emit_asm_protoes ctxt outfile fs = let 1140 val asm_info = maps (scan_func_body_asm_instructions ctxt) fs 1141 |> sort_distinct (fn ((s, _, _), (t, _, _)) => fast_string_ord (s, t)) 1142 fun mk_args n = (map (fn i => "arg" ^ string_of_int i ^ " " ^ machine_word) (1 upto n)) 1143 fun mk_rets has_lhs = (if has_lhs then ["ret1 " ^ machine_word] else []) 1144 fun emit_it (nm, has_lhs, nm_args) = emit outfile 1145 ("Function " ^ nm 1146 ^ " " ^ space_pad_list (mk_args nm_args @ all_asm_params) 1147 ^ " " ^ space_pad_list (mk_rets has_lhs @ all_asm_params) 1148 ) 1149 in app emit_it asm_info end 1150 1151fun emit_C_everything ctxt csenv outfile = let 1152 val fs = ProgramAnalysis.get_functions csenv 1153 val structs = ProgramAnalysis.get_senv csenv 1154 val params = get_all_export_params ctxt csenv 1155 in app (emit_struct ctxt outfile csenv) structs; 1156 app (emit_func_body ctxt outfile params) fs; 1157 emit_asm_protoes ctxt outfile fs end 1158\<close> 1159 1160ML \<open> 1161fun openOut_relative thy = ParseGraph.filename_relative thy #> TextIO.openOut; 1162 1163fun emit_C_everything_relative ctxt csenv fname = let 1164 val thy = Proof_Context.theory_of ctxt 1165 val outfile = openOut_relative thy fname 1166 in emit_C_everything ctxt csenv outfile; TextIO.closeOut outfile end 1167\<close> 1168 1169end 1170 1171 1172