diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 4 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 1 | ||||
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 13 |
3 files changed, 15 insertions, 3 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 94c3e283..6edebc49 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -1338,12 +1338,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (fun iv_whole lm le -> let iv = match iv_whole with | V_track v _ -> v | _ -> iv_whole end in match iv with + | V_unknown -> (Value V_unknown,lm,le) | V_lit (L_aux (L_num n) ln) -> resolve_outcome (interp_main mode t_level l_env lm vec) (fun vvec lm le -> match vvec with - | V_vector _ _ _ -> (Value (access_vector vvec n),lm,le) + | V_vector _ _ _ -> (Value (access_vector vvec n),lm,le) | V_track ((V_vector _ _ _) as vvec) r -> (match iv_whole with | V_track _ ir -> (Value (taint (access_vector vvec n) (r++ir)),lm,le) @@ -1994,6 +1995,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( | (Value i_whole,lm,le) -> let i = match i_whole with | V_track v _ -> v | _ -> i_whole end in (match i with + | V_unknown -> ((Value V_unknown,lm,le),Nothing) | V_lit (L_aux (L_num n) ln) -> let next_builder le_builder = (fun e env -> diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index bc9610de..afa58f6d 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -31,6 +31,7 @@ let intern_value v = match v with (to_bits (List.reverse (List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys)))) | Unknown -> Interp.V_unknown + | _ -> Interp.V_unknown end let extern_reg r slice = match (r,slice) with diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index c04ff73d..c0237cbc 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -146,8 +146,10 @@ let to_vec ord len n = else to_vec_dec (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n])) ;; -let exts len ((V_vector _ inc _) as v) = - to_vec inc len (to_num true v) +let exts len v = match v with + | V_vector _ inc _ -> to_vec inc len (to_num true v) + | V_unknown -> V_unknown +end ;; let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;; @@ -233,18 +235,24 @@ let rec arith_op_vec_range_range op (V_tuple args) = match args with end ;; let compare_op op (V_tuple args) = match args with + | [V_unknown;_] -> V_unknown + | [_;V_unknown] -> V_unknown | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> if (op x y) then V_lit(L_aux L_one lx) else V_lit(L_aux L_zero lx) end ;; let compare_op_vec op (V_tuple args) = match args with + | [V_unknown;_] -> V_unknown + | [_;V_unknown] -> V_unknown | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] -> let (l1',l2') = (to_num true l1, to_num true l2) in compare_op op (V_tuple[l1';l2']) end ;; let rec duplicate (V_tuple args) = match args with + | [V_unknown;_] -> V_unknown + | [_;V_unknown] -> V_unknown | [(V_lit _ as v);(V_lit (L_aux (L_num n) _))] -> (V_vector 0 true (List.replicate (natFromInteger n) v)) end @@ -267,6 +275,7 @@ let function_map = [ ("add_range_vec_range", arith_op_range_vec_range (+)); ("minus", arith_op (-)); ("minus_vec", arith_op_vec (-) 1); + ("minus_vec_range", arith_op_vec_range (-) 1); ("multiply", arith_op ( * )); ("multiply_vec", arith_op_vec ( * ) 2); ("mod", arith_op (mod)); |