To protect your data, the CISO officer has suggested users to enable GitLab 2FA as soon as possible.

Commit 2fd5a16b authored by Adam Nelson's avatar Adam Nelson
Browse files

Types + values match spec better, bytesTheory, etc

parent b1d3c66c
open HolKernel Parse boolLib bossLib;
open arithmeticTheory
open optionTheory
open patriciaTheory
open wordsTheory
open uvmTypesTheory
val _ = new_theory "uvmBytes"
(* This file is a dumping ground for incomplete binary-representation-related
code. A lot of the code here isn't useful for anything yet.
*)
val _ = Datatype`
machine = <|
atomic_sizes: num set;
min_int_bytes: num;
pointer_bytes: num;
float_bits: num;
double_bits: num;
num_to_bytes: num -> num -> word8 list;
bytes_to_num: word8 list -> num;
alignment: num -> num -> num
|>
`
val num_to_bytes_ok_def = Define`
num_to_bytes_ok (n2b : num -> num -> word8 list)
(b2n : word8 list -> num)
(sz b. n2b sz (b2n b) = b)
(sz n. b2n (n2b sz n) = n)
(sz n. sz LENGTH (n2b sz n))
(sz n1 n2. n1 n2 n2b sz n1 n2b sz n2)
(sz n1 n2. n1 < n2 LENGTH (n2b sz n1) LENGTH (n2b sz n2))
`
val machine_ok_def = Define`
machine_ok m
m.atomic_sizes
0 < m.min_int_bytes
m.min_int_bytes m.pointer_bytes
m.min_int_bytes * 8 m.float_bits
m.float_bits m.double_bits
num_to_bytes_ok m.num_to_bytes m.bytes_to_num
`
(*
val align_cells_def = Define`
align_cells (alignment : num -> num -> num) (start : num) (szs : num list) =
FOLDL (λ(n, ns) sz. let n' = n + alignment n sz in (n' + sz, SNOC ns n'))
(start, []) szs
`
*)
(*
val ceil_div_def = Define`
ceil_div num den = num DIV den + if num MOD den = 0 then 0 else 1
`
val ceil_div_0 = store_thm("ceil_div_0",
``∀n d. 0 < d ∧ ceil_div n d = 0 ⇒ n = 0``,
rw[ceil_div_def] >> rfs[DIV_EQ_X] >> fs[MOD_EQ_0_DIVISOR] >>
rw[] >> Cases_on `d'` >> fs[])
val ceil_div_le = store_thm("ceil_div_le",
``∀n d. 0 < d ⇒ ceil_div n d ≤ n``,
rw[ceil_div_def, DIV_LESS_EQ] >>
`n DIV d < n` suffices_by simp[] >> match_mp_tac DIV_LESS >>
`n ≠ 0 ∧ d ≠ 0 ∧ d ≠ 1` suffices_by simp[] >>
`0 MOD d = 0` by simp[] >> fs[] >> metis_tac[MOD_1])
*)
val size_of_type_def = Define`
size_of_type _ Void = 0
size_of_type _ TagRef64 = 8
size_of_type m (Int n) =
LENGTH (m.num_to_bytes m.min_int_bytes (2 ** n - 1))
size_of_type m Float = (m.float_bits + 7) DIV 8
size_of_type m Double = (m.double_bits + 7) DIV 8
size_of_type _ (Array _ _) = 0
size_of_type _ (Vector _ _) = 0
size_of_type _ (Hybrid _ _) = 0
size_of_type _ (Struct _ _) = 0
size_of_type m _ = m.pointer_bytes
`
(* canconvert M convtype (src : uvm_type) (tgt : uvm_type) *)
val (canconvert_rules, canconvert_ind, canconvert_cases) = Hol_reln`
(m n. m n canconvert M TRUNC (Int n) (Int m))
(m n. m n canconvert M ZEXT (Int m) (Int n))
(m n. m n canconvert M SEXT (Int m) (Int n))
canconvert M FPTRUNC Double Float
canconvert M FPEXT Float Double
(ty n. fpType ty canconvert M FPTOUI ty (Int n))
(ty n. fpType ty canconvert M FPTOSI ty (Int n))
(ty n. fpType ty canconvert M UITOFP (Int n) ty)
(ty n. fpType ty canconvert M SITOFP (Int n) ty)
canconvert M BITCAST (Int M.float_bits) Float
canconvert M BITCAST Float (Int M.float_bits)
canconvert M BITCAST (Int M.double_bits) Double
canconvert M BITCAST Double (Int M.double_bits)
(* ptrcast cases *)
(n ty.
M.pointer_bytes = n * 8
canconvert M BITCAST (Int n) (IRef PTR ty))
(n ty.
M.pointer_bytes = n * 8 (* tell KW *)
canconvert M BITCAST (IRef PTR ty) (Int n))
(* refcast cases *)
(ty. canconvert M REFCAST (Ref (Type Void)) (Ref ty))
(ty. canconvert M REFCAST (Ref ty) (Ref (Type Void)))
(ty1 ty2. prefix_of ty1 ty2
canconvert M REFCAST (Ref (Type ty1)) (Ref (Type ty2)))
(*
∧ (∀fx1 fx2 tys1 tys2.
(* FIXME: Equivalence is MUCH harder than this w.r.t. fixpoints *)
(tys1 <<= tys2 ∨ tys2 <<= tys1)
⇒ canconvert M REFCAST (Ref (Type (Struct fx1 tys1)))
(Ref (Type (Struct fx2 tys2))))
*)
`
val _ = type_abbrev("bytes", ``:num # word8 ptree``)
val new_bytes_def = Define `new_bytes : bytes = (0, <{}>)`
val append_bytes_def = Define`
append_bytes : bytes -> word8 option list -> bytes =
FOLDL (λ(n, t) b. (SUC n, case b of SOME b => t |+ (n, b) | NONE => t))
`
val read_bytes_def = Define`
read_bytes ((_, t) : bytes) (start : num) (len : num) : word8 list option =
FOLDR (OPTION_MAP2 CONS) (SOME []) (GENLIST (PEEK t o $+ start) len)
`
val write_bytes_def = Define`
write_bytes ((n, t) : bytes) (start : num) (bs : word8 option list) : bytes =
let t' = FOLDL (λt b. case b of SOME b => t |+ (n, b) | NONE => t) t bs in
(MAX n (start + LENGTH bs), t')
`
val append_aligned_bytes_def = Define`
append_aligned_bytes (* start len offset *)
(alignment : num -> num -> num )
(old_bytes : bytes)
(new_bytes : word8 list)
: bytes # num =
let start = FST old_bytes in
let offset = alignment start (LENGTH new_bytes) in
let padding = GENLIST (K NONE) offset in
(append_bytes old_bytes (padding ++ MAP SOME new_bytes), start + offset)
`
(*
val pack_int_def = Define`
pack_int m sz n =
let bits = m.max_atomic_bytes * 8 in (
members_of_type m NONE (Int sz) :> LENGTH :>
GENLIST (IntV (MIN sz bits) o n2w o $DIV n o $** 2 o $* bits) :>
if m.little_endian then I else REVERSE)
`
val unpack_int_def = Define`
unpack_int m words =
let words = if m.little_endian then words else REVERSE words in
let ext word (n, e) =
case word of
| IntV sz w => return (n + w2n w * (2 ** e), e + sz)
| _ => Fail (UndefinedBehavior "not an int") in
FST <$> FOLDL (λs w. s >>= ext w) (return (0, 0)) words
`
*)
val _ = export_theory()
......@@ -22,6 +22,8 @@ val _ = new_theory "uvmInstructionSemantics"
val _ = add_monadsyntax()
val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
val _ = type_abbrev("from_regs", ``:(num -> value or_error) -> α or_error``)
(* Evaluates a binary operation, returning the result. Returns an error if the
values `v1`, `v2` are incorrectly typed, or if the result is undefined.
*)
......
......@@ -6,32 +6,30 @@ open uvmErrorsTheory
open DefineUtils
open monadsyntax
open listTheory
open llistTheory
open optionTheory
open patriciaTheory
open patriciaLib
open numpairTheory
open Parse
val _ = new_theory "uvmMemory"
val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
val _ = add_monadsyntax()
val _ = ParseExtras.tight_equality()
val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
val _ = computeLib.add_funs[OPTION_MAP2_DEF, PEEK_def]
val _ = define_num_newtype("thread_id", "Thread")
val _ = define_num_newtype("frame_id", "Frame")
val _ = define_num_newtype("stack_id", "Stack")
val _ = define_num_newtype("action_id", "Action")
val _ = Datatype`
ssavar = SSA string ;
func_name = Func string ;
func_version = FuncVersion func_name num ;
addr =
| GlobalAddr num
| HeapAddr thread_id action_id
| StackAddr stack_id frame_id thread_id action_id
`
val _ = Datatype `ssavar = SSA string`
val _ = Datatype `func_name = Func string`
val _ = Datatype `func_version = FuncVersion func_name num`
val _ = Datatype `alloc = Global | Heap | Stack stack_id frame_id`
val _ = type_abbrev("addr", ``:alloc # num``)
val _ = type_abbrev("value", ``:(addr, func_name, stack_id, thread_id) gen_value``)
val _ = type_abbrev("iaddr", ``:addr gen_iaddr``)
val _ = type_abbrev("uvm_error", ``:(addr, func_name) gen_uvm_error``)
......@@ -55,121 +53,177 @@ val action_id_lt_irreflexive = store_thm("action_id_lt_irreflexive",
rw[relationTheory.irreflexive_def, definition "action_id_lt_def"] >>
BasicProvers.every_case_tac >> simp[])
val _ = type_abbrev("mem_cell", ``:value # uvm_type # num list``)
val _ = type_abbrev("mem_region", ``:mem_cell ptree``)
val _ = type_abbrev("mem_reader", ``:mem_region -> α or_error``)
val _ = define_monad("mem_reader", (fn a => ``:^a mem_reader``),
``K o OK``, ``λx fn m. join (fn <$> x m <*> OK m)``)
val get_value_def = Define`
get_value (loc : num) : value mem_reader = λm.
FST <$> expect (m ' loc) (InvalidState "no such location")
`
val mem_fail_def = Define`
mem_fail (err : uvm_error) : α mem_reader = K (Fail err)
`
val new_mem_cells_def = Define`
new_mem_cells (sz : num option)
(ty : uvm_type)
(next_loc : α -> num # α)
(loc_src : α)
: ((num # mem_cell) list # α) or_error =
let ts = component_types sz ty in
let (locs, loc_src) = FOLDL
(λ(ns, s) _. (C SNOC ns ## I) (next_loc s)) ([], loc_src) ts in
(λcells. cells, loc_src) <$>
FOLDR (λn accum.
let sz = if n = 0 then sz else NONE in
let ty = EL n ts in do
cells <- accum;
z <- zero_value ty;
return ((
EL n locs,
(z, ty, TAKE (LENGTH (component_types sz ty)) (DROP n locs)))
::cells)
od) (OK []) (GENLIST I (LENGTH ts))
`
val region_alloc_def = Define`
region_alloc (region : mem_region)
(sz : num option)
(ty : uvm_type)
(next_loc : α -> num # α)
(loc_src : α)
: (num # α # mem_region) or_error = do
(cells, loc_src) <- new_mem_cells sz ty next_loc loc_src;
assert (EVERY (λ(n, _). region ' n = NONE) cells)
(InvalidState "double allocation");
return (FST (HD cells), loc_src, region |++ cells)
od
`
val _ = Datatype`
resume_values =
| NOR (α list)
| EXC (α list) α
`
val _ = type_abbrev("store", ``:thread_id # action_id # iaddr # value``)
val _ = Datatype`
store =
| Store iaddr value
| StoreNew uvm_type (num option)
| StoreAlloca stack_id frame_id uvm_type (num option)
address_space = <|
globals : α ptree;
heap : num # α ptree;
stack : (num # α ptree) ptree
|>
`
(*
| StoreCmpXchg cmp_xchg_action_args
| StoreAtomicRMW atomic_rmw_action_args ;
cmp_xchg_action_args = <|
addr: iaddr;
strength: strength;
success_order: memory_order;
failure_order: memory_order;
expected: value;
desired: value
|> ;
atomic_rmw_action_args = <|
addr: iaddr;
order: memory_order;
op: atomicrmw_op;
opnd: value
|> ;
strength = STRONG | WEAK
*)
val _ = type_abbrev("store_message", ``:thread_id # action_id # store``)
val _ = type_abbrev("memory", ``:mem_cell address_space``)
val _ = type_abbrev("buffer", ``:value list address_space``)
val _ = Datatype`
memory = <|
globals : value ptree;
heap : value ptree;
stack : value ptree ptree
val new_address_space_def = Define`
new_address_space = <|
globals := Empty;
heap := (0, Empty);
stack := Empty
|>
`
val new_memory_def = Define`
new_memory (globals : (string # uvm_type) list) : memory or_error =
(λgs. <|
globals := Empty |++ ZIP (GENLIST I (LENGTH gs), gs);
heap := Empty;
stack := Empty
|>) <$> mapM (C zero_value NONE o SND) globals
let global_locs = GENLIST I (LENGTH globals) in
let loc_gen = LUNFOLD (λn. SOME (SUC n, n)) (LENGTH globals) in do
(_, globals) <-
FOLDL (λaccum (loc, ty). do
(loc_gen, region) <- accum;
SND <$> region_alloc region NONE ty
(λl. THE (LHD l), THE (LTL l)) (loc:::loc_gen)
od) (OK (loc_gen, Empty)) (ZIP (global_locs, (MAP SND globals)));
return (new_address_space with globals := globals)
od
`
val memory_get_def = Define`
memory_get mem (GlobalAddr n) = mem.globals ' n
memory_get mem (HeapAddr (Thread tid) (Action id)) = mem.heap ' (tid id)
memory_get mem (StackAddr (Stack sid) (Frame fid) (Thread tid) (Action id)) =
OPTION_BIND (mem.stack ' (sid fid)) (λm. m ' (tid id))
val get_region_def = Define`
get_region as Global = as.globals
get_region as Heap = SND as.heap
get_region as (Stack sid fid) =
case as.stack ' (stack_id_dest sid frame_id_dest fid) of
| SOME r => SND r
| NONE => Empty
`
val memory_update_def = Define`
memory_update (mem : memory) (v : value) (ia : iaddr) : memory or_error = do
base <- expect (memory_get mem ia.base) (UnallocatedMemory ia.base);
updated <- iaddr_update base ia v;
return (
case ia.base of
| GlobalAddr n => mem with globals updated_by C $|+ (n, updated)
| HeapAddr (Thread tid) (Action id) =>
mem with heap updated_by λm. m |+ (tid id, updated)
| StackAddr (Stack sid) (Frame fid) (Thread tid) (Action id) =>
mem with stack updated_by λm. m |+ (sid fid,
(case m ' (sid fid) of SOME m' => m' | NONE => Empty)
|+ (tid id, updated)))
od
(* TODO: fix put_region *)
val put_region_def = Define`
put_region as Global r = as with globals := r
put_region as Heap r = as with heap := r
put_region as (Stack sid fid) r =
as with stack updated_by
λs. s |+ (stack_id_dest sid frame_id_dest fid, r)
`
val get_addr_def = Define `get_addr as (a, n) = get_region as a ' n`
val put_addr_def = Define `
put_addr as (a, n) v = put_region as a (get_region as a |+ (n, v))
`
val get_iaddr_cell_addrs_def = Define`
get_iaddr_cell_addrs (m : machine) (mem : memory) (ia : iaddr)
: addr list or_error =
let region = get_region mem (FST ia.base) in
let base = expect (region ' (SND ia.base)) (UnallocatedMemory ia.base) in
MAP (λn. FST ia.base, n) <$>
if ia.offset = 0 ia.base_ty = ia.ty
then SND o SND <$> base
else do
(_, tys, idxs) <- base;
assert (EXISTS ($= ia.base_ty) tys)
(TypeMismatch "iaddr base" ia.base_ty (LAST tys));
assert (LENGTH idxs < ia.offset) (ReadOutOfBounds (LAST tys) ia.offset);
(_, tys', idxs') <- expect (region ' (EL ia.offset idxs))
(UnallocatedMemory (FST ia.base, ia.offset));
assert (EXISTS ($= ia.ty) tys')
(TypeMismatch "iaddr" ia.ty (LAST tys'));
return (TAKE (LENGTH (members_of_type m NONE ia.ty)) idxs')
od
`
val memory_get_def = Define`
memory_get mem a : value or_error =
FST <$> expect (get_addr mem a) (UnallocatedMemory a)
`
val apply_store_def = Define`
apply_store mem (_, _, Store ia v) = memory_update mem v ia
apply_store mem (Thread tid, Action id, StoreNew ty sz) =
(λz. mem with heap updated_by λm. m |+ (tid id, z))
<$> zero_value ty sz
apply_store mem (Thread tid, Action id, StoreAlloca (Stack sid) (Frame fid) ty sz) =
(λz. mem with stack updated_by λm. m |+ (sid fid,
(case m ' (sid fid) of SOME m' => m' | NONE => Empty)
|+ (tid id, z)))
<$> zero_value ty sz
val memory_put_def = Define`
memory_put mem (a, n) v : memory or_error =
let region = get_region mem a in
assert (IS_SOME (region ' n)) (UnallocatedMemory (a, n)) *>
return (put_region mem a (region |+ (n, v)))
`
val update_with_store_def = Define`
update_with_store (HeapAddr tid' id' : addr)
((tid, id, StoreNew ty sz) : store_message)
(old : value option)
: value option or_error =
(if tid = tid' id = id'
then SOME <$> zero_value ty sz
else return old)
update_with_store _ (_, _, StoreNew _ _) old = return old
update_with_store (StackAddr sid' fid' tid' id')
(tid, id, StoreAlloca sid fid ty sz)
old =
(if tid = tid' id = id' sid = sid' fid = fid'
then SOME <$> zero_value ty sz
else return old)
update_with_store _ (_, _, StoreAlloca _ _ _ _) old = return old
update_with_store base (_, _, Store ia v') (SOME v) =
(if base = ia.base
then SOME <$> iaddr_update v ia v'
else return (SOME v))
update_with_store _ (_, _, Store _ _) NONE = return NONE
val memory_alloc_def = Define`
memory_alloc (m : machine)
(mem : memory)
(alloc_region : alloc)
(ty : uvm_type)
(sz : num option)
(next_loc : α -> num # α)
(loc_src : α)
: (memory # addr option # α) or_error =
let region = get_region mem alloc_region in do
(region, n, loc_src) <- region_alloc m region ty sz next_loc loc_src;
return (
put_region mem alloc_region region,
OPTION_MAP (λn. alloc_region, n) n,
loc_src)
od
`
val memory_load_def = Define`
memory_load (mem : memory)
(pending_stores : store_message list)
(sb : store list)
(ib : store list)
(ia : iaddr)
: value or_error =
......
......@@ -30,11 +30,23 @@ val _ = Datatype`
| ThreadPopFrame stack_id frame_id
`
val _ = type_abbrev("from_regs", ``:(num -> value or_error) -> α or_error``)
val _ = Datatype`
opn =
| NonMem (value ptree from_regs)
| Ld (num or_const) num
| St (store from_regs)
| ThAct (thread_action from_regs)
`
val _ = Datatype`
thread = <|
sid: stack_id;
next_act: action_id;
next_reg: num;
opns: opn list;
terminst: num terminst;
regs: value ptree;
sb: store_message list;
ib: store_message list;
......
This diff is collapsed.
......@@ -10,26 +10,41 @@ open DefineUtils
val _ = new_theory "uvmValues"
val _ = add_monadsyntax()
val _ = ParseExtras.tight_equality()
val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
val _ = Datatype`
(* The type "value" is defined as:
('addr, 'func, 'stack, 'thread) gen_value
Its generic parameters are:
(* An iaddr (iref address) is an address with an offset. The offset refers to a
value nested within the parent value that "iaddr.base" refers to.
∙ 'addr: Value address type used by Ref and IRef
∙ 'func: Function address type used by FuncRef
∙ 'stack: Stack address type used by StackRef
∙ 'thread: Thread address type used by ThreadRef
"gen_iaddr", like "gen_value" (next definition), is generic in its address
type. The alias "iaddr" is defined in uvmMemoryTheory.
*)
val _ = Datatype`
gen_iaddr = <|
base: 'addr;
offset: num;
base_ty: uvm_type;
ty: uvm_type
|>
`
This type is defined as generic in order to separate the definition of the
"addr" type, and several other types it depends on, into "uvmMemoryTheory"
where it belongs. The "value" alias is also defined in "uvmMemoryTheory".
*)
(* The type "value" is defined as:
('addr, 'func, 'stack, 'thread) gen_value
Its generic parameters are:
∙ 'addr: Value address type used by Ref and IRef
∙ 'func: Function address type used by FuncRef
∙ 'stack: Stack address type used by StackRef
∙ 'thread: Thread address type used by ThreadRef
This type is defined as generic in order to separate the definition of the
"addr" type, and several other types it depends on, into uvmMemoryTheory
where it belongs. The "value" alias is also defined in uvmMemoryTheory.
*)
val _ = Datatype`
gen_value =
| IntV num word64 (* word64 because 64 bits is the max int size *)
| IntV num num
| FloatV word32
| DoubleV word64
| RefV uvm_type ('addr option)
......@@ -37,55 +52,151 @@ val _ = Datatype`
| FuncRefV ref_type funcsig ('func option)
| StackRefV ('stack option)
| ThreadRefV ('thread option)
| ArrayV uvm_type (gen_value list)
| VectorV uvm_type (gen_value list)
| HybridV ((gen_value # uvm_type) list) uvm_type (gen_value list)
| StructV num ((gen_value # uvm_type) list) ;
`
(* An iaddr (iref address) is an address with an offset. The offset refers to
a value nested within the parent value that "iaddr.base" refers to.
val type_of_value_def = Define`
type_of_value (IntV n _) = Int n
type_of_value (FloatV _) = Float
type_of_value (DoubleV _) = Double
type_of_value (RefV t _) = Ref (Type t)
type_of_value (IRefV r (SOME a)) = IRef r (Type a.ty)
type_of_value (IRefV r NONE) = IRef r (Type Void) (* FIXME: This might cause typechecking errors *)