autocorres: add some missing WordAbstract rules.

tools/autocorres/WordAbstract.thy

@@ -583,6 +583,41 @@ lemma corresTA_L2_call_exec_abstract:
   apply fastforce
   done
 
+(* More backup rules for calls. *)
+lemma corresTA_L2_call_exec_concrete':
+  "\<lbrakk> corresTA P f1 x1 A B;
+     valid_typ_abs_fn Q1 Q1' f1 f1';
+     valid_typ_abs_fn Q2 Q2' f2 f2'
+   \<rbrakk> \<Longrightarrow>
+   corresTA (\<lambda>s. \<forall>s'. s = st s' \<longrightarrow> P s') f2 x2
+       (L2_seq (exec_concrete st (L2_call A)) (\<lambda>ret. (L2_seq (L2_guard (\<lambda>_. Q1' ret)) (\<lambda>_. L2_gets (\<lambda>_. f2 (f1' ret)) [''ret'']))))
+       (exec_concrete st (L2_call B))"
+  apply (clarsimp simp: L2_defs L2_call_def corresXF_def)
+  apply (monad_eq split: sum.splits)
+  apply (rule conjI)
+   apply clarsimp
+   apply metis
+  apply clarsimp
+  apply blast
+  done
+
+lemma corresTA_L2_call_exec_abstract':
+  "\<lbrakk> corresTA P f1 x1 A B;
+     valid_typ_abs_fn Q1 Q1' f1 f1';
+     valid_typ_abs_fn Q2 Q2' f2 f2'
+   \<rbrakk> \<Longrightarrow>
+   corresTA (\<lambda>s. P (st s)) f2 x2
+       (L2_seq (exec_abstract st (L2_call A)) (\<lambda>ret. (L2_seq (L2_guard (\<lambda>_. Q1' ret)) (\<lambda>_. L2_gets (\<lambda>_. f2 (f1' ret)) [''ret'']))))
+       (exec_abstract st (L2_call B))"
+  apply (clarsimp simp: L2_defs L2_call_def corresXF_def)
+  apply (monad_eq split: sum.splits)
+  apply (rule conjI)
+   apply metis
+  apply clarsimp
+  apply blast
+  done
+
+
 lemma abstract_val_fun_app:
    "\<lbrakk> abstract_val Q b id b'; abstract_val P a id a' \<rbrakk> \<Longrightarrow>
            abstract_val (P \<and> Q) (f $ (a $ b)) f (a' $ b')"
@@ -846,7 +881,9 @@ lemmas [word_abs] =
   corresTA_L2_unknown
   corresTA_L2_recguard
   corresTA_case_prod
+  corresTA_L2_call_exec_concrete'
   corresTA_L2_call_exec_concrete
+  corresTA_L2_call_exec_abstract'
   corresTA_L2_call_exec_abstract
   corresTA_L2_call'
   corresTA_L2_call

tools/autocorres/tests/proof-tests/WordAbsFnCall.thy

@@ -15,7 +15,8 @@ begin
 install_C_file "word_abs_fn_call.c"
 
 (* Test interaction of abstracted/non-abstracted functions calling the
- * opposite. *)
-autocorres [unsigned_word_abs = bar bar2 foo3 foo4 ] "word_abs_fn_call.c"
+ * opposite. Also test interaction with heap abstraction. *)
+autocorres [ unsigned_word_abs = bar bar2 bar5 bar6 foo3 foo4 foo7 foo8,
+             no_heap_abs = foo3 foo4 foo7 foo8 ] "word_abs_fn_call.c"
 
 end

tools/autocorres/tests/proof-tests/word_abs_fn_call.c

@@ -51,4 +51,44 @@ uint32_t bar4(int a, uint32_t b, uint8_t c)
             return foo4(a, b, foo2(1, 2, 3));
 }
 
+uint8_t foo5(int a, uint32_t b, uint8_t c)
+{
+            return a + b + c;
+}
+
+uint8_t bar5(int a, uint32_t b, uint8_t c)
+{
+            return foo(1, 2, foo(1, 2, 3));
+}
+
+uint32_t foo6(int a, uint32_t b, uint8_t c)
+{
+            return a + b + c;
+}
+
+uint32_t bar6(int a, uint32_t b, uint8_t c)
+{
+            return foo2(a, b, foo2(1, 2, 3));
+}
+
+uint8_t foo7(int a, uint32_t b, uint8_t c)
+{
+            return a + b + c;
+}
+
+uint8_t bar7(int a, uint32_t b, uint8_t c)
+{
+            return foo3(1, 2, foo3(1, 2, 3));
+}
+
+uint32_t foo8(int a, uint32_t b, uint8_t c)
+{
+            return a + b + c;
+}
+
+uint32_t bar8(int a, uint32_t b, uint8_t c)
+{
+            return foo4(a, b, foo2(1, 2, 3));
+}
+