diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 16 | ||||
| -rw-r--r-- | src/test/power.sail | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 2 | ||||
| -rw-r--r-- | src/type_internal.ml | 7 |
4 files changed, 21 insertions, 6 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 37f73a1e..8cdd13ce 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -492,6 +492,14 @@ let rec update_vector_slice vector value start stop mem = | (V_track v1 r1, v) -> (update_vector_slice v1 value start stop mem) end +let rec update_vector_start new_start 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_track v r -> taint (update_vector_start new_start v) r +end + val in_ctors : list (id * typ) -> id -> maybe typ let rec in_ctors ctors id = match ctors with @@ -1085,8 +1093,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = match (value,mode.eager_eval) with | (V_lit(L_aux L_true _),true) -> interp_main mode t_level l_env lm thn | (V_track (V_lit (L_aux L_true _)) _, true) -> interp_main mode t_level l_env lm thn + | (V_lit(L_aux L_one _),true) -> interp_main mode t_level l_env lm thn + | (V_track (V_lit (L_aux L_one _)) _, true) -> interp_main mode t_level l_env lm thn | (V_lit(L_aux L_true _),false) -> debug_out Nothing Nothing thn t_level lm l_env | (V_track (V_lit (L_aux L_true _)) _, false) -> debug_out Nothing Nothing thn t_level lm l_env + | (V_lit(L_aux L_one _),false) -> debug_out Nothing Nothing thn t_level lm l_env + | (V_track (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)) | (V_track V_unknown _,_) -> interp_main mode t_level l_env lm (E_aux (E_block [thn;els]) (l,annot)) | (_,true) -> interp_main mode t_level l_env lm els @@ -2022,7 +2034,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( | (V_unknown,_) -> ((Value v,lm,l_env),Nothing) | _ -> ((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)) value) s,lm,le), Just (next_builder lexp_builder)) + ((Action + (Write_reg regf (Just (n1,n2)) (update_vector_start n1 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)) | ((Action a s,lm,le), Just lexp_builder) -> diff --git a/src/test/power.sail b/src/test/power.sail index a57193fd..4305c099 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -347,7 +347,7 @@ val extern unit -> unit effect { barr } EIEIO_Sync (* XXX effect for trap? *) val extern unit -> unit effect pure trap -register (bool) mode64bit +register (bit[1]) mode64bit register (bool) bigendianmode val bit[64] -> unit effect {rreg,wreg} set_overflow_cr0 diff --git a/src/type_check.ml b/src/type_check.ml index a78a5db1..b2a48174 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -722,7 +722,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let t',cs',ef',e' = type_coerce (Expr l) d_env false t (E_aux(E_tuple(exps),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in (e',t',t_env,consts@cs',union_effects ef' effect)) | E_if(cond,then_,else_) -> - let (cond',_,_,c1,ef1) = check_exp envs imp_param bool_t cond in + let (cond',_,_,c1,ef1) = check_exp envs imp_param bit_t cond in (match expect_t.t with | Tuvar _ -> let then',then_t,then_env,then_c,then_ef = check_exp envs imp_param (new_t ()) then_ in diff --git a/src/type_internal.ml b/src/type_internal.ml index ba1dd4e2..6df6572e 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -818,6 +818,7 @@ let initial_abbrev_env = ("uint16",Base(([],uint16_t),Emp_global,[],pure_e)); ("uint32",Base(([],uint32_t),Emp_global,[],pure_e)); ("uint64",Base(([],uint64_t),Emp_global,[],pure_e)); + ("bool",Base(([],bit_t),Emp_global,[],pure_e)); ] @@ -1602,12 +1603,12 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 = let cs = [Eq(co,r1,{nexp = Nconst one})] in (*WARNING: shrinking i to an int; should add a check*) let t2' = {t = Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp {nexp=Nconst one};TA_ord o;TA_typ {t=Tid "bit"}])} in - (t2',cs,E_aux(E_vector_indexed([((int_of_big_int i),e)],Def_val_aux(Def_val_empty,(l,NoTyp))) ,(l,Base(([],t2),Emp_local,cs,pure_e)))) + (t2',cs,E_aux(E_vector_indexed([((int_of_big_int i),e)],Def_val_aux(Def_val_empty,(l,NoTyp))) ,(l,Base(([],t2),Emp_local,cs,pure_e))))*) | Tapp("vector",[TA_nexp ({nexp=Nconst i} as b1);TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") -> let cs = [Eq(co,r1,{nexp = Nconst one})] in - (t2,cs,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num (int_of_big_int i),l)), + (t2,cs,pure_e,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num (int_of_big_int i),l)), (l,Base(([],{t=Tapp("range",[TA_nexp b1;TA_nexp {nexp=Nconst zero}])}),Emp_local,cs,pure_e)))))), - (l,Base(([],t2),Emp_local,cs,pure_e))))*) + (l,Base(([],t2),Emp_local,cs,pure_e)))) | Tid("bit"),Tapp("range",[TA_nexp b1;TA_nexp r1]) -> let t',cs'= type_consistent co d_env {t=Tapp("range",[TA_nexp{nexp=Nconst zero};TA_nexp{nexp=Nconst one}])} t2 in (t2,cs',pure_e, |