From 07cb3d88e3692b68463279e6154f19ce71ecef82 Mon Sep 17 00:00:00 2001 From: Simon Winwood Date: Wed, 26 Jun 2024 22:19:22 +1000 Subject: [PATCH] Make 'a signed word have a different name than 'a word Signed-off-by: Simon Winwood --- tools/autocorres/TypHeapSimple.thy | 3 +- tools/c-parser/UMM_Proofs.ML | 4 +- .../umm_heap/AARCH64/Word_Mem_Encoding.thy | 2 +- .../umm_heap/ARM/Word_Mem_Encoding.thy | 2 +- .../umm_heap/ARM_HYP/Word_Mem_Encoding.thy | 2 +- .../umm_heap/RISCV64/Word_Mem_Encoding.thy | 2 +- tools/c-parser/umm_heap/StructSupport.thy | 6 +- tools/c-parser/umm_heap/Vanilla32.thy | 23 +++---- .../umm_heap/Vanilla32_Preliminaries.thy | 69 ++++++++++++++++++- .../umm_heap/X64/Word_Mem_Encoding.thy | 2 +- 10 files changed, 91 insertions(+), 24 deletions(-) diff --git a/tools/autocorres/TypHeapSimple.thy b/tools/autocorres/TypHeapSimple.thy index d5e303c10a..2378049156 100644 --- a/tools/autocorres/TypHeapSimple.thy +++ b/tools/autocorres/TypHeapSimple.thy @@ -807,7 +807,8 @@ lemmas simple_lift_simps = simple_lift_field_update_t c_guard_array_field nat_to_bin_string_simps - + signed_or_unsigned + (* Old name for the above simpset. *) lemmas typ_simple_heap_simps = simple_lift_simps diff --git a/tools/c-parser/UMM_Proofs.ML b/tools/c-parser/UMM_Proofs.ML index ebd8bbbf77..1e9e59e176 100644 --- a/tools/c-parser/UMM_Proofs.ML +++ b/tools/c-parser/UMM_Proofs.ML @@ -545,8 +545,8 @@ fun umm_struct_calculation ((recname, flds), st, thy) = let Simplifier.asm_full_rewrite ((thy2ctxt thy) addsimps [tag_def_thm, typtag_thm, - @{thm "pad_typ_name_def"}, @{thm "insert_commute"}, - @{thm "nat_to_bin_string.simps"}]) + @{thm "pad_typ_name_def"}, @{thm "insert_commute"}] @ + @{thms "signed_or_unsigned"} @ @{thms "nat_to_bin_string.simps"}) (Thm.cterm_of (thy2ctxt thy) (mk_td_names typtag_lhs)) |> Drule.export_without_context (* Declare the td_names (typ_info_t ..) = ... and add it to the simpset *) diff --git a/tools/c-parser/umm_heap/AARCH64/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/AARCH64/Word_Mem_Encoding.thy index 2190af6124..25936f2caa 100644 --- a/tools/c-parser/umm_heap/AARCH64/Word_Mem_Encoding.thy +++ b/tools/c-parser/umm_heap/AARCH64/Word_Mem_Encoding.thy @@ -17,6 +17,6 @@ where (len_exp TYPE('a)) \ field_access = \v bs. (rev o word_rsplit) v, field_update = \bs v. (word_rcat (rev bs)::'a::len8 word) \) - (''word'' @ nat_to_bin_string (len_of TYPE('a)))" + (signed_or_unsigned_as_str TYPE('a) @ ''word'' @ nat_to_bin_string (len_of TYPE('a)))" end diff --git a/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy index 92a20f5523..95d04782be 100644 --- a/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy +++ b/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy @@ -12,6 +12,6 @@ begin definition word_tag :: "'a::len8 word itself \ 'a word typ_info" where - "word_tag (w::'a::len8 word itself) \ TypDesc (TypScalar (len_of TYPE('a) div 8) (len_exp TYPE('a)) \ field_access = \v bs. (rev o word_rsplit) v, field_update = \bs v. (word_rcat (rev bs)::'a::len8 word) \) (''word'' @ nat_to_bin_string (len_of TYPE('a)) )" + "word_tag (w::'a::len8 word itself) \ TypDesc (TypScalar (len_of TYPE('a) div 8) (len_exp TYPE('a)) \ field_access = \v bs. (rev o word_rsplit) v, field_update = \bs v. (word_rcat (rev bs)::'a::len8 word) \) (signed_or_unsigned_as_str TYPE('a) @ ''word'' @ nat_to_bin_string (len_of TYPE('a)) )" end diff --git a/tools/c-parser/umm_heap/ARM_HYP/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/ARM_HYP/Word_Mem_Encoding.thy index 92a20f5523..35b66ced2c 100644 --- a/tools/c-parser/umm_heap/ARM_HYP/Word_Mem_Encoding.thy +++ b/tools/c-parser/umm_heap/ARM_HYP/Word_Mem_Encoding.thy @@ -12,6 +12,6 @@ begin definition word_tag :: "'a::len8 word itself \ 'a word typ_info" where - "word_tag (w::'a::len8 word itself) \ TypDesc (TypScalar (len_of TYPE('a) div 8) (len_exp TYPE('a)) \ field_access = \v bs. (rev o word_rsplit) v, field_update = \bs v. (word_rcat (rev bs)::'a::len8 word) \) (''word'' @ nat_to_bin_string (len_of TYPE('a)) )" + "word_tag (w::'a::len8 word itself) \ TypDesc (TypScalar (len_of TYPE('a) div 8) (len_exp TYPE('a)) \ field_access = \v bs. (rev o word_rsplit) v, field_update = \bs v. (word_rcat (rev bs)::'a::len8 word) \) (signed_or_unsigned_as_str TYPE('a) @ ''word'' @ nat_to_bin_string (len_of TYPE('a)) )" end diff --git a/tools/c-parser/umm_heap/RISCV64/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/RISCV64/Word_Mem_Encoding.thy index 2190af6124..25936f2caa 100644 --- a/tools/c-parser/umm_heap/RISCV64/Word_Mem_Encoding.thy +++ b/tools/c-parser/umm_heap/RISCV64/Word_Mem_Encoding.thy @@ -17,6 +17,6 @@ where (len_exp TYPE('a)) \ field_access = \v bs. (rev o word_rsplit) v, field_update = \bs v. (word_rcat (rev bs)::'a::len8 word) \) - (''word'' @ nat_to_bin_string (len_of TYPE('a)))" + (signed_or_unsigned_as_str TYPE('a) @ ''word'' @ nat_to_bin_string (len_of TYPE('a)))" end diff --git a/tools/c-parser/umm_heap/StructSupport.thy b/tools/c-parser/umm_heap/StructSupport.thy index a18f00d3b6..e928be6990 100644 --- a/tools/c-parser/umm_heap/StructSupport.thy +++ b/tools/c-parser/umm_heap/StructSupport.thy @@ -485,15 +485,15 @@ lemma td_names_ptr [simp]: lemma td_names_word8 [simp]: fixes x :: "byte itself" shows "td_names (typ_info_t x) = {''word00010''}" - by (simp add: pad_typ_name_def nat_to_bin_string.simps) + by (simp add: pad_typ_name_def nat_to_bin_string.simps signed_or_unsigned) lemma td_names_word32 [simp]: "td_names (typ_info_t TYPE(32 word)) = {''word0000010''}" - by (simp add: pad_typ_name_def nat_to_bin_string.simps) + by (simp add: pad_typ_name_def nat_to_bin_string.simps signed_or_unsigned) lemma td_names_word64 [simp]: "td_names (typ_info_t TYPE(64 word)) = {''word00000010''}" - by (simp add: pad_typ_name_def nat_to_bin_string.simps) + by (simp add: pad_typ_name_def nat_to_bin_string.simps signed_or_unsigned) lemma td_names_export_uinfo [simp]: "td_names (export_uinfo td) = td_names td" diff --git a/tools/c-parser/umm_heap/Vanilla32.thy b/tools/c-parser/umm_heap/Vanilla32.thy index d8928b35e0..55901112fb 100644 --- a/tools/c-parser/umm_heap/Vanilla32.thy +++ b/tools/c-parser/umm_heap/Vanilla32.thy @@ -9,7 +9,6 @@ theory Vanilla32 imports Word_Mem_Encoding CTypes begin - overloading typ_info_word \ typ_info_t begin definition typ_info_word: "typ_info_word (w::'a::len8 word itself) \ word_tag w" @@ -337,7 +336,7 @@ lemma ptr_typ_name [simp]: by simp lemma word_typ_name [simp]: - "typ_name (typ_info_t TYPE('a::len8 word)) = ''word'' @ nat_to_bin_string (len_of TYPE('a))" + "typ_name (typ_info_t TYPE('a::len8 word)) = signed_or_unsigned_as_str TYPE('a) @ ''word'' @ nat_to_bin_string (len_of TYPE('a))" by simp lemma nat_to_bin_string_word_sizes [simp]: @@ -357,19 +356,19 @@ lemma typ_name_words [simp]: "typ_name (typ_info_t TYPE(16 word)) = ''word000010''" "typ_name (typ_info_t TYPE(32 word)) = ''word0000010''" "typ_name (typ_info_t TYPE(64 word)) = ''word00000010''" - by (auto simp: typ_uinfo_t_def) + by (auto simp: typ_uinfo_t_def signed_or_unsigned) lemma typ_name_swords [simp]: - "typ_name (typ_uinfo_t TYPE(8 sword)) = ''word00010''" - "typ_name (typ_uinfo_t TYPE(16 sword)) = ''word000010''" - "typ_name (typ_uinfo_t TYPE(32 sword)) = ''word0000010''" - "typ_name (typ_uinfo_t TYPE(64 sword)) = ''word00000010''" + "typ_name (typ_uinfo_t TYPE(8 sword)) = ''sword00010''" + "typ_name (typ_uinfo_t TYPE(16 sword)) = ''sword000010''" + "typ_name (typ_uinfo_t TYPE(32 sword)) = ''sword0000010''" + "typ_name (typ_uinfo_t TYPE(64 sword)) = ''sword00000010''" (* these do not fire in a simple simp, because typ_info_word takes precedence (innermost term): *) - "typ_name (typ_info_t TYPE(8 sword)) = ''word00010''" - "typ_name (typ_info_t TYPE(16 sword)) = ''word000010''" - "typ_name (typ_info_t TYPE(32 sword)) = ''word0000010''" - "typ_name (typ_info_t TYPE(64 sword)) = ''word00000010''" - by (auto simp: typ_uinfo_t_def) + "typ_name (typ_info_t TYPE(8 sword)) = ''sword00010''" + "typ_name (typ_info_t TYPE(16 sword)) = ''sword000010''" + "typ_name (typ_info_t TYPE(32 sword)) = ''sword0000010''" + "typ_name (typ_info_t TYPE(64 sword)) = ''sword00000010''" + by (auto simp: typ_uinfo_t_def signed_or_unsigned) lemma ptr_arith[simp]: "(x +\<^sub>p a = y +\<^sub>p a) = ((x::('a::c_type) ptr) = (y::'a ptr))" diff --git a/tools/c-parser/umm_heap/Vanilla32_Preliminaries.thy b/tools/c-parser/umm_heap/Vanilla32_Preliminaries.thy index cdf76c6d78..6349d90e6c 100644 --- a/tools/c-parser/umm_heap/Vanilla32_Preliminaries.thy +++ b/tools/c-parser/umm_heap/Vanilla32_Preliminaries.thy @@ -80,7 +80,74 @@ by (simp add: len_exp_def bogus_log2lessthree_def) lemma lx_signed' [simp]: "len_exp (x::('a::len) signed itself) = len_exp (TYPE('a))" by (simp add: len_exp_def) -class len8 = len + +(* Maybe not required, but keeps everything neat *) +class typ_num + +instantiation num0 and num1 :: typ_num +begin +instance .. +end + +instantiation bit0 and bit1 :: (typ_num) typ_num +begin +instance .. +end + +class signed_or_unsigned = + fixes signed_or_unsigned_as_str :: "'a itself \ char list" + +instantiation num0 :: signed_or_unsigned +begin + +definition + num0_signed_or_unsigned_def: "signed_or_unsigned_as_str (w :: num0 itself) = []" + +instance .. +end + +instantiation num1 :: signed_or_unsigned +begin + +definition + num1_signed_or_unsigned_def: "signed_or_unsigned_as_str (w :: num1 itself) = []" + +instance .. +end + +instantiation bit0 :: (type) signed_or_unsigned +begin + +definition + bit0_signed_or_unsigned_def: "signed_or_unsigned_as_str (w :: 'a bit0 itself) = []" + +instance .. +end + +instantiation bit1 :: (type) signed_or_unsigned +begin + +definition + bit1_signed_or_unsigned_def: "signed_or_unsigned_as_str (w :: 'a bit1 itself) = []" + +instance .. +end + +instantiation signed :: (type) signed_or_unsigned +begin + +definition + signed_signed_or_unsigned_def: "signed_or_unsigned_as_str (w :: 'a signed itself) = ''s''" + +instance .. +end + +lemmas signed_or_unsigned = num0_signed_or_unsigned_def + num1_signed_or_unsigned_def + bit0_signed_or_unsigned_def + bit1_signed_or_unsigned_def + signed_signed_or_unsigned_def + +class len8 = signed_or_unsigned + len + (* this constraint gives us (in the most convoluted way possible) that we're only interested in words with a length that is divisible by 8 *) assumes len8_bytes: "len_of TYPE('a::len) = 8 * (2^len_exp TYPE('a))" diff --git a/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy index 2190af6124..57f74073cb 100644 --- a/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy +++ b/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy @@ -17,6 +17,6 @@ where (len_exp TYPE('a)) \ field_access = \v bs. (rev o word_rsplit) v, field_update = \bs v. (word_rcat (rev bs)::'a::len8 word) \) - (''word'' @ nat_to_bin_string (len_of TYPE('a)))" + (signed_or_unsigned_as_str TYPE('a) @ ''word'' nat_to_bin_string (len_of TYPE('a)))" end