diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 24 | ||||
| -rw-r--r-- | src/type_check.ml | 4 | ||||
| -rw-r--r-- | src/type_internal.ml | 18 |
3 files changed, 24 insertions, 22 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 06aabd46..c7f42e02 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -86,10 +86,19 @@ let is_unknown v = match v with | _ -> false end +let is_undef v = match v with + | V_lit (L_aux L_undef _) -> true + | _ -> false +end + let has_unknown v = match detaint v with | V_vector _ _ vs -> List.any is_unknown vs end +let has_undef v = match detaint v with + | V_vector _ _ vs -> List.any is_undef vs +end + let rec sparse_walker update ni processed_length length ls df = if processed_length = length then [] @@ -189,13 +198,15 @@ let to_num signed v = (match detaint v with | (V_vector idx inc l) -> if has_unknown v then V_unknown else if l=[] then V_unknown - else + else if has_undef v then V_lit (L_aux L_undef 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_lit (L_aux L_undef _) -> v end) let to_vec_inc (V_tuple[v1;v2]) = @@ -283,6 +294,8 @@ let arith_op op (V_tuple [vl;vr]) = | (V_lit(L_aux (L_num x) lx), V_lit(L_aux (L_num y) ly)) -> V_lit(L_aux (L_num (op x y)) lx) | (V_unknown,_) -> V_unknown | (_,V_unknown) -> V_unknown + | (V_lit (L_aux L_undef lx),_) -> vl + | (_, (V_lit (L_aux L_undef ly))) -> vr end in binary_taint arith_op_help vl vr let rec arith_op_vec op sign size (V_tuple [vl;vr]) = @@ -651,8 +664,7 @@ let library_functions direction = [ ("neq", neq); ("vec_concat", vec_concat); ("is_one", is_one); - ("to_num_inc", to_num Unsigned); - ("to_num_dec", to_num Unsigned); + ("to_num", to_num Unsigned); ("EXTS", exts direction); ("EXTZ", extz direction); ("to_vec_inc", to_vec_inc); diff --git a/src/type_check.ml b/src/type_check.ml index 134a2c6c..5b5a0864 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -200,8 +200,8 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) | L_unit -> unit_t,lit | L_zero -> bit_t,lit | L_one -> bit_t,lit - | L_true -> bool_t,lit - | L_false -> bool_t,lit + | L_true -> bit_t,L_one + | L_false -> bit_t,L_zero | L_num i -> (match expect_actual.t with | Tid "bit" -> diff --git a/src/type_internal.ml b/src/type_internal.ml index 9b3eab6d..f46b5409 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -2307,14 +2307,10 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2 | _ -> raise (Reporting_basic.err_unreachable l "vector is not properly kinded")) | "vector","range",_ -> (match args1,args2 with - | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], + | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> let cs = [Eq(co,b2,n_zero);LtEq(co,Guarantee,mk_sub {nexp=N2n(r1,None)} n_one,r2)] in - (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) - | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], - [TA_nexp b2;TA_nexp r2;] -> - let cs = [Eq(co,b2,n_zero);LtEq(co,Guarantee,mk_sub {nexp=N2n(r1,None)} n_one,r2)] in - (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) + (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> eq_error l "Cannot convert a vector to an range without an order" | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> @@ -2322,16 +2318,10 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2 | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded")) | "vector","atom",_ -> (match args1,args2 with - | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], + | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}], [TA_nexp b2] -> let cs = [GtEq(co,Guarantee,b2,n_zero);LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in - (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) - | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], - [TA_nexp b2] -> - let cs = [Eq(co,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in - (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) - | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> - eq_error l "Cannot convert a vector to an range without an order" + (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> eq_error l "Cannot convert non-bit vector into an range" | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded")) |