1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory CommonOps 8imports 9 "CLib.CTranslationNICTA" 10 GlobalsSwap 11 ArchSetup 12begin 13 14text \<open>Additional constants needed to make conversion to and from the graph lang easy\<close> 15 16definition 17 bvshl :: "'a :: len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word" 18where 19 "bvshl x y = x << (unat y)" 20 21definition 22 bvlshr :: "'a :: len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word" 23where 24 "bvlshr x y = x >> (unat y)" 25 26definition 27 bvashr :: "'a :: len word \<Rightarrow> 'a word \<Rightarrow> 'a word" 28where 29 "bvashr x y = x >>> (unat y)" 30 31definition 32 bv_shift_amount :: "nat => 'a :: len word" 33where 34 "bv_shift_amount n = of_nat (min n ((2 ^ len_of TYPE('a)) - 1))" 35 36definition 37 bv_clz :: "('a :: len) word \<Rightarrow> 'a word" 38where 39 "bv_clz x = of_nat (word_clz x)" 40 41definition 42 bv_ctz :: "('a :: len) word \<Rightarrow> 'a word" 43where 44 "bv_ctz x = of_nat (word_ctz x)" 45 46definition 47 bv_popcount :: "('a :: len) word \<Rightarrow> 'a word" 48where 49 "bv_popcount x = of_nat (pop_count x)" 50 51definition 52 "mem_acc mem addr = h_val mem (Ptr addr)" 53 54definition 55 "mem_upd mem addr v = heap_update (Ptr addr) v mem" 56 57definition 58 "store_word8 (addr :: addr) (w :: word8) m = m (addr := w)" 59 60definition 61 "load_word8 (addr :: addr) m = (m addr :: word8)" 62 63definition 64 "store_word32 (addr :: addr) (w :: word32) 65 = heap_update_list addr (rev (word_rsplit w))" 66 67definition 68 "load_word32 (addr :: addr) memory 69 = (word_rcat (rev (heap_list memory 4 addr)) :: word32)" 70 71definition 72 "store_word64 (addr :: addr) (w :: word64) 73 = heap_update_list addr (rev (word_rsplit w))" 74 75definition 76 "load_word64 (addr :: addr) memory 77 = (word_rcat (rev (heap_list memory 8 addr)) :: word64)" 78 79abbreviation (input) 80 "store_machine_word :: machine_word mem_upd 81 \<equiv> arch_store_machine_word store_word32 store_word64" 82 83abbreviation (input) 84 "load_machine_word :: machine_word mem_read 85 \<equiv> arch_load_machine_word load_word32 load_word64" 86 87definition 88 word_add_with_carry :: "('a :: len) word \<Rightarrow> 'a word \<Rightarrow> bool 89 \<Rightarrow> ('a word \<times> (bool \<times> bool))" 90where 91 "word_add_with_carry x y cin \<equiv> 92 let cinw = if cin then 1 else 0 93 in (x + y + cinw, 94 unat (x + y + cinw) \<noteq> unat x + unat y + unat cinw, 95 (msb x \<noteq> msb y) \<and> (msb x \<noteq> msb (x + y + cinw)))" 96 97\<comment> \<open> 98 `all_htd_updates` is a utility term that we use to stash HTD updates when 99 going into and out of GraphLang. 100\<close> 101definition 102 all_htd_updates :: "('a :: c_type) itself \<Rightarrow> machine_word \<Rightarrow> addr \<Rightarrow> machine_word 103 \<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc" 104where 105 "all_htd_updates (tp :: ('a :: c_type) itself) mode p sz 106 = (if mode = 0 107 then typ_clear_region p (unat sz) 108 else if mode = 1 then ptr_retyps (unat sz) (Ptr p:: 'a ptr) 109 else if mode = 2 then typ_region_bytes p (unat sz) 110 else if mode = 3 then ptr_retyps (2 ^ unat sz) (Ptr p :: 'a ptr) 111 else if mode = 4 then ptr_arr_retyps (unat sz) (Ptr p :: 'a ptr) 112 else ptr_arr_retyps (2 ^ unat sz) (Ptr p :: 'a ptr))" 113 114\<comment> \<open> 115 This type has a weird domain @{typ "50 word"} to help you figure out the 116 source of your problem when asmrefine breaks - if you see `50 word`, it's 117 probably a ghost_assertions problem. 118\<close> 119type_synonym ghost_assertions = "50 word \<Rightarrow> addr" 120 121definition 122 ghost_assertion_data_get :: "int \<Rightarrow> ('a \<Rightarrow> ghost_assertions) \<Rightarrow> 'a \<Rightarrow> addr" 123where 124 "ghost_assertion_data_get k acc s = (acc s) (word_of_int k)" 125 126definition 127 ghost_assertion_data_set :: "int \<Rightarrow> addr \<Rightarrow> ((ghost_assertions \<Rightarrow> ghost_assertions) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" 128where 129 "ghost_assertion_data_set k v upd = upd (\<lambda>f. f (word_of_int k := v))" 130 131definition 132 "pvalid htd (v :: ('a :: c_type) itself) x = h_t_valid htd c_guard (Ptr x :: 'a ptr)" 133 134definition 135 "palign_valid (v :: ('a :: c_type) itself) x = c_guard (Ptr x :: 'a ptr)" 136 137definition 138 "pweak_valid htd (v :: ('a :: c_type) itself) x = ptr_safe (Ptr x :: 'a ptr) htd" 139 140definition 141 "pglobal_valid htd (v :: ('a :: mem_type) itself) x = ptr_inverse_safe (Ptr x :: 'a ptr) htd" 142 143definition 144 "parray_valid htd (v :: ('a :: c_type) itself) x n 145 = array_assertion (Ptr x :: 'a ptr) (unat n) htd" 146 147end 148 149