Small tweaks to interp_interface interface

Also adding more comments and getting the ml files built in the build process

1 files changed, 31 insertions, 15 deletions

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index a1ddef88..b1275d14 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -2,19 +2,29 @@ import Interp
 open import Pervasives
 open import Num
 
-type read_kind = Interp.read_kind
-type write_kind = Interp.write_kind
-type barrier_kind = Interp.barrier_kind
-
 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
+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 = Plain | Sync | LwSync | Eieio | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD
+
 type value = 
-| Bitvector of list bool (* For register accesses *)
+| Bitvector of list bool   (* For register accesses *)
+(*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
-
-type instruction_state = Interp.stack
-type context = Interp.top_level
+(*To add: an abstract value representing an unknown but named memory address?*)
 
 type slice = (integer * integer)
 
@@ -49,19 +59,25 @@ type event =
 | E_read_reg of reg_name
 | E_write_reg of reg_name * value
 | E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*)
-(*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
+(*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*)
 
+(* 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 initial_instruction_state : context -> string -> list value -> instruction_state 
+  (* string is a function name, list of value are the parameters to that function *)
 
-val build_context : Interp_ast.defs Interp.tannot -> context
-val initial_instruction_state : context -> string -> value -> instruction_state
-
-type interp_mode = Interp.interp_mode 
+(* Big step of the interpreter, to the next request for an external action *)
+(* When interp_mode has eager_eval false, interpreter is (close to) small step *)
 val interp : interp_mode -> instruction_state -> outcome
 
-val interp_exhaustive : instruction_state -> list event
+(* Run the interpreter without external interaction, feeding in Unknown on all reads *)
+val interp_exhaustive : interp_mode -> instruction_state -> list event
+
+(* As above, but will request register reads: outcome will only be rreg, done, or error *)
+val rr_interp_exhaustive : interp_mode -> instruction_state -> list event -> (outcome * (list event)) 
 
-val rr_interp_exhaustive : instruction_state -> list event -> (outcome * (list event)) (* Like interp_exhaustive but will read registers; the outcome will only ever be a rreg request, done, or error *)
 
+(*To discuss: Are these functions needed, since the memory requests carry the register dependencies for that request? *)
 val mem_read_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory reads to compute the addressses in is*)
 
 val mem_write_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory writes to compute the address (and value?, in a separate list?)*)