Merge pull request #159 in SEL4/l4v from ~TSEWELL/l4v:length-1-array to master

* commit 'dbd226f899c83ae0b44d58446b88d2dd0fb67a83':
  SimplExportAndRefine: length 1 arrays.

tools/asmrefine/ProveGraphRefine.thy

@@ -74,6 +74,7 @@ lemma unat_mono_thms:
 lemma unat_mono_intro:
   "unat a \<le> x \<Longrightarrow> x < b \<Longrightarrow> unat a < b"
   "unat a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> unat a \<le> b"
+  "unat a \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> unat a = 0"
   by simp_all
 
 lemma word_neq_0_conv_neg_conv:

tools/asmrefine/SimplExport.thy

@@ -175,7 +175,8 @@ type export_params = {cons_field_upds: term -> term,
 
 fun get_all_export_params ctxt csenv : export_params = let
     (* assuming DefineGlobalsList has already run *)
-    val defs = Proof_Context.get_thms ctxt "global_data_defs"
+    val defs = if (can (Proof_Context.get_thms ctxt) "no_global_data_defs")
+      then [] else Proof_Context.get_thms ctxt "global_data_defs"
     val rhss = map (Thm.concl_of #> Logic.dest_equals #> snd) defs
     val const_globals = map_filter
       (fn (Const (@{const_name const_global_data}, _) $ nm $ v)

tools/asmrefine/testfiles/global_array_swap.c

@@ -85,4 +85,30 @@ update_a_global (int x) {
   a_modified_global = x;
 }
 
+/* small const global array */
+typedef int reference_val;
+
+static const reference_val a_reference_array[] = {
+        12
+};
+
+static int
+get_num_reference_vals(void)
+{
+    return sizeof(a_reference_array) / sizeof(reference_val);
+}
+
+static reference_val
+get_reference_val(int i, int extra_param)
+{
+    reference_val ref = a_reference_array[i];
+
+    if (ref < extra_param) {
+      return 0;
+    }
+    else {
+      return ref;
+    }
+}
+
 

tools/asmrefine/testfiles/global_array_swap_gref.thy

@@ -158,7 +158,7 @@ ML {* ProveSimplToGraphGoals.test_all_graph_refine_proofs_parallel
 
 text {* Manual test for debugging. *}
 
-ML {* val nm = "global_array_swap.add_a_thing" *}
+ML {* val nm = "global_array_swap.get_reference_val" *}
 
 local_setup {* define_graph_fun_short funs nm *}
 
@@ -191,6 +191,8 @@ val debug_tac = ProveSimplToGraphGoals.debug_tac
 schematic_goal "PROP ?P"
   apply (tactic {* resolve_tac @{context} [init_thm] 1 *})
   apply (tactic {* ALLGOALS (TRY o (debug_tac @{context} THEN_ALL_NEW K no_tac)) *})
+
+  apply (tactic {* ALLGOALS (debug_tac @{context}) *})
   oops
 
 end