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