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