added prompt.lem for connecting to concurrency model and {power,armv8}_extras.lem; fixes

1 files changed, 299 insertions, 0 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
new file mode 100644
index 00000000..0b616b7e
--- /dev/null
+++ b/src/gen_lib/prompt.lem
@@ -0,0 +1,299 @@
+open import Pervasives_extra
+open import Vector
+open import Arch
+
+let compose f g x = f (g x)
+
+type end_flag =
+  | E_big_endian
+  | E_little_endian
+
+type direction = 
+  | D_increasing
+  | D_decreasing
+
+type register_value = <| 
+    rv_bits: list bit (* MSB first, smallest index number *); 
+    rv_dir: direction; 
+    rv_start: nat ;
+    rv_start_internal: nat; 
+    (*when dir is increasing, rv_start = rv_start_internal. 
+      Otherwise, tells interpreter how to reconstruct a proper decreasing value*)
+    |>
+
+type byte = list bit (* of length 8 *)  (*MSB first everywhere*)
+
+type address = integer
+type address_lifted = address
+
+type memory_value = list byte
+(* the list is of length >=1 *)
+(* for both big-endian (Power) and little-endian (ARM), the head of the
+     list is the byte stored at the lowest address *)
+(* for big-endian Power the head of the list is the most-significant
+   byte, in both the interpreter and machineDef* code. *)
+(* For little-endian ARM, the head of the list is the
+   least-significant byte in machineDef* code and the
+   most-significant byte in interpreter code, with the switch over
+   (a list-reverse) being done just inside the interpreter interface*)
+(* In other words, in the machineDef* code the lowest-address byte is first,
+   and in the interpreter code the most-significant byte is first *)
+
+type opcode = Opcode of list byte (* of length 4 *)
+
+type read_kind =
+  (* common reads *)
+  | Read_plain
+  (* Power reads *)
+  | Read_reserve
+  (* AArch64 reads *)
+  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
+
+type write_kind =
+  (* common writes *)
+  | Write_plain
+  (* Power writes *)
+  | Write_conditional
+  (* AArch64 writes *)
+  | Write_release | Write_exclusive | Write_exclusive_release
+
+type barrier_kind =
+  (* Power barriers *)
+  | Sync | LwSync | Eieio | Isync
+  (* AArch64 barriers *)
+  | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
+
+type slice = (nat * nat)
+
+type reg_name = 
+  (* Name of the register, accessing the entire register, the start and size of this register, 
+   * and its direction *)
+  | Reg of string * nat * nat * direction
+                                  
+  (* Name of the register, accessing from the bit indexed by the first
+   * to the bit indexed by the second integer of the slice, inclusive. For
+   * machineDef* the first is a smaller number or equal to the second.  *)
+  | Reg_slice of string * nat * direction * slice 
+                                              
+  (* Name of the register, start and direction, and name of the field of the register
+   * accessed. The slice specifies where this field is in the register*)
+  | Reg_field of string * nat * direction * string * slice 
+
+  (* The first four components are as in Reg_field; the final slice
+   * specifies a part of the field, indexed w.r.t. the register as a whole *)
+  | Reg_f_slice of string * nat * direction * string * slice * slice 
+
+type outcome 'a =
+  (* Request to read memory, value is location to read followed by registers that location depended 
+   * on when mode.track_values, integer is size to read, followed by registers that were used in 
+   * computing that size *)
+  (* address_lifted should go away: doesn't make sense to allow for undefined bits in addresses *)
+  | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) *
+                  (memory_value -> outcome 'a)
+                    
+  (* Request to write memory, first value and dependent registers is location, second is the value 
+   * to write *)
+  | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value *
+                   maybe (list reg_name) * (bool -> outcome 'a)
+                                             
+  (* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
+  | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * outcome 'a
+                                                                              
+  (* Request to write memory at last signaled address. Memory value should be 8* the size given in 
+   * ea signal *)
+  | Write_memv of memory_value * maybe (list reg_name) * (bool -> outcome 'a)
+                                                           
+  (* Request a memory barrier *)
+  (* outcome 'a used to be (unit -> outcome 'a), but since the code is purely functional we don't 
+   * need that *)
+  | Barrier of barrier_kind * outcome 'a
+                                
+  (* Tell the system to dynamically recalculate dependency footprint *)
+  | Footprint of outcome 'a
+                   
+  (* Request to read register *)
+  | Read_reg of reg_name * (register_value -> outcome 'a)
+                             
+  (* Request to write register *)
+  | Write_reg of reg_name * register_value * outcome 'a
+                                               
+  (* List of instruction states to be run in parrallel, any order permitted.
+     Expects concurrency model to choose an order: a permutation of the original list *)
+  | Nondet_choice of list (outcome unit) * (list (outcome unit) -> outcome 'a)
+                                                
+  (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally 
+   * provide a handler. *)
+  | Escape (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
+
+  (* Stop for incremental stepping, function can be used to display function call data *)
+  | Done of 'a
+
+type M 'a = outcome 'a
+
+val return : forall 'a. 'a -> M 'a
+let return a = Done a
+
+val bind : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b
+let rec bind m f = match m with
+  | Done a -> f a
+  | Read_mem rk addr sz rs k ->        Read_mem rk addr sz rs        (fun v -> bind (k v) f)
+  | Write_mem wk addr sz rs v rs2 k -> Write_mem wk addr sz rs v rs2 (fun b -> bind (k b) f)
+  | Write_ea wk addr sz rs k ->        Write_ea wk addr sz rs        (bind k f)
+  | Write_memv v rs k ->               Write_memv v rs               (fun b -> bind (k b) f)
+  | Barrier bk k ->                    Barrier bk                    (bind k f)
+  | Footprint k ->                     Footprint                     (bind k f)
+  | Read_reg reg k ->                  Read_reg reg                  (fun v -> bind (k v) f)
+  | Write_reg reg v k ->               Write_reg reg v               (bind k f)
+  | Nondet_choice actions k ->         Nondet_choice actions         (fun c -> bind (k c) f)
+  | Escape -> Escape
+  end
+
+val exit : forall 'a 'e. 'e -> M 'a
+let exit _ = Escape
+
+let (>>=) = bind
+let (>>) m n = m >>= fun _ -> n
+
+val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
+let rec byte_chunks n list = match (n,list) with
+  | (0,_) -> []
+  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
+  | _ -> failwith "byte_chunks not given enough bits"
+end
+
+val bitvFromBytes : list byte -> vector bit
+let bitvFromBytes v = V (foldl (++) [] v) 0 defaultDir
+
+let dir is_inc = if is_inc then D_increasing else D_decreasing
+
+val bitvFromRegisterValue : register_value -> vector bit
+let bitvFromRegisterValue v =
+  V (v.rv_bits) (integerFromNat (v.rv_start)) (v.rv_dir = D_increasing)
+
+val registerValueFromBitv : vector bit -> register -> register_value
+let registerValueFromBitv (V bits start is_inc) reg = 
+  let start = natFromInteger start in
+  <| rv_bits = bits;
+     rv_dir = dir is_inc;
+     rv_start_internal = start;
+     rv_start = start+1 - (natFromInteger (length_reg reg)) |>
+
+val read_memory : read_kind -> integer -> integer -> M (vector bit)
+let read_memory rk addr sz =
+  let sz = natFromInteger sz in
+  Read_mem rk addr sz Nothing (compose Done bitvFromBytes)
+
+val write_memory : write_kind -> integer -> integer -> vector bit -> M bool
+let write_memory wk addr sz (V v _ _) =
+  let sz = natFromInteger sz in
+  Write_mem wk addr sz Nothing (byte_chunks sz v) Nothing Done
+
+val read_reg_range : register -> (integer * integer) -> M (vector bit)
+let read_reg_range reg (i,j) =
+  let (i,j) = (natFromInteger i,natFromInteger j) in
+  let start = natFromInteger (start_index_reg reg) in
+  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+  Read_reg reg (compose Done bitvFromRegisterValue)
+
+val write_reg_range : register -> (integer * integer) -> vector bit -> M unit
+let write_reg_range reg (i,j) v =
+  let rv = registerValueFromBitv v reg in
+  let start = natFromInteger (start_index_reg reg) in
+  let (i,j) = (natFromInteger i,natFromInteger j) in
+  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+  Write_reg reg rv (Done ())
+
+val read_reg_bit : register -> integer -> M bit
+let read_reg_bit reg i = 
+  let i = natFromInteger i in
+  let start = natFromInteger (start_index_reg reg) in
+  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,i) in
+  Read_reg reg (fun v -> Done (access (bitvFromRegisterValue v) 1))
+
+val write_reg_bit : register -> integer -> bit -> M unit
+let write_reg_bit reg i bit = write_reg_range reg (i,i) (V [bit] 0 true)
+
+val read_reg : register -> M (vector bit)
+let read_reg reg =
+  let start = natFromInteger (start_index_reg reg) in
+  let sz = natFromInteger (length_reg reg) in
+  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
+  Read_reg reg (compose Done bitvFromRegisterValue)
+
+val write_reg : register -> vector bit -> M unit
+let write_reg reg v =
+  let rv = registerValueFromBitv v reg in
+  let start = natFromInteger (start_index_reg reg) in
+  let sz = natFromInteger (length_reg reg) in
+  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
+  Write_reg reg rv (Done ())
+
+val read_reg_field : register -> register_field -> M (vector bit)
+let read_reg_field reg rfield = 
+  let (i,j) =
+    let (i,j) = field_indices rfield in
+    (natFromInteger i,natFromInteger j) in
+  let start = natFromInteger (start_index_reg reg) in
+  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+  Read_reg reg (compose Done bitvFromRegisterValue)
+
+val write_reg_field : register -> register_field -> vector bit -> M unit
+let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)
+
+val read_reg_field_bit : register -> register_field_bit -> M bit
+let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit)
+
+val write_reg_field_bit : register -> register_field_bit -> bit -> M unit
+let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit)
+
+val foreach_inc :  forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
+                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+let rec foreach_inc (i,stop,by) vars body = 
+  if i <= stop
+  then
+    let (_,vars) = body i vars in
+    foreach_inc (i + by,stop,by) vars body
+  else ((),vars)
+
+val foreach_dec : forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
+                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+let rec foreach_dec (i,stop,by) vars body = 
+  if i >= stop
+  then
+    let (_,vars) = body i vars in
+    foreach_dec (i - by,stop,by) vars body
+  else ((),vars)
+
+
+val foreachM_inc : forall 'vars. (nat * nat * nat) -> 'vars ->
+                  (nat -> 'vars -> M (unit * 'vars)) -> M (unit * 'vars)
+let rec foreachM_inc (i,stop,by) vars body = 
+  if i <= stop
+  then
+    body i vars >>= fun (_,vars) ->
+    foreachM_inc (i + by,stop,by) vars body
+  else return ((),vars)
+
+
+val foreachM_dec : forall 'vars. (nat * nat * nat) -> 'vars ->
+                  (nat -> 'vars -> M (unit * 'vars)) -> M (unit * 'vars)
+let rec foreachM_dec (i,stop,by) vars body = 
+  if i >= stop
+  then
+    body i vars >>= fun (_,vars) ->
+    foreachM_dec (i - by,stop,by) vars body
+  else return ((),vars)
+
+
+let length l = integerFromNat (length l)
+
+let write_two_regs r1 r2 vec =
+  let size = length_reg r1 in
+  let start = get_start vec in
+  let vsize = length vec in
+  let r1_v = slice vec start ((if defaultDir then size - start else start - size) - 1) in
+  let r2_v =
+    (slice vec)
+      (if defaultDir then size - start else start - size)
+      (if defaultDir then vsize - start else start - vsize) in
+  write_reg r1 r1_v >> write_reg r2 r2_v