Many changes:

Split out specification specific memory and external functions
Reduce the presence of big_int
Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction

Also some bug fixes exposed by above and running ARM second instruction

1 files changed, 121 insertions, 165 deletions

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 3b83dd89..0b77909d 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -9,11 +9,6 @@ to take an opcode as defined above, instead of a value
 
 and change 
 
-  type instruction = (string * list (string * instr_parm_typ * value) * list base_effect)
-
-to 
-
-  type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect)
 *)
 
 
@@ -35,139 +30,13 @@ end
 
 type word8 = nat (* bounded at a byte, for when lem supports it*)
 
-(* Abstract types, to be accessed only through this interface *)
-type instruction_state = Interp.stack
-type context = Interp.top_level
-type interp_mode = Interp.interp_mode
+type interpreter_state = Interp.stack (*Deem abstract*)
+(* Will come from a .lem file generated by Sail, bound to a 'defs' identifier *)
+type specification = Interp_ast.defs Interp.tannot (*Deem abstract*)
+type interp_mode = Interp.interp_mode (*Deem abstract*)
 val make_mode : bool -> bool -> interp_mode
 val tracking_dependencies : interp_mode -> bool
 
-(*Concrete types*)
-type read_kind = Read_plain | Read_reserve | Read_acquire
-type write_kind = Write_plain | Write_conditional | Write_release
-type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (* PS removed "plain" and added "Isync" and "ISB" *)
-
-(*type value = 
-| Bitvector of list bool  * bool * integer 
-(* In Bitvector bs b n:
-   - the bs are the bits (true represents 1 and false represents 0)
-   - the b specifies whether the indicies are increasing (true) or decreasing (false) along the list (for Power the Bitvector values are always increasing)    
-   - the n is the index of the head of the list
-*)
-(*To discuss:  ARM8 uses at least one abstract record form for 
-  some special registers, with no clear mapping to bits. Should
-  we permit Record of (string * Bitvector) values as well?
-*)
-| Bytevector of list word8 (* For memory accesses *)
-| Unknown
-(*To add: an abstract value representing an unknown but named memory address?*)
-
-instance (Ord bool)
-  let compare = defaultCompare
-  let (<) = defaultLess
-  let (<=) = defaultLessEq
-  let (>) = defaultGreater
-  let (>=) = defaultGreaterEq
-end
-
-let valueCompare v1 v2 = 
-  match (v1,v2) with
-  | (Bitvector bits1 inc1 start1, Bitvector bits2 inc2 start2) ->
-    tripleCompare compare compare compare (bits1,inc1,start1) (bits2,inc2,start2)
-  | (Bytevector words1, Bytevector words2) -> compare words1 words2
-  | (Unknown,Unknown) -> EQ
-  | (Bitvector _ _ _, _)  -> LT
-  | (Bytevector _, _) -> LT
-  | (_, _) -> GT
-  end
-
-instance (Ord value)
-  let compare = valueCompare
-  let (<) v1 v2 = (valueCompare v1 v2) = LT
-  let (<=) v1 v2 = (valueCompare v1 v2) <> GT
-  let (>) v1 v2 = (valueCompare v1 v2) = GT
-  let (>=) v1 v2 = (valueCompare v1 v2) <> LT
-end
-
-let valueEqual v1 v2 =
-  match (v1,v2) with
-    | (Bitvector bits1 inc1 start1, Bitvector bits2 inc2 start2) ->
-      bits1 = bits2 && inc1 = inc2 && start1 = start2
-    | (Bytevector words1, Bytevector words2) -> words1 = words2
-    | (Unknown,Unknown) -> true
-    | _ -> false
-end 
-
-instance  (Eq value)
-  let (=) = valueEqual
-  let (<>) x y = not (valueEqual x y)
-end
-*)
-type slice = (integer * integer)
-
-
-type reg_name = 
-| Reg of string * integer
-(*Name of the register, accessing the entire register, and the size of this register *)
-
-| Reg_slice of string * slice 
-(* 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
-Power the first will be a smaller number than or equal to the second;
-for other architectures it might be the other way round.  *)
-
-| Reg_field of string * string * slice 
-(*Name of the register and name of the field of the register
-accessed. The slice specifies where this field is in the register*)
-
-| Reg_f_slice of string * string * slice * slice 
-(* The first three components are as in Reg_field; the final slice
-specifies a part of the field, indexed w.r.t. the register as a whole *)
-
-
-(* because reg_name contains slice which currently contains Big_int.big_int, the default OCaml comparison is not sufficient and we need to define explicit type classes *)
-let slice_eq (s1l,s1r) (s2l,s2r) = (s1l = s2l) && (s1r = s2r)
-
-let reg_nameEqual r1 r2 = 
-  match (r1,r2) with
-  | (Reg s1 l1, Reg s2 l2) -> s1=s2 && l1=l2
-  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> s1=s2 && (slice_eq sl1 sl2)
-  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> s1=s2 && f1=f2 && (slice_eq sl1 sl2)
-  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> s1=s2 && f1=f2 && (slice_eq sl1 sl2) && (slice_eq sl1' sl2')
-  | _ -> false
-  end
-
-instance  (Eq reg_name)
-  let (=) = reg_nameEqual
-  let (<>) x y = not (reg_nameEqual x y)
-end
-
-let reg_nameCompare r1 r2 = 
-  match (r1,r2) with
-  | (Reg s1 l1, Reg s2 l2) -> pairCompare compare compare (s1,l1) (s2,l2)
-  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> pairCompare compare compare (s1,sl1) (s2,sl2)
-  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> 
-      tripleCompare compare compare compare (s1,f1,sl1) (s2,f2,sl2)
-  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> 
-      pairCompare compare (tripleCompare compare compare compare) (s1,(f1,sl1,sl1')) (s2,(f2,sl2,sl2'))
-  | (Reg _ _, _)  -> LT
-  | (Reg_slice _ _, _) -> LT
-  | (Reg_field _ _ _, _) -> LT
-  | (_, _) -> GT
-  end
-
-instance (SetType reg_name)
-  let setElemCompare = reg_nameCompare
-end
-
-instance (Ord reg_name)
-  let compare = reg_nameCompare
-  let (<)  r1 r2 = (reg_nameCompare r1 r2) = LT
-  let (<=) r1 r2 = (reg_nameCompare r1 r2) <> GT
-  let (>)  r1 r2 = (reg_nameCompare r1 r2) = GT
-  let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT
-end
-
 (** basic values *)
 
 type bit =
@@ -184,7 +53,7 @@ type direction =
   | D_increasing
   | D_decreasing
 
-type register_value = <| rv_bits: list bit_lifted (* MSB first, smallest index number *); rv_dir: direction; rv_start: int |>  (* beter for this to be int, not integer *)
+type register_value = <| rv_bits: list bit_lifted (* MSB first, smallest index number *); rv_dir: direction; rv_start: nat |>
 
 type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *)
 
@@ -260,12 +129,102 @@ instance (Ord address_lifted)
   let (>=) = defaultGreaterEq
 end
 
+(* Registers *)
+(*Can be nat nat, but finding out where ppcmem doens't like that is maybe not worth the effort *)
+type slice = (int * int)
+
+type reg_name = 
+| Reg of string * nat
+(*Name of the register, accessing the entire register, and the size of this register *)
+
+| Reg_slice of string * slice 
+(* 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
+Power the first will be a smaller number than or equal to the second;
+for other architectures it might be the other way round.  *)
+
+| Reg_field of string * string * slice 
+(*Name of the register and name of the field of the register
+accessed. The slice specifies where this field is in the register*)
+
+| Reg_f_slice of string * string * slice * slice 
+(* The first three components are as in Reg_field; the final slice
+specifies a part of the field, indexed w.r.t. the register as a whole *)
+
+
+(* because reg_name contains slice which currently contains Big_int.big_int, the default OCaml comparison is not sufficient and we need to define explicit type classes *)
+let slice_eq (s1l,s1r) (s2l,s2r) = (s1l = s2l) && (s1r = s2r)
+
+let reg_nameEqual r1 r2 = 
+  match (r1,r2) with
+  | (Reg s1 l1, Reg s2 l2) -> s1=s2 && l1=l2
+  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> s1=s2 && (slice_eq sl1 sl2)
+  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> s1=s2 && f1=f2 && (slice_eq sl1 sl2)
+  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> s1=s2 && f1=f2 && (slice_eq sl1 sl2) && (slice_eq sl1' sl2')
+  | _ -> false
+  end
+
+instance  (Eq reg_name)
+  let (=) = reg_nameEqual
+  let (<>) x y = not (reg_nameEqual x y)
+end
+
+let reg_nameCompare r1 r2 = 
+  match (r1,r2) with
+  | (Reg s1 l1, Reg s2 l2) -> pairCompare compare compare (s1,l1) (s2,l2)
+  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> pairCompare compare compare (s1,sl1) (s2,sl2)
+  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> 
+      tripleCompare compare compare compare (s1,f1,sl1) (s2,f2,sl2)
+  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> 
+      pairCompare compare (tripleCompare compare compare compare) (s1,(f1,sl1,sl1')) (s2,(f2,sl2,sl2'))
+  | (Reg _ _, _)  -> LT
+  | (Reg_slice _ _, _) -> LT
+  | (Reg_field _ _ _, _) -> LT
+  | (_, _) -> GT
+  end
+
+instance (SetType reg_name)
+  let setElemCompare = reg_nameCompare
+end
+
+instance (Ord reg_name)
+  let compare = reg_nameCompare
+  let (<)  r1 r2 = (reg_nameCompare r1 r2) = LT
+  let (<=) r1 r2 = (reg_nameCompare r1 r2) <> GT
+  let (>)  r1 r2 = (reg_nameCompare r1 r2) = GT
+  let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT
+end
+
+(* Data structures for building up instructions *)
+
+type read_kind = Read_plain | Read_reserve | Read_acquire
+type write_kind = Write_plain | Write_conditional | Write_release
+type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
+
+(*Map between external functions as preceived from a Sail spec and the actual implementation of the function *)
+type external_functions = list (string * (Interp.value -> Interp.value))
+
+(*Maps between the memory functions as preceived from a Sail spec and the values needed for actions in the memory model*)
+type barriers = list (string * barrier_kind)
+type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name))
+type memory_read = MR of read_kind * memory_parameter_transformer
+type memory_reads  = list (string * memory_read)
+type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state))
+and memory_writes = list (string * memory_write)
+
+(* Definition information needed to run an instruction *)
+and context = Context of Interp.top_level * direction * memory_reads * memory_writes * barriers * external_functions
+
+(* An instruction in flight *)
+and instruction_state = IState of interpreter_state * context
+
+
 type outcome =
 (* 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 *)
-| Read_mem of read_kind * address_lifted * integer * maybe (list reg_name) *  (memory_value -> instruction_state)
+| Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) *  (memory_value -> instruction_state)
 (* Request to write memory, first value and dependent registers is location, second is the value to write *)
-| Write_mem of write_kind * address_lifted * integer * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state)
+| Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state)
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
 (* Request to read register, will track dependency when mode.track_values *)
@@ -282,18 +241,15 @@ type outcome =
 | Error of string
 
 type event = 
-| E_read_mem of read_kind * address_lifted * integer * maybe (list reg_name)
-| E_write_mem of write_kind * address_lifted * integer * maybe (list reg_name) * memory_value * maybe (list reg_name)
+| E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
+| E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
 | E_barrier of barrier_kind
 | E_read_reg of reg_name
 | E_write_reg of reg_name * register_value
 | E_escape
 | E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*)
-(*To discuss: Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
-
 
-
-(* more explicit type classes to work around the occurrences of big_int in reg_name *)
+(* more explicit type classes to work around the occurrences of big_int in reg_name ::no longer necessary?*)
 instance (Ord read_kind)
   let compare = defaultCompare
   let (<) = defaultLess
@@ -340,18 +296,17 @@ instance (SetType event)
   let setElemCompare = eventCompare
 end
 
-
 (* Functions to build up the initial state for interpretation *)
-val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come from a .lem file generated by Sail*)
+val build_context : specification -> memory_reads -> memory_writes -> barriers -> external_functions -> context 
 val initial_instruction_state : context -> string -> list register_value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)
 
 (*Type representint the constructor parameters in instruction, other is a type not representable externally*)
 type instr_parm_typ = 
   | Bit (*A single bit, represented as a one element Bitvector as a value*)
-  | Range of maybe int (*Internall represented as a number, externally as a bitvector of length int *)
+  | Range of maybe nat (*Internall represented as a number, externally as a bitvector of length int *)
   | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
-  | Bvector of maybe int (* A bitvector type, with length when statically known *)
+  | Bvector of maybe nat (* A bitvector type, with length when statically known *)
 
 let instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
   | (Bit,Bit) -> true
@@ -366,8 +321,9 @@ instance (Eq instr_parm_typ)
   let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
 end 
 
-(*A representation of the AST node for each instruction in the spec, with concrete values from this call, and the potential static effects from the funcl clause for this instruction 
-Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
+(*A representation of the AST node for each instruction in the spec, with concrete values from this call,
+  and the potential static effects from the funcl clause for this instruction 
+  Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
 *)
 type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect)
 
@@ -438,17 +394,17 @@ val word8_list_of_integer : integer -> integer -> list word8
 
 (* constructing values *)
 
-val register_value : bit_lifted -> direction -> int -> int -> register_value
+val register_value : bit_lifted -> direction -> nat -> nat -> register_value
 let register_value b dir width start_index = 
-  <| rv_bits = List.replicate (natFromInt width) b;
-     rv_dir = dir; (* D_increasing for Power *)
+  <| rv_bits = List.replicate width b;
+     rv_dir = dir; (* D_increasing for Power, D_decreasing for ARM *)
      rv_start = start_index; |>
 
-val register_value_zeros : direction -> int -> int -> register_value
+val register_value_zeros : direction -> nat -> nat -> register_value
 let register_value_zeros dir width start_index = 
   register_value Bitl_zero dir width start_index
 
-val register_value_ones : direction -> int -> int -> register_value
+val register_value_ones : direction -> nat -> nat -> register_value
 let register_value_ones dir width start_index = 
   register_value Bitl_one dir width start_index
 
@@ -462,8 +418,8 @@ let memory_value_unknown (width:int) : memory_value =
 
 (* lengths *)  
 
-val memory_value_length : memory_value -> integer
-let memory_value_length (mv:memory_value) = integerFromNat (List.length mv)
+val memory_value_length : memory_value -> nat
+let memory_value_length (mv:memory_value) = List.length mv
 
 
 (* aux fns *)
@@ -549,16 +505,16 @@ let integer_of_bit_list b =
   integerFromBoolList (false,(List.reverse (List.map bit_to_bool b)))
   (* integerFromBoolList takes a list with LSB first, so we reverse it *)
 
-val bit_list_of_integer : int -> integer -> list bit 
+val bit_list_of_integer : nat -> integer -> list bit 
 let bit_list_of_integer len b = 
   List.map (fun b -> if b then Bitc_one else Bitc_zero) 
-    (reverse (boolListFrombitSeq (natFromInt len) (bitSeqFromInteger Nothing b)))
+    (reverse (boolListFrombitSeq len (bitSeqFromInteger Nothing b)))
 
 val integer_of_byte_list : list byte -> integer 
 let integer_of_byte_list bytes = integer_of_bit_list (List.concatMap (fun (Byte bs) -> bs) bytes)
 
-val byte_list_of_integer : int -> integer -> list byte 
-let byte_list_of_integer (len:int) (a:integer):list byte = 
+val byte_list_of_integer : nat -> integer -> list byte 
+let byte_list_of_integer (len:nat) (a:integer):list byte = 
   let bits = bit_list_of_integer (len * 8) a in bytes_of_bits bits
 
 
@@ -620,8 +576,8 @@ let integer_of_memory_value (mv:memory_value):maybe integer =
   | Nothing -> Nothing 
   end
 
-val memory_value_of_integer : int -> integer -> memory_value 
-let memory_value_of_integer (len:int) (i:integer):memory_value =
+val memory_value_of_integer : nat -> integer -> memory_value 
+let memory_value_of_integer (len:nat) (i:integer):memory_value =
   List.map (byte_lifted_of_byte) (byte_list_of_integer len i)
 
 
@@ -633,8 +589,8 @@ let integer_of_register_value (rv:register_value):maybe integer =
   end 
 
   
-val register_value_of_integer : int -> int -> integer -> register_value 
-let register_value_of_integer (len:int) (start:int) (i:integer):register_value =
+val register_value_of_integer : nat -> nat -> integer -> register_value 
+let register_value_of_integer (len:nat) (start:nat) (i:integer):register_value =
   let bs = bit_list_of_integer len i in
   <| 
   rv_bits = List.map bit_lifted_of_bit bs;