Try to avoid emitting const-globals via memory.

Sometimes it's simpler to access an unknown field of a const
global by just computing the offset from its symbol in memory
and assuming the relevant words are in the .rodata section. But
for known fields, it's easier to just figure out what the
constant value is. This complicates the proof slightly, since
it has to guess which case it is in.

proof/asmrefine/SEL4GraphRefine.thy

@@ -32,8 +32,7 @@ val csenv = let
     val the_csenv = CalculateState.get_csenv @{theory} "c/kernel_all.c_pp" |> the
   in fn () => the_csenv end
 *}
-term ghost_assertion_data_get
-term ghost'state_'
+
 consts
   encode_machine_state :: "machine_state \<Rightarrow> unit \<times> nat"
 
@@ -65,7 +64,7 @@ lemma snd_snd_gs_new_frames_new_cnodes[simp]:
   by (simp_all add: gs_new_frames_def gs_new_cnodes_def gs_clear_region_def)
 
 (*
-ML {* val nm = "Kernel_C.memcpy" *}
+ML {* val nm = "Kernel_C.resolveVAddr" *}
 
 local_setup {*  define_graph_fun_short funs nm *}
 

tools/asmrefine/FieldAccessors.thy

@@ -262,7 +262,7 @@ fun add_field_h_val_rewrites lthy =
   Local_Theory.note ((@{binding field_h_val_rewrites}, []),
       get_field_h_val_rewrites lthy) lthy |> snd
 *}
-ML Global_Theory.facts_of
+
 ML {*
 fun get_field_to_bytes_rewrites lthy = let
     val fl_thms = Global_Theory.facts_of (Proof_Context.theory_of lthy)

tools/asmrefine/ProveGraphRefine.thy

@@ -360,13 +360,33 @@ fun get_globals_rewrites ctxt = let
         handle ERROR _ => raise THM
             ("run add_globals_swap_rewrites on ctxt", 1, [])
 
-fun normalise_mem_accs ctxt = DETERM o let
+fun add_symbols (Free (_, T) $ s) xs = (case try HOLogic.dest_string s
+        of SOME str => str :: xs | _ => xs)
+  | add_symbols (f $ x) xs = add_symbols f (add_symbols x xs)
+  | add_symbols (Abs (_, _, t)) xs = add_symbols t xs
+  | add_symbols _ xs = xs
+
+fun get_symbols t = add_symbols t [] |> Ord_List.make fast_string_ord
+
+fun adj_globals_rewrite_for_symbols ctxt symbs thm = let
+    (* we don't want to do rewrites that introduce symbols that
+       aren't already in the goal. instead we just unfold those
+       constant globals *)
+    val t_symbs = get_symbols (Thm.concl_of thm)
+    val (c, _) = Thm.concl_of thm |> HOLogic.dest_Trueprop
+      |> HOLogic.dest_eq |> fst |> dest_Const
+  in if Ord_List.subset fast_string_ord (t_symbs, symbs)
+    then thm
+    else Proof_Context.get_thm ctxt (c ^ "_def") end
+
+fun normalise_mem_accs ctxt = DETERM o SUBGOAL (fn (t, i) => let
+    val gr = get_globals_rewrites ctxt
+    val symbs = get_symbols t
     val init_simps = @{thms hrs_mem_update
                        heap_access_Array_element'
                        o_def
             } @ get_field_h_val_rewrites ctxt
-        @ #2 (get_globals_rewrites ctxt)
-        @ #1 (get_globals_rewrites ctxt)
+        @ #1 gr @ map (adj_globals_rewrite_for_symbols ctxt symbs) (#2 gr)
     val h_val = get_disjoint_h_val_globals_swap ctxt
     val disjoint_h_val_tac
     = (eqsubst_asm_wrap_tac ctxt [h_val] ORELSE' eqsubst_wrap_tac ctxt [h_val])
@@ -389,7 +409,7 @@ fun normalise_mem_accs ctxt = DETERM o let
               => prove_ptr_safe "normalise_mem_accs" ctxt i
             | _ => all_tac)
     THEN_ALL_NEW full_simp_tac (ctxt addsimps @{thms h_val_ptr h_val_word32 h_val_word8})
-  end
+  end i)
 
 val heap_update_id_nonsense
     = Thm.trivial @{cpat "Trueprop

tools/asmrefine/SimplExport.thy

@@ -244,7 +244,7 @@ fun dest_global_mem_acc_addr (params : export_params) t = let
     val const = #const_globals params t
     val T = fastype_of t
   in case (const, acc) of
-      (SOME nm, _) => SOME (TermsTypes.mk_global_addr_ptr (nm, T))
+      (SOME _, _) => NONE
     | (NONE, SOME nm) => SOME (TermsTypes.mk_global_addr_ptr (nm, T))
     | (NONE, NONE) => NONE
   end
@@ -514,6 +514,26 @@ fun mk_acc_array i xs = let
       | inner [] = error "mk_acc_array: empty"
   in inner (xs ~~ (0 upto (n - 1))) end
 
+fun phase2_convert_global ctxt params accs
+    ((idx as Const (@{const_name Arrays.index}, _)) $ i $ t)
+    = phase2_convert_global ctxt params ((idx $ try_norm_index ctxt i) :: accs) t
+  | phase2_convert_global ctxt params accs (Const acc $ t)
+    = phase2_convert_global ctxt params (Const acc :: accs) t
+  | phase2_convert_global ctxt params accs t = case #const_globals params t
+  of SOME nm => let
+    val known_offs = forall (fn Const (@{const_name Arrays.index}, _) $ i
+          => (try dest_nat i) <> NONE
+        | _ => true) accs
+    val (c, _) = dest_Const t
+    val c_def = Proof_Context.get_thm ctxt (c ^ "_def")
+    val def_body = safe_mk_meta_eq c_def |> Thm.rhs_of |> Thm.term_of
+        |> Envir.beta_eta_contract
+    val p = TermsTypes.mk_global_addr_ptr (nm, fastype_of t)
+    val t' = if known_offs then def_body else mk_memacc p
+    val t_thm = if known_offs then SOME c_def else NONE
+  in SOME (t', t_thm) end
+    | _ => NONE
+
 fun convert_fetch_ph2 ctxt params [] (t as (Const (@{const_name CTypesDefs.ptr_add}, T) $ _ $ _))
     = convert_fetch_ph2 ctxt params [] (ptr_simp_term ctxt "ptr_add"
         (head_of t $ Free ("p", domain_type T) $ Free ("n", @{typ int})) t)
@@ -523,7 +543,7 @@ fun convert_fetch_ph2 ctxt params [] (t as (Const (@{const_name CTypesDefs.ptr_a
   | convert_fetch_ph2 ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs)
             (t as (Const (@{const_name fupdate}, _) $ _ $ _ $ _)) = let
         val xs = dest_array_init (#cons_field_upds (params : export_params) t)
-      in case (try dest_nat (try_norm_index ctxt i)) of
+      in case (try dest_nat i) of
         SOME i => convert_fetch_ph2 ctxt params accs (nth xs i)
       | NONE => mk_acc_array (convert_fetch_ph2 ctxt params [] i)
             (map (convert_fetch_ph2 ctxt params accs) xs)
@@ -531,7 +551,7 @@ fun convert_fetch_ph2 ctxt params [] (t as (Const (@{const_name CTypesDefs.ptr_a
   | convert_fetch_ph2 ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs)
             (t as (Const (@{const_name FCP}, _) $ _)) = let
         val xs = dest_array_init (#cons_field_upds params t)
-      in case (try dest_nat (try_norm_index ctxt i)) of
+      in case (try dest_nat i) of
         SOME i => convert_fetch_ph2 ctxt params accs (nth xs i)
       | NONE => mk_acc_array (convert_fetch_ph2 ctxt params [] i)
             (map (convert_fetch_ph2 ctxt params accs) xs)
@@ -546,7 +566,7 @@ fun convert_fetch_ph2 ctxt params [] (t as (Const (@{const_name CTypesDefs.ptr_a
          val eq = HOLogic.mk_eq (i, i')
          val eq = ptr_simp_term ctxt "idx_eq_simp" eq eq handle TERM _ => eq
          val x = convert_fetch_ph2 ctxt params accs v
-         val y = convert_fetch_ph2 ctxt params (idx $ try_norm_index ctxt i :: accs) arr'
+         val y = convert_fetch_ph2 ctxt params (idx $ i :: accs) arr'
          val T = fastype_of x
       in case eq of @{term True} => x | @{term False} => y
         | _ => Const (@{const_name If}, HOLogic.boolT --> T --> T --> T)
@@ -568,7 +588,7 @@ fun convert_fetch_ph2 ctxt params [] (t as (Const (@{const_name CTypesDefs.ptr_a
     val T = get_acc_type accs T
     fun canon s [] = mk_pseudo_acc s T
       | canon s (Const (@{const_name Arrays.index}, idxT) $ i :: accs) = (case
-            (try dest_nat (try_norm_index ctxt i))
+            (try dest_nat i)
         of SOME i => canon (s ^ "." ^ string_of_int i) accs
           | NONE => let val (_, n) = dest_arrayT (domain_type idxT)
           in mk_acc_array (convert_fetch_ph2 ctxt params [] i)
@@ -585,9 +605,12 @@ fun convert_fetch_ph2 ctxt params [] (t as (Const (@{const_name CTypesDefs.ptr_a
   | convert_fetch_ph2 ctxt params accs t = let
     val (f, xs) = strip_comb t
     val (c, _) = dest_Const f
+    val cnv = phase2_convert_global ctxt params accs f
+        |> Option.map (fst #> convert_fetch_phase1 params)
   in if (get_field ctxt c |> Option.map #3) = SOME false
     then case xs of [x] => convert_fetch_ph2 ctxt params (f :: accs) x
         | _ => raise TERM ("convert_fetch_ph2: expected single", f :: xs)
+  else if cnv <> NONE then convert_fetch_ph2 ctxt params accs (the cnv)
   else if (get_field ctxt c <> NONE orelse #cons_fields params c <> NONE)
   then let
     val _ = (accs <> []) orelse raise TERM ("convert_fetch_ph2: no accs", [t])