diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 25 | ||||
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 7 | ||||
| -rw-r--r-- | src/type_internal.ml | 10 |
3 files changed, 32 insertions, 10 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index ef0dbc00..5556a61b 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -97,20 +97,39 @@ type env = list (id * value) let emem = LMem 1 Map.empty -(* These may need to be refined or expanded based on memory requirement *) +type read_kind = Read_plain | Read_reserve | Read_acquire +type write_kind = Write_plain | Write_conditional | Write_release + +(*type outcome = (* these should be related to the Sail effect language, obviously...*) + | Read_mem of read_kind * value (*the address*) * (value -> instruction_state) (* the continuation parameterised just on a value or on a write? *) + | Write_mem of write_kind * value (*the address*) * value (*the value*) * (bool (*ss wcond success*) -> instruction state) + | Barrier of barrier_kind * instruction_state + | Read_reg of reg_name * (value -> instruction_state) + | Write_reg of reg_name * value * instruction_state + | Write_next_instruction_address of value * instruction_state (* separate out NIA and _PC from the real Write_reg? *) + | Internal of instruction_state (* normally we'll want the system to eagerly do these, either within the interpreter or outside. But not always: sometimes we'll want to single-step through them - or at the block-level or somesuch *) + | Nondet_choice of list instruction_state (* for (1) explicit nondet choices of single bits in the ISA, (2) interpreting conditionals that hit a "don't know" value in register/memory footprint calculation, and perhaps (3) interpreting intra-instruction parallelism, eg for load-multiple *) + | Done + | Error of ... (* for internal errors that should all be prevented by Sail typechecking and careful writing of the ISA semantics *) + | Undefined_instruction of ... (* for dynamically detected occurrences of UNPREDICTABLE *) +*) + type action = | Read_reg of reg_form * maybe (integer * integer) | Write_reg of reg_form * maybe (integer* integer) * value | Read_mem of id * value * maybe (integer * integer) | Write_mem of id * value * maybe (integer * integer) * value + | Barrier of id * value + | Write_next_IA of value + | Nondet of list (exp tannot) + | Debug of l | Call_extern of string * value -(* Inverted call stack, where top item on the stack is waiting for an action and all other frames for the right stack *) +(* Inverted call stack, where top item on the stack is waiting for an action to resolve and all other frames for the right stack *) type stack = | Top | Frame of id * exp tannot * env * lmem * stack -(* Either a case must be added for parallel options or action must be tied to a list *) type outcome = | Value of value * tag (* If tag is external and value is register, then register value should be read *) | Action of action * stack diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index a7cf265f..753de883 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -66,9 +66,12 @@ let arith_op op (V_tuple args) = match args with | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx) end ;; let arith_op_vec op (V_tuple args) = match args with - | [(V_vector _ _ _ as l1);(V_vector _ _ _ as l2)] -> + | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] -> let (l1',l2') = (to_num true l1,to_num true l2) in - arith_op op (V_tuple [l1';l2']) + let n = arith_op op (V_tuple [l1';l2']) in + if ord + then to_vec_inc (List.length cs) n + else to_vec_dec (List.length cs) n end ;; let arith_op_range_vec op (V_tuple args) = match args with | [l1; (V_vector _ _ _ as l2)] -> diff --git a/src/type_internal.ml b/src/type_internal.ml index 827c5525..26a03d6a 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -544,7 +544,7 @@ let initial_typ_env = Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) - (mk_range {nexp = Nconst 0} {nexp = N2n (mk_nv "n")}))), External (Some "add_vec"),[],pure_e); + (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n")))), External (Some "add_vec"),[],pure_e); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_range (mk_nv "o") (mk_nv "p")]) @@ -1070,7 +1070,7 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 = and type_coerce co d_env t1 e t2 = type_coerce_internal co d_env t1 [] e t2 [];; let rec conforms_to_t spec actual = - let _ = Printf.printf "conforms_to_t called with %s, %s\n" (t_to_string spec) (t_to_string actual) in + (*let _ = Printf.printf "conforms_to_t called with %s, %s\n" (t_to_string spec) (t_to_string actual) in*) match spec.t,actual.t with | Tuvar _,_ -> true | Ttup ss, Ttup acs -> (List.length ss = List.length acs) && List.for_all2 conforms_to_t ss acs @@ -1080,20 +1080,20 @@ let rec conforms_to_t spec actual = then List.for_all2 conforms_to_ta tas [TA_typ t] else conforms_to_t spec t | Tapp(is,tas), Tapp(ia, taa) -> - let _ = Printf.printf "conforms to given two apps: %b, %b\n" (is = ia) (List.length tas = List.length taa) in + (*let _ = Printf.printf "conforms to given two apps: %b, %b\n" (is = ia) (List.length tas = List.length taa) in*) (is = ia) && (List.length tas = List.length taa) && (List.for_all2 conforms_to_ta tas taa) | Tabbrev(_,s),a -> conforms_to_t s actual | s,Tabbrev(_,a) -> conforms_to_t spec a | _,_ -> false and conforms_to_ta spec actual = - let _ = Printf.printf "conforms_to_ta called with %s, %s\n" (targ_to_string spec) (targ_to_string actual) in + (*let _ = Printf.printf "conforms_to_ta called with %s, %s\n" (targ_to_string spec) (targ_to_string actual) in*) match spec,actual with | TA_typ s, TA_typ a -> conforms_to_t s a | TA_nexp s, TA_nexp a -> conforms_to_n s a | TA_ord s, TA_ord a -> conforms_to_o s a | TA_eft s, TA_eft a -> conforms_to_e s a and conforms_to_n spec actual = - let _ = Printf.printf "conforms_to_n called with %s, %s\n" (n_to_string spec) (n_to_string actual) in + (*let _ = Printf.printf "conforms_to_n called with %s, %s\n" (n_to_string spec) (n_to_string actual) in*) match spec.nexp,actual.nexp with | Nuvar _,_ -> true | Nconst si,Nconst ai -> si==ai |