summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp.lem45
-rw-r--r--src/lem_interp/interp_lib.lem27
-rw-r--r--src/lem_interp/interp_utilities.lem6
-rw-r--r--src/lem_interp/printing_functions.ml10
4 files changed, 62 insertions, 26 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 3052a369..3e125b99 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -580,9 +580,10 @@ let rec update_vector_start new_start expected_size v = match v with
| V_vector m inc vs -> V_vector new_start inc vs
(*Note, may need to shrink and check if still sparse *)
| V_vector_sparse m n inc vals d -> V_vector_sparse new_start n inc vals d
- | V_unknown -> V_unknown
+ | V_unknown ->
+ V_vector new_start true (List.replicate (natFromInteger expected_size) V_unknown)
| V_lit (L_aux L_undef _) -> v
- | V_track v r -> taint (update_vector_start new_start v) r
+ | V_track v r -> taint (update_vector_start new_start expected_size v) r
end
val in_ctors : list (id * typ) -> id -> maybe typ
@@ -1128,9 +1129,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
match v with
| V_vector start inc vs ->
- if start = i then (Value v,lm,le) else (Value (update_vector_start i v),lm,le)
+ if start = i then (Value v,lm,le) else (Value (update_vector_start i 1 v),lm,le)
| V_track (V_vector start inc vs) r ->
- if start = i then (Value v,lm,le) else (Value (update_vector_start i v),lm,le)
+ if start = i then (Value v,lm,le) else (Value (update_vector_start i 1 v),lm,le)
| _ -> (Value v,lm,le) end
| _ -> (Value v,lm,le) end in
(match (tag,v) with
@@ -2168,17 +2169,24 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
(match (nth(),is_top_level,maybe_builder) with
| (V_register regform,true,_) ->
let start_pos = reg_start_pos regform in
- ((Action (Write_reg regform Nothing (update_vector_start start_pos 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),Nothing)
+ let reg_size = reg_size regform in
+ ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size 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),Nothing)
| (V_register regform,false,Just lexp_builder) ->
let start_pos = reg_start_pos regform in
- ((Action (Write_reg regform Nothing (update_vector_start start_pos 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),
+ let reg_size = reg_size regform in
+ ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size 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),
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_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),Nothing)
- | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
+ ((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 ->
((Error l ("Vector access to write of non-vector" ^ (string_of_value v)),lm,l_env),Nothing)
@@ -2186,9 +2194,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| ((Action a s,lm,le),Just lexp_builder) ->
(match (a,is_top_level) with
| ((Write_reg regf Nothing value),true) ->
- ((Action (Write_reg regf (Just (n,n)) (update_vector_start n value)) s, lm,le), Nothing)
+ ((Action (Write_reg regf (Just (n,n)) (update_vector_start n 1 value)) s, lm,le), Nothing)
| ((Write_reg regf Nothing value),false) ->
- ((Action (Write_reg regf (Just (n,n)) (update_vector_start n value)) s,lm,le), Just (next_builder lexp_builder))
+ ((Action (Write_reg regf (Just (n,n)) (update_vector_start n 1 value)) 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),false) ->
((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
@@ -2230,7 +2239,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| _ -> ((Error l "Vector required",lm,le),Nothing) end)
| ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
((Action
- (Write_reg regf (Just (n1,n2)) (update_vector_start n1 value)) s,lm,le),
+ (Write_reg regf (Just (n1,n2)) (update_vector_start n1 ((abs (n1-n2)) +1) value)) s,lm,le),
Just (next_builder lexp_builder))
| ((Action (Write_mem id a Nothing value) s,lm,le), Just lexp_builder) ->
((Action (Write_mem id a (Just (n1,n2)) value) s,lm,le), Just (next_builder lexp_builder))
@@ -2271,7 +2280,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| Just(indexes) ->
match in_env indexes id with
| Just ir ->
- ((Action (Write_reg (SubReg id regf ir) Nothing (update_vector_start (get_first_index_range ir) value)) s,lm,le),
+ ((Action (Write_reg (SubReg id regf ir) Nothing
+ (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value)) s,
+ lm,le),
(if is_top_level then Nothing else next_builder))
| _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
end
@@ -2281,7 +2292,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| Just(indexes) ->
match in_env indexes id with
| Just ir ->
- ((Action (Write_reg (SubReg id regf ir) Nothing (update_vector_start (get_first_index_range ir) value)) s,lm,le),
+ ((Action (Write_reg (SubReg id regf ir) Nothing
+ (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value)) s,
+ lm,le),
(if is_top_level then Nothing else next_builder))
| _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
end
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 22250e46..bdd5fcca 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -15,6 +15,15 @@ let zeroi = integerFromNat 0
let onei = integerFromNat 1
let twoi = integerFromNat 2
+let is_unknown v = match v with
+ | V_unknown -> true
+ | _ -> false
+end
+
+let has_unknown v = match v with
+ | V_vector _ _ vs -> List.any is_unknown vs
+end
+
let rec sparse_walker update ni processed_length length ls df =
if processed_length = length
then []
@@ -60,9 +69,6 @@ let bit_to_bool b = match b with
| V_track (V_lit (L_aux L_zero _)) _ -> false
| V_lit (L_aux L_one _) -> true
| V_track (V_lit (L_aux L_one _)) _ -> true
-(* PS HACK TO MAKE BUILD *)
- | _ -> false (* ARGH - SHOULDN'T HAVE TO CHOOSE *)
-(* END HACK *)
end ;;
let bool_to_bit b = match b with
false -> V_lit (L_aux L_zero Unknown)
@@ -124,11 +130,14 @@ type signed = Unsigned | Signed
let rec to_num signed v =
match v with
| (V_vector idx inc l) ->
+ if has_unknown v
+ then V_unknown
+ else
(* Word library in Lem expects bitseq with LSB first *)
- let l = reverse l in
+ let l = reverse l in
(* Make sure the last bit is a zero to force unsigned numbers *)
- let l = match signed with | Signed -> l | Unsigned -> l ++ [V_lit (L_aux L_zero Unknown)] end in
- V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
+ let l = (match signed with | Signed -> l | Unsigned -> l ++ [V_lit (L_aux L_zero Unknown)] end) in
+ V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
| V_unknown -> V_unknown
| V_track v r -> taint (to_num signed v) r
end ;;
@@ -140,7 +149,8 @@ let rec to_vec_inc (V_tuple[v1;v2]) = match (v1,v2) with
| (V_track v1 r1,V_track v2 r2) -> taint (to_vec_inc (V_tuple[v1;v2])) (r1++r2)
| (V_track v1 r1,v2) -> taint (to_vec_inc (V_tuple[v1;v2])) r1
| (v1,V_track v2 r2) -> taint (to_vec_inc (V_tuple[v1;v2])) r2
- | (V_unknown,_) -> V_unknown
+ | ((V_lit(L_aux (L_num n) ln)),V_unknown) ->
+ V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
| (_,V_unknown) -> V_unknown
| _ -> Assert_extra.failwith ("to_vec_inc parameters were " ^ (string_of_value (V_tuple[v1;v2])))
end
@@ -152,7 +162,8 @@ let rec to_vec_dec (V_tuple([v1;v2])) = match (v1,v2) with
| (V_track v1 r1,V_track v2 r2) -> taint (to_vec_dec (V_tuple[v1;v2])) (r1++r2)
| (V_track v1 r1,v2) -> taint (to_vec_dec (V_tuple[v1;v2])) r1
| (v1,V_track v2 r2) -> taint (to_vec_dec (V_tuple[v1;v2])) r2
- | (V_unknown,_) -> V_unknown
+ | ((V_lit(L_aux (L_num n) ln)),V_unknown) ->
+ V_vector (n-1) false (List.replicate (natFromInteger n) V_unknown)
| (_,V_unknown) -> V_unknown
end
;;
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index 7aa211e7..1bfa698b 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -95,5 +95,11 @@ let rec get_first_index_range (BF_aux i _) = match i with
| BF_single i -> i
| BF_range i j -> i
| BF_concat s _ -> get_first_index_range s
+end
+
+let rec get_index_range_size (BF_aux i _) = match i with
+ | BF_single _ -> 1
+ | BF_range i j -> (abs (i-j)) + 1
+ | BF_concat i j -> (get_index_range_size i) + (get_index_range_size j)
end
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 73feb8ac..69dbaca8 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -58,6 +58,10 @@ let bit_lifted_to_string = function
| Bitl_undef -> "u"
| Bitl_unknown -> "?"
+let bit_to_string = function
+ | Bitc_zero -> "0"
+ | Bitc_one -> "1"
+
let reg_value_to_string v =
let l = List.length v.rv_bits in
let start = string_of_int v.rv_start in
@@ -67,6 +71,8 @@ let reg_value_to_string v =
else (string_of_int l) ^ "_" ^ start ^ "'b" ^
collapse_leading (List.fold_right (^) (List.map bit_lifted_to_string v.rv_bits) "")
+let ifield_to_string v =
+ "0b"^ collapse_leading (List.fold_right (^) (List.map bit_to_string v) "")
let register_value_to_string rv =
reg_value_to_string rv
@@ -292,10 +298,10 @@ let instr_parm_to_string (name, typ, value) =
name ^"="^
match typ with
| Other -> "Unrepresentable external value"
- | _ -> let intern_v = (Interp_inter_imp.intern_reg_value value) in
+ | _ -> let intern_v = (Interp_inter_imp.intern_ifield_value value) in
match Interp_lib.to_num Interp_lib.Unsigned intern_v with
| V_lit (L_aux(L_num n, _)) -> string_of_big_int n
- | _ -> reg_value_to_string value
+ | _ -> ifield_to_string value
let rec instr_parms_to_string ps =
match ps with
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 05:46:38 +0000