Revert "Need to separate out the 0.10 lem library from upcoming 0.11"

This reverts commit 3fb4cf236c0d4b15831576faa45c763853632568.

1 files changed, 0 insertions, 326 deletions

diff --git a/src/lem_interp/0.11/interp_interface.lem b/src/lem_interp/0.11/interp_interface.lem
deleted file mode 100644
index 32744da2..00000000
--- a/src/lem_interp/0.11/interp_interface.lem
+++ /dev/null
@@ -1,326 +0,0 @@
-(*========================================================================*)
-(*     Sail                                                               *)
-(*                                                                        *)
-(*  Copyright (c) 2013-2017                                               *)
-(*    Kathyrn Gray                                                        *)
-(*    Shaked Flur                                                         *)
-(*    Stephen Kell                                                        *)
-(*    Gabriel Kerneis                                                     *)
-(*    Robert Norton-Wright                                                *)
-(*    Christopher Pulte                                                   *)
-(*    Peter Sewell                                                        *)
-(*    Alasdair Armstrong                                                  *)
-(*    Brian Campbell                                                      *)
-(*    Thomas Bauereiss                                                    *)
-(*    Anthony Fox                                                         *)
-(*    Jon French                                                          *)
-(*    Dominic Mulligan                                                    *)
-(*    Stephen Kell                                                        *)
-(*    Mark Wassell                                                        *)
-(*                                                                        *)
-(*  All rights reserved.                                                  *)
-(*                                                                        *)
-(*  This software was developed by the University of Cambridge Computer   *)
-(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
-(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
-(*                                                                        *)
-(*  Redistribution and use in source and binary forms, with or without    *)
-(*  modification, are permitted provided that the following conditions    *)
-(*  are met:                                                              *)
-(*  1. Redistributions of source code must retain the above copyright     *)
-(*     notice, this list of conditions and the following disclaimer.      *)
-(*  2. Redistributions in binary form must reproduce the above copyright  *)
-(*     notice, this list of conditions and the following disclaimer in    *)
-(*     the documentation and/or other materials provided with the         *)
-(*     distribution.                                                      *)
-(*                                                                        *)
-(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
-(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
-(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
-(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
-(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
-(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
-(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
-(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
-(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
-(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
-(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
-(*  SUCH DAMAGE.                                                          *)
-(*========================================================================*)
-
-(* PS NOTES FOR KATHY:
-
-pls also change:  
-
-  decode_to_istate
-  decode_to_instruction 
-
-to take an opcode as defined above, instead of a value 
-
-and change 
-
-*)
-
-
-open import Sail_impl_base
-import Interp
-open import Interp_ast
-open import Pervasives
-open import Num
-
-open import Assert_extra
-
-(*Type representing 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*)
-  | Bvector of maybe nat (* A bitvector type, with length when statically known *)
-  | Range of maybe nat (*Internally represented as a number, externally as a bitvector of length nat *)
-  | Enum of string * nat (*Internally represented as either a number or constructor, externally as a bitvector*)
-  | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
-
-let {coq} instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
-  | (Bit,Bit) -> true
-  | (Bvector i1,Bvector i2) -> i1 = i2
-  | (Range i1,Range i2) -> i1 = i2
-  | (Enum s1 i1,Enum s2 i2) -> s1 = s2 && i1 = i2
-  | (Other,Other) -> true
-  | _ -> false
-end
-let inline ~{coq} instr_parm_typEqual = unsafe_structural_equality
-
-let {coq} instr_parm_typInequal ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
-let inline ~{coq} instr_parm_typInequal = unsafe_structural_inequality
-
-instance (Eq instr_parm_typ) 
-  let (=) = instr_parm_typEqual
-  let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
-end 
-
-let instr_parm_typShow ip = match ip with
-  | Bit -> "Bit"
-  | Bvector i -> "Bvector " ^ show i
-  | Range i -> "Range " ^ show i
-  | Enum s i -> "Enum " ^ s ^ " " ^ show i
-  | Other -> "Other"
- end
-
-instance (Show instr_parm_typ)
-let show = instr_parm_typShow
-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
-*)
-
-
-type instruction_field_value = list bit
-
-type instruction = (string * list (string * instr_parm_typ * instruction_field_value))
-
-let {coq} instructionEqual i1 i2 = match (i1,i2) with
-  | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2
-end
-let inline ~{coq} instructionEqual = unsafe_structural_equality
-
-let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2)
-let inline ~{coq} instructionInequal = unsafe_structural_inequality
-
-type v_kind = Bitv | Bytev
-
-type decode_error = 
-  | Unsupported_instruction_error of Interp_ast.value
-  | Not_an_instruction_error of opcode
-  | Internal_error of string
-
-
-let decode_error_compare e1 e2 =
-  match (e1, e2) with
-  | (Unsupported_instruction_error i1, Unsupported_instruction_error i2)
-      -> defaultCompare i1 i2
-  | (Unsupported_instruction_error _, _) -> LT
-  | (_, Unsupported_instruction_error _) -> GT
-
-  | (Not_an_instruction_error o1, Not_an_instruction_error o2) -> defaultCompare o1 o2
-  | (Not_an_instruction_error _, _) -> LT
-  | (_, Not_an_instruction_error _) -> GT
-
-  | (Internal_error s1, Internal_error s2) -> compare s1 s2
-  (* | (Internal_error _, _) -> LT *)
-  (* | (_, Internal_error _) -> GT *)
-  end
-
-let decode_error_less e1 e2       = decode_error_compare e1 e2 =  LT
-let decode_error_less_eq e1 e2    = decode_error_compare e1 e2 <> GT
-let decode_error_greater e1 e2    = decode_error_compare e1 e2 =  GT
-let decode_error_greater_eq e1 e2 = decode_error_compare e1 e2 <> LT
-
-instance (Ord decode_error)
-  let compare = decode_error_compare
-  let (<)  = decode_error_less
-  let (<=) = decode_error_less_eq
-  let (>)  = decode_error_greater
-  let (>=) = decode_error_greater_eq
-end
-
-let decode_error_equal e1 e2 = (decode_error_compare e1 e2) = EQ
-let decode_error_inequal e1 e2 = not (decode_error_equal e1 e2)
-
-instance  (Eq decode_error)
-  let (=)  = decode_error_equal
-  let (<>) = decode_error_inequal
-end
-
-
-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_ast.tannot (*Deem abstract*)
-type interpreter_mode = Interp.interp_mode (*Deem abstract*)
-type interp_mode = <| internal_mode: interpreter_mode |>
-val make_mode : (*eager*) bool -> (*tracking*) bool -> interp_mode
-val tracking_dependencies : interp_mode -> bool
-
-
-
-(*Map between external functions as preceived from a Sail spec and the actual implementation of the function *)
-type external_functions = list (string * (Interp_ast.value -> Interp_ast.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_ast.value -> (memory_value * nat * maybe (list reg_name))
-type optional_memory_transformer = interp_mode -> Interp_ast.value -> maybe memory_value
-type memory_read = MR of read_kind * memory_parameter_transformer
-type memory_reads  = list (string * memory_read)
-type memory_read_tagged  = MRT of read_kind * memory_parameter_transformer
-type memory_read_taggeds = list (string * memory_read_tagged)
-type memory_write_ea = MEA of write_kind * memory_parameter_transformer
-type memory_write_eas = list (string * memory_write_ea)
-type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state))
-and memory_writes = list (string * memory_write)
-and memory_write_val = MV of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state))
-and memory_write_vals = list (string * memory_write_val)
-and excl_res_t = ER of maybe (instruction_state -> bool -> instruction_state)
-and excl_res = maybe (string * excl_res_t)
-and memory_write_val_tagged = MVT of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state))
-and memory_write_vals_tagged = list (string * memory_write_val_tagged)
-
-(* Definition information needed to run an instruction *)
-and context =
-    Context of Interp.top_level * direction * 
-	memory_reads * memory_read_taggeds * memory_writes * memory_write_eas * memory_write_vals * memory_write_vals_tagged * barriers * excl_res * external_functions
-
-(* An instruction in flight *)
-and instruction_state = IState of interpreter_state * context
-
-
-type outcome =
-(* Request to read N bytes at address *)
-(* The register list, used when mode.track_values, is those that the address depended on *)
-| Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) * (memory_value -> instruction_state)
-| Read_mem_tagged of read_kind * address_lifted * nat * maybe (list reg_name) * ((bit_lifted * memory_value) -> instruction_state)
-
-(* Request to write memory *)
-| Write_mem of write_kind * address_lifted * nat * maybe (list reg_name)
-  * memory_value * maybe (list reg_name)  * (bool -> instruction_state)
-
-(* Request the result of store-exclusive *)
-| Excl_res of (bool -> instruction_state)
-
-(* Tell the system a write is imminent, at address lifted tainted by register list, of size nat *)
-| Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * instruction_state
-
-(* Request to write memory at last signaled address. Memory value should be 8* the size given in Write_ea *)
-| Write_memv of maybe address_lifted * memory_value * maybe (list reg_name) * (bool -> instruction_state)
-| Write_memv_tagged of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name) * (bool -> instruction_state)
-
-(* Request a memory barrier *)
-| Barrier of barrier_kind * instruction_state
-
-(* Tell the system to dynamically recalculate dependency footprint *)
-| Footprint of instruction_state
-
-(* Request to read register, will track dependency when mode.track_values *)
-| Read_reg of reg_name * (register_value -> instruction_state) 
-
-(* Request to write register *)
-| Write_reg of reg_name * register_value * instruction_state
-
-(* List of instruciton states to be run in parallel, any order*)
-| Nondet_choice of list instruction_state * instruction_state
-
-(* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally 
-   provide a handler.  The non-optional instruction_state is what we would be doing if we're 
-   not escaping. This is for exhaustive interp *)
-| Escape of maybe instruction_state * instruction_state
-
-(*Result of a failed assert with possible error message to report*)
-| Fail of maybe string
-
-(* Stop for incremental stepping, function can be used to display function call data *)
-| Internal of maybe string * maybe (unit -> string) * instruction_state
-
-(* Analysis can lead to non_deterministic evaluation, represented with this outcome *)
-(*Note: this should not be externally visible *)
-| Analysis_non_det of list instruction_state * instruction_state
-
-(*Completed interpreter*)
-| Done
-
-(*Interpreter error*)
-| Error of string
-
-
-(* Functions to build up the initial state for interpretation *)
-val build_context : bool -> specification -> memory_reads -> memory_read_taggeds-> memory_writes -> memory_write_eas -> memory_write_vals -> memory_write_vals_tagged -> barriers -> excl_res -> 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 instruction_or_decode_error =
-  | IDE_instr of Interp_ast.value
-  | IDE_decode_error of decode_error
-
-(** propose to remove the following type and use the above instead *)
-type i_state_or_error =
-  | Instr of Interp_ast.value * instruction_state
-  | Decode_error of decode_error
-
-
-(** PS:I agree. propose to remove this: Function to decode an instruction and build the state to run it*)
-val decode_to_istate : context -> maybe (list (reg_name * register_value)) -> opcode -> i_state_or_error
-
-(** propose to add this, and then use instruction_to_istate on the result: Function to decode an instruction and build the state to run it*)
-(** PS made a placeholder in interp_inter_imp.lem, but it just uses decode_to_istate and throws away the istate; surely it's easy to just do what's necessary to get the instruction.   This sort-of works, but it crashes on ioid 10 after 167 steps - maybe instruction_to_istate (which I wasn't using directly before) isn't quite right? *)
-val decode_to_instruction : context -> maybe (list (reg_name * register_value))-> opcode -> instruction_or_decode_error
-
-(*Function to generate the state to run from an instruction form; is always an Instr*)
-val instruction_to_istate : context -> instruction -> instruction_state (*i_state_or_error*)
-
-(* Slice a register value into a smaller vector, starting at first number (wrt the indices of the register value, not raw positions in its list of bits) and going to second (inclusive) according to order. *)
-val slice_reg_value : register_value -> nat -> nat -> register_value
-(*Create a new register value where the contents of nat to nat are replaced by the second register_value *)  
-val update_reg_value_slice : reg_name -> register_value -> nat -> nat -> register_value -> register_value
-
-
-(* 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
-
-(* Run the interpreter without external interaction, feeding in Unknown on all reads 
-except for those register values provided *)
-val interp_exhaustive : maybe (list (reg_name * register_value)) -> 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 translate_address :
-  context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address
-  -> maybe address * maybe (list event)
-
-                      
-val instruction_analysis :
-  context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat)))
-  -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind)
-
-
-val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit
-