diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/Interp_interface.lem | 46 | ||||
| -rw-r--r-- | src/lem_interp/interp.lem | 8 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 63 | ||||
| -rw-r--r-- | src/pretty_print.ml | 7 | ||||
| -rw-r--r-- | src/type_check.ml | 4 | ||||
| -rw-r--r-- | src/type_internal.ml | 2 |
7 files changed, 98 insertions, 34 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 2548bf19..95578d9f 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -354,7 +354,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) | Parse_ast.E_for(id,e1,e2,e3,atyp,e4) -> E_for(to_ast_id id,to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3,to_ast_order k_env atyp, to_ast_exp k_env e4) | Parse_ast.E_vector(exps) -> E_vector(List.map (to_ast_exp k_env) exps) - | Parse_ast.E_vector_indexed(iexps) -> E_vector_indexed(List.map (fun (i,e) -> (i,to_ast_exp k_env e)) iexps) + | Parse_ast.E_vector_indexed(iexps,default) -> E_vector_indexed(List.map (fun (i,e) -> (i,to_ast_exp k_env e)) iexps, Def_val_aux(Def_val_empty,(l,NoTyp))) (*TODO transform the default *) | Parse_ast.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env vexp, to_ast_exp k_env exp) | Parse_ast.E_vector_subrange(vex,exp1,exp2) -> E_vector_subrange(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2) | Parse_ast.E_vector_update(vex,exp1,exp2) -> E_vector_update(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2) diff --git a/src/lem_interp/Interp_interface.lem b/src/lem_interp/Interp_interface.lem index 0767ea79..0e05fafe 100644 --- a/src/lem_interp/Interp_interface.lem +++ b/src/lem_interp/Interp_interface.lem @@ -4,49 +4,49 @@ type read_kind = Interp.read_kind type write_kind = Interp.write_kind type barrier_kind = Interp.barrier_kind +type word8 = nat (* bounded at a byte, for when lem supports it*) + type value = -| Bitvector of list nat (*Always 0 or 1; should this be a Word.bitSequence? *) -| Bytevector of list (list nat) (* Should this be a list of Word.bitSequence? *) +| Bitvector of list bool (* For register accesses *) +| Bytevector of list word8 (* For memory accesses *) | Unknown type instruction_state = Interp.stack type context = Interp.top_level -type reg_name = Interp.reg_form (*for now...*) +type slice = (integer * integer) + +type reg_name = +| Reg of string (*Name of the register, accessing the entire register*) +| Reg_slice of string * slice (*Name of the register, accessing from the first to second integer of the slice*) +| Reg_field of string * string * slice (*Name of the register, name of the field of the register accessed, the slice of the field*) +| Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *) type outcome = | Read_mem of read_kind * value * (value -> instruction_state) | Write_mem of write_kind * value * value * (bool -> instruction_state) | Barrier of barrier_kind * instruction_state -| Read_reg of reg_name * (value -> instruction_state) (*What about slicing?*) +| Read_reg of reg_name * (value -> instruction_state) | Write_reg of reg_name * value * instruction_state | Nondet_choice of list instruction_state | Internal of instruction_state | Done | Error of string +type event = +| E_read_mem of read_kind * value +| E_write_mem of write_kind * value +| E_barrier of barrier_kind +| E_read_reg of reg_name +| E_write_reg of reg_name +(*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*) + + val build_context : Interp.defs Interp.tannot -> context val initial_instruction_state : context -> string -> value -> instruction_state type interp_mode = <| eager_eval : bool |> -val interp : instruction_state -> interp_mode -> outcome - -val interp_exhaustive : instruction_state -> list outcome (*not sure what event was ment to be*) - -val intern_value : value -> Interp.value -val extern_value : Interp.value -> value - -let build_context defs = Interp.to_top_env defs - -let intern_value v = match v with - | Bitvector bs -> Interp.V_vector 0 true (List.map (fun | 0 -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown)) - | _ -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown))) bs) - | Unknown -> Interp.V_unknown +val interp : interp_mode -> instruction_state -> outcome -let extern_value v = match v with - | Interp.V_vector _ true bits -> Bitvector (List.map (fun | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> 0 - | _ -> 1) bits) - | _ -> Unknown +val interp_exhaustive : instruction_state -> list event -let initial_instruction_state top_level main arg = - Interp.Frame Nothing (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [ intern_value arg ]) (Interp_ast.Unknown, Nothing)) top_level [] Interp.emem diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 84bf6960..efd2f866 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -427,9 +427,9 @@ let rec to_exp v = if (inc && n=0) then E_vector (List.map to_exp vals) else if inc then - E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals))) + E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals))) (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing)) else - E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals)) + E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals)) (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing)) | V_record t ivals -> E_record(FES_aux (FES_Fexps (List.map (fun (id,value) -> (FE_aux (FE_Fexp id (to_exp value)) (Unknown,Nothing))) ivals) false) @@ -964,12 +964,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps | E_vector(exps) -> exp_list mode t_level (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps - | E_vector_indexed(iexps) -> + | E_vector_indexed iexps default -> let (indexes,exps) = List.unzip iexps in let is_inc = match typ with | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp _; T_arg_order (Ord_aux Ord_inc _); _]) -> true | _ -> false end in - exp_list mode t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)) (l,annot))) + exp_list mode t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es) default) (l,annot))) (fun vals -> V_vector (List_extra.head indexes) is_inc vals) l_env l_mem [] exps | E_block(exps) -> interp_block mode t_level l_env l_env l_mem exps | E_app f args -> diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem new file mode 100644 index 00000000..59acb04a --- /dev/null +++ b/src/lem_interp/interp_inter_imp.lem @@ -0,0 +1,63 @@ +import Interp +import Interp_lib +open import Interp_interface + +import Num + +val intern_value : value -> Interp.value +val extern_value : Interp.value -> value +val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name + +let build_context defs = Interp.to_top_env defs + +let to_bits l = (List.map (fun b -> match b with + | false -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown)) + | true -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown)) end) l) +let from_bits l = (List.map (fun b -> match b with + | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> false + | _ -> true end) l) +let rec to_bytes l = match l with + | [] -> [] + | (a::b::c::d::e::f::g::h::rest) -> + (integerFromBoolList [a;b;c;d;e;f;g;h])::(to_bytes rest) +end + +let intern_value v = match v with + | Bitvector bs -> Interp.V_vector 0 true (to_bits bs) + | Bytevector bys -> Interp.V_vector 0 true (to_bits (List.concat (List.map (bitSeqFromInteger 8 Nothing) bys))) + | Unknown -> Interp.V_unknown +end + +let extern_value for_mem v = match v with + | Interp.V_vector _ true bits -> + if for_mem + then Bytevector (to_bytes (from_bits bits)) + else Bitvector (from_bits bits) + | _ -> Unknown +end + +let extern_reg r slice = match (r,slice) with + | (Interp.Reg(Id_aux (Id x,_)),Nothing) -> Reg x + | (Interp.Reg(Id_aux (Id x,_)),Just(i1,i2)) -> Reg_slice x (i1,i2) + | (Interp.SubReg (Id_aux (Id x,_)) (Interp.Reg(Id_aux (Id y,_))) (Interp_ast.BF_aux(Interp_ast.BF_single i) _),Nothing) -> Reg_field x y (i,i) +end + +let initial_instruction_state top_level main arg = + Interp.Frame Nothing (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [ intern_value arg ]) (Interp_ast.Unknown, Nothing)) top_level [] Interp.emem + +let interp mode i_state = + match Interp.resume mode i_state None with + | Interp.Value _ -> Done + | Interp.Error l msg -> Error msg (*Todo, add the l information the string format*) + | Interp.Action a next_state -> + match a with + | Interp.Read_reg reg_form slice -> Read_reg reg_form (fun v -> Interp.add_answer_to_stack (intern_value v) next_state) + | Interp.Write_reg reg_form slice value -> Write_reg reg_form (extern_value value) next_state + | Interp.Read_mem (Id_aux (Id i) _) value slice + (*Need to lookup the Mem function used to determine appropriate value, and possible appropriate read_kind *) + -> Read_mem Interp.Read_plain (extern_value value) (fun v -> Interp.add_answer_to_stack (intern_value v) next_state) + | Interp.Write_mem (Id_aux (id i) _) loc_val slice write_val -> + Write_mem Interp.Write_plain (extern_value loc_val) (extern_value write_val) next_state + | Interp.Call_extern id value -> (*Connect here to a list of external functions*) foo + end + end diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 75075c69..9f0382f5 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -236,7 +236,7 @@ and pp_exp ppf (E_aux(e,(_,annot))) = fprintf ppf "@[<0> %a %a (%a %a %a %a %a %a %a %a)@ @[<1>%a@]@]" kwd "foreach " pp_id id kwd "from " pp_exp exp1 kwd " to " pp_exp exp2 kwd "by " pp_exp exp3 kwd "in" pp_ord order pp_exp exp4 | E_vector(exps) -> fprintf ppf "@[<0>%a%a%a@]" kwd "[" (list_pp pp_comma_exp pp_exp) exps kwd "]" - | E_vector_indexed(iexps) -> + | E_vector_indexed(iexps,default) -> let iformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a%a@]" i kwd " = " pp_exp e kwd "," in let lformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a@]" i kwd " = " pp_exp e in fprintf ppf "@[<0> %a%a%a@]" kwd "[" (list_pp iformat lformat) iexps kwd "]" @@ -671,7 +671,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = fprintf ppf "@[<0>(E_aux (%a %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]" kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot | E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot - | E_vector_indexed(iexps) -> + | E_vector_indexed(iexps,default) -> (*TODO print out default when it is an nonempty*) let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps pp_lem_l l pp_annot annot @@ -1127,7 +1127,8 @@ let doc_exp, doc_let = braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps)) | E_vector exps -> brackets (separate_map comma exp exps) - | E_vector_indexed iexps -> + | E_vector_indexed (iexps, default) -> + (* XXX TODO print default when it is non-empty *) let iexp (i,e) = doc_op equals (doc_int i) (exp e) in brackets (separate_map comma iexp iexps) | E_vector_update(v,e1,e2) -> diff --git a/src/type_check.ml b/src/type_check.ml index 258873ce..5499c3e2 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -622,7 +622,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst 0});TA_nexp({nexp=Nconst (List.length es)});TA_ord({order=Oinc});TA_typ item_t])} in let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in (e',t',t_env,cs@cs',effect) - | E_vector_indexed eis -> + | E_vector_indexed(eis,default) -> let item_t = match expect_t.t with | Tapp("vector",[base;rise;ord;TA_typ item_t]) -> item_t | _ -> new_t () in @@ -639,7 +639,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp eis) ([],[],pure_e,first)) in let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst first});TA_nexp({nexp=Nconst (List.length eis)}); TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in - let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector_indexed es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in + let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector_indexed(es,default),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in (e',t',t_env,cs@cs',effect) | E_vector_access(vec,i) -> let base,rise,ord = new_n(),new_n(),new_o() in diff --git a/src/type_internal.ml b/src/type_internal.ml index 26a03d6a..abee5a9c 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1017,7 +1017,7 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 = | Tid("bit"),Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) -> let cs = [Eq(co,r1,{nexp = Nconst 1})] in let t2' = {t = Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp {nexp=Nconst 1};TA_ord o;TA_typ {t=Tid "bit"}])} in - (t2',cs,E_aux(E_vector_indexed [(i,e)],(l,Base(([],t2),Emp_local,cs,pure_e)))) + (t2',cs,E_aux(E_vector_indexed([(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 1})] in (t2,cs,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num i,l)), |