diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 11 | ||||
| -rw-r--r-- | src/initial_check.ml | 60 | ||||
| -rw-r--r-- | src/interpreter.ml | 4 | ||||
| -rw-r--r-- | src/parse_ast.ml | 1 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 1 | ||||
| -rw-r--r-- | src/rewriter.ml | 11 | ||||
| -rw-r--r-- | src/rewriter.mli | 3 | ||||
| -rw-r--r-- | src/rewrites.ml | 32 | ||||
| -rw-r--r-- | src/sail.ml | 3 | ||||
| -rw-r--r-- | src/type_check.ml | 267 | ||||
| -rw-r--r-- | src/type_check.mli | 9 | ||||
| -rw-r--r-- | src/value.ml | 5 |
12 files changed, 228 insertions, 179 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 2f2d27d8..f7574b9d 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -449,6 +449,7 @@ and map_lexp_annot_aux f = function | LEXP_memory (id, exps) -> LEXP_memory (id, List.map (map_exp_annot f) exps) | LEXP_cast (typ, id) -> LEXP_cast (typ, id) | LEXP_tup lexps -> LEXP_tup (List.map (map_lexp_annot f) lexps) + | LEXP_vector_concat lexps -> LEXP_vector_concat (List.map (map_lexp_annot f) lexps) | LEXP_vector (lexp, exp) -> LEXP_vector (map_lexp_annot f lexp, map_exp_annot f exp) | LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2) | LEXP_field (lexp, id) -> LEXP_field (map_lexp_annot f lexp, id) @@ -645,8 +646,8 @@ let rec string_of_exp (E_aux (exp, _)) = | E_try (exp, cases) -> "try " ^ string_of_exp exp ^ " catch { case " ^ string_of_list " case " string_of_pexp cases ^ "}" | E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp - | E_assign (lexp, bind) -> string_of_lexp lexp ^ " := " ^ string_of_exp bind - | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp + | E_assign (lexp, bind) -> string_of_lexp lexp ^ " = " ^ string_of_exp bind + | E_cast (typ, exp) -> string_of_exp exp ^ " : " ^ string_of_typ typ | E_vector vec -> "[" ^ string_of_list ", " string_of_exp vec ^ "]" | E_vector_access (v, n) -> string_of_exp v ^ "[" ^ string_of_exp n ^ "]" | E_vector_update (v, n, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " = " ^ string_of_exp exp ^ "]" @@ -702,7 +703,7 @@ and string_of_pat (P_aux (pat, l)) = | P_wild -> "_" | P_id v -> string_of_id v | P_var (pat, tpat) -> string_of_pat pat ^ " as " ^ string_of_typ_pat tpat - | P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat + | P_typ (typ, pat) -> string_of_pat pat ^ " : " ^ string_of_typ typ | P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")" | P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")" | P_cons (pat1, pat2) -> string_of_pat pat1 ^ " :: " ^ string_of_pat pat2 @@ -719,7 +720,9 @@ and string_of_lexp (LEXP_aux (lexp, _)) = | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")" | LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]" | LEXP_vector_range (lexp, exp1, exp2) -> - string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ ".." ^ string_of_exp exp2 ^ "]" + string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ " .. " ^ string_of_exp exp2 ^ "]" + | LEXP_vector_concat lexps -> + string_of_list " @ " string_of_lexp lexps | LEXP_field (lexp, id) -> string_of_lexp lexp ^ "." ^ string_of_id id | LEXP_memory (f, xs) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")" and string_of_letbind (LB_aux (lb, l)) = diff --git a/src/initial_check.ml b/src/initial_check.ml index 62c1af02..1ba1b9e6 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -539,35 +539,45 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) ), (l,())) and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp = - LEXP_aux( - (match exp with - | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id) - | Parse_ast.E_deref(exp) -> LEXP_deref(to_ast_exp k_env def_ord exp) - | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) -> - LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id) - | Parse_ast.E_tuple(tups) -> + let lexp = match exp with + | Parse_ast.E_id id -> LEXP_id (to_ast_id id) + | Parse_ast.E_deref exp -> LEXP_deref (to_ast_exp k_env def_ord exp) + | Parse_ast.E_cast (typ, Parse_ast.E_aux (Parse_ast.E_id id, l')) -> + LEXP_cast (to_ast_typ k_env def_ord typ, to_ast_id id) + | Parse_ast.E_tuple tups -> let ltups = List.map (to_ast_lexp k_env def_ord) tups in - let is_ok_in_tup (LEXP_aux (le,(l,_))) = + let is_ok_in_tup (LEXP_aux (le, (l, _))) = match le with - | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> () + | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_vector_concat _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> () | LEXP_memory _ | LEXP_deref _ -> - typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in + typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None + in List.iter is_ok_in_tup ltups; - LEXP_tup(ltups) - | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),args) -> - (match f with - | Parse_ast.Id(id) -> - (match List.map (to_ast_exp k_env def_ord) args with - | [E_aux(E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory(to_ast_id f',[]) - | [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps) - | args -> LEXP_memory(to_ast_id f', args)) - | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None) - | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp) - | Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> - LEXP_vector_range(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) - | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env def_ord fexp, to_ast_id id) - | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None) - , (l,())) + LEXP_tup ltups + | Parse_ast.E_app ((Parse_ast.Id_aux (f, l') as f'), args) -> + begin match f with + | Parse_ast.Id(id) -> + (match List.map (to_ast_exp k_env def_ord) args with + | [E_aux (E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory (to_ast_id f', []) + | [E_aux (E_tuple exps,_)] -> LEXP_memory (to_ast_id f', exps) + | args -> LEXP_memory(to_ast_id f', args)) + | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None + end + | Parse_ast.E_vector_append (exp1, exp2) -> + LEXP_vector_concat (to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2) + | Parse_ast.E_vector_access (vexp, exp) -> LEXP_vector (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp) + | Parse_ast.E_vector_subrange (vexp, exp1, exp2) -> + LEXP_vector_range (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) + | Parse_ast.E_field (fexp, id) -> LEXP_field (to_ast_lexp k_env def_ord fexp, to_ast_id id) + | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None + in + LEXP_aux (lexp, (l, ())) + +and to_ast_lexp_vector_concat k_env def_ord (Parse_ast.E_aux (exp_aux, l) as exp) = + match exp_aux with + | Parse_ast.E_vector_append (exp1, exp2) -> + to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2 + | _ -> [to_ast_lexp k_env def_ord exp] and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : unit pexp = match pex with diff --git a/src/interpreter.ml b/src/interpreter.ml index 87439e83..e62fcfc3 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -505,6 +505,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = else puts (lstate, { gstate with boxes = StringMap.add name (value_of_exp exp) gstate.boxes }) >> wrap unit_exp | E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> failwith "Tuple assignment" + | E_assign (LEXP_aux (LEXP_vector_concat lexps, annot), exp) -> failwith "Vector concat assignment" (* let values = coerce_tuple (value_of_exp exp) in wrap (E_block (List.map2 (fun lexp v -> E_aux (E_assign (lexp, exp_of_value v), (Parse_ast.Unknown, None))) lexps values)) @@ -556,6 +557,9 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) = | LEXP_tup lexps -> mk_exp (E_tuple (List.map exp_of_lexp lexps)) | LEXP_vector (lexp, exp) -> mk_exp (E_vector_access (exp_of_lexp lexp, exp)) | LEXP_vector_range (lexp, exp1, exp2) -> mk_exp (E_vector_subrange (exp_of_lexp lexp, exp1, exp2)) + | LEXP_vector_concat [] -> failwith "Empty LEXP_vector_concat node in exp_of_lexp" + | LEXP_vector_concat [lexp] -> exp_of_lexp lexp + | LEXP_vector_concat (lexp :: lexps) -> mk_exp (E_vector_append (exp_of_lexp lexp, exp_of_lexp (mk_lexp (LEXP_vector_concat lexps)))) | LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id)) and pattern_match env (P_aux (p_aux, _) as pat) value = diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 826d8eb1..55ed57d2 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -517,6 +517,7 @@ lexp_aux = (* lvalue expression, can't occur out of the parser *) | LEXP_mem of id * (exp) list | LEXP_vector of lexp * exp (* vector element *) | LEXP_vector_range of lexp * exp * exp (* subvector *) + | LEXP_vector_concat of lexp list | LEXP_field of lexp * id (* struct field *) and lexp = diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index c0658a83..5a26cb42 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -418,6 +418,7 @@ and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) = | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp) | LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2]) + | LEXP_vector_concat lexps -> parens (separate_map (string " @ ") doc_lexp lexps) | LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps) | _ -> parens (doc_lexp lexp) and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace diff --git a/src/rewriter.ml b/src/rewriter.ml index 203e8a58..82e3ab05 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -197,6 +197,8 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with | LEXP_memory (_,es) -> union_eff_exps es | LEXP_tup les -> List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les + | LEXP_vector_concat les -> + List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les | LEXP_vector (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e) | LEXP_vector_range (lexp,e1,e2) -> union_effects (effect_of_lexp lexp) @@ -384,6 +386,7 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = rewrap (LEXP_vector_range (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters exp1, rewriters.rewrite_exp rewriters exp2)) + | LEXP_vector_concat lexps -> rewrap (LEXP_vector_concat (List.map (rewriters.rewrite_lexp rewriters) lexps)) | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewriters.rewrite_lexp rewriters lexp,id)) let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = @@ -556,6 +559,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; lEXP_tup : 'lexp list -> 'lexp_aux ; lEXP_vector : 'lexp * 'exp -> 'lexp_aux ; lEXP_vector_range : 'lexp * 'exp * 'exp -> 'lexp_aux + ; lEXP_vector_concat : 'lexp list -> 'lexp_aux ; lEXP_field : 'lexp * id -> 'lexp_aux ; lEXP_aux : 'lexp_aux * 'a annot -> 'lexp ; fE_Fexp : id * 'exp -> 'fexp_aux @@ -635,7 +639,8 @@ and fold_lexp_aux alg = function | LEXP_vector (lexp,e) -> alg.lEXP_vector (fold_lexp alg lexp, fold_exp alg e) | LEXP_vector_range (lexp,e1,e2) -> alg.lEXP_vector_range (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2) - | LEXP_field (lexp,id) -> alg.lEXP_field (fold_lexp alg lexp, id) + | LEXP_vector_concat les -> alg.lEXP_vector_concat (List.map (fold_lexp alg) les) + | LEXP_field (lexp,id) -> alg.lEXP_field (fold_lexp alg lexp, id) and fold_lexp alg (LEXP_aux (lexp_aux,annot)) = alg.lEXP_aux (fold_lexp_aux alg lexp_aux, annot) and fold_fexp_aux alg (FE_Fexp (id,e)) = alg.fE_Fexp (id, fold_exp alg e) @@ -706,6 +711,7 @@ let id_exp_alg = ; lEXP_tup = (fun tups -> LEXP_tup tups) ; lEXP_vector = (fun (lexp,e2) -> LEXP_vector (lexp,e2)) ; lEXP_vector_range = (fun (lexp,e2,e3) -> LEXP_vector_range (lexp,e2,e3)) + ; lEXP_vector_concat = (fun lexps -> LEXP_vector_concat lexps) ; lEXP_field = (fun (lexp,id) -> LEXP_field (lexp,id)) ; lEXP_aux = (fun (lexp,annot) -> LEXP_aux (lexp,annot)) ; fE_Fexp = (fun (id,e) -> FE_Fexp (id,e)) @@ -813,6 +819,9 @@ let compute_exp_alg bot join = ; lEXP_vector = (fun ((vl,lexp),(v2,e2)) -> (join vl v2, LEXP_vector (lexp,e2))) ; lEXP_vector_range = (fun ((vl,lexp),(v2,e2),(v3,e3)) -> (join_list [vl;v2;v3], LEXP_vector_range (lexp,e2,e3))) + ; lEXP_vector_concat = (fun ls -> + let (vs,ls) = List.split ls in + (join_list vs, LEXP_vector_concat ls)) ; lEXP_field = (fun ((vl,lexp),id) -> (vl, LEXP_field (lexp,id))) ; lEXP_aux = (fun ((vl,lexp),annot) -> (vl, LEXP_aux (lexp,annot))) ; fE_Fexp = (fun (id,(v,e)) -> (v, FE_Fexp (id,e))) diff --git a/src/rewriter.mli b/src/rewriter.mli index f8982d69..ccc1f951 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -155,6 +155,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; lEXP_tup : 'lexp list -> 'lexp_aux ; lEXP_vector : 'lexp * 'exp -> 'lexp_aux ; lEXP_vector_range : 'lexp * 'exp * 'exp -> 'lexp_aux + ; lEXP_vector_concat : 'lexp list -> 'lexp_aux ; lEXP_field : 'lexp * id -> 'lexp_aux ; lEXP_aux : 'lexp_aux * 'a annot -> 'lexp ; fE_Fexp : id * 'exp -> 'fexp_aux @@ -167,7 +168,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; pat_exp : 'pat * 'exp -> 'pexp_aux ; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux ; pat_aux : 'pexp_aux * 'a annot -> 'pexp - ; lB_val : 'pat * 'exp -> 'letbind_aux + ; lB_val : 'pat * 'exp -> 'letbind_aux ; lB_aux : 'letbind_aux * 'a annot -> 'letbind ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg } diff --git a/src/rewrites.ml b/src/rewrites.ml index cfeae1e3..a61f2622 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -127,7 +127,7 @@ let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with | LEXP_memory _ | LEXP_deref _ -> false | LEXP_id id | LEXP_cast (_, id) -> id_is_local_var id env - | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps + | LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps | LEXP_vector (lexp,_) | LEXP_vector_range (lexp,_,_) | LEXP_field (lexp,_) -> lexp_is_local lexp env @@ -136,7 +136,7 @@ let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with | LEXP_memory _ | LEXP_deref _ -> false | LEXP_id id | LEXP_cast (_, id) -> id_is_unbound id env - | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps + | LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps | LEXP_vector (lexp,_) | LEXP_vector_range (lexp,_,_) | LEXP_field (lexp,_) -> lexp_is_local_intro lexp env @@ -281,7 +281,7 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = scope. *) | Some size when prove env (nc_eq (nsum size (nint 1)) nexp) -> let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in - Some (E_aux (E_app (mk_id "add_range", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect)))) + Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect)))) | _ -> begin match destruct_vector env typ with @@ -293,12 +293,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = let rec split_nexp (Nexp_aux (nexp_aux, l) as nexp) = match nexp_aux with | Nexp_sum (n1, n2) -> - mk_exp (E_app (mk_id "add_range", [split_nexp n1; split_nexp n2])) + mk_exp (E_app (mk_id "add_atom", [split_nexp n1; split_nexp n2])) | Nexp_minus (n1, n2) -> - mk_exp (E_app (mk_id "sub_range", [split_nexp n1; split_nexp n2])) + mk_exp (E_app (mk_id "sub_atom", [split_nexp n1; split_nexp n2])) | Nexp_times (n1, n2) -> - mk_exp (E_app (mk_id "mult_range", [split_nexp n1; split_nexp n2])) - | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_range", [split_nexp nexp])) + mk_exp (E_app (mk_id "mult_atom", [split_nexp n1; split_nexp n2])) + | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_atom", [split_nexp nexp])) | _ -> mk_exp (E_sizeof nexp) in let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) = @@ -487,6 +487,7 @@ let rewrite_sizeof (Defs defs) = ; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups')) ; lEXP_vector = (fun ((lexp,lexp'),(e2,e2')) -> (LEXP_vector (lexp,e2), LEXP_vector (lexp',e2'))) ; lEXP_vector_range = (fun ((lexp,lexp'),(e2,e2'),(e3,e3')) -> (LEXP_vector_range (lexp,e2,e3), LEXP_vector_range (lexp',e2',e3'))) + ; lEXP_vector_concat = (fun lexps -> let (lexps,lexps') = List.split lexps in (LEXP_vector_concat lexps, LEXP_vector_concat lexps')) ; lEXP_field = (fun ((lexp,lexp'),id) -> (LEXP_field (lexp,id), LEXP_field (lexp',id))) ; lEXP_aux = (fun ((lexp,lexp'),annot) -> (LEXP_aux (lexp,annot), LEXP_aux (lexp',annot))) ; fE_Fexp = (fun (id,(e,e')) -> (FE_Fexp (id,e), FE_Fexp (id,e'))) @@ -2281,11 +2282,11 @@ let rewrite_simple_types (Defs defs) = let defs = Defs (List.map simple_def defs) in rewrite_defs_base simple_defs defs -let rewrite_tuple_vector_assignments defs = +let rewrite_vector_concat_assignments defs = let assign_tuple e_aux annot = let env = env_of_annot annot in match e_aux with - | E_assign (LEXP_aux (LEXP_tup lexps, lannot), exp) -> + | E_assign (LEXP_aux (LEXP_vector_concat lexps, lannot), exp) -> let typ = Env.base_typ_of env (typ_of exp) in if is_vector_typ typ then (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *) @@ -2518,8 +2519,11 @@ let rewrite_defs_letbind_effects = | LEXP_vector_range (lexp,e1,e2) -> n_lexp lexp (fun lexp -> n_exp_name e1 (fun e1 -> - n_exp_name e2 (fun e2 -> + n_exp_name e2 (fun e2 -> k (fix_eff_lexp (LEXP_aux (LEXP_vector_range (lexp,e1,e2),annot)))))) + | LEXP_vector_concat es -> + n_lexpL es (fun es -> + k (fix_eff_lexp (LEXP_aux (LEXP_vector_concat es,annot)))) | LEXP_field (lexp,id) -> n_lexp lexp (fun lexp -> k (fix_eff_lexp (LEXP_aux (LEXP_field (lexp,id),annot)))) @@ -3198,7 +3202,7 @@ let merge_funcls (Defs defs) = let recheck_defs defs = fst (check initial_env defs) let rewrite_defs_lem = [ - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); @@ -3233,7 +3237,7 @@ let rewrite_defs_ocaml = [ (* ("undefined", rewrite_undefined); *) ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("pat_lits", rewrite_defs_pat_lits); - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); @@ -3252,7 +3256,7 @@ let rewrite_defs_ocaml = [ let rewrite_defs_c = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("pat_lits", rewrite_defs_pat_lits); - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); @@ -3268,7 +3272,7 @@ let rewrite_defs_c = [ let rewrite_defs_interpreter = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); diff --git a/src/sail.ml b/src/sail.ml index 4d32fb94..f459d774 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -157,6 +157,9 @@ let options = Arg.align ([ ( "-enum_casts", Arg.Set Initial_check.opt_enum_casts, " allow enumerations to be automatically casted to numeric range types"); + ( "-no_lexp_bounds_check", + Arg.Set Type_check.opt_no_lexp_bounds_check, + " turn off bounds checking for vector assignments in l-expressions"); ( "-no_effects", Arg.Set Type_check.opt_no_effects, " (experimental) turn off effect checking"); diff --git a/src/type_check.ml b/src/type_check.ml index de4c22c3..65d07859 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -63,6 +63,10 @@ let opt_tc_debug = ref 0 re-writer passes, so it should only be used for debugging. *) let opt_no_effects = ref false +(* opt_no_lexp_bounds_check turns of the bounds checking in vector + assignments in l-expressions *) +let opt_no_lexp_bounds_check = ref false + let depth = ref 0 let rec indent n = match n with @@ -314,6 +318,7 @@ module Env : sig val add_union_id : id -> typquant * typ -> t -> t val add_flow : id -> (typ -> typ) -> t -> t val get_flow : id -> t -> typ -> typ + val remove_flow : id -> t -> t val is_register : id -> t -> bool val get_register : id -> t -> typ val add_register : id -> typ -> t -> t @@ -346,7 +351,7 @@ module Env : sig val add_cast : id -> t -> t val allow_polymorphic_undefineds : t -> t val polymorphic_undefineds : t -> bool - val lookup_id : id -> t -> lvar + val lookup_id : ?raw:bool -> id -> t -> lvar val fresh_kid : ?kid:kid -> t -> kid val expand_synonyms : t -> typ -> typ val canonicalize : t -> typ -> typ @@ -856,10 +861,12 @@ end = struct | Not_found -> fun typ -> typ let add_flow id f env = - begin - typ_print (lazy ("Adding flow constraints for " ^ string_of_id id)); - { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow } - end + typ_print (lazy ("Adding flow constraints for " ^ string_of_id id)); + { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow } + + let remove_flow id env = + typ_print (lazy ("Removing flow constraints for " ^ string_of_id id)); + { env with flow = Bindings.remove id env.flow } let is_register id env = Bindings.mem id env.registers @@ -898,11 +905,11 @@ end = struct let get_locals env = env.locals - let lookup_id id env = + let lookup_id ?raw:(raw=false) id env = try let (mut, typ) = Bindings.find id env.locals in let flow = get_flow id env in - Local (mut, flow typ) + Local (mut, if raw then typ else flow typ) with | Not_found -> begin @@ -943,12 +950,11 @@ end = struct let add_constraint (NC_aux (nc_aux, l) as constr) env = wf_constraint env constr; - begin - typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr)); - match nc_aux with - | NC_true -> env - | _ -> { env with constraints = constr :: env.constraints } - end + match nc_aux with + | NC_true -> env + | _ -> + typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr)); + { env with constraints = constr :: env.constraints } let get_ret_typ env = env.ret_typ @@ -1095,6 +1101,12 @@ let destruct_numeric env typ = Some ([kid], nc_true, nvar kid) | _, _ -> None +let bind_numeric l typ env = + match destruct_numeric env typ with + | Some (kids, nc, nexp) -> + nexp, add_existential kids nc env + | None -> typ_error l ("Expected " ^ string_of_typ typ ^ " to be numeric") + (** Pull an (potentially)-existentially qualified type into the global typing environment **) let bind_existential typ env = @@ -1224,7 +1236,7 @@ let prove_z3' env constr = | Constraint.Unknown -> typ_debug (lazy "unknown"); false let prove_z3 env nc = - typ_print (lazy ("Prove " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)); + typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)); prove_z3' env (fun var_of -> Constraint.negate (nc_constraint env var_of nc)) let solve env nexp = @@ -1743,7 +1755,10 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t match destruct_exist env typ1, unwrap_exist env (Env.canonicalize env typ2) with | Some (kids, nc, typ1), _ -> let env = add_existential kids nc env in subtyp l env typ1 typ2 + (* | None, ([], _, typ2) -> + typ_error l (string_of_typ typ1 ^ " < " ^ string_of_typ typ2) *) | None, (kids, nc, typ2) -> + typ_debug (lazy "Subtype check with unification"); let env = add_typ_vars kids env in let kids' = KidSet.elements (KidSet.diff (KidSet.of_list kids) (typ_frees typ2)) in let unifiers, existential_kids, existential_nc = @@ -1913,6 +1928,10 @@ let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot) let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot) +let lexp_typ_of (LEXP_aux (_, (l, tannot))) = typ_of_annot (l, tannot) + +let lexp_env_of (LEXP_aux (_, (l, tannot))) = env_of_annot (l, tannot) + (* Flow typing *) let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with @@ -2096,7 +2115,7 @@ let rec filter_casts env from_typ to_typ casts = let crule r env exp typ = incr depth; - typ_print (lazy ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ)); + typ_print (lazy (Util.("Check " |> cyan |> clear) ^ string_of_exp exp ^ " <= " ^ string_of_typ typ)); try let checked_exp = r env exp typ in decr depth; checked_exp @@ -2107,7 +2126,7 @@ let irule r env exp = incr depth; try let inferred_exp = r env exp in - typ_print (lazy ("Infer " ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp))); + typ_print (lazy (Util.("Infer " |> blue |> clear) ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp))); decr depth; inferred_exp with @@ -2695,7 +2714,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in annot_assign tlexp checked_exp, env' | LEXP_id v when has_typ v env -> - begin match Env.lookup_id v env with + begin match Env.lookup_id ~raw:true v env with | Local (Mutable, vtyp) | Register vtyp -> let checked_exp = crule check_exp env exp vtyp in let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in @@ -2708,9 +2727,26 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as annot_assign tlexp inferred_exp, env' and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = + typ_print (lazy ("Binding mutable " ^ string_of_lexp lexp ^ " to " ^ string_of_typ typ)); let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in match lexp_aux with + | LEXP_cast (typ_annot, v) -> + begin match Env.lookup_id ~raw:true v env with + | Local (Immutable, _) | Enum _ -> + typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) + | Local (Mutable, vtyp) -> + subtyp l env typ typ_annot; + subtyp l env typ_annot vtyp; + annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env + | Register vtyp -> + subtyp l env typ typ_annot; + subtyp l env typ_annot vtyp; + annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env + | Unbound -> + subtyp l env typ typ_annot; + annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env + end | LEXP_deref exp -> let inferred_exp = infer_exp env exp in begin match typ_of inferred_exp with @@ -2719,39 +2755,16 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env | _ -> - typ_error l (string_of_typ typ ^ " must be a ref or register type in (*" ^ string_of_exp exp ^ ")") + typ_error l (string_of_typ typ ^ " must be a ref or register type in " ^ string_of_exp exp ^ ")") end | LEXP_id v -> - begin match Env.lookup_id v env with + begin match Env.lookup_id ~raw:true v env with | Local (Immutable, _) | Enum _ -> typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) - | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env + | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, Env.remove_flow v env | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env end - | LEXP_cast (typ_annot, v) -> - begin - match Env.lookup_id v env with - | Local (Immutable, _) | Enum _ -> - typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) - | Local (Mutable, vtyp) -> - begin - subtyp l env typ typ_annot; - subtyp l env typ_annot vtyp; - annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env - end - | Register vtyp -> - begin - subtyp l env typ typ_annot; - subtyp l env typ_annot vtyp; - annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env - end - | Unbound -> - begin - subtyp l env typ typ_annot; - annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env - end - end | LEXP_tup lexps -> begin let typ = Env.expand_synonyms env typ in @@ -2766,99 +2779,85 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Invalid_argument _ -> typ_error l "Tuple l-expression and tuple type have different length" in annot_lexp (LEXP_tup tlexps) typ, env - (* This case is pretty much just for the PSTATE.<N,Z,C,V> := vector pattern which is really common in ASL. *) - (* Maybe this code can be made not horrible? *) - | Typ_app (id, _) when Id.compare id (mk_id "vector") == 0 -> - begin - match destruct_vector env typ with - | Some (vec_len, _, _) -> - let bind_bits_tuple lexp (tlexps, env, llen) = - match lexp with - | LEXP_aux (LEXP_id v, _) -> - begin - match Env.lookup_id v env with - | Local (Immutable, _) | Enum _ -> - typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) - | Unbound -> - typ_error l "Unbound variable in vector tuple assignment" - | Local (Mutable, vtyp) | Register vtyp -> - let llen' = match destruct_vector env vtyp with - | Some (llen', _, _) -> llen' - | None -> typ_error l "Variables in vector tuple assignment must be vectors" - in - let tlexp, env = bind_lexp env lexp vtyp in - tlexp :: tlexps, env, nsum llen llen' - end - | LEXP_aux (LEXP_field (LEXP_aux (LEXP_id v, _), fid), _) -> - (* FIXME: will only work for ASL *) - let rec_id = - match Env.lookup_id v env with - | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id - | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here") - in - let typq, _, vtyp, _ = Env.get_accessor rec_id fid env in - let llen' = match destruct_vector env vtyp with - | Some (llen', _, _) -> llen' - | None -> typ_error l "Variables in vector tuple assignment must be vectors" - in - let tlexp, env = bind_lexp env lexp vtyp in - tlexp :: tlexps, env, nsum llen llen' - | _ -> typ_error l "bit vector assignment must only contain identifiers" - in - let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nint 0) in - if prove env (nc_eq vec_len lexp_len) - then annot_lexp (LEXP_tup tlexps) typ, env - else typ_error l "Vector and tuple length must be the same in assignment" - | None -> typ_error l ("Malformed vector type " ^ string_of_typ typ) + | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple type " ^ string_of_typ typ) + end + | _ -> + let inferred_lexp = infer_lexp env lexp in + subtyp l env typ (lexp_typ_of inferred_lexp); + inferred_lexp, env + +and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) = + let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in + let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in + match lexp_aux with + | LEXP_id v -> + begin match Env.lookup_id v env with + | Local (Mutable, typ) -> annot_lexp (LEXP_id v) typ + (* Probably need to remove flows here *) + | Register typ -> annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]) + | Local (Immutable, _) | Enum _ -> + typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) + | Unbound -> + typ_error l ("Cannot create a new identifier in this l-expression " ^ string_of_lexp lexp) + end + | LEXP_vector_range (v_lexp, exp1, exp2) -> + begin + let inferred_v_lexp = infer_lexp env v_lexp in + let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 -> + let inferred_exp1 = infer_exp env exp1 in + let inferred_exp2 = infer_exp env exp2 in + let nexp1, env = bind_numeric l (typ_of inferred_exp1) env in + let nexp2, env = bind_numeric l (typ_of inferred_exp2) env in + begin match ord with + | Ord_aux (Ord_inc, _) when !opt_no_lexp_bounds_check || prove env (nc_lteq nexp1 nexp2) -> + let len = nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)) in + annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ) + | Ord_aux (Ord_dec, _) when !opt_no_lexp_bounds_check || prove env (nc_gteq nexp1 nexp2) -> + let len = nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)) in + annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ) + | _ -> typ_error l ("Could not infer length of vector slice assignment " ^ string_of_lexp lexp) end - | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ) + | _ -> typ_error l "Cannot assign slice of non vector type" end - | LEXP_vector_range (LEXP_aux (LEXP_id v, _), exp1, exp2) -> + | LEXP_vector (v_lexp, exp) -> begin - let is_immutable, is_register, vtyp = match Env.lookup_id v env with - | Unbound -> typ_error l "Cannot assign to element of unbound vector" - | Enum _ -> typ_error l "Cannot vector assign to enumeration element" - | Local (Immutable, vtyp) -> true, false, vtyp - | Local (Mutable, vtyp) -> false, false, vtyp - | Register vtyp -> false, true, vtyp - in - let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in - let inferred_exp1, inferred_exp2 = match access with - | E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) -> inferred_exp1, inferred_exp2 - | _ -> assert false - in - match typ_of access with - | _ when not is_immutable && is_register -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env - | _ when not is_immutable -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector_range (annot_lexp (LEXP_id v) vtyp, inferred_exp1, inferred_exp2)) typ, env - | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp) + let inferred_v_lexp = infer_lexp env v_lexp in + let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 -> + let inferred_exp = infer_exp env exp in + let nexp, env = bind_numeric l (typ_of inferred_exp) env in + if !opt_no_lexp_bounds_check || prove env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then + annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) elem_typ + else + typ_error l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp) + | _ -> typ_error l "Cannot assign vector element of non vector type" end - (* Not sure about this case... can the left lexp be anything other than an identifier? *) - | LEXP_vector (LEXP_aux (LEXP_id v, _), exp) -> + | LEXP_vector_concat [] -> typ_error l "Cannot have empty vector concatenation l-expression" + | LEXP_vector_concat (v_lexp :: v_lexps) -> begin - let is_immutable, is_register, vtyp = match Env.lookup_id v env with - | Unbound -> typ_error l "Cannot assign to element of unbound vector" - | Enum _ -> typ_error l "Cannot vector assign to enumeration element" - | Local (Immutable, vtyp) -> true, false, vtyp - | Local (Mutable, vtyp) -> false, false, vtyp - | Register vtyp -> false, true, vtyp - in - let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in - let inferred_exp = match access with - | E_aux (E_app (_, [_; inferred_exp]), _) -> inferred_exp - | _ -> assert false + let sum_lengths first_ord first_elem_typ acc (Typ_aux (v_typ_aux, _) as v_typ) = + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 && ord_identical ord first_ord -> + typ_equality l env elem_typ first_elem_typ; + nsum acc len + | _ -> typ_error l "Vector concatentation l-expression must only contain vector types of the same order" in - match typ_of access with - | _ when not is_immutable && is_register -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env - | _ when not is_immutable -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp)) typ, env - | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp) + let inferred_v_lexp = infer_lexp env v_lexp in + let inferred_v_lexps = List.map (infer_lexp env) v_lexps in + let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in + let v_typs = List.map (fun lexp -> Env.expand_synonyms env (lexp_typ_of lexp)) inferred_v_lexps in + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 -> + let len = List.fold_left (sum_lengths ord elem_typ) len v_typs in + annot_lexp (LEXP_vector_concat (inferred_v_lexp :: inferred_v_lexps)) (vector_typ (nexp_simp len) ord elem_typ) + | _ -> typ_error l ("Vector concatentation l-expression must only contain vector types, found " ^ string_of_typ v_typ) end | LEXP_field (LEXP_aux (LEXP_id v, _), fid) -> (* FIXME: will only work for ASL *) @@ -2868,7 +2867,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here") in let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in - annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]), env + annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]) | _ -> typ_error l ("Unhandled l-expression " ^ string_of_lexp lexp) and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = @@ -2951,7 +2950,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_app (f, xs) -> infer_funapp l env f xs None | E_loop (loop_type, cond, body) -> let checked_cond = crule check_exp env cond bool_typ in - let checked_body = crule check_exp env body unit_typ in + let flows, constrs = infer_flow env checked_cond in + let checked_body = crule check_exp (add_flows true flows env) body unit_typ in annot_exp (E_loop (loop_type, checked_cond, checked_body)) unit_typ | E_for (v, f, t, step, ord, body) -> begin @@ -3485,6 +3485,9 @@ and propagate_lexp_effect_aux = function let p_exp2 = propagate_exp_effect exp2 in LEXP_vector_range (p_lexp, p_exp1, p_exp2), union_effects (collect_effects [p_exp1; p_exp2]) (effect_of_lexp p_lexp) + | LEXP_vector_concat lexps -> + let p_lexps = List.map propagate_lexp_effect lexps in + LEXP_vector_concat p_lexps, collect_effects_lexp p_lexps | LEXP_field (lexp, id) -> let p_lexp = propagate_lexp_effect lexp in LEXP_field (p_lexp, id),effect_of_lexp p_lexp diff --git a/src/type_check.mli b/src/type_check.mli index bb52f2aa..ed240839 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -63,6 +63,10 @@ val opt_tc_debug : int ref re-writer passes, so it should only be used for debugging. *) val opt_no_effects : bool ref +(** [opt_no_lexp_bounds_check] turns of the bounds checking in vector + assignments in l-expressions. *) +val opt_no_lexp_bounds_check : bool ref + (** {2 Type errors} *) type type_error = @@ -148,8 +152,9 @@ module Env : sig (** Lookup id searchs for a specified id in the environment, and returns it's type and what kind of identifier it is, using the lvar type. Returns Unbound if the identifier is unbound, and - won't throw any exceptions. *) - val lookup_id : id -> t -> lvar + won't throw any exceptions. If the raw option is true, then look + up the type without any flow typing modifiers. *) + val lookup_id : ?raw:bool -> id -> t -> lvar val is_union_constructor : id -> t -> bool diff --git a/src/value.ml b/src/value.ml index 4b4f0865..e9a98160 100644 --- a/src/value.ml +++ b/src/value.ml @@ -183,6 +183,10 @@ let value_eq_string = function | [v1; v2] -> V_bool (Sail_lib.eq_string (coerce_string v1, coerce_string v2)) | _ -> failwith "value eq_string" +let value_eq_bit = function + | [v1; v2] -> V_bool (Sail_lib.eq_bit (coerce_bit v1, coerce_bit v2)) + | _ -> failwith "value eq_bit" + let value_length = function | [v] -> V_int (coerce_gv v |> List.length |> Big_int.of_int) | _ -> failwith "value length" @@ -417,6 +421,7 @@ let primops = ("eq_list", value_eq_list); ("eq_bool", value_eq_bool); ("eq_string", value_eq_string); + ("eq_bit", value_eq_bit); ("eq_anything", value_eq_anything); ("length", value_length); ("subrange", value_subrange); |