1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory Substitute 12 13imports 14 "CKernel.Kernel_C" 15 "AsmRefine.GlobalsSwap" 16begin 17 18ML {* 19 20structure SubstituteSpecs = struct 21 22val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t))); 23 24fun get_rhs thm = 25 snd (Logic.dest_equals (Thm.concl_of thm)) 26 handle TYPE _ => 27 snd (HOLogic.dest_eq (Thm.concl_of thm)); 28 29fun get_lhs thm = 30 fst (Logic.dest_equals (Thm.concl_of thm)) 31 handle TYPE _ => 32 fst (HOLogic.dest_eq (Thm.concl_of thm)); 33 34fun term_convert prefix convs (tm as Const (name, _)) = 35 if not (String.isPrefix prefix name) then tm 36 else the (Termtab.lookup convs tm) 37 | term_convert _ _ tm = tm; 38 39fun suspicious_term ctxt s t = if Term.add_var_names t [] = [] then () 40 else (tracing ("suspicious " ^ s); 41 Syntax.pretty_term ctxt t |> Pretty.string_of |> tracing; 42 ()) 43 44val debug_trace = ref (Bound 0); 45 46fun convert prefix src_ctxt proc (tm as Const (name, _)) (convs, ctxt) = 47 ((term_convert prefix convs tm; (convs, ctxt)) 48 handle Option => 49 let 50 val cname = unprefix prefix name; 51 val def_thm = Proof_Context.get_thm src_ctxt (cname ^ "_def") 52 val rhs = get_rhs def_thm; 53 val _ = suspicious_term ctxt "init rhs" rhs; 54 val consts = Term.add_consts rhs []; 55 val (convs, ctxt) = fold (convert prefix src_ctxt proc o Const) 56 consts (convs, ctxt); 57 val rhs' = map_aterms (term_convert prefix convs) rhs; 58 val rhs'' = proc ctxt cname rhs'; 59 val _ = suspicious_term ctxt "adjusted rhs" rhs''; 60 61 in if rhs'' aconv rhs 62 then (Termtab.insert (K true) (tm, tm) convs, 63 Local_Theory.abbrev Syntax.mode_default 64 ((Binding.name cname, NoSyn), get_lhs def_thm) ctxt 65 |> snd |> Local_Theory.note ((Binding.name (cname ^ "_def"), []), [def_thm]) 66 |> snd |> Local_Theory.reset 67 ) 68 69 else let 70 val _ = tracing ("Defining " ^ cname); 71 72 val pre_def_ctxt = ctxt 73 val b = Binding.name cname 74 val ((tm', _), ctxt) = Local_Theory.define 75 ((b, NoSyn), ((Thm.def_binding b, []), rhs'')) ctxt 76 val tm'' = Morphism.term (Proof_Context.export_morphism ctxt pre_def_ctxt) tm' 77 val ctxt = Local_Theory.reset ctxt 78 79 val lhs_argTs = get_lhs def_thm |> strip_comb |> snd |> map fastype_of; 80 val abs_tm = list_abs (map (pair "_") lhs_argTs, tm'') 81 82 in (Termtab.insert (K true) (tm, abs_tm) convs, ctxt) end 83 end) 84 | convert _ _ _ (tm) _ = raise TERM ("convert: not Const", [tm]) 85 86 87fun prove_impl_tac ctxt ss = 88 SUBGOAL (fn (t, n) => let 89 val lhs = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst; 90 val cnames = Term.add_const_names lhs [] 91 |> filter (String.isSuffix "_'proc"); 92 val unfolds = map (Proof_Context.get_thm ctxt o suffix "_def" 93 o Long_Name.base_name) cnames; 94 in simp_tac (put_simpset ss ctxt addsimps unfolds) n 95 end); 96 97fun convert_impls ctxt = let 98 99 val thm = Proof_Context.get_thm ctxt "\<Gamma>_def" 100 101 val proc_defs = (Term.add_const_names (Thm.concl_of thm) []) 102 |> filter (String.isSuffix Hoare.proc_deco) 103 |> map (suffix "_def" #> Proof_Context.get_thm ctxt) 104 105 val tree_lemmata = StaticFun.prove_partial_map_thms thm 106 (ctxt addsimps proc_defs) 107 108 fun impl_name_from_proc (Const (s, _)) = s 109 |> Long_Name.base_name 110 |> unsuffix Hoare.proc_deco 111 |> suffix HoarePackage.implementationN 112 | impl_name_from_proc t = raise TERM ("impl_name_from_proc", [t]) 113 114 val saves = tree_lemmata |> map (apfst (fst #> impl_name_from_proc)) 115 116 in Local_Theory.notes (map (fn (n, t) => ((Binding.name n, []), [([t], [])])) saves) 117 ctxt |> snd end 118 119fun take_all_actions prefix src_ctxt proc tm csenv 120 styargs ctxt = let 121 val (_, ctxt) = convert prefix src_ctxt proc tm (Termtab.empty, ctxt); 122 in ctxt 123 |> convert_impls 124 |> Modifies_Proofs.prove_all_modifies_goals_local csenv (fn _ => true) styargs 125 end 126 127end 128 129*} 130 131ML {* 132fun com_rewrite f t = case fastype_of t of 133 (comT as Type (@{type_name com}, [s, _, ft])) 134 => let 135 val gd = Const (@{const_name Guard}, 136 ft --> (HOLogic.mk_setT s) --> comT --> comT) 137 fun add_guard ((f, gd_s), c) = gd $ f $ gd_s $ c; 138 139 val seq = Const (@{const_name Seq}, comT --> comT --> comT); 140 val skip = Const (@{const_name Skip}, comT); 141 fun add_guards_to_seq gs (Const (@{const_name Seq}, _) $ a $ b) 142 = seq $ add_guards_to_seq gs a $ b 143 | add_guards_to_seq gs c 144 = seq $ foldr add_guard skip gs $ c; 145 146 fun add_guards c [] = c 147 | add_guards ((w as Const (@{const_name While}, _)) $ S $ c) gs 148 = seq $ (w $ S $ add_guards_to_seq gs c) $ foldr add_guard skip gs 149 | add_guards (call as (Const (@{const_name call}, _) $ _ $ _ $ _ $ _)) gs 150 = foldr add_guard (seq $ call $ foldr add_guard skip gs) gs 151 | add_guards c gs = foldr add_guard c gs; 152 153 fun inner t = case t of 154 (Const (@{const_name "switch"}, T) $ v $ set_com_list) => let 155 val (ss, cs) = map_split HOLogic.dest_prod 156 (HOLogic.dest_list set_com_list); 157 val cs' = map inner cs; 158 val (v', gs) = f v; 159 val (ss', gss) = map_split f ss; 160 val listT = HOLogic.mk_prodT 161 (HOLogic.mk_setT (range_type (domain_type T)), comT); 162 in foldr add_guard (head_of t $ v' $ HOLogic.mk_list listT 163 (map HOLogic.mk_prod (ss' ~~ cs'))) 164 (gs @ flat gss) 165 end 166 | _ => let 167 val (h, xs) = strip_comb t; 168 (* assumption: we can only get into the com type with one of the 169 constructors or pseudo-constructors, which don't need rewriting, 170 so we can ignore h *) 171 val xTs = xs ~~ (fastype_of h |> strip_type |> fst); 172 fun upd_arg (x, T) = if T = comT then (inner x, []) else f x; 173 val (ys, gss) = map_split upd_arg xTs; 174 in add_guards (list_comb (h, ys)) (flat gss) end 175 in inner (Envir.beta_eta_contract t) end 176 | _ => t; 177 178*} 179 180setup {* DefineGlobalsList.define_globals_list_i 181 "../c/build/$L4V_ARCH/kernel_all.c_pp" @{typ globals} *} 182 183 184locale substitute_pre 185 = fixes symbol_table :: "string \<Rightarrow> addr" 186 and domain :: "addr set" 187 188begin 189 190abbreviation 191 "globals_list \<equiv> kernel_all_global_addresses.global_data_list" 192 193end 194 195locale kernel_all_substitute = substitute_pre 196begin 197 198ML {* 199fun mk_rew (t as Abs (s, T, _)) = mk_rew (betapply (t, Var ((s, 0), T))) 200 | mk_rew t = HOLogic.dest_eq t 201 202val mk_varifyT = Term.map_types Logic.varifyT_global 203 204local 205val c_guard_rew = 206 @{term "\<lambda>p b. Guard C_Guard {s. c_guard (p s)} b 207 = Guard C_Guard {s. h_t_valid (hrs_htd (t_hrs_' (globals s))) c_guard (p s)} b"} 208 |> mk_varifyT |> mk_rew 209 210val c_guard_rew_weak = 211 @{term "\<lambda>p b. Guard C_Guard {s. c_guard (p s)} b 212 = Guard C_Guard {s. ptr_safe (p s) (hrs_htd (t_hrs_' (globals s))) 213 \<and> c_guard (p s)} b"} 214 |> mk_varifyT |> mk_rew 215 216in 217fun strengthen_c_guards ss thy s = 218 if (exists (curry (=) s) ss) 219 then Pattern.rewrite_term thy [c_guard_rew_weak] [] 220 else Pattern.rewrite_term thy [c_guard_rew] [] 221end; 222*} 223 224lemmas global_data_defs 225 = kernel_all_global_addresses.global_data_defs 226 227lemmas globals_list_def 228 = kernel_all_global_addresses.global_data_list_def 229 230ML {* 231 232(* the unvarify sets ?symbol_table back to symbol_table. be careful *) 233val global_datas = @{thms global_data_defs} 234 |> map (Thm.concl_of #> Logic.unvarify_global 235 #> Logic.dest_equals #> snd #> Envir.beta_eta_contract) 236 237val const_globals = map_filter 238 (fn (Const (@{const_name const_global_data}, _) $ nm $ t) 239 => SOME (HOLogic.dest_string nm, t) 240 | _ => NONE) global_datas 241 242local 243 244val hrs_htd_update_guard_rew1 = 245 @{term "\<lambda>u. Basic (\<lambda>s. globals_update (t_hrs_'_update (hrs_htd_update (u s))) s) 246 = Guard C_Guard {s. globals_list_distinct (fst ` dom_s (u s (hrs_htd (t_hrs_' (globals s))))) 247 symbol_table globals_list} 248 (Basic (\<lambda>s. globals_update (t_hrs_'_update (id hrs_htd_update (u s))) s))"} 249 |> mk_rew 250 251val hrs_htd_update_guard_rew2 = 252 @{term "t_hrs_'_update (id hrs_htd_update f) = t_hrs_'_update (hrs_htd_update f)"} 253 |> Logic.varify_global |> HOLogic.dest_eq; 254 255val consts = map snd const_globals 256 257val index_eq_set_helper 258 = Syntax.parse_term @{context} (String.concat 259 ["\<lambda>str t n c. {s :: globals myvars. c \<longrightarrow>", 260 "h_val (hrs_mem (t_hrs_' (globals s)))", 261 " (CTypesDefs.ptr_add (Ptr (symbol_table str)) (of_nat (n s)))", 262 " = t s}"]) 263 264val eq_set_helper 265 = Syntax.parse_term @{context} (String.concat 266 ["\<lambda>str t c. {s :: globals myvars. c \<longrightarrow>", 267 "h_val (hrs_mem (t_hrs_' (globals s)))", 268 " (Ptr (symbol_table str)) = t}"]) 269 270val s = @{term "s :: globals myvars"} 271 272val grab_name_str = head_of #> dest_Const #> fst #> Long_Name.base_name 273 #> HOLogic.mk_string 274 275in 276 277fun const_global_asserts ctxt cond 278 (t as (Const (@{const_name index}, _) $ arr $ n)) = if member (=) consts arr 279 then [(index_eq_set_helper $ grab_name_str arr 280 $ lambda s t $ lambda s n $ cond) |> Syntax.check_term ctxt] 281 else [] 282 | const_global_asserts ctxt cond (Const c) = if member (=) consts (Const c) 283 then [(eq_set_helper $ grab_name_str (Const c) $ Const c $ cond) 284 |> Syntax.check_term ctxt] 285 else [] 286 | const_global_asserts ctxt cond (f $ x) = if member (=) consts (f $ x) 287 then [(eq_set_helper $ grab_name_str (f $ x) $ (f $ x) $ cond) 288 |> Syntax.check_term ctxt] 289 else const_global_asserts ctxt cond f @ const_global_asserts ctxt cond x 290 | const_global_asserts ctxt cond (a as Abs (_, @{typ "globals myvars"}, _)) 291 = const_global_asserts ctxt cond (betapply (a, s)) 292 | const_global_asserts ctxt cond (Abs (_, _, t)) 293 = const_global_asserts ctxt cond t 294 | const_global_asserts _ _ _ = [] 295 296fun guard_rewritable_globals const_cond ctxt = 297 Pattern.rewrite_term @{theory} [hrs_htd_update_guard_rew2] [] 298 o Pattern.rewrite_term @{theory} [hrs_htd_update_guard_rew1] [] 299 o com_rewrite (fn t => 300 (t, map (pair @{term C_Guard}) 301 (case const_cond of SOME cond => const_global_asserts ctxt cond t 302 | NONE => []))) 303 304val guard_htd_updates_with_domain = com_rewrite 305 (fn t => if fastype_of t = @{typ "globals myvars \<Rightarrow> globals myvars"} 306 andalso Term.exists_Const (fn (s, _) => s = @{const_name "hrs_htd_update"}) t 307 then (t, [(@{term MemorySafety}, betapply (@{term "\<lambda>f :: globals myvars \<Rightarrow> globals myvars. 308 {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) 309 \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (f s))))}"}, t))]) 310 else (t, [])) 311 312val guard_halt = com_rewrite 313 (fn t => if t = @{term "halt_'proc"} 314 then (t, [(@{term DontReach}, @{term "{} :: globals myvars set"})]) 315 else (t, [])) 316 317fun acc_ptr_adds (Const (@{const_name h_val}, _) $ m $ (Const (@{const_name ptr_add}, _) $ p $ n)) 318 = [(p, n, true)] @ maps acc_ptr_adds [m, p, n] 319 | acc_ptr_adds (Const (@{const_name heap_update}, _) $ (Const (@{const_name ptr_add}, _) $ p $ n)) 320 = [(p, n, true)] @ maps acc_ptr_adds [p, n] 321 | acc_ptr_adds (Const (@{const_name ptr_add}, _) $ p $ n) 322 = [(p, n, false)] @ maps acc_ptr_adds [p, n] 323 | acc_ptr_adds (f $ x) = maps acc_ptr_adds [f, x] 324 | acc_ptr_adds (abs as Abs (_, T, t)) = if T = @{typ "globals myvars"} 325 then acc_ptr_adds (betapply (abs, @{term "s :: globals myvars"})) 326 else acc_ptr_adds t 327 | acc_ptr_adds _ = [] 328 329fun mk_bool true = @{term True} | mk_bool false = @{term False} 330 331val guard_acc_ptr_adds = com_rewrite 332 (fn t => (t, acc_ptr_adds t |> map (fn (p, n, strong) => let 333 val assn = Const (@{const_name ptr_add_assertion'}, 334 fastype_of p --> @{typ "int \<Rightarrow> bool \<Rightarrow> heap_typ_desc \<Rightarrow> bool"}) 335 $ p $ n $ mk_bool strong 336 $ @{term "hrs_htd (t_hrs_' (globals (s :: globals myvars)))"} 337 val gd = HOLogic.mk_Collect ("s", @{typ "globals myvars"}, assn) 338 in (@{term MemorySafety}, gd) end))) 339 340end 341 342*} 343 344cond_sorry_modifies_proofs SORRY_MODIFIES_PROOFS 345 346local_setup {* 347SubstituteSpecs.take_all_actions 348 "Kernel_C.kernel_all_global_addresses." 349 (Locale.init "Kernel_C.kernel_all_global_addresses" @{theory}) 350 (fn ctxt => fn s => guard_rewritable_globals NONE ctxt 351 o (strengthen_c_guards ["memset_body", "memcpy_body", "memzero_body"] 352 (Proof_Context.theory_of ctxt) s) 353 o guard_halt 354 o guard_htd_updates_with_domain 355 o guard_acc_ptr_adds) 356 @{term kernel_all_global_addresses.\<Gamma>} 357 (CalculateState.get_csenv @{theory} "../c/build/$L4V_ARCH/kernel_all.c_pp" |> the) 358 [@{typ "globals myvars"}, @{typ int}, @{typ strictc_errortype}] 359*} 360 361end 362 363end 364