summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp.lem334
-rw-r--r--src/lem_interp/interp_inter_imp.lem182
-rw-r--r--src/lem_interp/interp_interface.lem178
-rw-r--r--src/lem_interp/interp_utilities.lem4
-rw-r--r--src/lem_interp/printing_functions.ml25
5 files changed, 411 insertions, 312 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index b1ee613d..ae773ad1 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1,6 +1,7 @@
open import Pervasives
import Map
import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *)
+import Set_extra (* For 'to_list' because map only goes to set *)
import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
open import Show_extra (* for 'show' to convert nat to string) *)
open import String_extra (* for chr *)
@@ -36,10 +37,10 @@ let is_inc = function | IInc -> true | _ -> false end
let id_of_string s = (Id_aux (Id s) Unknown)
type reg_form =
- | Reg of id * tannot
+ | Reg of id * tannot * i_direction
| SubReg of id * reg_form * index_range
-type ctor_kind = C_Enum | C_Union
+type ctor_kind = C_Enum of nat | C_Union
type value =
| V_boxref of nat * t
@@ -57,17 +58,6 @@ type value =
| V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *)
| V_track of value * (list reg_form) (* Used when memory system wants to track what register(s) a value came from *)
-(*let rec integerToString n acc =
- if n = 0 then
- acc
- else
- integerToString (n / 10) (chr (natFromInteger (n mod 10 + 48)) :: acc)
-
-let string_of_integer i = if i = 0 then "0" else toString(integerToString i [])*)
-(*val string_of_integer : integer -> string
-declare ocaml target_rep function string_of_integer = `Big_int_Z.string_of_big_int`*)
-
-
let rec string_of_value v = match v with
| V_boxref nat t -> "$#" ^ (show nat) ^ "$"
| V_lit (L_aux lit _) ->
@@ -124,6 +114,8 @@ and value_eq left right =
t = t' &&
listEqualBy id_value_eq l l'
| (V_ctor i t ckind v, V_ctor i' t' ckind' v') -> t = t' && ckind=ckind' && id_value_eq (i, v) (i', v')
+ | (V_ctor _ _ (C_Enum i) _,V_lit (L_aux (L_num j) _)) -> i = (natFromInteger j)
+ | (V_lit (L_aux (L_num j) _), V_ctor _ _ (C_Enum i) _) -> i = (natFromInteger j)
| (V_unknown,_) -> true
| (_,V_unknown) -> true
| (V_track v _, v2) -> value_eq v v2
@@ -138,7 +130,7 @@ end
let reg_start_pos reg =
match reg with
- | Reg _ (Just(typ,_,_,_)) ->
+ | Reg _ (Just(typ,_,_,_)) _ ->
let start_from_vec targs = match targs with
| T_args [T_arg_nexp (Ne_const s);_;_;_] -> natFromInteger s
end in
@@ -158,7 +150,7 @@ end
let reg_size reg =
match reg with
- | Reg _ (Just(typ,_,_,_)) ->
+ | Reg _ (Just(typ,_,_,_)) _ ->
let end_from_vec targs = match targs with
| T_args [_;T_arg_nexp (Ne_const s);_;_] -> natFromInteger s
end in
@@ -190,17 +182,17 @@ let unitv = V_lit (L_aux L_unit Unknown)
type lmem = LMem of nat * map nat value
(* Environment for bindings *)
-type env = list (id * value)
+type env = map string value
(* Environment for lexical bindings, nat is a counter to build new unique variables when necessary *)
type lenv = LEnv of nat * env
let emem = LMem 1 Map.empty
-let eenv = LEnv 1 []
+let eenv = LEnv 1 Map.empty
-type sub_reg_map = list (id * index_range)
+type sub_reg_map = map string index_range
(*top_level is a tuple of
- (all definitions,
+ (function definitions environment,
all extracted instructions (where possible),
default direction
letbound and enum values,
@@ -208,7 +200,14 @@ type sub_reg_map = list (id * index_range)
Typedef union constructors,
sub register mappings, and register aliases) *)
type top_level =
- | Env of (defs tannot) * list instruction_form * i_direction * env * env * list (id * typ) * list (id * sub_reg_map) * list (id * (alias_spec tannot))
+ | Env of map string (list (funcl tannot)) (*function definitions environment*)
+ * list instruction_form (* extracted instructions (where extractable) *)
+ * i_direction (*default direction*)
+ * env (*letbound and enum values*)
+ * env (*register values*)
+ * map string typ (*typedef union constructors *)
+ * map string sub_reg_map (*sub register mappings*)
+ * map string (alias_spec tannot) (*register aliases*)
type action =
| Read_reg of reg_form * maybe (nat * nat)
@@ -220,16 +219,18 @@ type action =
| Nondet of list (exp tannot)
| Call_extern of string * value
| Exit of (exp tannot)
- (* For stepper, no action needed. String is function called, value is parameter, on next state is a new function body *)
+ (* For stepper, no action needed. String is function called, value is parameter where applicable *)
| Step of l * maybe string * maybe value
-(* Inverted call stack, where top item on the stack is waiting for an action to resolve and all other frames for the right stack *)
+(* Inverted call stack, where the frame with a Top stack waits for an action to resolve and
+ all other frames for their inner stack *)
type stack =
| Top
| Hole_frame of id * exp tannot * top_level * lenv * lmem * stack (* Stack frame waiting to fill a hole with a value *)
| Thunk_frame of exp tannot * top_level * lenv * lmem * stack (* Paused stack frame *)
-(*Internal representation of outcomes from running the interpreter. Actions request an external party to resolve a request or pause*)
+(*Internal representation of outcomes from running the interpreter.
+ Actions request an external party to resolve a request *)
type outcome =
| Value of value
| Action of action * stack
@@ -248,91 +249,104 @@ val interp :interp_mode -> (i_direction -> outcome -> maybe value) -> defs tanno
val resume : interp_mode -> stack -> maybe value -> outcome
(* Internal definitions to setup top_level *)
-val to_register_fields : defs tannot -> list (id * list (id * index_range))
+val to_fdefs : defs tannot -> map string (list (funcl tannot))
+let rec to_fdefs (Defs defs) =
+ match defs with
+ | [] -> Map.empty
+ | def::defs ->
+ match def with
+ | DEF_fundef f -> (match f with
+ | FD_aux (FD_function _ _ _ fcls) _ ->
+ match fcls with
+ | [] -> to_fdefs (Defs defs)
+ | (FCL_aux (FCL_Funcl name _ _) _)::_ ->
+ Map.insert (get_id name) fcls (to_fdefs (Defs defs)) end end)
+ | _ -> to_fdefs (Defs defs) end end
+
+val to_register_fields : defs tannot -> map string (map string index_range)
let rec to_register_fields (Defs defs) =
match defs with
- | [ ] -> [ ]
+ | [ ] -> Map.empty
| def::defs ->
match def with
| DEF_type (TD_aux (TD_register id n1 n2 indexes) l') ->
- (id,List.map (fun (a,b) -> (b,a)) indexes)::(to_register_fields (Defs defs))
+ Map.insert (get_id id)
+ (List.foldr (fun (a,b) imap -> Map.insert (get_id b) a imap) Map.empty indexes)
+ (to_register_fields (Defs defs))
| _ -> to_register_fields (Defs defs)
end
end
-val to_registers : defs tannot -> env
-let rec to_registers (Defs defs) =
+val to_registers : i_direction -> defs tannot -> env
+let rec to_registers dd (Defs defs) =
match defs with
- | [ ] -> [ ]
+ | [ ] -> Map.empty
| def::defs ->
match def with
- | DEF_reg_dec (DEC_aux (DEC_reg typ id) (l,tannot)) -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs))
- | DEF_reg_dec (DEC_aux (DEC_alias id aspec) (l,tannot)) -> (id, V_register_alias aspec tannot) :: (to_registers (Defs defs))
- | _ -> to_registers (Defs defs)
+ | DEF_reg_dec (DEC_aux (DEC_reg typ id) (l,tannot)) ->
+ let dir = match tannot with
+ | Nothing -> dd
+ | Just(t, _, _, _) -> dd (*TODO, lets pull the direction out properly*)
+ end in
+ Map.insert (get_id id) (V_register(Reg id tannot dir)) (to_registers dd (Defs defs))
+ | DEF_reg_dec (DEC_aux (DEC_alias id aspec) (l,tannot)) ->
+ Map.insert (get_id id) (V_register_alias aspec tannot) (to_registers dd (Defs defs))
+ | _ -> to_registers dd (Defs defs)
end
end
-val to_aliases : defs tannot -> list (id * (alias_spec tannot))
+val to_aliases : defs tannot -> map string (alias_spec tannot)
let rec to_aliases (Defs defs) =
match defs with
- | [] -> []
+ | [] -> Map.empty
| def::defs ->
match def with
- | DEF_reg_dec (DEC_aux (DEC_alias id aspec) _) -> (id, aspec) :: (to_aliases (Defs defs))
- | DEF_reg_dec (DEC_aux (DEC_typ_alias typ id aspec) _) -> (id, aspec) :: (to_aliases (Defs defs))
+ | DEF_reg_dec (DEC_aux (DEC_alias id aspec) _) ->
+ Map.insert (get_id id) aspec (to_aliases (Defs defs))
+ | DEF_reg_dec (DEC_aux (DEC_typ_alias typ id aspec) _) ->
+ Map.insert (get_id id) aspec (to_aliases (Defs defs))
| _ -> to_aliases (Defs defs)
end
end
-val to_data_constructors : defs tannot -> list (id * typ)
+val to_data_constructors : defs tannot -> map string typ
let rec to_data_constructors (Defs defs) =
match defs with
- | [] -> []
+ | [] -> Map.empty
| def :: defs ->
match def with
| DEF_type (TD_aux t _)->
match t with
| TD_variant id _ tq tid_list _ ->
- (List.map
- (fun (Tu_aux t _) ->
+ (List.foldr
+ (fun (Tu_aux t _) map ->
match t with
- | (Tu_ty_id x y) -> (y,x)
- | Tu_id x -> (x,unit_t) end) tid_list)++(to_data_constructors (Defs defs))
+ | (Tu_ty_id x y) -> Map.insert (get_id y) x map
+ | Tu_id x -> Map.insert (get_id x) unit_t map end)
+ (to_data_constructors (Defs defs))) tid_list
| _ -> to_data_constructors (Defs defs) end
| _ -> to_data_constructors (Defs defs) end
end
(*Memory and environment helper functions*)
-val in_env :forall 'a. (list (id * 'a)) -> id -> maybe 'a
-let rec in_env env id =
- match env with
- | [] -> Nothing
- | (eid,value)::env -> if (get_id eid) = (get_id id) then Just value else in_env env id
- end
+val env_from_list : list (id * value) -> env
+let env_from_list ls = List.foldr (fun (id,v) env -> Map.insert (get_id id) v env) Map.empty ls
+
+val in_env :forall 'a. map string 'a -> string -> maybe 'a
+let in_env env id = Map.lookup id env
val in_lenv : lenv -> id -> value
let in_lenv (LEnv _ env) id =
- match in_env env id with
+ match in_env env (get_id id) with
| Nothing -> V_unknown
| Just v -> v
end
-(*Prefer entries in the first when conflict*)
-let rec list_union first second =
- match first with
- | [] -> second
- | (id,v)::frst ->
- match in_env second id with
- | Nothing -> (id,v)::(list_union frst second)
- | Just _ -> (id,v)::(list_union frst
- (List.deleteBy (fun (id,v) (id2,v2) -> (get_id id) = (get_id id2))
- (id,v) second)) end
-end
-
+(*Prefer entries in the first when in conflict*)
val union_env : lenv -> lenv -> lenv
let union_env (LEnv i1 env1) (LEnv i2 env2) =
let l = if i1 < i2 then i2 else i1 in
- LEnv l (list_union env1 env2)
+ LEnv l (Map.(union) env2 env1)
val fresh_var : lenv -> (id * lenv)
let fresh_var (LEnv i env) =
@@ -340,7 +354,7 @@ let fresh_var (LEnv i env) =
((Id_aux (Id ((show i) ^ "var")) Interp_ast.Unknown), lenv)
val add_to_env : (id * value) -> lenv -> lenv
-let add_to_env entry (LEnv i env) = (LEnv i (entry::env))
+let add_to_env (id, entry) (LEnv i env) = (LEnv i (Map.insert (get_id id) entry env))
val in_mem : lmem -> nat -> value
let in_mem (LMem _ m) n =
@@ -481,7 +495,7 @@ let slice_vector v n1 n2 =
| V_vector m dir vs ->
if is_inc(dir)
then V_vector n1 dir (from_n_to_n (n1 - m) (n2 - m) vs)
- else V_vector (n1 - n2 + 1) dir (from_n_to_n (m - n1) (m - n2) vs)
+ else V_vector n1 dir (from_n_to_n (m - n1) (m - n2) vs)
| V_vector_sparse m n dir vs d ->
let (slice, still_sparse) =
if is_inc(dir)
@@ -490,15 +504,15 @@ let slice_vector v n1 n2 =
if still_sparse && is_inc(dir)
then V_vector_sparse n1 (n2 - n1) dir slice d
else if is_inc(dir) then V_vector 0 dir (List.map snd slice)
- else if still_sparse then V_vector_sparse (n1 - n2 +1) (n1 - n2) dir slice d
- else V_vector (n1 - n2 +1) dir (List.map snd slice)
+ else if still_sparse then V_vector_sparse n1 (n1 - n2) dir slice d
+ else V_vector n1 dir (List.map snd slice)
end )
-val update_field_list : list (id * value) -> list (id * value) -> list (id * value)
+val update_field_list : list (id * value) -> env -> list (id * value)
let rec update_field_list base updates =
match base with
| [] -> []
- | (id,v)::bs -> match in_env updates id with
+ | (id,v)::bs -> match in_env updates (get_id id) with
| Just v -> (id,v)::(update_field_list bs updates)
| Nothing -> (id,v)::(update_field_list bs updates) end
end
@@ -507,7 +521,7 @@ val fupdate_record : value -> value -> value
let fupdate_record base updates =
let fupdate_record_helper base updates =
(match (base,updates) with
- | (V_record t bs,V_record _ us) -> V_record t (update_field_list bs us)
+ | (V_record t bs,V_record _ us) -> V_record t (update_field_list bs (env_from_list us))
end) in
binary_taint fupdate_record_helper base updates
@@ -654,7 +668,7 @@ val add_answer_to_stack : stack -> value -> stack
let rec add_answer_to_stack stack v =
match stack with
| Top -> Top
- | Hole_frame id e t_level (LEnv i env) mem Top -> Thunk_frame e t_level (LEnv i ((id,v)::env)) mem Top
+ | Hole_frame id e t_level env mem Top -> Thunk_frame e t_level (add_to_env (id,v) env) mem Top
| Thunk_frame e t_level env mem Top -> Thunk_frame e t_level env mem Top
| Hole_frame id e t_level env mem stack -> Hole_frame id e t_level env mem (add_answer_to_stack stack v)
| Thunk_frame e t_level env mem stack -> Thunk_frame e t_level env mem (add_answer_to_stack stack v)
@@ -717,7 +731,7 @@ let rec combine_typs ts =
let reg_to_t r =
match r with
- | Reg id (Just (t,_,_,_)) -> t
+ | Reg _ (Just (t,_,_,_)) _ -> t
| _ -> T_var "fresh"
end
@@ -765,7 +779,7 @@ let rec to_exp mode env v : (exp tannot * lenv) =
(Interp_ast.Unknown,
if is_ctor
then match ctor_kind with
- | Just(C_Enum) -> (enum_annot (val_typ v))
+ | Just(C_Enum _) -> (enum_annot (val_typ v))
| _ -> (ctor_annot (val_typ v)) end
else (val_annot (val_typ v))) in
let annot = mk_annot false Nothing in
@@ -775,7 +789,7 @@ let rec to_exp mode env v : (exp tannot * lenv) =
if mode.track_values
then ((e::es), union_env ev env)
else ((e::es), env))
- ([],(LEnv l [])) vs in
+ ([],(LEnv l Map.empty)) vs in
(es, union_env env lenv)
in
match v with
@@ -827,7 +841,7 @@ let rec to_exp mode env v : (exp tannot * lenv) =
else let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) annotation, env')
| _ ->
let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) annotation,env') end)
- | V_register (Reg id tan) -> (E_aux (E_id id) annot, env)
+ | V_register (Reg id tan dir) -> (E_aux (E_id id) annot, env)
| V_track v' _ ->
if mode.track_values
then begin let (fid,env') = fresh_var env in
@@ -845,11 +859,11 @@ let rec env_to_let_help mode env taint_env = match env with
let tan = (val_annot t) in
let (e,taint_env) = to_exp mode taint_env v in
let (rest,taint_env) = env_to_let_help mode env taint_env in
- ((((P_aux (P_id i) (Unknown,tan)),e),t)::rest, taint_env)
+ ((((P_aux (P_id (id_of_string i)) (Unknown,tan)),e),t)::rest, taint_env)
end
let env_to_let mode (LEnv _ env) (E_aux e annot) taint_env =
- match env_to_let_help mode env taint_env with
+ match env_to_let_help mode (Set_extra.toList (Map.toSet env)) taint_env with
| ([],taint_env) -> (E_aux e annot,taint_env)
| ([((p,e),t)],tain_env) ->
(E_aux (E_let (LB_aux (LB_val_implicit p e) (Unknown,(val_annot t))) e) annot,taint_env)
@@ -874,11 +888,11 @@ let rec match_pattern (P_aux p _) value_whole =
match p with
| P_lit(lit) ->
if is_lit_vector lit then
- let (V_vector n inc bits) = litV_to_vec lit IInc in (*TODO use type annotation to select between increasing and decreasing*)
+ let (V_vector n inc bits) = litV_to_vec lit IInc in
match value with
| V_lit litv ->
if is_lit_vector litv then
- let (V_vector n' inc' bits') = litV_to_vec litv IInc in (*TODO use type annotation to select between increasing and decreasing *)
+ let (V_vector n' inc' bits') = litV_to_vec litv IInc in
if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l = r) && rest) true bits bits',false, eenv)
else (false,false,eenv)
else (false,false,eenv)
@@ -896,12 +910,12 @@ let rec match_pattern (P_aux p _) value_whole =
end
| P_wild -> (true,false,eenv)
| P_as pat id ->
- let (matched_p,used_unknown,(LEnv bi bounds)) = match_pattern pat value in
+ let (matched_p,used_unknown,bounds) = match_pattern pat value in
if matched_p then
- (matched_p,used_unknown,(LEnv bi ((id,value_whole)::bounds)))
+ (matched_p,used_unknown,(add_to_env (id,value_whole) bounds))
else (false,false,eenv)
- | P_typ typ pat -> match_pattern pat value_whole (* Might like to destructure against the type to get information, but that's looking less useful *)
- | P_id id -> (true, false, (LEnv 0 [(id,value_whole)]))
+ | P_typ typ pat -> match_pattern pat value_whole
+ | P_id id -> (true, false, (LEnv 0 (Map.fromList [((get_id id),value_whole)])))
| P_app (Id_aux id _) pats ->
match value with
| V_ctor (Id_aux cid _) t ckind (V_tuple vals) ->
@@ -935,10 +949,11 @@ let rec match_pattern (P_aux p _) value_whole =
| P_record fpats _ ->
match value with
| V_record t fvals ->
+ let fvals_env = env_from_list fvals in
List.foldr
(fun (FP_aux (FP_Fpat id pat) _) (matched_p,used_unknown,bounds) ->
if matched_p then
- let (matched_p,used_unknown',new_bounds) = match in_env fvals id with
+ let (matched_p,used_unknown',new_bounds) = match in_env fvals_env (get_id id) with
| Nothing -> (false,false,eenv)
| Just v -> match_pattern pat v end in
(matched_p, (used_unknown || used_unknown'), (union_env new_bounds bounds))
@@ -1055,10 +1070,11 @@ and vec_concat_match_plev pat r_vals dir l t =
| P_id id -> (match t with
| T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
- let (matched_p,used_unknown,(LEnv bi bounds),matcheds,r_vals) = vec_concat_match wilds r_vals in
+ let (matched_p,used_unknown,bounds,matcheds,r_vals) = vec_concat_match wilds r_vals in
if matched_p
then (matched_p, used_unknown,
- (LEnv bi ((id,(V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds))::bounds)),
+ (add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds))
+ bounds),
matcheds,r_vals)
else (false,false,eenv,[],[])
| T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
@@ -1072,10 +1088,10 @@ and vec_concat_match_plev pat r_vals dir l t =
(false,false,eenv,[],[]) (*TODO see if can have some constraint bounds here*)
| _ -> (false,false,eenv,[],[]) end)
| P_as (P_aux pat (l',Just(t,_,_,_))) id ->
- let (matched_p, used_unknown, (LEnv bi bounds),matcheds,r_vals) = vec_concat_match_plev pat r_vals dir l t in
+ let (matched_p, used_unknown, bounds,matcheds,r_vals) = vec_concat_match_plev pat r_vals dir l t in
if matched_p
then (matched_p, used_unknown,
- (LEnv bi ((id,V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds)::bounds)),
+ (add_to_env (id,V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds) bounds),
matcheds,r_vals)
else (false,false,eenv,[],[])
| P_typ _ (P_aux p (l',Just(t',_,_,_))) -> vec_concat_match_plev p r_vals dir l t
@@ -1159,7 +1175,7 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
end
and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
- let (Env defs instrs default_dir lets regs ctors subregs aliases) = t_level in
+ let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in
let (typ,tag,ncs,effect) = match annot with
| Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
| Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -1184,6 +1200,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| V_vector start dir vs ->
if start = i then (Value v,lm,le) else (Value (update_vector_start dir i 1 v),lm,le)
| _ -> (Value v,lm,le) end
+ | Typ_app (Id_aux (Id "vector") _)
+ [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_var (Kid_aux (Var "length") _)) _)) _;_;_;_] ->
+ match (detaint v) with
+ | V_vector start dir vs ->
+ let i = (List.length vs) - 1 in
+ if start = i then (Value v,lm,le) else (Value (update_vector_start dir i 1 v),lm,le)
+ | _ -> (Value v,lm,le) end
+
| _ -> (Value v,lm,le) end in
(match (tag,detaint v) with
(*Cast is telling us to read a register*)
@@ -1202,14 +1226,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| V_boxref n t -> (Value (in_mem l_mem n),l_mem,l_env)
| value -> (Value value,l_mem,l_env) end
| Tag_global ->
- match in_env lets id with
+ match in_env lets name with
| Just(value) -> (Value value, l_mem,l_env)
| Nothing ->
- (match in_env regs id with
+ (match in_env regs name with
| Just(value) -> (Value value, l_mem,l_env)
| Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_global"),l_mem,l_env) end) end
| Tag_enum ->
- match in_env lets id with
+ match in_env lets name with
| Just(value) -> (Value value,l_mem,l_env)
| Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_enum "), l_mem,l_env)
end
@@ -1217,14 +1241,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
let regf = match in_lenv l_env id with (* Check for local treatment of a register as a value *)
| V_register regform -> regform
| _ ->
- match in_env regs id with (* Register isn't a local value, so pull from global environment *)
+ match in_env regs name with (* Register isn't a local value, so pull from global environment *)
| Just(V_register regform) -> regform
- | _ -> Reg id annot end end in
+ | _ -> Reg id annot default_dir end end in
(Action (Read_reg regf Nothing)
(Hole_frame redex_id
(E_aux (E_id redex_id) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env)
| Tag_alias ->
- match in_env aliases id with
+ match in_env aliases name with
| Just aspec -> interp_alias_read mode t_level l_env l_mem aspec
| _ -> (Error l ("Internal error: alias not found"), l_mem,l_env) end
| _ ->
@@ -1393,17 +1417,17 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(fun value_whole lm le ->
match detaint value_whole with
| V_record t fexps ->
- (match in_env fexps id with
+ (match in_env (env_from_list fexps) (get_id id) with
| Just v -> (Value (retaint value_whole v),lm,l_env)
| Nothing -> (Error l "Internal_error: Field not found in record",lm,le) end)
- | V_register ((Reg _ annot) as reg_form) ->
+ | V_register ((Reg _ annot _) as reg_form) ->
let id' = match annot with
| Just((T_id id'),_,_,_) -> id'
| Just((T_abbrev (T_id id') _),_,_,_) -> id'
end in
- (match in_env subregs (Id_aux (Id id') Unknown) with
+ (match in_env subregs id' with
| Just(indexes) ->
- (match in_env indexes id with
+ (match in_env indexes (get_id id) with
| Just ir ->
let sub_reg = SubReg id reg_form ir in
(Action (Read_reg sub_reg Nothing)
@@ -1418,20 +1442,20 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(fun a ->
match (exp,a) with
| (E_aux _ (l,Just(_,Tag_extern _,_,_)),
- (Action (Read_reg ((Reg _ (Just((T_id id'),_,_,_))) as regf) Nothing) s)) ->
- match in_env subregs (Id_aux (Id id') Unknown) with
+ (Action (Read_reg ((Reg _ (Just((T_id id'),_,_,_)) _) as regf) Nothing) s)) ->
+ match in_env subregs id' with
| Just(indexes) ->
- (match in_env indexes id with
+ (match in_env indexes (get_id id) with
| Just ir ->
(Action (Read_reg (SubReg id regf ir) Nothing) s)
| _ -> Error l "Internal error, unrecognized read, no id"
end)
| Nothing -> Error l "Internal error, unrecognized read, no reg" end
| (E_aux _ (l,Just(_,Tag_extern _,_,_)),
- (Action (Read_reg ((Reg _ (Just((T_abbrev (T_id id') _),_,_,_))) as regf) Nothing) s))->
- match in_env subregs (Id_aux (Id id') Unknown) with
+ (Action (Read_reg ((Reg _ (Just((T_abbrev (T_id id') _),_,_,_)) _) as regf) Nothing) s))->
+ match in_env subregs id' with
| Just(indexes) ->
- match in_env indexes id with
+ match in_env indexes (get_id id) with
| Just ir ->
(Action (Read_reg (SubReg id regf ir) Nothing) s)
| _ -> Error l "Internal error, unrecognized read, no id"
@@ -1714,7 +1738,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
let name = get_id f in
(match tag with
| Tag_global ->
- (match find_function defs f with
+ (match Map.lookup name fdefs with
| Just(funcls) ->
(match find_funcl funcls v with
| [] ->
@@ -1737,9 +1761,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot))
end)
| Nothing ->
- (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
+ (Error l (String.stringAppend "Internal error: function with tag global unfound " name),lm,le) end)
| Tag_empty ->
- (match find_function defs f with
+ (match Map.lookup name fdefs with
| Just(funcls) ->
(match find_funcl funcls v with
| [] ->
@@ -1758,7 +1782,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| Nothing ->
(Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
| Tag_spec ->
- (match find_function defs f with
+ (match Map.lookup name fdefs with
| Just(funcls) ->
(match find_funcl funcls v with
| [] ->
@@ -1777,7 +1801,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| Nothing ->
(Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end)
| Tag_ctor ->
- (match in_ctors ctors f with
+ (match Map.lookup name ctors with
| Just(_) -> (Value (V_ctor f typ C_Union v), lm, le)
| Nothing -> (Error l (String.stringAppend "Internal error: function with ctor tag unfound " name),lm,le)
end)
@@ -1824,7 +1848,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(fun rv lm le ->
match tag with
| Tag_global ->
- (match find_function defs op with
+ (match Map.lookup name fdefs with
| Nothing -> (Error l ("Internal error, no function def for " ^ name),lm,le)
| Just (funcls) ->
(match find_funcl funcls (V_tuple [lv;rv]) with
@@ -1842,7 +1866,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
t_level l_env l_mem stack)))
end)end)
| Tag_empty ->
- (match find_function defs op with
+ (match Map.lookup name fdefs with
| Nothing -> (Error l ("Internal error, no function def for " ^ name),lm,le)
| Just (funcls) ->
(match find_funcl funcls (V_tuple [lv;rv]) with
@@ -1858,7 +1882,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
t_level l_env l_mem stack)))
end)end)
| Tag_spec ->
- (match find_function defs op with
+ (match Map.lookup name fdefs with
| Nothing -> (Error l ("No function definition found for " ^ name),lm,le)
| Just (funcls) ->
(match find_funcl funcls (V_tuple [lv;rv]) with
@@ -1938,12 +1962,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot)
: ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) =
- let (Env defs instrs default_dir lets regs ctors subregs aliases) = t_level in
+ let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in
let (typ,tag,ncs,ef) = match annot with
| Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
| Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
match lexp with
| LEXP_id id ->
+ let name = get_id id in
match tag with
| Tag_empty ->
match detaint (in_lenv l_env id) with
@@ -1963,7 +1988,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
end
| Tag_global ->
- (match in_env lets id with
+ (match in_env lets name with
| Just v ->
if is_top_level then ((Error l "Writes must be to reg or registers",l_mem,l_env),Nothing)
else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
@@ -1971,7 +1996,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
end)
| Tag_extern _ ->
let regf =
- match in_env regs id with (*pull the regform with the most specific type annotation from env *)
+ match in_env regs name with (*pull the regform with the most specific type annotation from env *)
| Just(V_register regform) -> regform
| _ -> Assert_extra.failwith "Register not known in regenv" end in
let start_pos = reg_start_pos regf in
@@ -1984,16 +2009,16 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
| Tag_alias ->
let request =
- (match in_env aliases id with
+ (match in_env aliases name with
| Just (AL_aux aspec (l,_)) ->
(match aspec with
| AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_id id),_,_,_)) as annot'))) subreg ->
- (match in_env subregs (Id_aux (Id id) Unknown) with
+ (match in_env subregs id with
| Just indexes ->
- (match in_env indexes subreg with
+ (match in_env indexes (get_id subreg) with
| Just ir ->
(Action
- (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing
+ (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing
(update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value))
(Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
t_level l_env l_mem Top), l_mem, l_env)
@@ -2001,12 +2026,12 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| _ ->
(Error l ("Internal error: alias spec has unknown register type " ^ id), l_mem, l_env) end)
| AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_abbrev (T_id id) _),_,_,_)) as annot'))) subreg ->
- (match in_env subregs (Id_aux (Id id) Unknown) with
+ (match in_env subregs id with
| Just indexes ->
- (match in_env indexes subreg with
+ (match in_env indexes (get_id subreg) with
| Just ir ->
(Action
- (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing
+ (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing
(update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value))
(Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
t_level l_env l_mem Top), l_mem, l_env)
@@ -2017,7 +2042,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
(fun v le lm -> match v with
| V_lit (L_aux (L_num i) _) ->
let i = natFromInteger i in
- (Action (Write_reg (Reg reg annot') (Just (i,i))
+ (Action (Write_reg (Reg reg annot' default_dir) (Just (i,i))
(update_vector_start default_dir i 1 value))
(Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
t_level l_env l_mem Top), l_mem, l_env) end)
@@ -2033,7 +2058,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| V_lit (L_aux (L_num stop) _) ->
let (start,stop) = (natFromInteger start,natFromInteger stop) in
let size = if start < stop then stop - start +1 else start -stop +1 in
- (Action (Write_reg (Reg reg annot') (Just (start,stop))
+ (Action (Write_reg (Reg reg annot' default_dir) (Just (start,stop))
(update_vector_start default_dir start size value))
(Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
t_level l_env l_mem Top),
@@ -2050,7 +2075,8 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| (T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); _;_]),
T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); _;_])) ->
(Action
- (Write_reg (Reg reg1 annot1) Nothing (slice_vector value (natFromInteger b1) (natFromInteger r1)))
+ (Write_reg (Reg reg1 annot1 default_dir) Nothing
+ (slice_vector value (natFromInteger b1) (natFromInteger r1)))
(Thunk_frame (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2)
(fst (to_exp <| mode with track_values =false|> eenv
(slice_vector value (natFromInteger (r1+1)) (natFromInteger r2)))))
@@ -2080,7 +2106,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
(LEXP_aux (LEXP_memory id parms) (l,annot), env)))
| Tag_global ->
let name = get_id id in
- (match find_function defs id with
+ (match Map.lookup name fdefs with
| Just(funcls) ->
let new_vals = match v with
| V_tuple vs -> V_tuple (vs ++ [value])
@@ -2113,6 +2139,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) env -> (LEXP_aux (LEXP_memory id es) (l,annot), env)))
| e -> (e,Nothing) end
| LEXP_cast typc id ->
+ let name = get_id id in
match tag with
| Tag_empty ->
match detaint (in_lenv l_env id) with
@@ -2135,7 +2162,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
end
| Tag_extern _ ->
let regf =
- match in_env regs id with (*pull the regform with the most specific type annotation from env *)
+ match in_env regs name with (*pull the regform with the most specific type annotation from env *)
| Just(V_register regform) -> regform
| _ -> Assert_extra.failwith "Register not known in regenv" end in
let start_pos = reg_start_pos regf in
@@ -2310,7 +2337,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| ((Value (V_record t fexps),lm,le),Just lexp_builder) ->
let next_builder = Just (fun e env -> let (lexp,env) = (lexp_builder e env) in
(LEXP_aux (LEXP_field lexp id) (l,annot), env)) in
- match (in_env fexps id,is_top_level) with
+ match (in_env (env_from_list fexps) (get_id id),is_top_level) with
| (Just (V_boxref n t),true) -> ((Value (V_lit (L_aux L_unit l)), update_mem lm n value, l_env),Nothing)
| (Just (V_boxref n t),false) -> ((Value (in_mem lm n),lm,l_env),next_builder)
| (Just v, true) -> ((Error l "Mutating a field access requires a reg type",lm,le),Nothing)
@@ -2323,10 +2350,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| Read_reg _ _ -> ((Action a s,lm,le), next_builder)
| Read_mem _ _ _ -> ((Action a s,lm,le), next_builder)
| Call_extern _ _ -> ((Action a s,lm,le), next_builder)
- | Write_reg ((Reg _ (Just(T_id id',_,_,_))) as regf) Nothing value ->
- match in_env subregs (Id_aux (Id id') Unknown) with
+ | Write_reg ((Reg _ (Just(T_id id',_,_,_)) _) as regf) Nothing value ->
+ match in_env subregs id' with
| Just(indexes) ->
- match in_env indexes id with
+ match in_env indexes (get_id id) with
| Just ir ->
((Action
(Write_reg (SubReg id regf ir) Nothing
@@ -2336,10 +2363,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
end
| Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end
- | Write_reg ((Reg _ (Just((T_abbrev(T_id id') _),_,_,_))) as regf) Nothing value ->
- match in_env subregs (Id_aux (Id id') Unknown) with
+ | Write_reg ((Reg _ (Just((T_abbrev(T_id id') _),_,_,_)) _) as regf) Nothing value ->
+ match in_env subregs id' with
| Just(indexes) ->
- match in_env indexes id with
+ match in_env indexes (get_id id) with
| Just ir ->
((Action
(Write_reg (SubReg id regf ir) Nothing
@@ -2352,7 +2379,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| _ -> ((Error l "Internal error, unrecognized write, no matching action",lm,le),Nothing)
end
| e -> e end)
- end
+ end
and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
match lbind with
@@ -2385,10 +2412,10 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
match alspec with
| AL_subreg (RI_aux (RI_id reg) (li,((Just (t,_,_,_)) as annot'))) subreg ->
let reg_ti = get_reg_typ_name t in
- (match in_env subregs (Id_aux (Id reg_ti) Unknown) with
+ (match in_env subregs reg_ti with
| Just indexes ->
- (match in_env indexes subreg with
- | Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot') ir) Nothing) stack, l_mem, l_env)
+ (match in_env indexes (get_id subreg) with
+ | Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing) stack, l_mem, l_env)
| _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
| _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " reg_ti), l_mem, l_env) end)
| AL_bit (RI_aux (RI_id reg) (_,annot')) e ->
@@ -2396,7 +2423,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
(fun v le lm -> match v with
| V_lit (L_aux (L_num i) _) ->
let i = natFromInteger i in
- (Action (Read_reg (Reg reg annot') (Just (i,i))) stack, l_mem, l_env) end)
+ (Action (Read_reg (Reg reg annot' default_dir) (Just (i,i))) stack, l_mem, l_env) end)
(fun a -> a) (*Should not currently happen as type system enforces constants*)
| AL_slice (RI_aux (RI_id reg) (_,annot')) start stop ->
resolve_outcome (interp_main mode t_level l_env l_mem start)
@@ -2409,11 +2436,11 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
(match v with
| V_lit (L_aux (L_num stop) _) ->
let (start,stop) = (natFromInteger start,natFromInteger stop) in
- (Action (Read_reg (Reg reg annot') (Just (start,stop))) stack, l_mem, l_env) end))
+ (Action (Read_reg (Reg reg annot' default_dir) (Just (start,stop))) stack, l_mem, l_env) end))
(fun a -> a)) end)
(fun a -> a) (*Neither action function should occur, due to above*)
| AL_concat (RI_aux (RI_id reg1) (l1, annot1)) (RI_aux (RI_id reg2) annot2) ->
- (Action (Read_reg (Reg reg1 annot1) Nothing)
+ (Action (Read_reg (Reg reg1 annot1 default_dir) Nothing)
(Hole_frame (Id_aux (Id "0") Unknown)
(E_aux (E_vector_append (E_aux (E_id (Id_aux (Id "0") l1)) (l1, (intern_annot annot1)))
(E_aux (E_id reg2) annot2))
@@ -2432,7 +2459,7 @@ let rec eval_toplevel_let handle_action tlevel env mem lbind =
| _ -> Nothing end
let rec to_global_letbinds handle_action (Defs defs) t_level =
- let (Env defs' instrs default_dir lets regs ctors subregs aliases) = t_level in
+ let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in
match defs with
| [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, eenv),t_level)
| def::defs ->
@@ -2440,15 +2467,22 @@ let rec to_global_letbinds handle_action (Defs defs) t_level =
| DEF_val lbind ->
match eval_toplevel_let handle_action t_level eenv emem lbind with
| Just le ->
- to_global_letbinds handle_action (Defs defs) (Env defs' instrs default_dir (lets++le) regs ctors subregs aliases)
+ to_global_letbinds handle_action (Defs defs)
+ (Env fdefs instrs default_dir (Map.(union) lets le) regs ctors subregs aliases)
| Nothing ->
- to_global_letbinds handle_action (Defs defs) (Env defs' instrs default_dir lets regs ctors subregs aliases) end
+ to_global_letbinds handle_action (Defs defs)
+ (Env fdefs instrs default_dir lets regs ctors subregs aliases) end
| DEF_type (TD_aux tdef _) ->
match tdef with
| TD_enum id ns ids _ ->
- let enum_vals = map (fun eid -> (eid,V_ctor eid (T_id (get_id id)) C_Enum unitv)) ids in
+ let typ = T_id (get_id id) in
+ let enum_vals =
+ Map.fromList
+ (snd
+ (List.foldl (fun (c,rst) eid -> (1+c,(get_id eid,V_ctor eid typ (C_Enum c) unitv)::rst)) (0,[]) ids)) in
to_global_letbinds
- handle_action (Defs defs) (Env defs' instrs default_dir (lets++enum_vals) regs ctors subregs aliases)
+ handle_action (Defs defs)
+ (Env fdefs instrs default_dir (Map.(union) lets enum_vals) regs ctors subregs aliases)
| _ -> to_global_letbinds handle_action (Defs defs) t_level end
| _ -> to_global_letbinds handle_action (Defs defs) t_level
end
@@ -2465,10 +2499,12 @@ let rec extract_default_direction (Defs defs) = match defs with
(*TODO Contemplate making decode and execute environment variables instead of these constants*)
let to_top_env external_functions defs =
let direction = (extract_default_direction defs) in
- let t_level = Env defs (extract_instructions "decode" "execute" defs)
+ let t_level = Env (to_fdefs defs)
+ (extract_instructions "decode" "execute" defs)
direction
- [] (* empty letbind and enum values, call below will fill in any *)
- (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
+ Map.empty (* empty letbind and enum values, call below will fill in any *)
+ (to_registers direction defs)
+ (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
let (o,t_level) = to_global_letbinds (external_functions direction) defs t_level in
match o with
| (Value _,_,_) -> (Nothing,t_level)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index da87842d..4a9964e2 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -9,13 +9,15 @@ open import Assert_extra
val intern_reg_value : register_value -> Interp.value
val intern_mem_value : direction -> memory_value -> Interp.value
-val extern_reg_value : maybe nat -> Interp.value -> register_value
+val extern_reg_value : Interp.i_direction -> maybe nat -> Interp.value -> register_value
val extern_mem_value : interp_mode -> Interp.value -> (memory_value * maybe (list reg_name))
val extern_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name
let make_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values |>;;
let tracking_dependencies mode = mode.Interp.track_values
+let make_eager_mode mode = <| mode with Interp.eager_eval = true |>;;
+let make_default_mode _ = <| Interp.eager_eval = false; Interp.track_values = false |>;;
let bitl_to_ibit = function
| Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown))
@@ -84,6 +86,11 @@ let intern_direction = function
| D_decreasing -> Interp.IDec
end
+let extern_direction = function
+ | Interp.IInc -> D_increasing
+ | Interp.IDec -> D_decreasing
+end
+
let intern_opcode direction (Opcode v) =
let bits = List.concatMap (fun (Byte(bits)) -> (List.map bit_to_ibit bits)) v in
let direction = intern_direction direction in
@@ -91,7 +98,7 @@ let intern_opcode direction (Opcode v) =
let intern_reg_value v = match v with
| <| rv_bits=[b] |> -> bitl_to_ibit b
- | _ -> Interp.V_vector v.rv_start (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits)
+ | _ -> Interp.V_vector v.rv_start_internal (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits)
end
let intern_mem_value direction v =
@@ -104,81 +111,76 @@ let intern_ifield_value direction v =
let direction = intern_direction direction in
Interp.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits
-(*let byte_list_of_integer size num =
- if (num < 0)
- then failwith "signed integer given to byte_list_of_integer"
- else let internal_value = (Interp_lib.to_vec_inc
- (Interp.V_tuple([Interp.V_lit(L_aux (L_num (size * 8)) Interp_ast.Unknown);
- Interp.V_lit(L_aux (L_num num) Interp_ast.Unknown)]))) in
- let num_check = Interp_lib.to_num Interp_lib.Unsigned internal_value in
- match (num_check,internal_value) with
- | (Interp.V_lit (L_aux (L_num n) _), Interp.V_vector _ _ bits) ->
- if num = n
- then (to_bytes (from_bits bits))
- else failwith "byte_list_of_integer given an integer larger than given size"
- end
-*)
-
let num_to_bits size kind num =
(* num_to_bits needed in src_power_get/trans_sail.gen - rather than reengineer the generation, we include a wrapper here *)
Interp_interface.bit_list_of_integer size num
-
-(*
- match kind with
- | Bitv -> Bitvector (match (Interp_lib.to_vec_inc
- (Interp.V_tuple([Interp.V_lit(L_aux (L_num (integerFromNat size)) Interp_ast.Unknown);
- Interp.V_lit(L_aux (L_num num) Interp_ast.Unknown)]))) with
- | Interp.V_vector _ _ bits -> from_bits bits end) true 0
- | Bytev -> Bytevector (byte_list_of_integer (integerFromNat (size/8)) num)
-end
-
-let integer_of_byte_list bytes =
- let intv = intern_value (Bytevector bytes) in
- match Interp_lib.to_num Interp_lib.Unsigned intv with
- | Interp.V_lit (L_aux (L_num n) _) -> n
- end
-*)
+let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
+ match d with
+ | D_increasing -> (i,j) (*This is the case the thread/concurrecny model expects, so no change needed*)
+ | D_decreasing ->
+ let slice_i = start - i in
+ let slice_j = (i - j) + slice_i in
+ (slice_i,slice_j)
+ end
let extern_reg r slice = match (r,slice) with
- | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_)),Nothing) ->
- Reg x (Interp.reg_size r)
- | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_)),Just(i1,i2)) -> Reg_slice x (intFromNat i1, intFromNat i2)
- | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) ->
- let i = intFromInteger i in
- Reg_field y x (i,i)
- | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_range i j) _), Nothing) ->
- Reg_field y x (intFromInteger i,intFromInteger j)
- | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_range i j) _), Just(i1,j1)) ->
- Reg_f_slice y x (intFromInteger i,intFromInteger j) (intFromNat i1, intFromNat j1)
+ | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_)) dir,Nothing) ->
+ Reg x (Interp.reg_start_pos r) (Interp.reg_size r) (extern_direction dir)
+ | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_)) dir,Just(i1,i2)) ->
+ let start = Interp.reg_start_pos r in
+ let edir = extern_direction dir in
+ Reg_slice x start edir (extern_slice edir start (i1, i2))
+ | (Interp.SubReg (Id_aux (Id x) _) ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_single i) _),Nothing) ->
+ let i = natFromInteger i in
+ let start = Interp.reg_start_pos main_r in
+ let edir = extern_direction dir in
+ Reg_field y start edir x (extern_slice edir start (i,i))
+ | (Interp.SubReg (Id_aux (Id x) _) ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Nothing) ->
+ let start = Interp.reg_start_pos main_r in
+ let edir = extern_direction dir in
+ Reg_field y start edir x (extern_slice edir start (natFromInteger i,natFromInteger j))
+ | (Interp.SubReg (Id_aux (Id x) _)
+ ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Just(i1,j1)) ->
+ let start = Interp.reg_start_pos main_r in
+ let edir = extern_direction dir in
+ Reg_f_slice y start edir x (extern_slice edir start (natFromInteger i,natFromInteger j))
+ (extern_slice edir start (i1, j1))
end
-let rec extern_reg_value optional_start v = match v with
- | Interp.V_track v regs -> extern_reg_value optional_start v
- | Interp.V_vector fst dir bits ->
- <| rv_bits=(bitls_from_ibits bits);
- rv_dir=(if Interp.is_inc(dir) then D_increasing else D_decreasing);
- rv_start=fst|>
- | Interp.V_vector_sparse fst stop inc bits default ->
- extern_reg_value optional_start (Interp_lib.fill_in_sparse v)
+let rec extern_reg_value dir optional_start v =
+ let start = match optional_start with | Nothing -> 0 | Just i -> i end in
+ let is_inc = Interp.is_inc(dir) in
+ match v with
+ | Interp.V_track v regs -> extern_reg_value dir optional_start v
+ | Interp.V_vector fst dir bits ->
+ let is_inc = Interp.is_inc(dir) in
+ let width = List.length bits in
+ <| rv_bits=(bitls_from_ibits bits);
+ rv_dir=(if is_inc then D_increasing else D_decreasing);
+ rv_start=if is_inc then fst else (fst +1 - width);
+ rv_start_internal = fst;
+ |>
+ | Interp.V_vector_sparse fst stop inc bits default ->
+ extern_reg_value dir optional_start (Interp_lib.fill_in_sparse v)
| Interp.V_lit (L_aux L_zero _) ->
- let start = match optional_start with | Nothing -> 0 | Just i -> i end in
- <| rv_bits=[Bitl_zero]; rv_dir=D_increasing; rv_start=start |>
+ <| rv_bits=[Bitl_zero]; rv_dir= if is_inc then D_increasing else D_decreasing;
+ rv_start= start; rv_start_internal=start |>
| Interp.V_lit (L_aux L_false _) ->
- let start = match optional_start with | Nothing -> 0 | Just i -> i end in
- <| rv_bits=[Bitl_zero]; rv_dir=D_increasing; rv_start=start |>
+ <| rv_bits=[Bitl_zero]; rv_dir=if is_inc then D_increasing else D_decreasing;
+ rv_start=start; rv_start_internal = start |>
| Interp.V_lit (L_aux L_one _) ->
- let start = match optional_start with | Nothing -> 0 | Just i -> i end in
- <| rv_bits=[Bitl_one]; rv_dir=D_increasing; rv_start=start |>
+ <| rv_bits=[Bitl_one]; rv_dir=if is_inc then D_increasing else D_decreasing;
+ rv_start=start; rv_start_internal = start |>
| Interp.V_lit (L_aux L_true _) ->
- let start = match optional_start with | Nothing -> 0 | Just i -> i end in
- <| rv_bits=[Bitl_one]; rv_dir=D_increasing; rv_start=start |>
+ <| rv_bits=[Bitl_one]; rv_dir=if is_inc then D_increasing else D_decreasing;
+ rv_start=start; rv_start_internal = start |>
| Interp.V_lit (L_aux L_undef _) ->
- let start = match optional_start with | Nothing -> 0 | Just i -> i end in
- <| rv_bits=[Bitl_undef]; rv_dir=D_increasing; rv_start=start |>
+ <| rv_bits=[Bitl_undef]; rv_dir=if is_inc then D_increasing else D_decreasing;
+ rv_start=start; rv_start_internal = start |>
| Interp.V_unknown ->
- let start = match optional_start with | Nothing -> 0 | Just i -> i end in
- <| rv_bits=[Bitl_unknown]; rv_dir=D_increasing; rv_start=start |>
+ <| rv_bits=[Bitl_unknown]; rv_dir=if is_inc then D_increasing else D_decreasing;
+ rv_start=start; rv_start_internal = start |>
end
let rec extern_mem_value mode v = match v with
@@ -416,14 +418,18 @@ let rec interp_to_outcome mode context thunk =
| Interp.Write_reg reg_form slice value ->
let optional_start =
match slice with | Just (st1,st2) -> if (st1=st2) then Just st1 else Nothing | _ -> Nothing end in
- Write_reg (extern_reg reg_form slice) (extern_reg_value optional_start value) (IState next_state context)
+ Write_reg (extern_reg reg_form slice)
+ (extern_reg_value internal_direction optional_start value) (IState next_state context)
| Interp.Read_mem (Id_aux (Id i) _) value slice ->
match List.lookup i mem_reads with
| (Just (MR read_k f)) ->
let (location, length, tracking) = (f mode value) in
if (List.length location) = 8
- then Read_mem read_k (Address_lifted location) length tracking
- (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value direction v)) context)
+ then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with
+ | Just bs -> Just (integer_of_byte_list bs)
+ | _ -> Nothing end in
+ Read_mem read_k (Address_lifted location address_int) length tracking
+ (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value direction v)) context)
else Error ("Memory address on read is not 64 bits")
| _ -> Error ("Memory " ^ i ^ " function with read kind not found")
end
@@ -433,9 +439,12 @@ let rec interp_to_outcome mode context thunk =
let (location, length, tracking) = (f mode loc_val) in
let (value, v_tracking) = (extern_mem_value mode write_val) in
if (List.length location) = 8
- then Write_mem write_k (Address_lifted location)
- length tracking value v_tracking
- (fun b ->
+ then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with
+ | Just bs -> Just (integer_of_byte_list bs)
+ | _ -> Nothing end in
+ Write_mem write_k (Address_lifted location address_int)
+ length tracking value v_tracking
+ (fun b ->
match return with
| Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context)
| Just return_bool -> return_bool (IState next_state context) b end)
@@ -472,40 +481,44 @@ let interp mode (IState interp_state context) =
interp_to_outcome mode context (fun _ -> Interp.resume mode interp_state Nothing)
(*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*)
+(*TODO immediate: this will be impacted by need to change slicing *)
let rec find_reg_name reg = function
| [] -> Nothing
| (reg_name,v)::registers ->
match (reg,reg_name) with
- | (Reg i size, Reg n size2) -> if i = n && size = size2 then (Just v) else find_reg_name reg registers
- | (Reg_slice i (p1,p2), Reg n _) ->
- if i = n then (Just (slice_reg_value v (natFromInt p1) (natFromInt p2))) else find_reg_name reg registers
- | (Reg_field i f (p1,p2), Reg n _) ->
- if i = n then (Just (slice_reg_value v (natFromInt p1) (natFromInt p2))) else find_reg_name reg registers
- | (Reg_slice i (p1,p2), Reg_slice n (p3,p4)) ->
+ | (Reg i start size dir, Reg n start2 size2 dir2) ->
+ if i = n && size = size2 then (Just v) else find_reg_name reg registers
+ | (Reg_slice i _ _ (p1,p2), Reg n _ _ _) ->
+ if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
+ | (Reg_field i _ _ f (p1,p2), Reg n _ _ _) ->
+ if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
+ | (Reg_slice i _ _ (p1,p2), Reg_slice n _ _ (p3,p4)) ->
if i=n
then if p1=p3 && p2 = p4 then (Just v)
- else if p1>=p3 && p2<= p4 then (Just (slice_reg_value v (natFromInt p1) (natFromInt p2)))
+ else if p1>=p3 && p2<= p4 then (Just (slice_reg_value v p1 p2))
else find_reg_name reg registers
else find_reg_name reg registers
- | (Reg_field i f _,Reg_field n fn _) ->
+ | (Reg_field i _ _ f _,Reg_field n _ _ fn _) ->
if i=n && f = fn then (Just v) else find_reg_name reg registers
- | (Reg_f_slice i f _ (p1,p2), Reg_f_slice n fn _ (p3,p4)) ->
+ | (Reg_f_slice i _ _ f _ (p1,p2), Reg_f_slice n _ _ fn _ (p3,p4)) ->
if i=n && f=fn && p1=p3 && p2=p3 then (Just v) else find_reg_name reg registers
| _ -> find_reg_name reg registers
end end
+(*Update slice potentially here*)
let reg_size = function
- | Reg i size -> size
- | Reg_slice i (p1,p2) -> natFromInt (if p1 < p2 then (p2-p1 +1) else (p1-p2 +1))
- | Reg_field i f (p1,p2) -> natFromInt (if p1 < p2 then (p2-p1 +1) else (p1-p2 +1))
- | Reg_f_slice i f _ (p1,p2) -> natFromInt (if p1 < p2 then p2-p1 +1 else p1-p2+1)
+ | Reg i _ size _ -> size
+ | Reg_slice i _ _ (p1,p2) -> if p1 < p2 then (p2-p1 +1) else (p1-p2 +1)
+ | Reg_field i _ _ f (p1,p2) -> if p1 < p2 then (p2-p1 +1) else (p1-p2 +1)
+ | Reg_f_slice i _ _ f _ (p1,p2) -> if p1 < p2 then p2-p1 +1 else p1-p2+1
end
let rec ie_loop mode register_values (IState interp_state context) =
let (Context _ direction externs reads writes barriers) = context in
let unknown_reg size =
<| rv_bits = (List.replicate size Bitl_unknown);
- rv_start = (if direction = D_increasing then 0 else (size-1));
+ rv_start = 0;
+ rv_start_internal = (if direction = D_increasing then 0 else (size-1));
rv_dir = direction |> in
let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in
match interp mode (IState interp_state context) with
@@ -538,7 +551,8 @@ let rec rr_ie_loop mode i_state =
let (IState _ (Context _ direction _ _ _ _)) = i_state in
let unknown_reg size =
<| rv_bits = (List.replicate size Bitl_unknown);
- rv_start = (if direction=D_increasing then 0 else (size-1));
+ rv_start = 0;
+ rv_start_internal = (if direction=D_increasing then 0 else (size-1));
rv_dir = direction |> in
let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in
match (interp mode i_state) with
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 213b7d51..830877e1 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -53,7 +53,14 @@ type direction =
| D_increasing
| D_decreasing
-type register_value = <| rv_bits: list bit_lifted (* MSB first, smallest index number *); rv_dir: direction; rv_start: nat |>
+type register_value = <|
+ rv_bits: list bit_lifted (* 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_lifted = Byte_lifted of list bit_lifted (* of length 8 *)
@@ -61,14 +68,14 @@ type instruction_field_value = list bit
type byte = Byte of list bit (* of length 8 *) (*MSB first*)
-type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*)
+type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer
type memory_byte = byte_lifted
type memory_value = list memory_byte (* the head of the list, most-significant first, at the lowest address, of length >=1 *)
(* not sure which of these is more handy yet *)
-type address = Address of list byte (* of length 8 *)
+type address = Address of list byte (* of length 8 *) * integer
(* type address = Address of integer *)
type opcode = Opcode of list byte (* of length 4 *)
@@ -130,40 +137,46 @@ instance (Ord address_lifted)
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 slice = (nat * nat)
type reg_name =
-| Reg of string * nat
-(*Name of the register, accessing the entire register, and the size of this register *)
+| Reg of string * nat * nat * direction
+(*Name of the register, accessing the entire register, the start and size of this register, and it's direction *)
-| Reg_slice of string * slice
+| Reg_slice of string * nat * direction * 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. *)
+machineDef* the first is a smaller number or equal to the second, adjusted
+to reflect the correct span direction in the interpreter side. *)
-| Reg_field of string * string * slice
-(*Name of the register and name of the field of the register
+| Reg_field of string * nat * direction * string * 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_f_slice of string * string * slice * slice
-(* The first three components are as in Reg_field; the final slice
+| Reg_f_slice of string * nat * direction * string * slice * 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 *)
-
-(* 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')
+ | (Reg s1 ns1 d1 l1, Reg s2 ns2 d2 l2) -> s1=s2 && ns1 = ns2 && l1=l2 && d1=d2
+ | (Reg_slice s1 ns1 d1 sl1, Reg_slice s2 ns2 d2 sl2) -> s1=s2 && ns1=ns2 && d1=d2 && (slice_eq sl1 sl2)
+ | (Reg_field s1 ns1 d1 f1 sl1, Reg_field s2 ns2 d2 f2 sl2) -> s1=s2 && ns1=ns2 && d1=d2 && f1=f2 && (slice_eq sl1 sl2)
+ | (Reg_f_slice s1 ns1 d1 f1 sl1 sl1', Reg_f_slice s2 ns2 d2 f2 sl2 sl2') ->
+ s1=s2 && ns1=ns2 && d1=d2 && f1=f2 && (slice_eq sl1 sl2) && (slice_eq sl1' sl2')
| _ -> false
end
+instance (Ord direction)
+ let compare = defaultCompare
+ let (<) = defaultLess
+ let (<=) = defaultLessEq
+ let (>) = defaultGreater
+ let (>=) = defaultGreaterEq
+end
+
instance (Eq reg_name)
let (=) = reg_nameEqual
let (<>) x y = not (reg_nameEqual x y)
@@ -171,15 +184,15 @@ 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) ->
+ | (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') ->
+ | (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
+ | (Reg _ _ _ _, _) -> LT
+ | (Reg_slice _ _ _ _, _) -> LT
+ | (Reg_field _ _ _ _ _, _) -> LT
| (_, _) -> GT
end
@@ -195,6 +208,20 @@ instance (Ord reg_name)
let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT
end
+let direction_of_reg_name r = match r with
+ | Reg _ _ _ d -> d
+ | Reg_slice _ _ d _ -> d
+ | Reg_field _ _ d _ _ -> d
+ | Reg_f_slice _ _ d _ _ _ -> d
+ end
+
+let start_of_reg_name r = match r with
+ | Reg _ start _ _ -> start
+ | Reg_slice _ start _ _ -> start
+ | Reg_field _ start _ _ _ -> start
+ | Reg_f_slice _ start _ _ _ _ -> start
+end
+
(* Data structures for building up instructions *)
type read_kind =
@@ -376,20 +403,9 @@ val decode_to_instruction : context -> 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*)
-(* Augment an address by the given value *)
-(*val add_to_address : value -> integer -> value
-
-(* Coerce a Bitvector value (presumed a multiple of 8 bits long) to a Bytevector value *)
-val coerce_Bytevector_of_Bitvector : value -> value
-
-(* Coerce a Bytevector value to a Bitvector value, increasing and starting at zero *)
-val coerce_Bitvector_of_Bytevector : value -> value*)
-
(* 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
-(*(*append two vectors (bit x byte -> bit) *)
-val append_value : value -> value -> 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 *)
@@ -410,13 +426,31 @@ val bitls_to_word8 : list bit_lifted -> word8
val integer_of_word8_list : list word8 -> integer
val word8_list_of_integer : integer -> integer -> list word8
+val concretizable_bitl : bit_lifted -> bool
+val concretizable_bytl : byte_lifted -> bool
+val concretizable_bytls : list byte_lifted -> bool
+
+let concretizable_bitl = function
+ | Bitl_zero -> true
+ | Bitl_one -> true
+ | Bitl_undef -> false
+ | Bitl_unknown -> false
+end
+
+let concretizable_bytl (Byte_lifted bs) = List.all concretizable_bitl bs
+let concretizable_bytls = List.all concretizable_bytl
+
(* constructing values *)
val register_value : bit_lifted -> direction -> nat -> nat -> register_value
let register_value b dir width start_index =
<| rv_bits = List.replicate width b;
rv_dir = dir; (* D_increasing for Power, D_decreasing for ARM *)
- rv_start = start_index; |>
+ rv_start_internal = start_index;
+ rv_start = if dir = D_increasing
+ then start_index
+ else (start_index+1) - width; (* Smaller index, as in Power, for external interaction *)
+ |>
val register_value_zeros : direction -> nat -> nat -> register_value
let register_value_zeros dir width start_index =
@@ -429,9 +463,9 @@ let register_value_ones dir width start_index =
val byte_lifted_unknown : byte_lifted
let byte_lifted_unknown = Byte_lifted (List.replicate 8 Bitl_unknown)
-val memory_value_unknown : int (*the number of bytes*) -> memory_value
-let memory_value_unknown (width:int) : memory_value =
- List.replicate (natFromInt width) byte_lifted_unknown
+val memory_value_unknown : nat (*the number of bytes*) -> memory_value
+let memory_value_unknown (width:nat) : memory_value =
+ List.replicate width byte_lifted_unknown
(* lengths *)
@@ -539,13 +573,12 @@ let byte_list_of_integer (len:nat) (a:integer):list byte =
val integer_of_address : address -> integer
let integer_of_address (a:address):integer =
match a with
- | Address bs -> integer_of_byte_list bs
+ | Address bs i -> i
end
val address_of_integer : integer -> address
let address_of_integer (i:integer):address =
- Address (byte_list_of_integer 8 i)
-
+ Address (byte_list_of_integer 8 i) i
(* regarding a list of int as a list of bytes in memory, MSB lowest-address first, convert to an integer *)
@@ -561,28 +594,26 @@ let integer_address_of_int_list (is: list int) =
val address_of_byte_list : list byte -> address
let address_of_byte_list bs =
if List.length bs <> 8 then failwith "address_of_byte_list given list not of length 8" else
- Address bs
-
+ Address bs (integer_of_byte_list bs)
(* operations on addresses *)
-val add_address_int : address -> int -> address
-let add_address_int (a:address) (i:int) : address =
- address_of_integer ((integer_of_address a) + (integerFromInt i))
+val add_address_nat : address -> nat -> address
+let add_address_nat (a:address) (i:nat) : address =
+ address_of_integer ((integer_of_address a) + (integerFromNat i))
val clear_low_order_bits_of_address : address -> address
let clear_low_order_bits_of_address a =
match a with
- | Address [b0;b1;b2;b3;b4;b5;b6;b7] ->
+ | Address [b0;b1;b2;b3;b4;b5;b6;b7] i ->
match b7 with
| Byte [bt0;bt1;bt2;bt3;bt4;bt5;bt6;bt7] ->
let b7' = Byte [bt0;bt1;bt2;bt3;bt4;bt5;Bitc_zero;Bitc_zero] in
- Address [b0;b1;b2;b3;b4;b5;b6;b7']
+ let bytes = [b0;b1;b2;b3;b4;b5;b6;b7'] in
+ Address bytes (integer_of_byte_list bytes)
end
end
-
-
val byte_list_of_memory_value : memory_value -> maybe (list byte)
let byte_list_of_memory_value mv = maybe_all (List.map byte_of_memory_byte mv)
@@ -605,29 +636,30 @@ let integer_of_register_value (rv:register_value):maybe integer =
| Nothing -> Nothing
| Just bs -> Just (integer_of_bit_list bs)
end
-
-val register_value_of_integer : nat -> nat -> integer -> register_value
-let register_value_of_integer (len:nat) (start:nat) (i:integer):register_value =
+val register_value_of_integer : nat -> nat -> direction -> integer -> register_value
+let register_value_of_integer (len:nat) (start:nat) (dir:direction) (i:integer):register_value =
let bs = bit_list_of_integer len i in
<|
rv_bits = List.map bit_lifted_of_bit bs;
- rv_dir = D_increasing;
+ rv_dir = dir;
rv_start = start;
+ rv_start_internal = if dir = D_increasing then start else start + (List.length bs) - 1
|>
-
(* *)
val opcode_of_bytes : byte -> byte -> byte -> byte -> opcode
let opcode_of_bytes b0 b1 b2 b3 : opcode = Opcode [b0;b1;b2;b3]
-val register_value_of_address : address -> register_value
-let register_value_of_address (Address bytes) : register_value =
- <| rv_bits = List.concatMap (fun (Byte bs) -> List.map bit_lifted_of_bit bs) bytes;
- rv_dir = D_increasing;
- rv_start = 0; |>
-
+val register_value_of_address : address -> direction -> register_value
+let register_value_of_address (Address bytes _) dir : register_value =
+ let bits = List.concatMap (fun (Byte bs) -> List.map bit_lifted_of_bit bs) bytes in
+ <| rv_bits = bits;
+ rv_dir = dir;
+ rv_start = 0;
+ rv_start_internal = if dir = D_increasing then 0 else (List.length bits) - 1
+ |>
val address_lifted_of_register_value : register_value -> maybe address_lifted
@@ -636,18 +668,22 @@ allowing Bitl_undef and Bitl_unknown *)
let address_lifted_of_register_value (rv:register_value) : maybe address_lifted =
if List.length rv.rv_bits <> 64 then Nothing
else
- Just (Address_lifted (byte_lifteds_of_bit_lifteds rv.rv_bits))
-
+ Just (Address_lifted (byte_lifteds_of_bit_lifteds rv.rv_bits)
+ (if List.all concretizable_bitl rv.rv_bits
+ then let (Just(bits)) = (maybe_all (List.map bit_of_bit_lifted rv.rv_bits)) in
+ Just (integer_of_bit_list bits)
+ else Nothing))
val address_of_address_lifted : address_lifted -> maybe address
(* returning Nothing iff the address contains any Bitl_undef or Bitl_unknown *)
let address_of_address_lifted (al:address_lifted): maybe address =
match al with
- | Address_lifted bls ->
+ | Address_lifted bls (Just i)->
match maybe_all ((List.map byte_of_byte_lifted) bls) with
| Nothing -> Nothing
- | Just bs -> Just (Address bs)
+ | Just bs -> Just (Address bs i)
end
+ | _ -> Nothing
end
val address_of_register_value : register_value -> maybe address
@@ -690,13 +726,13 @@ let int_of_memory_byte (mb:memory_byte) : int =
val memory_value_of_address_lifted : address_lifted -> memory_value
let memory_value_of_address_lifted (al:address_lifted) =
match al with
- | Address_lifted bs -> bs
+ | Address_lifted bs _ -> bs
end
val byte_list_of_address : address -> list byte
let byte_list_of_address (a:address) : list byte =
match a with
- | Address bs -> bs
+ | Address bs _ -> bs
end
val byte_list_of_opcode : opcode -> list byte
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index 0a23e74c..e87600a3 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -22,6 +22,10 @@ let lit_eq (L_aux left _) (L_aux right _) =
| (L_one, L_one) -> true
| (L_true, L_true) -> true
| (L_false, L_false) -> true
+ | (L_zero, L_num i) -> i = 0
+ | (L_num i,L_zero) -> i = 0
+ | (L_one, L_num i) -> i = 1
+ | (L_num i, L_one) -> i = 1
| (L_num n, L_num m) -> n = m
| (L_hex h, L_hex h') -> h = h'
| (L_bin b, L_bin b') -> b = b'
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 5bf3acc8..b4c5fa96 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -231,11 +231,20 @@ let rec bit_to_hex v =
;;*)
let reg_name_to_string = function
- | Reg0(s,_) -> s
- | Reg_slice(s,(first,second)) ->
+ | Reg0(s,_,_,_) -> s
+ | Reg_slice(s,start,dir,(first,second)) ->
+ let first,second =
+ match dir with
+ | D_increasing -> (first,second)
+ | D_decreasing -> (start - first, start - second) in
s ^ "[" ^ string_of_int first ^ (if (first = second) then "" else ".." ^ (string_of_int second)) ^ "]"
- | Reg_field(s,f,_) -> s ^ "." ^ f
- | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f ^ "]" ^ string_of_int first ^ (if (first = second) then "" else ".." ^ (string_of_int second)) ^ "]"
+ | Reg_field(s,_,_,f,_) -> s ^ "." ^ f
+ | Reg_f_slice(s,start,dir,f,_,(first,second)) ->
+ let first,second =
+ match dir with
+ | D_increasing -> (first,second)
+ | D_decreasing -> (start - first, start - second) in
+ s ^ "." ^ f ^ "]" ^ string_of_int first ^ (if (first = second) then "" else ".." ^ (string_of_int second)) ^ "]"
let dependencies_to_string dependencies = String.concat ", " (List.map reg_name_to_string dependencies)
@@ -335,10 +344,10 @@ let rec format_events = function
" Failed with message : " ^ s ^ "\n"
| (E_error s)::events ->
" Failed with message : " ^ s ^ " but continued on erroneously\n"
- | (E_read_mem(read_kind, (Address_lifted location), length, tracking))::events ->
+ | (E_read_mem(read_kind, (Address_lifted(location, _)), length, tracking))::events ->
" Read_mem at " ^ (memory_value_to_string location) ^ " for " ^ (string_of_int length) ^ " bytes \n" ^
(format_events events)
- | (E_write_mem(write_kind,(Address_lifted location), length, tracking, value, v_tracking))::events ->
+ | (E_write_mem(write_kind,(Address_lifted (location,_)), length, tracking, value, v_tracking))::events ->
" Write_mem at " ^ (memory_value_to_string location) ^ " writing " ^ (memory_value_to_string value) ^ " across " ^ (string_of_int length) ^ " bytes\n" ^
(format_events events)
| ((E_barrier b_kind)::events) ->
@@ -401,8 +410,8 @@ let local_variables_to_string (IState(stack,_)) =
| LEnv(_,env) ->
String.concat ", " (option_map (fun (id,value)->
match id with
- | Id_aux(Id "0",_) -> None (*Let's not print out the context hole again*)
- | _ -> Some (id_to_string id ^ "=" ^ val_to_string_internal mem value)) env)
+ | "0" -> None (*Let's not print out the context hole again*)
+ | _ -> Some (id ^ "=" ^ val_to_string_internal mem value)) (Pmap.bindings_list env))
let instr_parm_to_string (name, typ, value) =
name ^"="^
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 12:02:25 +0000