Refactor C translation around an explicit ABI and pointer model

.github/actions/setup-isabelle-action/action.yml

@@ -11,6 +11,16 @@ runs:
         repository: isabelle-prover/mirror-afp-2025-1
         path: afp
 
+    - name: Patch AFP Isabelle/C parser
+      shell: bash
+      run: |
+        TARGET=afp/thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Language.thy
+        sed -i \
+          '/| (CDecl0 (\[CTypeSpec0 (CIntType0 _)\], \[\], _)) => ("int",decl)/{
+            n
+            c\                  | (CDecl0 (_, [((Some (CDeclr0 (nameIdent,_,_,_,_)),_),_)], _)) =>\n                      (getVarName nameIdent, decl)\n                  | (CDecl0 (_, [], _)) => ("unknown", decl)\n                  | dd => ("unknown", dd)
+          }' "$TARGET"
+
     - name: Set AFP component base
       shell: bash
       run: |

.github/patches/isabelle_c_parser_language.patch

@@ -0,0 +1,16 @@
+--- a/thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Language.thy
++++ b/thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Language.thy
+@@ -344,8 +344,11 @@
+                   | (CDecl0 ([CTypeSpec0 (CSignedType0 _)], [], _)) => ("signed",decl)
+                   | (CDecl0 ([CTypeSpec0 (CUnsigType0 _)], [], _)) => ("unsigned",decl)
+                   | (CDecl0 ([CTypeSpec0 (CBoolType0 _)], [], _)) => ("bool",decl)
+-                  | (CDecl0 ([CTypeSpec0 (CIntType0 _)], [], _)) => ("int",decl)
+-                  | dd => error ("unknown declaration format : "^ @{make_string} dd)
++                  | (CDecl0 ([CTypeSpec0 (CIntType0 _)], [], _)) => ("int",decl)
++                  | (CDecl0 (_, [((Some (CDeclr0 (nameIdent,_,_,_,_)),_),_)], _)) =>
++                      (getVarName nameIdent, decl)
++                  | (CDecl0 (_, [], _)) => ("unknown", decl)
++                  | dd => ("unknown", dd)
+     in
+     case ident of [CFunDeclr0 (Right (declarations,_),_,_)] => Some (map transformDeclaration declarations)
+                                                | _ => None

AutoCorrode.thy

@@ -18,11 +18,14 @@ theory AutoCorrode
     "Micro_C_Parsing_Frontend.C_To_Core_Translation"
     "Micro_C_Parsing_Frontend.C_File_Load_Smoke"
     "Micro_C_Parsing_Frontend.C_Parser_Smoke"
+    "Micro_C_Parsing_Frontend.C_Translation_Smoke_Advanced"
     "Micro_C_Parsing_Frontend.C_Translation_Smoke_Control"
     "Micro_C_Parsing_Frontend.C_Translation_Smoke_Core"
     "Micro_C_Parsing_Frontend.C_Translation_Smoke_Memory"
     "Micro_C_Parsing_Frontend.C_Translation_Smoke_Options"
     "Micro_C_Parsing_Frontend.C_Translation_Smoke_Types"
+    "Micro_C_Parsing_Frontend.C_Translation_Smoke_ILP32"
+    "Micro_C_Parsing_Frontend.C_Translation_Smoke_Compiler"
     "Shallow_Micro_C.C_Arithmetic_Rules"
     "Shallow_Micro_C.C_Abort"
     "Shallow_Micro_C.C_Abort_Rules"
@@ -40,6 +43,7 @@ theory AutoCorrode
     "Micro_C_Examples.C_Void_Pointer_Examples"
     "Micro_C_Examples.C_Union_Examples"
     "Micro_C_Examples.C_Byte_Refinement"
+    "Micro_C_Examples.C_Misc_Examples"
     "Misc.Misc"
     "Lenses_And_Other_Optics.Lenses_And_Other_Optics"
     "Separation_Lenses.Separation_Lenses"

Micro_C_Examples/C_ABI_Examples.thy

@@ -14,10 +14,21 @@ text \<open>
 \<close>
 
 locale c_char_uint_verification_ctx =
+    c_pointer_model c_ptr_add c_ptr_shift_signed c_ptr_diff c_ptr_less c_ptr_le c_ptr_greater c_ptr_ge
+      c_ptr_to_uintptr c_uintptr_to_ptr +
     reference reference_types +
     ref_c_char: reference_allocatable reference_types _ _ _ _ _ _ _ c_char_prism +
     ref_c_uint: reference_allocatable reference_types _ _ _ _ _ _ _ c_uint_prism
-  for reference_types :: \<open>'s::{sepalg} \<Rightarrow> 'addr \<Rightarrow> 'gv \<Rightarrow> c_abort \<Rightarrow> 'i prompt \<Rightarrow>
+  for c_ptr_add :: \<open>('addr, 'gv) gref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ('addr, 'gv) gref\<close>
+  and c_ptr_shift_signed :: \<open>('addr, 'gv) gref \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> ('addr, 'gv) gref\<close>
+  and c_ptr_diff :: \<open>('addr, 'gv) gref \<Rightarrow> ('addr, 'gv) gref \<Rightarrow> nat \<Rightarrow> int\<close>
+  and c_ptr_less :: \<open>('addr, 'gv) gref \<Rightarrow> ('addr, 'gv) gref \<Rightarrow> bool\<close>
+  and c_ptr_le :: \<open>('addr, 'gv) gref \<Rightarrow> ('addr, 'gv) gref \<Rightarrow> bool\<close>
+  and c_ptr_greater :: \<open>('addr, 'gv) gref \<Rightarrow> ('addr, 'gv) gref \<Rightarrow> bool\<close>
+  and c_ptr_ge :: \<open>('addr, 'gv) gref \<Rightarrow> ('addr, 'gv) gref \<Rightarrow> bool\<close>
+  and c_ptr_to_uintptr :: \<open>('addr, 'gv) gref \<Rightarrow> int\<close>
+  and c_uintptr_to_ptr :: \<open>int \<Rightarrow> ('addr, 'gv) gref\<close>
+  and reference_types :: \<open>'s::{sepalg} \<Rightarrow> 'addr \<Rightarrow> 'gv \<Rightarrow> c_abort \<Rightarrow> 'i prompt \<Rightarrow>
         'o prompt_output \<Rightarrow> unit\<close>
   and c_char_prism :: \<open>('gv, c_char) prism\<close>
   and c_uint_prism :: \<open>('gv, c_uint) prism\<close>
@@ -26,8 +37,15 @@ begin
 adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_char.new
 adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_uint.new
 adhoc_overloading store_update_const \<rightleftharpoons> update_fun
+adhoc_overloading c_void_cast_prism_for \<rightleftharpoons> c_char_prism
 adhoc_overloading c_void_cast_prism_for \<rightleftharpoons> c_uint_prism
 
+definition c_char_ref_at :: \<open>('addr, 'gv, c_char) Global_Store.ref \<Rightarrow> nat \<Rightarrow> ('addr, 'gv, c_char) Global_Store.ref\<close> where
+  \<open>c_char_ref_at buf i \<equiv>
+    make_focused
+      (c_ptr_add (unwrap_focused buf) i (c_sizeof TYPE(c_char)))
+      (get_focus buf)\<close>
+
 definition be32_from_bytes4 :: \<open>c_char list \<Rightarrow> c_uint\<close> where
   \<open>be32_from_bytes4 vs \<equiv>
       (push_bit 24 (ucast (vs ! 0) :: c_uint))
@@ -81,18 +99,29 @@ lemma wire_le_abi_profile_values:
 by (simp_all add: wire_le_abi_pointer_bits_def wire_le_abi_long_bits_def wire_le_abi_big_endian_def)
 
 definition wire_le_load_be32_portable_contract ::
-  \<open>('addr, 'gv, c_char list) Global_Store.ref \<Rightarrow> 'gv \<Rightarrow> c_char list \<Rightarrow>
+  \<open>('addr, 'gv, c_char) Global_Store.ref \<Rightarrow> c_char \<Rightarrow> c_char \<Rightarrow> c_char \<Rightarrow> c_char \<Rightarrow>
     ('s::{sepalg}, c_uint, 'b) function_contract\<close> where
-  [crush_contracts]: \<open>wire_le_load_be32_portable_contract buf bg vs \<equiv>
-    let pre  = buf \<mapsto>\<langle>\<top>\<rangle> bg\<down>vs \<star> \<langle>3 < size buf\<rangle> \<star> \<langle>length vs \<ge> 4\<rangle>;
-        post = \<lambda>r. buf \<mapsto>\<langle>\<top>\<rangle> bg\<down>vs \<star> \<langle>r = be32_from_bytes4 vs\<rangle>
+  [crush_contracts]: \<open>wire_le_load_be32_portable_contract buf b0 b1 b2 b3 \<equiv>
+    let r0 = c_char_ref_at buf 0;
+        r1 = c_char_ref_at buf 1;
+        r2 = c_char_ref_at buf 2;
+        r3 = c_char_ref_at buf 3;
+        pre  = (\<Squnion>g0. r0 \<mapsto>\<langle>\<top>\<rangle> g0\<down>b0)
+             \<star> (\<Squnion>g1. r1 \<mapsto>\<langle>\<top>\<rangle> g1\<down>b1)
+             \<star> (\<Squnion>g2. r2 \<mapsto>\<langle>\<top>\<rangle> g2\<down>b2)
+             \<star> (\<Squnion>g3. r3 \<mapsto>\<langle>\<top>\<rangle> g3\<down>b3);
+        post = \<lambda>r. (\<Squnion>g0. r0 \<mapsto>\<langle>\<top>\<rangle> g0\<down>b0)
+             \<star> (\<Squnion>g1. r1 \<mapsto>\<langle>\<top>\<rangle> g1\<down>b1)
+             \<star> (\<Squnion>g2. r2 \<mapsto>\<langle>\<top>\<rangle> g2\<down>b2)
+             \<star> (\<Squnion>g3. r3 \<mapsto>\<langle>\<top>\<rangle> g3\<down>b3)
+             \<star> \<langle>r = be32_from_bytes4 [b0, b1, b2, b3]\<rangle>
      in make_function_contract pre post\<close>
 ucincl_auto wire_le_load_be32_portable_contract
 
 lemma wire_le_load_be32_portable_spec [crush_specs]:
-  shows \<open>\<Gamma>; wire_le_load_be32_portable buf \<Turnstile>\<^sub>F wire_le_load_be32_portable_contract buf bg vs\<close>
+  shows \<open>\<Gamma>; wire_le_load_be32_portable buf \<Turnstile>\<^sub>F wire_le_load_be32_portable_contract buf b0 b1 b2 b3\<close>
   apply (crush_boot f: wire_le_load_be32_portable_def contract: wire_le_load_be32_portable_contract_def)
-  apply (crush_base simp add: be32_from_bytes4_def c_unsigned_or_def c_unsigned_shl_def c_ucast_def)
+  apply (crush_base simp add: c_char_ref_at_def be32_from_bytes4_def c_unsigned_or_def c_unsigned_shl_def c_ucast_def)
   apply (simp add: ac_simps)
   done
 
@@ -143,18 +172,29 @@ lemma wire_be_abi_profile_values:
 by (simp_all add: wire_be_abi_pointer_bits_def wire_be_abi_long_bits_def wire_be_abi_big_endian_def)
 
 definition wire_be_load_be32_portable_contract ::
-  \<open>('addr, 'gv, c_char list) Global_Store.ref \<Rightarrow> 'gv \<Rightarrow> c_char list \<Rightarrow>
+  \<open>('addr, 'gv, c_char) Global_Store.ref \<Rightarrow> c_char \<Rightarrow> c_char \<Rightarrow> c_char \<Rightarrow> c_char \<Rightarrow>
     ('s::{sepalg}, c_uint, 'b) function_contract\<close> where
-  [crush_contracts]: \<open>wire_be_load_be32_portable_contract buf bg vs \<equiv>
-    let pre  = buf \<mapsto>\<langle>\<top>\<rangle> bg\<down>vs \<star> \<langle>3 < size buf\<rangle> \<star> \<langle>length vs \<ge> 4\<rangle>;
-        post = \<lambda>r. buf \<mapsto>\<langle>\<top>\<rangle> bg\<down>vs \<star> \<langle>r = be32_from_bytes4 vs\<rangle>
+  [crush_contracts]: \<open>wire_be_load_be32_portable_contract buf b0 b1 b2 b3 \<equiv>
+    let r0 = c_char_ref_at buf 0;
+        r1 = c_char_ref_at buf 1;
+        r2 = c_char_ref_at buf 2;
+        r3 = c_char_ref_at buf 3;
+        pre  = (\<Squnion>g0. r0 \<mapsto>\<langle>\<top>\<rangle> g0\<down>b0)
+             \<star> (\<Squnion>g1. r1 \<mapsto>\<langle>\<top>\<rangle> g1\<down>b1)
+             \<star> (\<Squnion>g2. r2 \<mapsto>\<langle>\<top>\<rangle> g2\<down>b2)
+             \<star> (\<Squnion>g3. r3 \<mapsto>\<langle>\<top>\<rangle> g3\<down>b3);
+        post = \<lambda>r. (\<Squnion>g0. r0 \<mapsto>\<langle>\<top>\<rangle> g0\<down>b0)
+             \<star> (\<Squnion>g1. r1 \<mapsto>\<langle>\<top>\<rangle> g1\<down>b1)
+             \<star> (\<Squnion>g2. r2 \<mapsto>\<langle>\<top>\<rangle> g2\<down>b2)
+             \<star> (\<Squnion>g3. r3 \<mapsto>\<langle>\<top>\<rangle> g3\<down>b3)
+             \<star> \<langle>r = be32_from_bytes4 [b0, b1, b2, b3]\<rangle>
      in make_function_contract pre post\<close>
 ucincl_auto wire_be_load_be32_portable_contract
 
 lemma wire_be_load_be32_portable_spec [crush_specs]:
-  shows \<open>\<Gamma>; wire_be_load_be32_portable buf \<Turnstile>\<^sub>F wire_be_load_be32_portable_contract buf bg vs\<close>
+  shows \<open>\<Gamma>; wire_be_load_be32_portable buf \<Turnstile>\<^sub>F wire_be_load_be32_portable_contract buf b0 b1 b2 b3\<close>
   apply (crush_boot f: wire_be_load_be32_portable_def contract: wire_be_load_be32_portable_contract_def)
-  apply (crush_base simp add: be32_from_bytes4_def c_unsigned_or_def c_unsigned_shl_def c_ucast_def)
+  apply (crush_base simp add: c_char_ref_at_def be32_from_bytes4_def c_unsigned_or_def c_unsigned_shl_def c_ucast_def)
   apply (simp add: ac_simps)
   done
 
@@ -182,6 +222,39 @@ lemma wire_be_u32_prism_is_be:
   shows \<open>wire_be_u32_prism = c_uint_byte_prism_be\<close>
   by (simp add: wire_be_u32_prism_def c_endianness_of_bool_def c_uint_byte_prism_of_def wire_be_abi_big_endian_def)
 
+section \<open>Raw Struct Field Address Regression\<close>
+
+text \<open>
+  Regression for raw @{verbatim "void *"} cast to struct pointer followed by
+  address-of field extraction and a helper that immediately reinterprets the
+  resulting field pointer as bytes.
+\<close>
+
+micro_c_translate prefix: raw_struct_ abi: ilp32-le \<open>
+  typedef unsigned char uint8_t;
+  typedef unsigned int uint32_t;
+
+  struct pair {
+    uint32_t x;
+    uint32_t y;
+  };
+
+  static uint32_t load_be32(const uint32_t *p) {
+    const uint8_t *bp = (const uint8_t *)p;
+    return ((uint32_t)bp[0] << 24)
+         | ((uint32_t)bp[1] << 16)
+         | ((uint32_t)bp[2] << 8)
+         |  (uint32_t)bp[3];
+  }
+
+  uint32_t read_pair_y_be(const void *p) {
+    return load_be32(&((const struct pair *)p)->y);
+  }
+\<close>
+
+thm raw_struct_load_be32_def
+thm raw_struct_read_pair_y_be_def
+
 end
 
 end