summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp.lem249
-rw-r--r--src/lem_interp/interp_inter_imp.lem366
-rw-r--r--src/lem_interp/interp_utilities.lem7
-rw-r--r--src/lem_interp/printing_functions.ml2
-rw-r--r--src/pretty_print.ml6
5 files changed, 360 insertions, 270 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 15584b60..aa7edf37 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -27,8 +27,8 @@ let ctor_annot typ = Just(typ,Tag_ctor,[],pure)
let enum_annot typ max = Just(typ,Tag_enum max,[],pure)
-let non_det_annot annot = match annot with
- | Just(t,_,cs,ef) -> Just(t,Tag_unknown,cs,ef)
+let non_det_annot annot maybe_id = match annot with
+ | Just(t,_,cs,ef) -> Just(t,Tag_unknown maybe_id,cs,ef)
| _ -> Nothing
end
@@ -187,15 +187,15 @@ end
(*Constant unit value, for use in interpreter *)
let unitv = V_lit (L_aux L_unit Unknown)
-(* Store for local memory of ref cells *)
-type lmem = LMem of nat * map nat value
+(* Store for local memory of ref cells, string stores the name of the function the memory is being created for*)
+type lmem = LMem of string * nat * map nat value * set nat
(* Environment for bindings *)
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 emem name = LMem name 1 Map.empty Set.empty
let eenv = LEnv 1 Map.empty
type sub_reg_map = map string index_range
@@ -368,15 +368,19 @@ val add_to_env : (id * value) -> lenv -> lenv
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 =
+let in_mem (LMem _ _ m _) n =
Map_extra.find n m
(* Map.lookup n m *)
-val update_mem : lmem -> nat -> value -> lmem
-let update_mem (LMem c m) loc value =
+val update_mem : bool -> lmem -> nat -> value -> lmem
+let update_mem track (LMem owner c m s) loc value =
let m' = Map.delete loc m in
let m' = Map.insert loc value m' in
- LMem c m'
+ let s' = if track then Set.insert loc s else s in
+ LMem owner c m' s'
+
+val clear_updates : lmem -> lmem
+let clear_updates (LMem owner c m _) = LMem owner c m Set.empty
(*Value helper functions*)
@@ -474,7 +478,8 @@ let rec merge_values v1 v2 =
else match (v1,v2) with
| (V_lit l, V_lit l') -> if lit_eq l l' then v1 else V_unknown
| (V_boxref n t, V_boxref m t') ->
- if n = m then v1 else V_unknown (*Any change to locations in memory should be handled above this level*)
+ (*Changes to memory handled by merge_mem*)
+ if n = m then v1 else V_unknown
| (V_tuple l, V_tuple l') ->
V_tuple (map2 merge_values l l')
| (V_list l, V_list l') ->
@@ -510,6 +515,29 @@ let rec merge_values v1 v2 =
| (_, _) -> V_unknown
end
+val merge_lmems : lmem -> lmem -> lmem
+let merge_lmems ((LMem owner1 c1 mem1 set1) as lmem1) ((LMem owner2 c2 mem2 set2) as lmem2) =
+ let diff1 = Set_extra.toList (set1 \ set2) in
+ let diff2 = Set_extra.toList (set2 \ set1) in
+ let inters = Set_extra.toList (set1 inter set2) in
+ let c = max c1 c2 in
+ let mem = LMem owner1 c (if c1 >= c2 then mem1 else mem2) Set.empty in
+ let diff_mem1 =
+ List.foldr
+ (fun i mem -> update_mem false mem i
+ (match Map.lookup i mem2 with
+ | Nothing -> V_unknown
+ | Just v -> merge_values (in_mem lmem1 i) v end)) mem diff1 in
+ let diff_mem2 =
+ List.foldr
+ (fun i mem -> update_mem false mem i
+ (match Map.lookup i mem1 with
+ | Nothing -> V_unknown
+ | Just v -> merge_values (in_mem lmem2 i) v end)) diff_mem1 diff2 in
+ List.foldr
+ (fun i mem -> update_mem false mem i (merge_values (in_mem lmem1 i) (in_mem lmem2 i)))
+ diff_mem2 inters
+
let vector_length v = match (detaint v) with
| V_vector n inc vals -> List.length vals
| V_vector_sparse n m inc vals def -> m
@@ -658,15 +686,15 @@ let fupdate_vector_slice vec replace start stop =
end) in
binary_taint fupdate_vec_help vec replace
-val update_vector_slice : value -> value -> nat -> nat -> lmem -> lmem
-let update_vector_slice vector value start stop mem =
+val update_vector_slice : bool -> value -> value -> nat -> nat -> lmem -> lmem
+let update_vector_slice track vector value start stop mem =
match (detaint vector,detaint value) with
| ((V_boxref n t), v) ->
- update_mem mem n (fupdate_vector_slice (in_mem mem n) (retaint value v) start stop)
+ update_mem track mem n (fupdate_vector_slice (in_mem mem n) (retaint value v) start stop)
| ((V_vector m _ vs),(V_vector n _ vals)) ->
let (V_vector m' _ vs') = slice_vector vector start stop in
foldr2 (fun vbox v mem -> match vbox with
- | V_boxref n t -> update_mem mem n v end)
+ | V_boxref n t -> update_mem track mem n v end)
mem vs' vals
| ((V_vector m dir vs),(V_vector_sparse n o _ vals d)) ->
let (V_vector m' _ vs') = slice_vector vector start stop in
@@ -674,7 +702,7 @@ let update_vector_slice vector value start stop mem =
match vbox with
| V_boxref n t ->
(if is_inc(dir) then i+1 else i-1,
- update_mem mem n (match List.lookup i vals with
+ update_mem track mem n (match List.lookup i vals with
| Nothing -> d
| Just v -> v end))
end) (m,mem) vs' in
@@ -682,7 +710,7 @@ let update_vector_slice vector value start stop mem =
| ((V_vector m _ vs),v) ->
let (V_vector m' _ vs') = slice_vector vector start stop in
List.foldr (fun vbox mem -> match vbox with
- | V_boxref n t -> update_mem mem n v end)
+ | V_boxref n t -> update_mem track mem n v end)
mem vs'
end
@@ -753,6 +781,26 @@ let get_stack_state stack =
| Thunk_frame exp top_level lenv lmem stack -> (lenv,lmem)
end
+let rec update_stack_state stack ((LMem name c mem _) as lmem) =
+ match stack with
+ | Top -> Top
+ | Hole_frame id oe t_level env (LMem _ _ _ s) Top ->
+ (match Map.lookup (0 : nat) mem with
+ | Nothing -> Thunk_frame oe t_level (add_to_env (id,V_unknown) env) (LMem name c mem s) Top
+ | Just v -> Thunk_frame oe t_level (add_to_env (id, v) env) (LMem name c (Map.delete (0 : nat) mem) s) Top end)
+ | Thunk_frame e t_level env _ Top -> Thunk_frame e t_level env lmem Top
+ | Hole_frame id e t_level env mem s -> Hole_frame id e t_level env mem (update_stack_state s lmem)
+ | Thunk_frame e t_level env mem s -> Thunk_frame e t_level env mem (update_stack_state s lmem)
+end
+
+let rec clear_stack_state stack =
+ match stack with
+ | Top -> Top
+ | Hole_frame id e t_level env lmem Top -> Hole_frame id e t_level env (clear_updates lmem) Top
+ | Thunk_frame e t_level env lmem Top -> Thunk_frame e t_level env (clear_updates lmem) Top
+ | Hole_frame id e t_level env lmem s -> Hole_frame id e t_level env lmem (clear_stack_state s)
+ | Thunk_frame e t_level env lmem s -> Thunk_frame e t_level env lmem (clear_stack_state s)
+end
(*functions for converting in progress evaluation back into expression for building current continuation*)
let rec combine_typs ts =
@@ -942,10 +990,14 @@ let env_to_let mode (LEnv _ env) (E_aux e annot) taint_env =
(E_aux e annot))
annot, taint_env)
end
-(*
+
let fix_up_nondet typ branches annot =
- match typ with
- | T_id "unit" -> *)
+ match typ with
+ | T_id "unit" -> (branches, Nothing)
+ | T_abbrev _ (T_id "unit") -> (branches, Nothing)
+ | _ -> ((List.map
+ (fun e -> E_aux (E_assign (LEXP_aux (LEXP_id redex_id) annot) e) annot) branches), Just "0")
+end
(* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
val match_pattern : top_level -> pat tannot -> value -> bool * bool * lenv
@@ -1379,7 +1431,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| (V_vector _ _ [(V_lit(L_aux L_one _))],true) -> interp_main mode t_level l_env lm thn
| (V_vector _ _ [(V_lit(L_aux L_one _))],false) -> debug_out Nothing Nothing thn t_level lm l_env
| (V_unknown,_) ->
- interp_main mode t_level l_env lm (E_aux (E_block [thn;els]) (l,annot))
+ let (branches,maybe_id) = fix_up_nondet typ [thn;els] (l,annot) in
+ interp_main mode t_level l_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id))
| (_,true) -> interp_main mode t_level l_env lm els
| (_,false) -> debug_out Nothing Nothing els t_level lm l_env end)
(fun a -> update_stack a (add_to_top_frame (fun c env -> (E_aux (E_if c thn els) (l,annot), env))))
@@ -1471,7 +1524,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
let (lets,taint_env) =
List.foldr (fun (env,_,exp) (rst,taint_env) ->
let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
- interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot))
+ let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
+ interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,(non_det_annot annot maybe_id)))
end)
(fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_case e pats) (l,annot), env))))
| E_record(FES_aux (FES_Fexps fexps _) fes_annot) ->
@@ -1848,7 +1902,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| E_block exps -> interp_block mode t_level l_env l_env l_mem l annot exps
| E_nondet exps ->
(Action (Nondet exps tag)
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,(intern_annot annot))) t_level l_env l_mem Top),
+ (match tag with
+ | Tag_unknown (Just id) ->
+ Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot))) t_level l_env l_mem Top
+ | _ ->
+ Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,(intern_annot annot))) t_level l_env l_mem Top end),
l_mem, l_env)
| E_app f args ->
(match (exp_list mode t_level
@@ -1868,8 +1926,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| [(env,_,exp)] ->
resolve_outcome
(if mode.eager_eval
- then (interp_main mode t_level env emem exp)
- else (debug_out (Just name) (Just v) exp t_level emem env))
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just v) exp t_level (emem name) env))
(fun ret lm le -> (Value ret, l_mem,l_env))
(fun a -> update_stack a
(fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
@@ -1878,7 +1936,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
let (lets,taint_env) =
List.foldr (fun (env,_,exp) (rst,taint_env) ->
let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
- interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot))
+ let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
+ interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,(non_det_annot annot maybe_id)))
end)
| Nothing ->
(Error l (String.stringAppend "Internal error: function with tag global unfound " name),lm,le) end)
@@ -1891,8 +1950,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| [(env,used_unknown,exp)] ->
resolve_outcome
(if mode.eager_eval
- then (interp_main mode t_level env emem exp)
- else (debug_out (Just name) (Just v) exp t_level emem env))
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just v) exp t_level (emem name) env))
(fun ret lm le -> (Value ret, l_mem,l_env))
(fun a -> update_stack a
(fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
@@ -1909,8 +1968,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| [(env,used_unknown,exp)] ->
resolve_outcome
(if mode.eager_eval
- then (interp_main mode t_level env emem exp)
- else (debug_out (Just name) (Just v) exp t_level emem env))
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just v) exp t_level (emem name) env))
(fun ret lm le -> (Value ret, l_mem,l_env))
(fun a -> update_stack a
(fun stack ->
@@ -1977,8 +2036,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| [(env,used_unknown,exp)] ->
resolve_outcome
(if mode.eager_eval
- then (interp_main mode t_level env emem exp)
- else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level emem env))
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level (emem name) env))
(fun ret lm le -> (Value ret,l_mem,l_env))
(fun a -> update_stack a
(fun stack ->
@@ -1994,8 +2053,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| [(env,used_unknown,exp)] ->
resolve_outcome
(if mode.eager_eval
- then (interp_main mode t_level env emem exp)
- else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level emem env))
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level (emem name) env))
(fun ret lm le -> (Value ret,l_mem,l_env))
(fun a -> update_stack a
(fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,annot))
@@ -2010,8 +2069,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| [(env,used_unknown,exp)] ->
resolve_outcome
(if mode.eager_eval
- then (interp_main mode t_level env emem exp)
- else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level emem env))
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level (emem name) env))
(fun ret lm le -> (Value ret,l_mem,l_env))
(fun a -> update_stack a
(fun stack -> (Hole_frame redex_id
@@ -2102,17 +2161,28 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
match detaint (in_lenv l_env id) with
| ((V_boxref n t) as v) ->
if is_top_level
- then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n (recenter_val t value), l_env),Nothing)
+ then ((Value (V_lit (L_aux L_unit l)),
+ update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
| V_unknown ->
if is_top_level then
- let (LMem c m) = l_mem in
- let l_mem = (LMem (c+1) m) in
- ((Value (V_lit (L_aux L_unit l)),
- update_mem l_mem c value, (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+ if name = "0" then
+ ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+ else
+ let (LMem owner c m s) = l_mem in
+ let l_mem = (LMem owner (c+1) m s) in
+ ((Value (V_lit (L_aux L_unit l)),
+ update_mem mode.track_lmem l_mem c value,
+ (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
| v ->
- if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
+ if is_top_level
+ then
+ if name = "0" then
+ ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+ else
+ ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),l_mem,l_env),
+ Nothing)
else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
end
| Tag_global ->
@@ -2251,8 +2321,8 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
" on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing)
| [(env,used_unknown,exp)] ->
(match (if mode.eager_eval
- then (interp_main mode t_level env emem exp)
- else (debug_out (Just name) (Just new_vals) exp t_level emem env)) with
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just new_vals) exp t_level (emem name) env)) with
| (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing)
| (Action action stack,lm,le) ->
(((update_stack (Action action stack)
@@ -2263,7 +2333,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
let (lets,taint_env) =
List.foldr (fun (env,_,exp) (rst,taint_env) ->
let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
- (interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot)), Nothing)
+ let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
+ (interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id)),
+ Nothing)
end)
| Nothing ->
((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end)
@@ -2280,8 +2352,8 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
" on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing)
| [(env,used_unknown,exp)] ->
(match (if mode.eager_eval
- then (interp_main mode t_level env emem exp)
- else (debug_out (Just name) (Just new_vals) exp t_level emem env)) with
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just new_vals) exp t_level (emem name) env)) with
| (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing)
| (Action action stack,lm,le) ->
(((update_stack (Action action stack)
@@ -2292,7 +2364,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
let (lets,taint_env) =
List.foldr (fun (env,_,exp) (rst,taint_env) ->
let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
- (interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot)), Nothing)
+ let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
+ (interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id)),
+ Nothing)
end)
| Nothing ->
((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end)
@@ -2307,14 +2381,16 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
match detaint (in_lenv l_env id) with
| ((V_boxref n t) as v) ->
if is_top_level
- then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n (recenter_val t value), l_env),Nothing)
- else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
+ then ((Value (V_lit (L_aux L_unit l)),
+ update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
+ else ((Value v, l_mem, l_env),
+ Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
| V_unknown ->
if is_top_level
then begin
- let (LMem c m) = l_mem in
- let l_mem = (LMem (c+1) m) in
- ((Value (V_lit (L_aux L_unit l)), update_mem l_mem c value,
+ let (LMem owner c m s) = l_mem in
+ let l_mem = (LMem owner (c+1) m s) in
+ ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value,
(add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
end
else ((Error l ("Undefined id " ^ (get_id id)),l_mem,l_env),Nothing)
@@ -2331,13 +2407,16 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
let reg_size = reg_size regf in
let request =
(Action (Write_reg regf Nothing
- (if is_top_level then (update_vector_start default_dir start_pos reg_size value) else value))
+ (if is_top_level
+ then (update_vector_start default_dir start_pos reg_size value)
+ else 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) in
if is_top_level then (request,Nothing)
else (request,Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
| _ ->
- ((Error l ("Internal error: writing to id not extern or empty " ^(get_id id)),l_mem,l_env),Nothing)
+ ((Error l ("Internal error: writing to id not extern or empty " ^(get_id id)),l_mem,l_env),
+ Nothing)
end
| LEXP_vector lexp exp ->
match (interp_main mode t_level l_env l_mem exp) with
@@ -2361,13 +2440,16 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
(match (in_mem lm i,is_top_level,maybe_builder) with
| ((V_vector _ _ _ as vec),true,_) ->
let new_vec = fupdate_vector_slice vec (V_vector 1 default_dir [value]) n n in
- ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm i new_vec, l_env), Nothing)
+ ((Value (V_lit (L_aux L_unit Unknown)),
+ update_mem mode.track_lmem lm i new_vec, l_env), Nothing)
| ((V_track (V_vector _ _ _ as vec) r), true,_) ->
let new_vec = fupdate_vector_slice vec (V_vector 1 default_dir [value]) n n in
- ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm i (taint new_vec r),l_env),Nothing)
+ ((Value (V_lit (L_aux L_unit Unknown)),
+ update_mem mode.track_lmem lm i (taint new_vec r),l_env),Nothing)
| ((V_vector _ _ _ as vec),false, Just lexp_builder) ->
((Value (access_vector vec n), lm, l_env), Just (next_builder lexp_builder))
- | (v,_,_) -> Assert_extra.failwith("no vector findable in set bit, found " ^ (string_of_value v))
+ | (v,_,_) ->
+ Assert_extra.failwith("no vector findable in set bit, found " ^ (string_of_value v))
end )
| V_vector inc m vs ->
(match (nth(),is_top_level,maybe_builder) with
@@ -2386,11 +2468,15 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
l_mem,l_env),
Just (next_builder lexp_builder))
| (V_boxref n t,true,_) ->
- ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
+ ((Value (V_lit (L_aux L_unit Unknown)), update_mem mode.track_lmem lm n value, l_env),
+ Nothing)
| (V_unknown,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, l_env),Nothing)
- | (v,true,_) -> ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing)
- | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
- | (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
+ | (v,true,_) ->
+ ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing)
+ | ((V_boxref n t),false, Just lexp_builder) ->
+ ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
+ | (v,false, Just lexp_builder) ->
+ ((Value v,lm,le), Just (next_builder lexp_builder)) end)
| V_vector_sparse n m inc vs d ->
(match (nth(),is_top_level,maybe_builder) with
| (V_register regform,true,_) ->
@@ -2407,13 +2493,15 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
l_mem,l_env),
Just (next_builder lexp_builder))
| (V_boxref n t,true,_) ->
- ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
- | (v,true,_) ->
- ((Error l ("Vector does not contain reg or register values " ^ (string_of_value v)),lm,l_env),
+ ((Value (V_lit (L_aux L_unit Unknown)), update_mem mode.track_lmem lm n value, l_env),
Nothing)
+ | (v,true,_) ->
+ ((Error l ("Vector does not contain reg or register values " ^ (string_of_value v)),
+ lm,l_env), Nothing)
| ((V_boxref n t),false, Just lexp_builder) ->
((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
- | (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
+ | (v,false, Just lexp_builder) ->
+ ((Value v,lm,le), Just (next_builder lexp_builder)) end)
| v ->
((Error l ("Vector access to write of non-vector" ^ (string_of_value v)),lm,l_env),Nothing)
end)
@@ -2430,13 +2518,16 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
then (update_vector_start default_dir n 1 value)
else (access_vector value n))) s,lm,le),
Just (next_builder lexp_builder))
- | ((Write_mem id a Nothing value),true) -> ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing)
+ | ((Write_mem id a Nothing value),true) ->
+ ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing)
| ((Write_mem id a Nothing value),false) ->
((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
| _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end)
| e -> e end)
- | v -> ((Error l ("Vector access must be a number given " ^ (string_of_value v)),lm,le),Nothing) end)
- | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector lexp e) (l,annot), env)))
+ | v ->
+ ((Error l ("Vector access must be a number given " ^ (string_of_value v)),lm,le),Nothing) end)
+ | (Action a s,lm,le) ->
+ ((Action a s,lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector lexp e) (l,annot), env)))
| e -> (e,Nothing) end
| LEXP_vector_range lexp exp1 exp2 ->
match (interp_main mode t_level l_env l_mem exp1) with
@@ -2460,16 +2551,19 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| ((Value v,lm,le), Just lexp_builder) ->
(match (detaint v,is_top_level) with
| (V_vector m inc vs,true) ->
- ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice v value n1 n2 lm, l_env), Nothing)
+ ((Value (V_lit (L_aux L_unit Unknown)),
+ update_vector_slice mode.track_lmem v value n1 n2 lm, l_env), Nothing)
| (V_boxref _ _, true) ->
- ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice v value n1 n2 lm, l_env), Nothing)
+ ((Value (V_lit (L_aux L_unit Unknown)),
+ update_vector_slice mode.track_lmem v value n1 n2 lm, l_env), Nothing)
| (V_vector m inc vs,false) ->
((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder))
| (V_unknown,_) ->
let inc = n1 < n2 in
let start = if inc then n1 else (n2-1) in
let size = if inc then n2-n1 +1 else n1 -n2 +1 in
- ((Value (V_vector start (if inc then IInc else IDec) (List.replicate size V_unknown)),lm,l_env),Nothing)
+ ((Value (V_vector start (if inc then IInc else IDec) (List.replicate size V_unknown)),
+ lm,l_env),Nothing)
| _ -> ((Error l "Vector required",lm,le),Nothing) end)
| ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
let len = (if n1 < n2 then n2 -n1 else n1 - n2) +1 in
@@ -2501,7 +2595,8 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
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 (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),true) ->
+ ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem 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)
| (Just v,false) -> ((Value v,lm,l_env),next_builder)
@@ -2624,11 +2719,11 @@ let rec eval_toplevel_let handle_action tlevel env mem lbind =
let rec to_global_letbinds handle_action (Defs defs) t_level =
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)
+ | [] -> ((Value (V_lit (L_aux L_unit Unknown)), (emem "global_letbinds"), eenv),t_level)
| def::defs ->
match def with
| DEF_val lbind ->
- match eval_toplevel_let handle_action t_level eenv emem lbind with
+ match eval_toplevel_let handle_action t_level eenv (emem "global_letbinds") lbind with
| Just le ->
to_global_letbinds handle_action (Defs defs)
(Env fdefs instrs default_dir (Map.(union) lets le) regs ctors subregs aliases)
@@ -2677,8 +2772,8 @@ let to_top_env external_functions defs =
let interp mode external_functions defs exp =
match (to_top_env external_functions defs) with
| (Nothing,t_level) ->
- interp_main mode t_level eenv emem exp
- | (Just o,_) -> (o,emem,eenv)
+ interp_main mode t_level eenv (emem "top level") exp
+ | (Just o,_) -> (o,(emem "top level error"),eenv)
end
let rec resume_with_env mode stack value =
@@ -2713,7 +2808,7 @@ let rec resume_with_env mode stack value =
let rec resume mode stack value =
match (stack,value) with
- | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume",emem,eenv)
+ | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume",(emem "top level error"),eenv)
| (Hole_frame id exp t_level env mem Top,Just value) ->
interp_main mode t_level (add_to_env (id,value) env) mem exp
| (Hole_frame id exp t_level env mem Top,Nothing) ->
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index ed576d2d..88ce56e4 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -20,6 +20,9 @@ let make_interp_mode eager_eval tracking_values =
let make_mode eager_eval tracking_values endian =
<|internal_mode = make_interp_mode eager_eval tracking_values;
endian = endian|>;;
+let make_mode_exhaustive endian =
+ <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true|>;
+ endian = endian |>;;
let tracking_dependencies mode = mode.internal_mode.Interp.track_values
let make_eager_mode mode = <| mode with internal_mode = <|mode.internal_mode with Interp.eager_eval = true |> |>;;
let make_default_mode _ = <|internal_mode = make_interp_mode false false; endian = E_big_endian|>;;
@@ -228,57 +231,6 @@ let rec slice_reg_value v start stop =
(if inc then (stop - v.rv_start) else (v.rv_start - stop)) v.rv_bits);
rv_start = (if inc then start else ((stop - start) + 1)) |>
-(*
-let append_value left right =
- match (left,right) with
- | (Bitvector bools1 inc fst, Bitvector bools2 _ _) -> Bitvector (bools1++bools2) inc fst
- | (Bytevector bytes1, Bytevector bytes2) -> Bytevector (bytes1++bytes2)
- | ((Bitvector _ _ _ as bit),(Bytevector _ as byte)) ->
- (match (intern_value bit,intern_value byte) with
- | (Interp.V_vector a b bits1,Interp.V_vector _ _ bits2) ->
- (fst (extern_value (make_mode true false) false Nothing (Interp.V_vector a b (bits1++bits2))))
- | _ -> Unknown end)
- | ((Bytevector _ as byte),(Bitvector _ _ _ as bit)) ->
- (match (intern_value byte,intern_value bit) with
- | (Interp.V_vector a b bits1,Interp.V_vector _ _ bits2) ->
- (fst (extern_value (make_mode true false) true Nothing (Interp.V_vector a b (bits1++bits2))))
- | _ -> Unknown end)
- | _ -> Unknown
-end
-
-let add_to_address value num =
- match value with
- | Unknown -> Unknown
- | Bitvector _ _ _ ->
- fst(extern_value (make_mode true false) false Nothing
- (Interp_lib.arith_op_vec_range (+) Interp_lib.Unsigned 1
- (Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
- | Bytevector _ ->
- fst(extern_value (make_mode true false) true Nothing
- (Interp_lib.arith_op_vec_range (+) Interp_lib.Unsigned 1
- (Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
-end
-
-
-let coerce_Bytevector_of_Bitvector (v: value) : value =
- match v with
- | Bitvector bs b i -> Bytevector (to_bytes bs)
- | _ -> Assert_extra.failwith "coerce_Bytevector_of_Bitvector given non-Bitvector"
- end
-
-let coerce_Bitvector_of_Bytevector (v: value) : value =
- match v with
- | Bytevector ws -> Bitvector
- (List.concatMap
- (fun w ->
- List.reverse
- (boolListFrombitSeq 8 (bitSeqFromNat w)))
- ws)
- true
- 0
- | _ -> Assert_extra.failwith "coerce_Bitvector_of_Bitvector given non-Bytevector"
- end
-*)
let initial_instruction_state top_level main args =
let e_args = match args with
@@ -287,7 +239,7 @@ let initial_instruction_state top_level main args =
| args -> List.map fst (List.map (Interp.to_exp (make_interp_mode true false) Interp.eenv)
(List.map intern_reg_value args)) end in
Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing))
- top_level Interp.eenv Interp.emem Interp.Top
+ top_level Interp.eenv (Interp.emem "istate top level") Interp.Top
let rec interp_to_value_helper arg err_str instr direction thunk =
@@ -375,7 +327,7 @@ let decode_to_istate top_level value =
mode
(Interp.Thunk_frame
(E_aux (E_app (Id_aux (Id "decode") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing))
- top_env Interp.eenv Interp.emem Interp.Top) Nothing) in
+ top_env Interp.eenv (Interp.emem "decode top level") Interp.Top) Nothing) in
match (instr_decoded,error) with
| (Just instr, _) ->
let instr_external = match instr with
@@ -400,14 +352,14 @@ let decode_to_istate top_level value =
(Interp.Thunk_frame
(E_aux (E_app (Id_aux (Id "supported_instructions") Interp_ast.Unknown) [arg])
(Interp_ast.Unknown, Nothing))
- top_env Interp.eenv Interp.emem Interp.Top) Nothing) in
+ top_env Interp.eenv (Interp.emem "decode second top level") Interp.Top) Nothing) in
match (instr_decoded,error) with
| (Just instr,_) ->
(*let (arg,_) = Interp.to_exp mode Interp.eenv instr in*)
Instr instr_external
(IState (Interp.Thunk_frame
(E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
- top_env Interp.eenv Interp.emem Interp.Top)
+ top_env Interp.eenv (Interp.emem "execute") Interp.Top)
top_level)
| (Nothing, Just err) -> Decode_error err
end
@@ -444,120 +396,125 @@ let instruction_to_istate (top_level:context) (((name, parms, _) as instr):instr
[(E_aux (E_app (Id_aux (Id name) Interp_ast.Unknown) (List.map get_value parms))
(Interp_ast.Unknown,Interp.ctor_annot (T_id "ast")) (*This type shouldn't be hard-coded*))])
(Interp_ast.Unknown,Nothing))
- top_env Interp.eenv Interp.emem Interp.Top)
+ top_env Interp.eenv (Interp.emem "execute") Interp.Top)
top_level)
let rec interp_to_outcome mode context thunk =
let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers spec_externs) = context in
let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
match thunk () with
- | (Interp.Value _,lm,le) -> Done
- | (Interp.Error l msg,lm,le) -> Error msg
+ | (Interp.Value _,lm,le) -> (Done,lm)
+ | (Interp.Error l msg,lm,le) -> (Error msg,lm)
| (Interp.Action a next_state,lm,le) ->
- match a with
- | Interp.Read_reg reg_form slice ->
- Read_reg (extern_reg reg_form slice)
- (fun v ->
- let v = (intern_reg_value v) in
- let v = if mode.internal_mode.Interp.track_values then (Interp.V_track v (Set.fromList [reg_form])) else v in
- IState (Interp.add_answer_to_stack next_state v) context)
- | Interp.Write_reg reg_form slice value ->
- let reg_name = extern_reg reg_form slice in
- Write_reg reg_name (extern_reg_value reg_name 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 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 mode direction v)) context)
- else Error ("Memory address on read is not 64 bits")
- | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
- end
- | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
- match List.lookup i mem_writes with
- | (Just (MW write_k f return)) ->
- 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 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)
- else Error "Memory address on write is not 64 bits"
- | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
- end
- | Interp.Write_ea (Id_aux (Id i) _) loc_val ->
- match List.lookup i mem_write_eas with
- | (Just (MEA write_k f)) ->
- let (location, length, tracking) = (f mode loc_val) in
- if (List.length location) = 8
- 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_ea write_k (Address_lifted location address_int) length tracking (IState next_state context)
- else Error "Memory address for write is not 64 bits"
- | _ -> Error ("Memory " ^ i ^ " function to signal impending write, not found") end
- | Interp.Write_memv (Id_aux (Id i) _) write_val ->
- match List.lookup i mem_write_vals with
- | (Just (MV return)) ->
- let (value, v_tracking) =
- match (Interp.detaint write_val) with
- | Interp.V_tuple[_;v] -> (extern_mem_value mode (Interp.retaint write_val v))
- | _ -> (extern_mem_value mode write_val) end in
- Write_memv 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)
- | _ -> Error ("Memory " ^ i ^ " function with write value kind not found") end
- | Interp.Barrier (Id_aux (Id i) _) lval ->
- match List.lookup i barriers with
- | Just barrier ->
- Barrier barrier (IState next_state context)
- | _ -> Error ("Barrier " ^ i ^ " function not found") end
- | Interp.Footprint (Id_aux (Id i) _) lval ->
- Footprint (IState next_state context)
- | Interp.Nondet exps tag ->
- match tag with
- | Tag_unknown ->
- let possible_states = List.map (Interp.set_in_context next_state) exps in
- Analysis_non_det (List.map (fun i -> IState i context) possible_states) (IState next_state context)
- | _ ->
- let nondet_states = List.map (Interp.set_in_context next_state) exps in
- Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context) end
- | Interp.Call_extern i value ->
- match List.lookup i ((Interp_lib.library_functions internal_direction) ++ spec_externs) with
- | Nothing -> Error ("External function not available " ^ i)
- | Just f ->
- if (mode.internal_mode.Interp.eager_eval)
- then interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode next_state (Just (f value)))
- else let new_v = f value in
- Internal (Just i)
+ (match a with
+ | Interp.Read_reg reg_form slice ->
+ (Read_reg (extern_reg reg_form slice)
+ (fun v ->
+ let v = (intern_reg_value v) in
+ let v = if mode.internal_mode.Interp.track_values then (Interp.V_track v (Set.fromList [reg_form])) else v in
+ IState (Interp.add_answer_to_stack next_state v) context), lm)
+ | Interp.Write_reg reg_form slice value ->
+ let reg_name = extern_reg reg_form slice in
+ (Write_reg reg_name (extern_reg_value reg_name value) (IState next_state context),lm)
+ | 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 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 mode direction v)) context)
+ else Error ("Memory address on read is not 64 bits")
+ | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
+ end , lm)
+ | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
+ (match List.lookup i mem_writes with
+ | (Just (MW write_k f return)) ->
+ 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 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)
+ else Error "Memory address on write is not 64 bits"
+ | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
+ end , lm)
+ | Interp.Write_ea (Id_aux (Id i) _) loc_val ->
+ (match List.lookup i mem_write_eas with
+ | (Just (MEA write_k f)) ->
+ let (location, length, tracking) = (f mode loc_val) in
+ if (List.length location) = 8
+ 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_ea write_k (Address_lifted location address_int) length tracking (IState next_state context)
+ else Error "Memory address for write is not 64 bits"
+ | _ -> Error ("Memory " ^ i ^ " function to signal impending write, not found") end, lm)
+ | Interp.Write_memv (Id_aux (Id i) _) write_val ->
+ (match List.lookup i mem_write_vals with
+ | (Just (MV return)) ->
+ let (value, v_tracking) =
+ match (Interp.detaint write_val) with
+ | Interp.V_tuple[_;v] -> (extern_mem_value mode (Interp.retaint write_val v))
+ | _ -> (extern_mem_value mode write_val) end in
+ Write_memv 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)
+ | _ -> Error ("Memory " ^ i ^ " function with write value kind not found") end, lm)
+ | Interp.Barrier (Id_aux (Id i) _) lval ->
+ (match List.lookup i barriers with
+ | Just barrier ->
+ Barrier barrier (IState next_state context)
+ | _ -> Error ("Barrier " ^ i ^ " function not found") end, lm)
+ | Interp.Footprint (Id_aux (Id i) _) lval ->
+ (Footprint (IState next_state context), lm)
+ | Interp.Nondet exps tag ->
+ (match tag with
+ | Tag_unknown _ ->
+ let possible_states = List.map (Interp.set_in_context next_state) exps in
+ let cleared_possibles = List.map Interp.clear_stack_state possible_states in
+ Analysis_non_det (List.map (fun i -> IState i context) cleared_possibles) (IState next_state context)
+ | _ ->
+ let nondet_states = List.map (Interp.set_in_context next_state) exps in
+ Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context) end, lm)
+ | Interp.Call_extern i value ->
+ (match List.lookup i ((Interp_lib.library_functions internal_direction) ++ spec_externs) with
+ | Nothing -> (Error ("External function not available " ^ i), lm)
+ | Just f ->
+ if (mode.internal_mode.Interp.eager_eval)
+ then interp_to_outcome mode context
+ (fun _ -> Interp.resume mode.internal_mode next_state (Just (f value)))
+ else let new_v = f value in
+ (Internal (Just i)
(Just (fun _ -> (Interp.string_of_value value) ^ "=>" ^ (Interp.string_of_value new_v)))
- (IState (Interp.add_answer_to_stack next_state new_v) context)
- end
- | Interp.Step l Nothing Nothing -> Internal Nothing Nothing (IState next_state context)
- | Interp.Step l (Just name) Nothing -> Internal (Just name) Nothing (IState next_state context)
- | Interp.Step l (Just name) (Just value) ->
- Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context)
- | Interp.Exit e ->
- Escape (match e with
- | E_aux (E_lit (L_aux L_unit _)) _ -> Nothing
- | _ -> Just (IState (Interp.set_in_context next_state e) context) end) (IState next_state context)
- end
- end
+ (IState (Interp.add_answer_to_stack next_state new_v) context), lm)
+ end)
+ | Interp.Step l Nothing Nothing -> (Internal Nothing Nothing (IState next_state context), lm)
+ | Interp.Step l (Just name) Nothing -> (Internal (Just name) Nothing (IState next_state context), lm)
+ | Interp.Step l (Just name) (Just value) ->
+ (Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context), lm)
+ | Interp.Exit e ->
+ (Escape (match e with
+ | E_aux (E_lit (L_aux L_unit _)) _ -> Nothing
+ | _ -> Just (IState (Interp.set_in_context next_state e) context) end) (IState next_state context),
+ (snd (Interp.get_stack_state next_state)))
+ end )
+ end
let interp mode (IState interp_state context) =
- interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing)
+ match interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) with
+ | (o,_) -> o
+end
(*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 *)
@@ -592,6 +549,7 @@ let reg_size = function
| Reg_f_slice i _ _ f _ (p1,p2) -> if p1 < p2 then p2-p1 +1 else p1-p2+1
end
+(*ie_loop returns a tuple of event list, and a tuple ofinternal interpreter memory, bool to indicate normal or exceptional termination*)
let rec ie_loop mode register_values (IState interp_state context) =
let (Context _ direction externs reads writes write_eas write_vals barriers) = context in
let unknown_reg size =
@@ -600,43 +558,73 @@ let rec ie_loop mode register_values (IState interp_state context) =
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
- | Done -> []
- | Error msg -> [E_error msg]
- | Escape Nothing i_state -> [E_escape]
+ match interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) with
+ | (Done,lm) -> ([],(lm,true))
+ | (Error msg,lm) -> ([E_error msg],(lm,false))
+ | (Escape Nothing i_state,lm) -> ([E_escape],(lm,false))
(*Do we want to record anything about the escape expression, which may be a function call*)
- | Escape _ i_state -> [E_escape]
- | Read_reg reg i_state_fun ->
- let v = match register_values with
+ | (Escape _ i_state,lm) -> ([E_escape],(lm,false))
+ | (Read_reg reg i_state_fun,_) ->
+ let v = (match register_values with
| Nothing -> unknown_reg (reg_size reg)
| Just(registers) -> match find_reg_name reg registers with
| Nothing -> unknown_reg (reg_size reg)
- | Just v -> v end end in
- (E_read_reg reg)::(ie_loop mode register_values (i_state_fun v))
- | Write_reg reg value i_state->
- (E_write_reg reg value)::(ie_loop mode register_values i_state)
- | Read_mem read_k loc length tracking i_state_fun ->
- (E_read_mem read_k loc length tracking)::
- (ie_loop mode register_values (i_state_fun (unknown_mem length)))
- | Write_mem write_k loc length tracking value v_tracking i_state_fun ->
- (E_write_mem write_k loc length tracking value v_tracking)::(ie_loop mode register_values (i_state_fun true))
- | Write_ea write_k loc length tracking i_state ->
- (E_write_ea write_k loc length tracking)::(ie_loop mode register_values i_state)
- | Write_memv value tracking i_state_fun ->
- (E_write_memv value tracking)::(ie_loop mode register_values (i_state_fun true))
- | Barrier barrier_k i_state ->
- (E_barrier barrier_k)::(ie_loop mode register_values i_state)
- | Footprint i_state ->
- E_footprint::(ie_loop mode register_values i_state)
- | Internal _ _ next -> (ie_loop mode register_values next)
- | Analysis_non_det possible_states i_state ->
- (*TODO: need to merge the stores from the stacks/results somehow (so probably need to have a different loop)*)
- (List.concat (List.map (ie_loop mode register_values) possible_states))++(ie_loop mode register_values i_state)
+ | Just v -> v end end) in
+ let (events,analysis_data) = ie_loop mode register_values (i_state_fun v) in
+ ((E_read_reg reg)::events,analysis_data)
+ | (Write_reg reg value i_state, _)->
+ let (events,analysis_data) = ie_loop mode register_values i_state in
+ ((E_write_reg reg value)::events,analysis_data)
+ | (Read_mem read_k loc length tracking i_state_fun, _) ->
+ let (events,analysis_data) = ie_loop mode register_values (i_state_fun (unknown_mem length)) in
+ ((E_read_mem read_k loc length tracking)::events,analysis_data)
+ | (Write_mem write_k loc length tracking value v_tracking i_state_fun, _) ->
+ let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in
+ let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
+ (*TODO: consider if lm and lm should be distinct and merged*)
+ ((E_write_mem write_k loc length tracking value v_tracking)::(events++events'),analysis_data)
+ | (Write_ea write_k loc length tracking i_state, _) ->
+ let (events,analysis_data) = ie_loop mode register_values i_state in
+ ((E_write_ea write_k loc length tracking)::events,analysis_data)
+ | (Write_memv value tracking i_state_fun, _) ->
+ let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in
+ let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
+ (*TODO: consider if lm and lm should be merged*)
+ ((E_write_memv value tracking)::(events++events'),analysis_data)
+ | (Barrier barrier_k i_state, _) ->
+ let (events,analysis_data) = ie_loop mode register_values i_state in
+ ((E_barrier barrier_k)::events,analysis_data)
+ | (Footprint i_state, _) ->
+ let (events,analysis_data) = ie_loop mode register_values i_state in
+ (E_footprint::events,analysis_data)
+ | (Internal _ _ next, _) -> (ie_loop mode register_values next)
+ | (Analysis_non_det possible_istates i_state,_) ->
+ if possible_istates = []
+ then ie_loop mode register_values i_state
+ else
+ let (possible_events,possible_states) = List.unzip(List.map (ie_loop mode register_values) possible_istates) in
+ let (unified_mem,update_mem) = List.foldr
+ (fun (lm,terminated_normally) (mem,update_mem) ->
+ if terminated_normally && update_mem
+ then (Interp.merge_lmems lm mem, true)
+ else if terminated_normally
+ then (lm, true)
+ else (mem, false))
+ (List_extra.head possible_states) (List_extra.tail possible_states) in
+ let updated_i_state =
+ if update_mem
+ then match i_state with
+ | (IState interp_state context) -> IState (Interp.update_stack_state interp_state unified_mem) context end
+ else i_state in
+ let (events,analysis_data) = ie_loop mode register_values updated_i_state in
+ ((List.concat possible_events)++events, analysis_data)
end ;;
let interp_exhaustive register_values i_state =
- let mode = make_mode true true E_big_endian in
- ie_loop mode register_values i_state
+ let mode = make_mode_exhaustive E_big_endian in
+ match ie_loop mode register_values i_state with
+ | (events,_) -> events
+end
let rec rr_ie_loop mode i_state =
let (IState _ (Context _ direction _ _ _ _ _ _)) = i_state in
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index 6d7cb9cf..d2a6b784 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -1,5 +1,6 @@
open import Interp_ast
open import Pervasives
+open import Show_extra
let rec power (a: integer) (b: integer) : integer =
if b <= 0
@@ -140,3 +141,9 @@ let rec get_index_range_size (BF_aux i _) = match i with
| BF_concat i j -> (get_index_range_size i) + (get_index_range_size j)
end
+let rec string_of_loc l = match l with
+ | Unknown -> "Unknown"
+ | Int s Nothing -> "Internal " ^ s
+ | Int s (Just l) -> "Internal " ^ s ^ " " ^ (string_of_loc l)
+ | Range file n1 n2 n3 n4 -> "File " ^ file ^ ": " ^ (show n1) ^ ": " ^ (show (n2:nat)) ^ ": " ^ (show (n3:nat)) ^ ": " ^ (show (n4:nat))
+end
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 35cd4d59..0140a922 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -271,7 +271,7 @@ let reg_name_to_string = function
let dependencies_to_string dependencies = String.concat ", " (List.map reg_name_to_string dependencies)
-let rec val_to_string_internal ((Interp.LMem (_,memory)) as mem) = function
+let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function
| Interp.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory)
| Interp.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
| Interp.V_tuple l ->
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 182c1929..266e8141 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -65,14 +65,14 @@ let pp_format_var (Kid_aux(Var v,_)) = v
let rec pp_format_l_lem = function
| Parse_ast.Unknown -> "Unknown"
- | _ -> "Unknown"
-(* | Parse_ast.Int(s,None) -> "(Int \"" ^ s ^ "\" Nothing)"
+(* | _ -> "Unknown"*)
+ | Parse_ast.Int(s,None) -> "(Int \"" ^ s ^ "\" Nothing)"
| Parse_ast.Int(s,(Some l)) -> "(Int \"" ^ s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))"
| Parse_ast.Range(p1,p2) -> "(Range \"" ^ p1.Lexing.pos_fname ^ "\" " ^
(string_of_int p1.Lexing.pos_lnum) ^ " " ^
(string_of_int (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) ^ " " ^
(string_of_int p2.Lexing.pos_lnum) ^ " " ^
- (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")"*)
+ (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")"
let pp_lem_l ppf l = base ppf (pp_format_l_lem l)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 22:08:22 +0000