diff options
Diffstat (limited to 'src')
37 files changed, 2141 insertions, 532 deletions
diff --git a/src/META b/src/META new file mode 100644 index 00000000..80194d98 --- /dev/null +++ b/src/META @@ -0,0 +1,6 @@ +# META file of package sail: +description = "Sail is a language for describing the instruction-set architecture (ISA) semantics of processors." +requires = "linenoise lem linksem omd base64 yojson" +version = "0.8" +archive(byte) = "libsail.cma" +archive(native) = "libsail.cmxa" diff --git a/src/Makefile b/src/Makefile index d71c9fb8..a002d4f3 100644 --- a/src/Makefile +++ b/src/Makefile @@ -103,7 +103,8 @@ sail: ast.ml jib.ml manifest.ml ocamlbuild -use-ocamlfind sail.native sail_lib.cma sail_lib.cmxa isail: ast.ml jib.ml manifest.ml - ocamlbuild -use-ocamlfind isail.native + ocamlbuild -use-ocamlfind isail.native sail_lib.cma sail_lib.cmxa libsail.cma libsail.cmxa + coverage: ast.ml jib.ml manifest.ml BISECT_COVERAGE=YES ocamlbuild -use-ocamlfind -plugin-tag 'package(bisect_ppx-ocamlbuild)' isail.native @@ -113,6 +114,9 @@ sail.native: sail sail.byte: ast.ml jib.ml manifest.ml ocamlbuild -use-ocamlfind -cflag -g sail.byte +isail.byte: ast.ml bytecode.ml share_directory.ml + ocamlbuild -use-ocamlfind isail.byte + interpreter: lem_interp/interp_ast.lem ocamlbuild -use-ocamlfind lem_interp/extract.cmxa ocamlbuild -use-ocamlfind lem_interp/extract.cma @@ -2,13 +2,13 @@ true: -traverse, debug, use_menhir <**/parser.ml>: bin_annot, annot <**/*.ml> and not <**/parser.ml>: bin_annot, annot -<sail.{byte,native}>: package(zarith), package(linksem), package(lem), package(omd), use_pprint -<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), package(omd), package(yojson), use_pprint +<sail.{byte,native}>: package(zarith), package(linksem), package(lem), package(omd), package(base64), use_pprint +<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), package(omd), package(base64), package(yojson), use_pprint <isail.ml>: package(linenoise), package(yojson) <elf_loader.ml>: package(linksem) <latex.ml>: package(omd) -<**/*.m{l,li}>: package(lem) +<**/*.m{l,li}>: package(lem), package(base64) <gen_lib>: include <jib>: include diff --git a/src/ast_util.ml b/src/ast_util.ml index d0efc0de..33af1be7 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -519,7 +519,7 @@ and map_exp_annot_aux f = function | E_tuple xs -> E_tuple (List.map (map_exp_annot f) xs) | E_if (cond, t, e) -> E_if (map_exp_annot f cond, map_exp_annot f t, map_exp_annot f e) | E_for (v, e1, e2, e3, o, e4) -> E_for (v, map_exp_annot f e1, map_exp_annot f e2, map_exp_annot f e3, o, map_exp_annot f e4) - | E_loop (loop_type, e1, e2) -> E_loop (loop_type, map_exp_annot f e1, map_exp_annot f e2) + | E_loop (loop_type, measure, e1, e2) -> E_loop (loop_type, map_measure_annot f measure, map_exp_annot f e1, map_exp_annot f e2) | E_vector exps -> E_vector (List.map (map_exp_annot f) exps) | E_vector_access (exp1, exp2) -> E_vector_access (map_exp_annot f exp1, map_exp_annot f exp2) | E_vector_subrange (exp1, exp2, exp3) -> E_vector_subrange (map_exp_annot f exp1, map_exp_annot f exp2, map_exp_annot f exp3) @@ -546,6 +546,10 @@ and map_exp_annot_aux f = function | E_var (lexp, exp1, exp2) -> E_var (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2) | E_internal_plet (pat, exp1, exp2) -> E_internal_plet (map_pat_annot f pat, map_exp_annot f exp1, map_exp_annot f exp2) | E_internal_return exp -> E_internal_return (map_exp_annot f exp) +and map_measure_annot f (Measure_aux (m, l)) = Measure_aux (map_measure_annot_aux f m, l) +and map_measure_annot_aux f = function + | Measure_none -> Measure_none + | Measure_some exp -> Measure_some (map_exp_annot f exp) and map_opt_default_annot f (Def_val_aux (df, annot)) = Def_val_aux (map_opt_default_annot_aux f df, f annot) and map_opt_default_annot_aux f = function | Def_val_empty -> Def_val_empty @@ -619,6 +623,84 @@ and map_lexp_annot_aux f = function | 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) +and map_typedef_annot f = function + | TD_aux (td_aux, annot) -> TD_aux (td_aux, f annot) + +and map_fundef_annot f = function + | FD_aux (fd_aux, annot) -> FD_aux (map_fundef_annot_aux f fd_aux, f annot) +and map_fundef_annot_aux f = function + | FD_function (rec_opt, tannot_opt, eff_opt, funcls) -> FD_function (map_recopt_annot f rec_opt, tannot_opt, eff_opt, + List.map (map_funcl_annot f) funcls) +and map_funcl_annot f = function + | FCL_aux (fcl, annot) -> FCL_aux (map_funcl_annot_aux f fcl, f annot) +and map_funcl_annot_aux f = function + | FCL_Funcl (id, pexp) -> FCL_Funcl (id, map_pexp_annot f pexp) +and map_recopt_annot f = function + | Rec_aux (rec_aux, l) -> Rec_aux (map_recopt_annot_aux f rec_aux, l) +and map_recopt_annot_aux f = function + | Rec_nonrec -> Rec_nonrec + | Rec_rec -> Rec_rec + | Rec_measure (pat, exp) -> Rec_measure (map_pat_annot f pat, map_exp_annot f exp) + +and map_mapdef_annot f = function + | MD_aux (md_aux, annot) -> MD_aux (map_mapdef_annot_aux f md_aux, f annot) +and map_mapdef_annot_aux f = function + | MD_mapping (id, tannot_opt, mapcls) -> MD_mapping (id, tannot_opt, List.map (map_mapcl_annot f) mapcls) + +and map_valspec_annot f = function + | VS_aux (vs_aux, annot) -> VS_aux (vs_aux, f annot) + +and map_scattered_annot f = function + | SD_aux (sd_aux, annot) -> SD_aux (map_scattered_annot_aux f sd_aux, f annot) +and map_scattered_annot_aux f = function + | SD_function (rec_opt, tannot_opt, eff_opt, name) -> SD_function (map_recopt_annot f rec_opt, tannot_opt, eff_opt, name) + | SD_funcl fcl -> SD_funcl (map_funcl_annot f fcl) + | SD_variant (id, typq) -> SD_variant (id, typq) + | SD_unioncl (id, tu) -> SD_unioncl (id, tu) + | SD_mapping (id, tannot_opt) -> SD_mapping (id, tannot_opt) + | SD_mapcl (id, mcl) -> SD_mapcl (id, map_mapcl_annot f mcl) + | SD_end id -> SD_end id + +and map_decspec_annot f = function + | DEC_aux (dec_aux, annot) -> DEC_aux (map_decspec_annot_aux f dec_aux, f annot) +and map_decspec_annot_aux f = function + | DEC_reg (eff1, eff2, typ, id) -> DEC_reg (eff1, eff2, typ, id) + | DEC_config (id, typ, exp) -> DEC_config (id, typ, map_exp_annot f exp) + | DEC_alias (id, als) -> DEC_alias (id, map_aliasspec_annot f als) + | DEC_typ_alias (typ, id, als) -> DEC_typ_alias (typ, id, map_aliasspec_annot f als) +and map_aliasspec_annot f = function + | AL_aux (al_aux, annot) -> AL_aux (map_aliasspec_annot_aux f al_aux, f annot) +and map_aliasspec_annot_aux f = function + | AL_subreg (reg_id, id) -> AL_subreg (map_regid_annot f reg_id, id) + | AL_bit (reg_id, exp) -> AL_bit (map_regid_annot f reg_id, map_exp_annot f exp) + | AL_slice (reg_id, exp1, exp2) -> AL_slice (map_regid_annot f reg_id, map_exp_annot f exp1, map_exp_annot f exp2) + | AL_concat (reg_id1, reg_id2) -> AL_concat (map_regid_annot f reg_id1, map_regid_annot f reg_id2) +and map_regid_annot f = function + | RI_aux (ri_aux, annot) -> RI_aux (map_regid_annot_aux f ri_aux, f annot) +and map_regid_annot_aux f = function + | RI_id id -> RI_id id + +and map_def_annot f = function + | DEF_type td -> DEF_type (map_typedef_annot f td) + | DEF_fundef fd -> DEF_fundef (map_fundef_annot f fd) + | DEF_mapdef md -> DEF_mapdef (map_mapdef_annot f md) + | DEF_val lb -> DEF_val (map_letbind_annot f lb) + | DEF_spec vs -> DEF_spec (map_valspec_annot f vs) + | DEF_fixity (prec, n, id) -> DEF_fixity (prec, n, id) + | DEF_overload (name, overloads) -> DEF_overload (name, overloads) + | DEF_default ds -> DEF_default ds + | DEF_scattered sd -> DEF_scattered (map_scattered_annot f sd) + | DEF_measure (id, pat, exp) -> DEF_measure (id, map_pat_annot f pat, map_exp_annot f exp) + | DEF_loop_measures (id, measures) -> DEF_loop_measures (id, List.map (map_loop_measure_annot f) measures) + | DEF_reg_dec ds -> DEF_reg_dec (map_decspec_annot f ds) + | DEF_internal_mutrec fds -> DEF_internal_mutrec (List.map (map_fundef_annot f) fds) + | DEF_pragma (name, arg, l) -> DEF_pragma (name, arg, l) +and map_defs_annot f = function + | Defs defs -> Defs (List.map (map_def_annot f) defs) + +and map_loop_measure_annot f = function + | Loop (loop, exp) -> Loop (loop, map_exp_annot f exp) + let id_loc = function | Id_aux (_, l) -> l @@ -648,6 +730,7 @@ let def_loc = function | DEF_internal_mutrec _ -> Parse_ast.Unknown | DEF_pragma (_, _, l) -> l | DEF_measure (id, _, _) -> id_loc id + | DEF_loop_measures (id, _) -> id_loc id let string_of_id = function | Id_aux (Id v, _) -> v @@ -838,8 +921,8 @@ let rec string_of_exp (E_aux (exp, _)) = ^ " by " ^ string_of_exp u ^ " order " ^ string_of_order ord ^ ") { " ^ string_of_exp body - | E_loop (While, cond, body) -> "while " ^ string_of_exp cond ^ " do " ^ string_of_exp body - | E_loop (Until, cond, body) -> "repeat " ^ string_of_exp body ^ " until " ^ string_of_exp cond + | E_loop (While, measure, cond, body) -> "while " ^ string_of_measure measure ^ string_of_exp cond ^ " do " ^ string_of_exp body + | E_loop (Until, measure, cond, body) -> "repeat " ^ string_of_measure measure ^ string_of_exp body ^ " until " ^ string_of_exp cond | E_assert (test, msg) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")" | E_exit exp -> "exit " ^ string_of_exp exp | E_throw exp -> "throw " ^ string_of_exp exp @@ -853,7 +936,12 @@ let rec string_of_exp (E_aux (exp, _)) = | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")" | E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body | E_nondet _ -> "NONDET" - | E_internal_value _ -> "INTERNAL VALUE" + | E_internal_value v -> "INTERNAL_VALUE(" ^ Value.string_of_value v ^ ")" + +and string_of_measure (Measure_aux (m,_)) = + match m with + | Measure_none -> "" + | Measure_some exp -> "termination_measure { " ^ string_of_exp exp ^ "}" and string_of_fexp (FE_aux (FE_Fexp (field, exp), _)) = string_of_id field ^ " = " ^ string_of_exp exp @@ -1448,8 +1536,8 @@ let rec subst id value (E_aux (e_aux, annot) as exp) = | E_if (cond, then_exp, else_exp) -> E_if (subst id value cond, subst id value then_exp, subst id value else_exp) - | E_loop (loop, cond, body) -> - E_loop (loop, subst id value cond, subst id value body) + | E_loop (loop, measure, cond, body) -> + E_loop (loop, subst_measure id value measure, subst id value cond, subst id value body) | E_for (id', exp1, exp2, exp3, order, body) when Id.compare id id' = 0 -> E_for (id', exp1, exp2, exp3, order, body) | E_for (id', exp1, exp2, exp3, order, body) -> @@ -1503,6 +1591,11 @@ let rec subst id value (E_aux (e_aux, annot) as exp) = in wrap e_aux +and subst_measure id value (Measure_aux (m_aux, l)) = + match m_aux with + | Measure_none -> Measure_aux (Measure_none, l) + | Measure_some exp -> Measure_aux (Measure_some (subst id value exp), l) + and subst_pexp id value (Pat_aux (pexp_aux, annot)) = let pexp_aux = match pexp_aux with | Pat_exp (pat, exp) when IdSet.mem id (pat_ids pat) -> Pat_exp (pat, exp) @@ -1660,7 +1753,7 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, ann | E_app_infix (exp1, op, exp2) -> E_app_infix (locate f exp1, locate_id f op, locate f exp2) | E_tuple exps -> E_tuple (List.map (locate f) exps) | E_if (cond_exp, then_exp, else_exp) -> E_if (locate f cond_exp, locate f then_exp, locate f else_exp) - | E_loop (loop, cond, body) -> E_loop (loop, locate f cond, locate f body) + | E_loop (loop, measure, cond, body) -> E_loop (loop, locate_measure f measure, locate f cond, locate f body) | E_for (id, exp1, exp2, exp3, ord, exp4) -> E_for (locate_id f id, locate f exp1, locate f exp2, locate f exp3, ord, locate f exp4) | E_vector exps -> E_vector (List.map (locate f) exps) @@ -1694,6 +1787,12 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, ann in E_aux (e_aux, (f l, annot)) +and locate_measure : 'a. (l -> l) -> 'a internal_loop_measure -> 'a internal_loop_measure = fun f (Measure_aux (m, l)) -> + let m = match m with + | Measure_none -> Measure_none + | Measure_some exp -> Measure_some (locate f exp) + in Measure_aux (m, f l) + and locate_letbind : 'a. (l -> l) -> 'a letbind -> 'a letbind = fun f (LB_aux (LB_val (pat, exp), (l, annot))) -> LB_aux (LB_val (locate_pat f pat, locate f exp), (f l, annot)) @@ -1728,6 +1827,15 @@ let unique l = incr unique_ref; l +let extern_assoc backend exts = + try + try + Some (List.assoc backend exts) + with Not_found -> + Some (List.assoc "_" exts) + with Not_found -> + None + (**************************************************************************) (* 1. Substitutions *) (**************************************************************************) diff --git a/src/ast_util.mli b/src/ast_util.mli index 1f459870..cfbc26fe 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -346,8 +346,17 @@ val map_mfpat_annot : ('a annot -> 'b annot) -> 'a mfpat -> 'b mfpat val map_mpexp_annot : ('a annot -> 'b annot) -> 'a mpexp -> 'b mpexp val map_mapcl_annot : ('a annot -> 'b annot) -> 'a mapcl -> 'b mapcl -(** {2 Extract locations from terms} *) +val map_typedef_annot : ('a annot -> 'b annot) -> 'a type_def -> 'b type_def +val map_fundef_annot : ('a annot -> 'b annot) -> 'a fundef -> 'b fundef +val map_funcl_annot : ('a annot -> 'b annot) -> 'a funcl -> 'b funcl +val map_mapdef_annot : ('a annot -> 'b annot) -> 'a mapdef -> 'b mapdef +val map_valspec_annot : ('a annot -> 'b annot) -> 'a val_spec -> 'b val_spec +val map_scattered_annot : ('a annot -> 'b annot) -> 'a scattered_def -> 'b scattered_def + +val map_def_annot : ('a annot -> 'b annot) -> 'a def -> 'b def +val map_defs_annot : ('a annot -> 'b annot) -> 'a defs -> 'b defs +(** {2 Extract locations from terms} *) val id_loc : id -> Parse_ast.l val kid_loc : kid -> Parse_ast.l val typ_loc : typ -> Parse_ast.l @@ -483,6 +492,8 @@ val locate_typ : (l -> l) -> typ -> typ a generated number. *) val unique : l -> l +val extern_assoc : string -> (string * string) list -> string option + (** Try to find the annotation closest to the provided (simplified) location. Note that this function makes no guarantees about finding the closest annotation or even finding an annotation at all. This diff --git a/src/constant_fold.ml b/src/constant_fold.ml index fd9b322b..f2e0add5 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -81,7 +81,8 @@ and exp_of_value = | V_tuple vs -> mk_exp (E_tuple (List.map exp_of_value vs)) | V_unit -> mk_lit_exp L_unit - | V_attempted_read str -> mk_exp (E_id (mk_id str)) + | V_attempted_read str -> + mk_exp (E_id (mk_id str)) | _ -> failwith "No expression for value" (* We want to avoid evaluating things like print statements at compile @@ -155,10 +156,20 @@ and is_constant_fexp (FE_aux (FE_Fexp (_, exp), _)) = is_constant exp let rec run frame = match frame with | Interpreter.Done (state, v) -> v + | Interpreter.Fail _ -> + (* something went wrong, raise exception to abort constant folding *) + assert false | Interpreter.Step (lazy_str, _, _, _) -> run (Interpreter.eval_frame frame) | Interpreter.Break frame -> run (Interpreter.eval_frame frame) + | Interpreter.Effect_request (out, st, stack, Interpreter.Read_reg (reg, cont)) -> + (* return a dummy value to read_reg requests which we handle above + if an expression finally evals to it, but the interpreter + will fail if it tries to actually use. See value.ml *) + run (cont (Value.V_attempted_read reg) st) + | Interpreter.Effect_request _ -> + assert false (* effectful, raise exception to abort constant folding *) (** This rewriting pass looks for function applications (E_app) expressions where every argument is a literal. It passes these @@ -177,9 +188,9 @@ let rec run frame = - Throws an exception that isn't caught. *) -let initial_state ast = +let initial_state ast env = let lstate, gstate = - Interpreter.initial_state ast safe_primops + Interpreter.initial_state ast env safe_primops in (lstate, { gstate with Interpreter.allow_registers = false }) @@ -240,10 +251,11 @@ let rec rewrite_constant_function_calls' ast = let rewrite_count = ref 0 in let ok () = incr rewrite_count in let not_ok () = decr rewrite_count in + let istate = initial_state ast Type_check.initial_env in let rw_defs = { rewriters_base with - rewrite_exp = (fun _ -> rw_exp ok not_ok (initial_state ast)) + rewrite_exp = (fun _ -> rw_exp ok not_ok istate) } in let ast = rewrite_defs_base rw_defs ast in (* We keep iterating until we have no more re-writes to do *) diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml index 5c99a534..608d25e1 100644 --- a/src/constant_propagation.ml +++ b/src/constant_propagation.ml @@ -110,7 +110,7 @@ let rec is_value (E_aux (e,(l,annot))) = match e with | E_id id -> is_constructor id | E_lit _ -> true - | E_tuple es -> List.for_all is_value es + | E_tuple es | E_vector es -> List.for_all is_value es | E_record fes -> List.for_all (fun (FE_aux (FE_Fexp (_, e), _)) -> is_value e) fes | E_app (id,es) -> is_constructor id && List.for_all is_value es @@ -310,7 +310,7 @@ let const_props defs ref_vars = let undefined_builtin_ids = ids_of_defs (Defs Initial_check.undefined_builtin_val_specs) in let remove_primop id = StringMap.remove (string_of_id id) in let remove_undefined_primops = IdSet.fold remove_primop undefined_builtin_ids in - let (lstate, gstate) = Constant_fold.initial_state defs in + let (lstate, gstate) = Constant_fold.initial_state defs Type_check.initial_env in (lstate, { gstate with primops = remove_undefined_primops gstate.primops }) in try @@ -440,11 +440,17 @@ let const_props defs ref_vars = let assigns = isubst_minus_set assigns (assigned_vars e4) in let e4',_ = const_prop_exp (Bindings.remove id (fst substs),snd substs) assigns e4 in re (E_for (id,e1',e2',e3',ord,e4')) assigns - | E_loop (loop,e1,e2) -> + | E_loop (loop,m,e1,e2) -> let assigns = isubst_minus_set assigns (IdSet.union (assigned_vars e1) (assigned_vars e2)) in + let m' = match m with + | Measure_aux (Measure_none,_) -> m + | Measure_aux (Measure_some exp,l) -> + let exp',_ = const_prop_exp substs assigns exp in + Measure_aux (Measure_some exp',l) + in let e1',_ = const_prop_exp substs assigns e1 in let e2',_ = const_prop_exp substs assigns e2 in - re (E_loop (loop,e1',e2')) assigns + re (E_loop (loop,m',e1',e2')) assigns | E_vector es -> let es',assigns = non_det_exp_list es in begin @@ -649,27 +655,106 @@ let const_props defs ref_vars = | _ -> exp and can_match_with_env env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns = - let rec findpat_generic check_pat description assigns = function + let rec check_exp_pat (E_aux (e,(l,annot)) as exp) (P_aux (p,(l',_)) as pat) = + match e, p with + | _, P_wild -> DoesMatch ([],[]) + | _, P_typ (_,p') -> check_exp_pat exp p' + | _, P_id id' when pat_id_is_variable env id' -> DoesMatch ([id',exp],[]) + | E_tuple es, P_tup ps -> + let rec check = function + | DoesNotMatch -> fun _ -> DoesNotMatch + | GiveUp -> fun _ -> GiveUp + | DoesMatch (s,ns) -> + fun (e,p) -> + match check_exp_pat e p with + | DoesMatch (s',ns') -> DoesMatch (s@s', ns@ns') + | x -> x + in List.fold_left check (DoesMatch ([],[])) (List.combine es ps) + | E_id id, _ -> + (match Env.lookup_id id env with + | Enum _ -> begin + match p with + | P_id id' + | P_app (id',[]) -> + if Id.compare id id' = 0 then DoesMatch ([],[]) else DoesNotMatch + | _ -> + (Reporting.print_err l' "Monomorphisation" + "Unexpected kind of pattern for enumeration"; GiveUp) + end + | _ -> GiveUp) + | E_lit (L_aux (lit_e, lit_l)), P_lit (L_aux (lit_p, _)) -> + if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch + | E_lit (L_aux (lit_e, lit_l)), + P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)) -> + begin + match lit_e with + | L_num i -> + DoesMatch ([id, E_aux (e,(l,annot))], + [kid,Nexp_aux (Nexp_constant i,Unknown)]) + (* For undefined we fix the type-level size (because there's no good + way to construct an undefined size), but leave the term as undefined + to make the meaning clear. *) + | L_undef -> + let nexp = fabricate_nexp l annot in + let typ = subst_kids_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in + DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))], + [kid,nexp]) + | _ -> + (Reporting.print_err lit_l "Monomorphisation" + "Unexpected kind of literal for var match"; GiveUp) + end + | E_lit _, _ -> + (Reporting.print_err l' "Monomorphisation" + "Unexpected kind of pattern for literal"; GiveUp) + | E_vector es, P_vector ps + when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es -> + let matches = List.map2 (fun e p -> + match e, p with + | E_aux (E_lit (L_aux (lit,_)),_), P_aux (P_lit (L_aux (lit',_)),_) -> + if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch + | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var -> + DoesMatch ([var, e],[]) + | _ -> GiveUp) es ps in + let final = List.fold_left (fun acc m -> match acc, m with + | _, GiveUp -> GiveUp + | GiveUp, _ -> GiveUp + | DoesMatch (sub,ksub), DoesMatch(sub',ksub') -> DoesMatch(sub@sub',ksub@ksub') + | _ -> DoesNotMatch) (DoesMatch ([],[])) matches in + (match final with + | GiveUp -> + (Reporting.print_err l "Monomorphisation" + "Unexpected kind of pattern for vector literal"; GiveUp) + | _ -> final) + | E_vector _, _ -> + (Reporting.print_err l "Monomorphisation" + "Unexpected kind of pattern for vector literal"; GiveUp) + | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)), + P_lit (L_aux (lit_p, _)) + -> DoesNotMatch + | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)), + P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)) -> + (* For undefined we fix the type-level size (because there's no good + way to construct an undefined size), but leave the term as undefined + to make the meaning clear. *) + let nexp = fabricate_nexp l annot in + let kids = equal_kids (env_of_annot p_id_annot) kid in + let ksubst = KidSet.fold (fun k b -> KBindings.add k nexp b) kids KBindings.empty in + let typ = subst_kids_typ ksubst (typ_of_annot p_id_annot) in + DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))], + KBindings.bindings ksubst) + | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)), _ -> + (Reporting.print_err l' "Monomorphisation" + "Unexpected kind of pattern for literal"; GiveUp) + | E_record _,_ | E_cast (_, E_aux (E_record _, _)),_ -> DoesNotMatch + | _ -> GiveUp + in + let check_pat = check_exp_pat exp0 in + let rec findpat_generic description assigns = function | [] -> (Reporting.print_err l "Monomorphisation" ("Failed to find a case for " ^ description); None) - | [Pat_aux (Pat_exp (P_aux (P_wild,_),exp),_)] -> Some (exp,[],[]) - | (Pat_aux (Pat_exp (P_aux (P_typ (_,p),_),exp),ann))::tl -> - findpat_generic check_pat description assigns ((Pat_aux (Pat_exp (p,exp),ann))::tl) - | (Pat_aux (Pat_exp (P_aux (P_id id',_),exp),_))::tlx - when pat_id_is_variable env id' -> - Some (exp, [(id', exp0)], []) - | (Pat_aux (Pat_when (P_aux (P_id id',_),guard,exp),_))::tl - when pat_id_is_variable env id' -> begin - let substs = Bindings.add id' exp0 substs, ksubsts in - let (E_aux (guard,_)),assigns = const_prop_exp substs assigns guard in - match guard with - | E_lit (L_aux (L_true,_)) -> Some (exp,[(id',exp0)],[]) - | E_lit (L_aux (L_false,_)) -> findpat_generic check_pat description assigns tl - | _ -> None - end | (Pat_aux (Pat_when (p,guard,exp),_))::tl -> begin match check_pat p with - | DoesNotMatch -> findpat_generic check_pat description assigns tl + | DoesNotMatch -> findpat_generic description assigns tl | DoesMatch (vsubst,ksubst) -> begin let guard = nexp_subst_exp (kbindings_from_list ksubst) guard in let substs = bindings_union substs (bindings_from_list vsubst), @@ -677,101 +762,17 @@ let const_props defs ref_vars = let (E_aux (guard,_)),assigns = const_prop_exp substs assigns guard in match guard with | E_lit (L_aux (L_true,_)) -> Some (exp,vsubst,ksubst) - | E_lit (L_aux (L_false,_)) -> findpat_generic check_pat description assigns tl + | E_lit (L_aux (L_false,_)) -> findpat_generic description assigns tl | _ -> None end | GiveUp -> None end | (Pat_aux (Pat_exp (p,exp),_))::tl -> match check_pat p with - | DoesNotMatch -> findpat_generic check_pat description assigns tl + | DoesNotMatch -> findpat_generic description assigns tl | DoesMatch (subst,ksubst) -> Some (exp,subst,ksubst) | GiveUp -> None - in - match e with - | E_id id -> - (match Env.lookup_id id env with - | Enum _ -> - let checkpat = function - | P_aux (P_id id',_) - | P_aux (P_app (id',[]),_) -> - if Id.compare id id' = 0 then DoesMatch ([],[]) else DoesNotMatch - | P_aux (_,(l',_)) -> - (Reporting.print_err l' "Monomorphisation" - "Unexpected kind of pattern for enumeration"; GiveUp) - in findpat_generic checkpat (string_of_id id) assigns cases - | _ -> None) - | E_lit (L_aux (lit_e, lit_l)) -> - let checkpat = function - | P_aux (P_lit (L_aux (lit_p, _)),_) -> - if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch - | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) -> - begin - match lit_e with - | L_num i -> - DoesMatch ([id, E_aux (e,(l,annot))], - [kid,Nexp_aux (Nexp_constant i,Unknown)]) - (* For undefined we fix the type-level size (because there's no good - way to construct an undefined size), but leave the term as undefined - to make the meaning clear. *) - | L_undef -> - let nexp = fabricate_nexp l annot in - let typ = subst_kids_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in - DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))], - [kid,nexp]) - | _ -> - (Reporting.print_err lit_l "Monomorphisation" - "Unexpected kind of literal for var match"; GiveUp) - end - | P_aux (_,(l',_)) -> - (Reporting.print_err l' "Monomorphisation" - "Unexpected kind of pattern for literal"; GiveUp) - in findpat_generic checkpat "literal" assigns cases - | E_vector es when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es -> - let checkpat = function - | P_aux (P_vector ps,_) -> - let matches = List.map2 (fun e p -> - match e, p with - | E_aux (E_lit (L_aux (lit,_)),_), P_aux (P_lit (L_aux (lit',_)),_) -> - if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch - | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var -> - DoesMatch ([var, e],[]) - | _ -> GiveUp) es ps in - let final = List.fold_left (fun acc m -> match acc, m with - | _, GiveUp -> GiveUp - | GiveUp, _ -> GiveUp - | DoesMatch (sub,ksub), DoesMatch(sub',ksub') -> DoesMatch(sub@sub',ksub@ksub') - | _ -> DoesNotMatch) (DoesMatch ([],[])) matches in - (match final with - | GiveUp -> - (Reporting.print_err l "Monomorphisation" - "Unexpected kind of pattern for vector literal"; GiveUp) - | _ -> final) - | _ -> - (Reporting.print_err l "Monomorphisation" - "Unexpected kind of pattern for vector literal"; GiveUp) - in findpat_generic checkpat "vector literal" assigns cases - - | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)) -> - let checkpat = function - | P_aux (P_lit (L_aux (lit_p, _)),_) -> DoesNotMatch - | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) -> - (* For undefined we fix the type-level size (because there's no good - way to construct an undefined size), but leave the term as undefined - to make the meaning clear. *) - let nexp = fabricate_nexp l annot in - let kids = equal_kids (env_of_annot p_id_annot) kid in - let ksubst = KidSet.fold (fun k b -> KBindings.add k nexp b) kids KBindings.empty in - let typ = subst_kids_typ ksubst (typ_of_annot p_id_annot) in - DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))], - KBindings.bindings ksubst) - | P_aux (_,(l',_)) -> - (Reporting.print_err l' "Monomorphisation" - "Unexpected kind of pattern for literal"; GiveUp) - in findpat_generic checkpat "literal" assigns cases - | E_record _ | E_cast (_, E_aux (E_record _, _)) -> - findpat_generic (fun _ -> DoesNotMatch) "record" assigns cases - | _ -> None + in findpat_generic (string_of_exp exp0) assigns cases and can_match exp = let env = Type_check.env_of exp in diff --git a/src/constant_propagation_mutrec.ml b/src/constant_propagation_mutrec.ml index 683cc6f3..285ba45d 100644 --- a/src/constant_propagation_mutrec.ml +++ b/src/constant_propagation_mutrec.ml @@ -125,7 +125,7 @@ let generate_val_spec env id args l annot = mk_typquant in let typschm = mk_typschm tq' typ' in - mk_val_spec (VS_val_spec (typschm, generate_fun_id id args, (fun _ -> None), false)), + mk_val_spec (VS_val_spec (typschm, generate_fun_id id args, [], false)), ksubsts | _, Typ_aux (_, l) -> raise (Reporting.err_unreachable l __POS__ "Function val spec is not a function type") diff --git a/src/elf_loader.ml b/src/elf_loader.ml index d6016c8b..99407393 100644 --- a/src/elf_loader.ml +++ b/src/elf_loader.ml @@ -176,6 +176,24 @@ let load_elf ?writer:(writer=write_sail_lib) name = opt_elf_class := ELF_Class_32 ) +let load_binary ?writer:(writer=write_sail_lib) addr name = + let f = open_in_bin name in + let buf = Buffer.create 1024 in + try + while true do + let char = input_char f in + Buffer.add_char buf char; + done; + assert false + with + | End_of_file -> begin + Bytes.iteri (fun i ch -> writer addr i (int_of_char ch)) (Buffer.to_bytes buf); + close_in f + end + | exc -> + close_in f; + raise exc + (* The sail model can access this by externing a unit -> int function as Elf_loader.elf_entry. *) let elf_entry () = !opt_elf_entry diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem index e0ac09f6..28c0a27e 100644 --- a/src/gen_lib/sail2_prompt_monad.lem +++ b/src/gen_lib/sail2_prompt_monad.lem @@ -170,8 +170,8 @@ let read_mem_bytes rk addr sz = (maybe_fail "nat_of_bv" (nat_of_bv addr)) (fun addr -> Read_mem rk addr (nat_of_int sz) return) -val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e -let read_mem rk addr sz = +val read_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monad 'rv 'b 'e +let read_mem rk addr_sz addr sz = bind (read_mem_bytes rk addr sz) (fun bytes -> @@ -185,15 +185,15 @@ let excl_result () = let k successful = (return successful) in Excl_res k -val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e -let write_mem_ea wk addr sz = +val write_mem_ea : forall 'rv 'a 'e 'addrsize. Bitvector 'a => write_kind -> 'addrsize -> 'a -> integer -> monad 'rv unit 'e +let write_mem_ea wk addr_size addr sz = bind (maybe_fail "nat_of_bv" (nat_of_bv addr)) (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ())) -val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => - write_kind -> 'a -> integer -> 'b -> monad 'rv bool 'e -let write_mem wk addr sz v = +val write_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b => + write_kind -> 'addrsize -> 'a -> integer -> 'b -> monad 'rv bool 'e +let write_mem wk addr_size addr sz v = match (mem_bytes_of_bits v, nat_of_bv addr) with | (Just v, Just addr) -> Write_mem wk addr (nat_of_int sz) v return diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem index 3042700c..8ea919f9 100644 --- a/src/gen_lib/sail2_state_monad.lem +++ b/src/gen_lib/sail2_state_monad.lem @@ -147,8 +147,8 @@ let read_memtS rk a sz = maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val -> returnS (mem_val, tag)))) -val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e -let read_memS rk a sz = +val read_memS : forall 'regs 'e 'a 'b 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monadS 'regs 'b 'e +let read_memS rk addr_size a sz = read_memtS rk a sz >>$= (fun (bytes, _) -> returnS bytes) @@ -186,9 +186,9 @@ let write_memtS wk addr sz v t = | _ -> failS "write_mem" end -val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => - write_kind -> 'a -> integer -> 'b -> monadS 'regs bool 'e -let write_memS wk addr sz v = write_memtS wk addr sz v B0 +val write_memS : forall 'regs 'e 'a 'b 'addrsize. Bitvector 'a, Bitvector 'b => + write_kind -> 'addrsize -> 'a -> integer -> 'b -> monadS 'regs bool 'e +let write_memS wk addr_size addr sz v = write_memtS wk addr sz v B0 val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e let read_regS reg = readS (fun s -> reg.read_from s.regstate) diff --git a/src/initial_check.ml b/src/initial_check.ml index df9af97f..790a6624 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -367,8 +367,8 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) = | P.E_for(id,e1,e2,e3,atyp,e4) -> E_for(to_ast_id id,to_ast_exp ctx e1, to_ast_exp ctx e2, to_ast_exp ctx e3,to_ast_order ctx atyp, to_ast_exp ctx e4) - | P.E_loop (P.While, e1, e2) -> E_loop (While, to_ast_exp ctx e1, to_ast_exp ctx e2) - | P.E_loop (P.Until, e1, e2) -> E_loop (Until, to_ast_exp ctx e1, to_ast_exp ctx e2) + | P.E_loop (P.While, m, e1, e2) -> E_loop (While, to_ast_measure ctx m, to_ast_exp ctx e1, to_ast_exp ctx e2) + | P.E_loop (P.Until, m, e1, e2) -> E_loop (Until, to_ast_measure ctx m, to_ast_exp ctx e1, to_ast_exp ctx e2) | P.E_vector(exps) -> E_vector(List.map (to_ast_exp ctx) exps) | P.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp ctx vexp, to_ast_exp ctx exp) | P.E_vector_subrange(vex,exp1,exp2) -> @@ -414,6 +414,16 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) = | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp") ), (l,())) +and to_ast_measure ctx (P.Measure_aux(m,l)) : unit internal_loop_measure = + let m = match m with + | P.Measure_none -> Measure_none + | P.Measure_some exp -> + if !opt_magic_hash then + Measure_some (to_ast_exp ctx exp) + else + raise (Reporting.err_general l "Internal loop termination measure found without -dmagic_hash") + in Measure_aux (m,l) + and to_ast_lexp ctx (P.E_aux(exp,l) : P.exp) : unit lexp = let lexp = match exp with | P.E_id id -> LEXP_id (to_ast_id id) @@ -762,6 +772,10 @@ let to_ast_prec = function | P.InfixL -> InfixL | P.InfixR -> InfixR +let to_ast_loop_measure ctx = function + | P.Loop (P.While, exp) -> Loop (While, to_ast_exp ctx exp) + | P.Loop (P.Until, exp) -> Loop (Until, to_ast_exp ctx exp) + let to_ast_def ctx def : unit def list ctx_out = match def with | P.DEF_overload (id, ids) -> @@ -800,6 +814,8 @@ let to_ast_def ctx def : unit def list ctx_out = [DEF_scattered sdef], ctx | P.DEF_measure (id, pat, exp) -> [DEF_measure (to_ast_id id, to_ast_pat ctx pat, to_ast_exp ctx exp)], ctx + | P.DEF_loop_measures (id, measures) -> + [DEF_loop_measures (to_ast_id id, List.map (to_ast_loop_measure ctx) measures)], ctx let rec remove_mutrec = function | [] -> [] @@ -856,8 +872,8 @@ let constraint_of_string str = let atyp = Parser.typ_eof Lexer.token (Lexing.from_string str) in to_ast_constraint initial_ctx atyp -let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> Some (string_of_id id)), false)) -let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> None), false)) +let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, [("_", string_of_id id)], false)) +let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, [], false)) let quant_item_param = function | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))] @@ -921,7 +937,7 @@ let generate_undefineds vs_ids (Defs defs) = let undefined_td = function | TD_enum (id, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let typschm = typschm_of_string ("unit -> " ^ string_of_id id ^ " effect {undef}") in - [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false)); + [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, [], false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) (mk_pat (P_lit (mk_lit L_unit))) (if !opt_fast_undefined && List.length ids > 0 then @@ -931,7 +947,7 @@ let generate_undefineds vs_ids (Defs defs) = [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]] | TD_record (id, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in - [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); + [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) pat (mk_exp (E_record (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields)))]] @@ -979,7 +995,7 @@ let generate_undefineds vs_ids (Defs defs) = (mk_exp (E_app (mk_id "internal_pick", [mk_exp (E_list (List.map (make_constr typ_to_var) constr_args))]))) letbinds in - [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); + [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) pat body]] @@ -1015,7 +1031,7 @@ let generate_enum_functions vs_ids (Defs defs) = let rec gen_enums = function | DEF_type (TD_aux (TD_enum (id, elems, _), _)) as enum :: defs -> let enum_val_spec name quants typ = - mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts)) + mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, [], !opt_enum_casts)) in let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) in diff --git a/src/interpreter.ml b/src/interpreter.ml index f01a3846..c1f84ae2 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -52,12 +52,16 @@ open Ast open Ast_util open Value + + type gstate = { registers : value Bindings.t; allow_registers : bool; (* For some uses we want to forbid touching any registers. *) primops : (value list -> value) StringMap.t; letbinds : (Type_check.tannot letbind) list; fundefs : (Type_check.tannot fundef) Bindings.t; + last_write_ea : (value * value * value) option; + typecheck_env : Type_check.Env.t; } type lstate = @@ -91,18 +95,19 @@ let value_of_lit (L_aux (l_aux, _)) = V_real (Rational.add whole frac) | _ -> failwith "could not parse real literal" end - | _ -> failwith "Unimplemented value_of_lit" (* TODO *) + | L_undef -> failwith "value_of_lit of undefined" + let is_value = function | (E_aux (E_internal_value _, _)) -> true | _ -> false let is_true = function - | (E_aux (E_internal_value (V_bool b), _)) -> b == true + | (E_aux (E_internal_value (V_bool b), annot)) -> b | _ -> false let is_false = function - | (E_aux (E_internal_value (V_bool b), _)) -> b == false + | (E_aux (E_internal_value (V_bool b), _)) -> not b | _ -> false let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot))) @@ -127,13 +132,24 @@ type return_value = | Return_ok of value | Return_exception of value +(* when changing effect arms remember to also update effect_request type below *) type 'a response = | Early_return of value | Exception of value | Assertion_failed of string | Call of id * value list * (return_value -> 'a) - | Gets of (state -> 'a) - | Puts of state * (unit -> 'a) + | Fail of string + | Read_mem of (* read_kind : *) value * (* address : *) value * (* length : *) value * (value -> 'a) + | Write_ea of (* write_kind : *) value * (* address : *) value * (* length : *) value * (unit -> 'a) + | Excl_res of (bool -> 'a) + | Write_mem of (* write_kind : *) value * (* address : *) value * (* length : *) value * (* value : *) value * (bool -> 'a) + | Barrier of (* barrier_kind : *) value * (unit -> 'a) + | Read_reg of string * (value -> 'a) + | Write_reg of string * value * (unit -> 'a) + | Get_primop of string * ((value list -> value) -> 'a) + | Get_local of string * (value -> 'a) + | Put_local of string * value * (unit -> 'a) + | Get_global_letbinds of ((Type_check.tannot letbind) list -> 'a) and 'a monad = | Pure of 'a @@ -143,9 +159,19 @@ let map_response f = function | Early_return v -> Early_return v | Exception v -> Exception v | Assertion_failed str -> Assertion_failed str - | Gets g -> Gets (fun s -> f (g s)) - | Puts (s, cont) -> Puts (s, fun () -> f (cont ())) | Call (id, vals, cont) -> Call (id, vals, fun v -> f (cont v)) + | Fail s -> Fail s + | Read_mem (rk, addr, len, cont) -> Read_mem (rk, addr, len, fun v -> f (cont v)) + | Write_ea (wk, addr, len, cont) -> Write_ea (wk, addr, len, fun () -> f (cont ())) + | Excl_res cont -> Excl_res (fun b -> f (cont b)) + | Write_mem (wk, addr, len, v, cont) -> Write_mem (wk, addr, len, v, fun b -> f (cont b)) + | Barrier (bk, cont) -> Barrier (bk, fun () -> f (cont ())) + | Read_reg (name, cont) -> Read_reg (name, fun v -> f (cont v)) + | Write_reg (name, v, cont) -> Write_reg (name, v, fun () -> f (cont ())) + | Get_primop (name, cont) -> Get_primop (name, fun op -> f (cont op)) + | Get_local (name, cont) -> Get_local (name, fun v -> f (cont v)) + | Put_local (name, v, cont) -> Put_local (name, v, fun () -> f (cont ())) + | Get_global_letbinds cont -> Get_global_letbinds (fun lbs -> f (cont lbs)) let rec liftM f = function | Pure x -> Pure (f x) @@ -179,12 +205,43 @@ let throw v = Yield (Exception v) let call (f : id) (args : value list) : return_value monad = Yield (Call (f, args, fun v -> Pure v)) -let gets : state monad = - Yield (Gets (fun s -> Pure s)) -let puts (s : state) : unit monad = - Yield (Puts (s, fun () -> Pure ())) +let read_mem rk addr len : value monad = + Yield (Read_mem (rk, addr, len, (fun v -> Pure v))) + +let write_ea wk addr len : unit monad = + Yield (Write_ea (wk, addr, len, (fun () -> Pure ()))) + +let excl_res () : bool monad = + Yield (Excl_res (fun b -> Pure b)) + +let write_mem wk addr len v : bool monad = + Yield (Write_mem (wk, addr, len, v, fun b -> Pure b)) + +let barrier bk : unit monad = + Yield (Barrier (bk, fun () -> Pure ())) + +let read_reg name : value monad = + Yield (Read_reg (name, fun v -> Pure v)) +let write_reg name v : unit monad = + Yield (Write_reg (name, v, fun () -> Pure ())) + +let fail s = + Yield (Fail s) + +let get_primop name : (value list -> value) monad = + Yield (Get_primop (name, fun op -> Pure op)) + +let get_local name : value monad = + Yield (Get_local (name, fun v -> Pure v)) + +let put_local name v : unit monad = + Yield (Put_local (name, v, fun () -> Pure ())) + +let get_global_letbinds () : (Type_check.tannot letbind) list monad = + Yield (Get_global_letbinds (fun lbs -> Pure lbs)) + let early_return v = Yield (Early_return v) let assertion_failed msg = Yield (Assertion_failed msg) @@ -220,12 +277,11 @@ let rec build_letchain id lbs (E_aux (_, annot) as exp) = let is_interpreter_extern id env = let open Type_check in - Env.is_extern id env "interpreter" || Env.is_extern id env "ocaml" + Env.is_extern id env "interpreter" let get_interpreter_extern id env = let open Type_check in - try Env.get_extern id env "interpreter" with - | Type_error _ -> Env.get_extern id env "ocaml" + Env.get_extern id env "interpreter" let rec step (E_aux (e_aux, annot) as orig_exp) = let wrap e_aux' = return (E_aux (e_aux', annot)) in @@ -236,19 +292,32 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_block (exp :: exps) -> step exp >>= fun exp' -> wrap (E_block (exp' :: exps)) - | E_lit lit -> return (exp_of_value (value_of_lit lit)) + | E_lit (L_aux (L_undef, _)) -> + begin + let env = Type_check.env_of_annot annot in + let typ = Type_check.typ_of_annot annot in + let undef_exp = Ast_util.undefined_of_typ false Parse_ast.Unknown (fun _ -> ()) typ in + let undef_exp = Type_check.check_exp env undef_exp typ in + return undef_exp + end + + | E_lit lit -> + begin + try return (exp_of_value (value_of_lit lit)) + with Failure s -> fail ("Failure: " ^ s) + end | E_if (exp, then_exp, else_exp) when is_true exp -> return then_exp | E_if (exp, then_exp, else_exp) when is_false exp -> return else_exp | E_if (exp, then_exp, else_exp) -> step exp >>= fun exp' -> wrap (E_if (exp', then_exp, else_exp)) - | E_loop (While, exp, body) -> wrap (E_if (exp, E_aux (E_block [body; orig_exp], annot), exp_of_value V_unit)) - | E_loop (Until, exp, body) -> wrap (E_block [body; E_aux (E_if (exp, exp_of_value V_unit, orig_exp), annot)]) + | E_loop (While, _, exp, body) -> wrap (E_if (exp, E_aux (E_block [body; orig_exp], annot), exp_of_value V_unit)) + | E_loop (Until, _, exp, body) -> wrap (E_block [body; E_aux (E_if (exp, exp_of_value V_unit, orig_exp), annot)]) | E_assert (exp, msg) when is_true exp -> wrap unit_exp | E_assert (exp, msg) when is_false exp && is_value msg -> - failwith (coerce_string (value_of_exp msg)) + assertion_failed (coerce_string (value_of_exp msg)) | E_assert (exp, msg) when is_false exp -> step msg >>= fun msg' -> wrap (E_assert (exp, msg')) | E_assert (exp, msg) -> @@ -287,7 +356,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = if matched then return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings)) else - failwith "Match failure" + fail "Match failure" | E_vector_subrange (vec, n, m) -> wrap (E_app (mk_id "vector_subrange_dec", [vec; n; m])) @@ -313,16 +382,50 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | [] when is_interpreter_extern id (env_of_annot annot) -> begin let extern = get_interpreter_extern id (env_of_annot annot) in - if extern = "reg_deref" then - let regname = List.hd evaluated |> value_of_exp |> coerce_ref in - gets >>= fun (_, gstate) -> - if gstate.allow_registers - then return (exp_of_value (Bindings.find (mk_id regname) gstate.registers)) - else raise Not_found - else - gets >>= fun (_, gstate) -> - let primop = try StringMap.find extern gstate.primops with Not_found -> failwith ("No primop " ^ extern) in - return (exp_of_value (primop (List.map value_of_exp evaluated))) + match extern with + | "reg_deref" -> + let regname = List.hd evaluated |> value_of_exp |> coerce_ref in + read_reg regname >>= fun v -> return (exp_of_value v) + | "read_mem" -> + begin match evaluated with + | [rk; addr; len] -> + read_mem (value_of_exp rk) (value_of_exp addr) (value_of_exp len) >>= fun v -> return (exp_of_value v) + | _ -> + fail "Wrong number of parameters to read_mem intrinsic" + end + | "write_mem_ea" -> + begin match evaluated with + | [wk; addr; len] -> + write_ea (value_of_exp wk) (value_of_exp addr) (value_of_exp len) >> wrap unit_exp + | _ -> + fail "Wrong number of parameters to write_ea intrinsic" + end + | "excl_res" -> + begin match evaluated with + | [_] -> + excl_res () >>= fun b -> return (exp_of_value (V_bool b)) + | _ -> + fail "Wrong number of parameters to excl_res intrinsic" + end + | "write_mem" -> + begin match evaluated with + | [wk; addr; len; v] -> + write_mem (value_of_exp wk) (value_of_exp v) (value_of_exp len) (value_of_exp v) >>= fun b -> return (exp_of_value (V_bool b)) + | _ -> + fail "Wrong number of parameters to write_memv intrinsic" + end + | "barrier" -> + begin match evaluated with + | [bk] -> + barrier (value_of_exp bk) >> wrap unit_exp + | _ -> + fail "Wrong number of parameters to barrier intrinsic" + end + | _ -> + get_primop extern >>= + fun op -> try + return (exp_of_value (op (List.map value_of_exp evaluated))) + with _ as exc -> fail ("Exception calling primop '" ^ extern ^ "': " ^ Printexc.to_string exc) end | [] -> call id (List.map value_of_exp evaluated) >>= @@ -352,22 +455,28 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_case (exp, pexps) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_case (exp', pexps)) - | E_case (_, []) -> failwith "Pattern matching failed" + | E_case (_, []) -> fail "Pattern matching failed" | E_case (exp, Pat_aux (Pat_exp (pat, body), _) :: pexps) -> - let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in - if matched then - return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings)) - else - wrap (E_case (exp, pexps)) + begin try + let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in + if matched then + return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings)) + else + wrap (E_case (exp, pexps)) + with Failure s -> fail ("Failure: " ^ s) + end | E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when not (is_value guard) -> - let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in - if matched then - let guard = List.fold_left (fun guard (id, v) -> subst id v guard) guard (Bindings.bindings bindings) in - let body = List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings) in - step guard >>= fun guard' -> - wrap (E_case (exp, Pat_aux (Pat_when (pat, guard', body), pat_annot) :: pexps)) - else - wrap (E_case (exp, pexps)) + begin try + let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in + if matched then + let guard = List.fold_left (fun guard (id, v) -> subst id v guard) guard (Bindings.bindings bindings) in + let body = List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings) in + step guard >>= fun guard' -> + wrap (E_case (exp, Pat_aux (Pat_when (pat, guard', body), pat_annot) :: pexps)) + else + wrap (E_case (exp, pexps)) + with Failure s -> fail ("Failure: " ^ s) + end | E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when is_true guard -> return body | E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when is_false guard -> wrap (E_case (exp, pexps)) @@ -379,35 +488,23 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_exit exp -> step exp >>= fun exp' -> wrap (E_exit exp') | E_ref id -> - gets >>= fun (lstate, gstate) -> - if Bindings.mem id gstate.registers && gstate.allow_registers then - return (exp_of_value (V_ref (string_of_id id))) - else - failwith ("Could not find register " ^ string_of_id id) + return (exp_of_value (V_ref (string_of_id id))) | E_id id -> begin let open Type_check in - gets >>= fun (lstate, gstate) -> match Env.lookup_id id (env_of_annot annot) with - | Register _ when gstate.allow_registers -> - let exp = - try exp_of_value (Bindings.find id gstate.registers) with - | Not_found -> - (* Replace with error message? *) - let exp = mk_exp (E_app (mk_id ("undefined_" ^ string_of_typ (typ_of orig_exp)), [mk_exp (E_lit (mk_lit (L_unit)))])) in - Type_check.check_exp (env_of_annot annot) exp (typ_of orig_exp) - in - return exp - | Register _ when not gstate.allow_registers -> - return (exp_of_value (V_attempted_read (string_of_id id))) - | Local (Mutable, _) -> return (local_variable id lstate gstate) + | Register _ -> + read_reg (string_of_id id) >>= fun v -> return (exp_of_value v) + | Local (Mutable, _) -> get_local (string_of_id id) >>= fun v -> return (exp_of_value v) | Local (Immutable, _) -> - let chain = build_letchain id gstate.letbinds orig_exp in + (* if we get here without already having substituted, it must be a top-level letbind *) + get_global_letbinds () >>= fun lbs -> + let chain = build_letchain id lbs orig_exp in return chain | Enum _ -> return (exp_of_value (V_ctor (string_of_id id, []))) - | _ -> failwith ("Couldn't find id " ^ string_of_id id) + | _ -> fail ("Couldn't find id " ^ string_of_id id) end | E_record fexps -> @@ -456,45 +553,51 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_assign (lexp, exp) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_assign (lexp, exp')) | E_assign (LEXP_aux (LEXP_memory (id, args), _), exp) -> wrap (E_app (id, args @ [exp])) | E_assign (LEXP_aux (LEXP_field (lexp, id), ul), exp) -> - let open Type_check in - let lexp_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp lexp)) in - let exp' = E_aux (E_record_update (lexp_exp, [FE_aux (FE_Fexp (id, exp), ul)]), ul) in - wrap (E_assign (lexp, exp')) + begin try + let open Type_check in + let lexp_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp lexp)) in + let exp' = E_aux (E_record_update (lexp_exp, [FE_aux (FE_Fexp (id, exp), ul)]), ul) in + wrap (E_assign (lexp, exp')) + with Failure s -> fail ("Failure: " ^ s) + end | E_assign (LEXP_aux (LEXP_vector (vec, n), lexp_annot), exp) -> - let open Type_check in - let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in - let exp' = E_aux (E_vector_update (vec_exp, n, exp), lexp_annot) in - wrap (E_assign (vec, exp')) + begin try + let open Type_check in + let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in + let exp' = E_aux (E_vector_update (vec_exp, n, exp), lexp_annot) in + wrap (E_assign (vec, exp')) + with Failure s -> fail ("Failure: " ^ s) + end | E_assign (LEXP_aux (LEXP_vector_range (vec, n, m), lexp_annot), exp) -> - let open Type_check in - let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in - (* FIXME: let the type checker check this *) - let exp' = E_aux (E_vector_update_subrange (vec_exp, n, m, exp), lexp_annot) in - wrap (E_assign (vec, exp')) + begin try + let open Type_check in + let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in + (* FIXME: let the type checker check this *) + let exp' = E_aux (E_vector_update_subrange (vec_exp, n, m, exp), lexp_annot) in + wrap (E_assign (vec, exp')) + with Failure s -> fail ("Failure: " ^ s) + end | E_assign (LEXP_aux (LEXP_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) -> begin let open Type_check in - gets >>= fun (lstate, gstate) -> + let name = string_of_id id in match Env.lookup_id id (env_of_annot annot) with - | Register _ when gstate.allow_registers -> - puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp + | Register _ -> + write_reg name (value_of_exp exp) >> wrap unit_exp | Local (Mutable, _) | Unbound -> - begin - puts ({ locals = Bindings.add id (value_of_exp exp) lstate.locals }, gstate) >> wrap unit_exp - end - | _ -> failwith "Assign" + put_local name (value_of_exp exp) >> wrap unit_exp + | Local (Immutable, _) -> + fail ("Assignment to immutable local: " ^ name) + | Enum _ -> + fail ("Assignment to union constructor: " ^ name) end | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) when not (is_value reference) -> step reference >>= fun reference' -> wrap (E_assign (LEXP_aux (LEXP_deref reference', annot), exp)) | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) -> let name = coerce_ref (value_of_exp reference) in - gets >>= fun (lstate, gstate) -> - if Bindings.mem (mk_id name) gstate.registers && gstate.allow_registers then - puts (lstate, { gstate with registers = Bindings.add (mk_id name) (value_of_exp exp) gstate.registers }) >> wrap unit_exp - else - failwith "Assign to nonexistent register" - | 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" + write_reg name (value_of_exp exp) >> wrap unit_exp + | E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> fail "Tuple assignment" + | E_assign (LEXP_aux (LEXP_vector_concat lexps, annot), exp) -> fail "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)) @@ -528,7 +631,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = wrap (E_block [subst id v_from body; E_aux (E_for (id, exp_of_value (value_sub_int [v_from; v_step]), exp_to, exp_step, ord, body), annot)]) | _ -> assert false end - | Ord_aux (Ord_var _, _) -> failwith "Polymorphic order in foreach" + | Ord_aux (Ord_var _, _) -> fail "Polymorphic order in foreach" end | E_for (id, exp_from, exp_to, exp_step, ord, body) when is_value exp_to && is_value exp_step -> step exp_from >>= fun exp_from' -> wrap (E_for (id, exp_from', exp_to, exp_step, ord, body)) @@ -537,9 +640,23 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_for (id, exp_from, exp_to, exp_step, ord, body) -> step exp_step >>= fun exp_step' -> wrap (E_for (id, exp_from, exp_to, exp_step', ord, body)) - | E_sizeof _ | E_constraint _ -> assert false (* Must be re-written before interpreting *) + | E_sizeof nexp -> + begin + match Type_check.big_int_of_nexp nexp with + | Some n -> return (exp_of_value (V_int n)) + | None -> fail "Sizeof unevaluable nexp" + end - | _ -> failwith ("Unimplemented " ^ string_of_exp orig_exp) + | E_cons (hd, tl) when is_value hd && is_value tl -> + let hd = value_of_exp hd in + let tl = coerce_listlike (value_of_exp tl) in + return (exp_of_value (V_list (hd :: tl))) + | E_cons (hd, tl) when is_value hd -> + step tl >>= fun tl' -> wrap (E_cons (hd, tl')) + | E_cons (hd, tl) -> + step hd >>= fun hd' -> wrap (E_cons (hd', tl)) + + | _ -> raise (Invalid_argument ("Unimplemented " ^ string_of_exp orig_exp)) and combine _ v1 v2 = match (v1, v2) with @@ -651,66 +768,197 @@ type frame = | Done of state * value | Step of string Lazy.t * state * (Type_check.tannot exp) monad * (string Lazy.t * lstate * (return_value -> (Type_check.tannot exp) monad)) list | Break of frame + | Effect_request of string Lazy.t * state * (string Lazy.t * lstate * (return_value -> (Type_check.tannot exp) monad)) list * effect_request + | Fail of string Lazy.t * state * (Type_check.tannot exp) monad * (string Lazy.t * lstate * (return_value -> (Type_check.tannot exp) monad)) list * string + +(* when changing effect_request remember to also update response type above *) +and effect_request = + | Read_mem of (* read_kind : *) value * (* address : *) value * (* length : *) value * (value -> state -> frame) + | Write_ea of (* write_kind : *) value * (* address : *) value * (* length : *) value * (unit -> state -> frame) + | Excl_res of (bool -> state -> frame) + | Write_mem of (* write_kind : *) value * (* address : *) value * (* length : *) value * (* value : *) value * (bool -> state -> frame) + | Barrier of (* barrier_kind : *) value * (unit -> state -> frame) + | Read_reg of string * (value -> state -> frame) + | Write_reg of string * value * (unit -> state -> frame) let rec eval_frame' = function | Done (state, v) -> Done (state, v) + | Fail (out, state, m, stack, msg) -> Fail (out, state, m, stack, msg) | Break frame -> Break frame + | Effect_request (out, state, stack, eff) -> Effect_request (out, state, stack, eff) | Step (out, state, m, stack) -> + let lstate, gstate = state in match (m, stack) with | Pure v, [] when is_value v -> Done (state, value_of_exp v) | Pure v, (head :: stack') when is_value v -> - Step (stack_string head, (stack_state head, snd state), stack_cont head (Return_ok (value_of_exp v)), stack') + Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_ok (value_of_exp v)), stack') | Pure exp', _ -> let out' = lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp')) in Step (out', state, step exp', stack) | Yield (Call(id, vals, cont)), _ when string_of_id id = "break" -> - let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in - let body = exp_of_fundef (Bindings.find id (snd state).fundefs) arg in - Break (Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack)) + begin + let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in + try + let body = exp_of_fundef (Bindings.find id gstate.fundefs) arg in + Break (Step (lazy "", (initial_lstate, gstate), return body, (out, lstate, cont) :: stack)) + with Not_found -> + Step (out, state, fail ("Fundef not found: " ^ string_of_id id), stack) + end | Yield (Call(id, vals, cont)), _ -> - let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in - let body = exp_of_fundef (Bindings.find id (snd state).fundefs) arg in - Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack) - | Yield (Gets cont), _ -> - eval_frame' (Step (out, state, cont state, stack)) - | Yield (Puts (state', cont)), _ -> + begin + let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in + try + let body = exp_of_fundef (Bindings.find id gstate.fundefs) arg in + Step (lazy "", (initial_lstate, gstate), return body, (out, lstate, cont) :: stack) + with Not_found -> + Step (out, state, fail ("Fundef not found: " ^ string_of_id id), stack) + end + + | Yield (Read_reg (name, cont)), _ -> + Effect_request (out, state, stack, Read_reg (name, fun v state' -> eval_frame' (Step (out, state', cont v, stack)))) + | Yield (Write_reg (name, v, cont)), _ -> + Effect_request (out, state, stack, Write_reg (name, v, fun () state' -> eval_frame' (Step (out, state', cont (), stack)))) + | Yield (Get_primop (name, cont)), _ -> + begin + try + let op = StringMap.find name gstate.primops in + eval_frame' (Step (out, state, cont op, stack)) + with Not_found -> + eval_frame' (Step (out, state, fail ("No such primop: " ^ name), stack)) + end + | Yield (Get_local (name, cont)), _ -> + begin + try + eval_frame' (Step (out, state, cont (Bindings.find (mk_id name) lstate.locals), stack)) + with Not_found -> + eval_frame' (Step (out, state, fail ("Local not found: " ^ name), stack)) + end + | Yield (Put_local (name, v, cont)), _ -> + let state' = ({ locals = Bindings.add (mk_id name) v lstate.locals }, gstate) in eval_frame' (Step (out, state', cont (), stack)) + | Yield (Get_global_letbinds cont), _ -> + eval_frame' (Step (out, state, cont gstate.letbinds, stack)) + | Yield (Read_mem (rk, addr, len, cont)), _ -> + Effect_request (out, state, stack, Read_mem (rk, addr, len, fun result state' -> eval_frame' (Step (out, state', cont result, stack)))) + | Yield (Write_ea (wk, addr, len, cont)), _ -> + Effect_request (out, state, stack, Write_ea (wk, addr, len, fun () state' -> eval_frame' (Step (out, state', cont (), stack)))) + | Yield (Excl_res cont), _ -> + Effect_request (out, state, stack, Excl_res (fun b state' -> eval_frame' (Step (out, state', cont b, stack)))) + | Yield (Write_mem (wk, addr, len, v, cont)), _ -> + Effect_request (out, state, stack, Write_mem (wk, addr, len, v, fun b state' -> eval_frame' (Step (out, state', cont b, stack)))) + | Yield (Barrier (bk, cont)), _ -> + Effect_request (out, state, stack, Barrier (bk, fun () state' -> eval_frame' (Step (out, state', cont (), stack)))) | Yield (Early_return v), [] -> Done (state, v) | Yield (Early_return v), (head :: stack') -> - Step (stack_string head, (stack_state head, snd state), stack_cont head (Return_ok v), stack') - | Yield (Assertion_failed msg), _ -> - failwith msg + Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_ok v), stack') + | Yield (Assertion_failed msg), _ | Yield (Fail msg), _ -> + Fail (out, state, m, stack, msg) | Yield (Exception v), [] -> - failwith ("Uncaught Exception" |> Util.cyan |> Util.clear) + Fail (out, state, m, stack, "Uncaught exception: " ^ string_of_value v) | Yield (Exception v), (head :: stack') -> - Step (stack_string head, (stack_state head, snd state), stack_cont head (Return_exception v), stack') + Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_exception v), stack') let eval_frame frame = try eval_frame' frame with | Type_check.Type_error (env, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) +let default_effect_interp state eff = + let lstate, gstate = state in + match eff with + | Read_mem (rk, addr, len, cont) -> + (* all read-kinds treated the same in single-threaded interpreter *) + let addr' = coerce_bv addr in + let len' = coerce_int len in + let result = mk_vector (Sail_lib.read_ram (List.length addr', len', [], addr')) in + cont result state + | Write_ea (wk, addr, len, cont) -> + (* just store the values for the next Write_memv *) + let state' = (lstate, { gstate with last_write_ea = Some (wk, addr, len) }) in + cont () state' + | Excl_res cont -> + (* always succeeds in single-threaded interpreter *) + cont true state + | Write_mem (wk, addr, len, v, cont) -> + begin + match gstate.last_write_ea with + | Some (wk', addr', len') -> + let state' = (lstate, { gstate with last_write_ea = None }) in + (* all write-kinds treated the same in single-threaded interpreter *) + let addr' = coerce_bv addr in + let len' = coerce_int len in + let v' = coerce_bv v in + if Big_int.mul len' (Big_int.of_int 8) = Big_int.of_int (List.length v') then + let b = Sail_lib.write_ram (List.length addr', len', [], addr', v') in + cont b state + else + failwith "Write_memv with length mismatch to preceding Write_ea" + | None -> + failwith "Write_memv without preceding Write_ea" + end + | Barrier (bk, cont) -> + (* no-op in single-threaded interpreter *) + cont () state + | Read_reg (name, cont) -> + begin + if gstate.allow_registers then + try + cont (Bindings.find (mk_id name) gstate.registers) state + with Not_found -> + failwith ("Read of nonexistent register: " ^ name) + else + failwith ("Register read disallowed by allow_registers setting: " ^ name) + end + | Write_reg (name, v, cont) -> + begin + let id = mk_id name in + if gstate.allow_registers then + if Bindings.mem id gstate.registers then + let state' = (lstate, { gstate with registers = Bindings.add id v gstate.registers }) in + cont () state' + else + failwith ("Write of nonexistent register: " ^ name) + else + failwith ("Register write disallowed by allow_registers setting: " ^ name) + end + + + + let rec run_frame frame = match frame with | Done (state, v) -> v + | Fail (_, _, _, _, msg) -> failwith ("run_frame got Fail: " ^ msg) | Step (lazy_str, _, _, _) -> run_frame (eval_frame frame) | Break frame -> run_frame (eval_frame frame) + | Effect_request (out, state, stack, eff) -> + run_frame (default_effect_interp state eff) let eval_exp state exp = run_frame (Step (lazy "", state, return exp, [])) -let initial_gstate primops ast = +let initial_gstate primops ast env = { registers = Bindings.empty; allow_registers = true; primops = primops; letbinds = ast_letbinds ast; fundefs = Bindings.empty; + last_write_ea = None; + typecheck_env = env; } let rec initialize_registers gstate = let process_def = function + | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), annot)) -> + begin + let env = Type_check.env_of_annot annot in + let typ = Type_check.Env.expand_synonyms env typ in + let exp = mk_exp (E_cast (typ, mk_exp (E_lit (mk_lit (L_undef))))) in + let exp = Type_check.check_exp env exp typ in + { gstate with registers = Bindings.add id (eval_exp (initial_lstate, gstate) exp) gstate.registers } + end | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> { gstate with registers = Bindings.add id (eval_exp (initial_lstate, gstate) exp) gstate.registers } | DEF_fundef fdef -> @@ -722,4 +970,44 @@ let rec initialize_registers gstate = initialize_registers (process_def def) (Defs defs) | Defs [] -> gstate -let initial_state ast primops = initial_lstate, initialize_registers (initial_gstate primops ast) ast +let initial_state ast env primops = initial_lstate, initialize_registers (initial_gstate primops ast env) ast + +type value_result = + | Value_success of value + | Value_error of exn + +let decode_instruction state bv = + try + let env = (snd state).typecheck_env in + let untyped = mk_exp (E_app ((mk_id "decode"), [mk_exp (E_vector (List.map mk_lit_exp bv))])) in + let typed = Type_check.check_exp + env untyped (app_typ (mk_id "option") + [A_aux (A_typ (mk_typ (Typ_id (mk_id "ast"))), Parse_ast.Unknown)]) in + let evaled = eval_exp state typed in + match evaled with + | V_ctor ("Some", [v]) -> Value_success v + | V_ctor ("None", _) -> failwith "decode returned None" + | _ -> failwith "decode returned wrong value type" + with _ as exn -> + Value_error exn + +let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, Type_check.mk_tannot env typ effect)) +let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect +let id_typ id = mk_typ (Typ_id (mk_id id)) + +let analyse_instruction state ast = + let env = (snd state).typecheck_env in + let unk = Parse_ast.Unknown in + let typed = annot_exp + (E_app (mk_id "initial_analysis", [annot_exp (E_internal_value ast) unk env (id_typ "ast")])) unk env + (tuple_typ [id_typ "regfps"; id_typ "regfps"; id_typ "regfps"; id_typ "niafps"; id_typ "diafp"; id_typ "instruction_kind"]) + in + Step (lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp typed)), state, return typed, []) + +let execute_instruction state ast = + let env = (snd state).typecheck_env in + let unk = Parse_ast.Unknown in + let typed = annot_exp + (E_app (mk_id "execute", [annot_exp (E_internal_value ast) unk env (id_typ "ast")])) unk env unit_typ + in + Step (lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp typed)), state, return typed, []) diff --git a/src/isail.ml b/src/isail.ml index cce56fb0..094ad3df 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -108,7 +108,7 @@ let sail_logo = let vs_ids = ref (val_spec_ids !Interactive.ast) -let interactive_state = ref (initial_state !Interactive.ast Value.primops) +let interactive_state = ref (initial_state !Interactive.ast !Interactive.env Value.primops) let interactive_bytecode = ref [] @@ -117,7 +117,9 @@ let sep = "-----------------------------------------------------" |> Util.blue | let print_program () = match !current_mode with | Normal | Emacs -> () - | Evaluation (Step (out, _, _, stack)) -> + | Evaluation (Step (out, _, _, stack)) + | Evaluation (Effect_request(out, _, stack, _)) + | Evaluation (Fail (out, _, _, stack, _)) -> List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline (Lazy.force code); print_endline sep); print_endline (Lazy.force out) | Evaluation (Done (_, v)) -> @@ -134,6 +136,9 @@ let rec run () = interactive_state := state; print_endline ("Result = " ^ Value.string_of_value v); current_mode := Normal + | Fail (_, _, _, _, msg) -> + print_endline ("Error: " ^ msg); + current_mode := Normal | Step (out, state, _, stack) -> begin try @@ -145,6 +150,14 @@ let rec run () = | Break frame -> print_endline "Breakpoint"; current_mode := Evaluation frame + | Effect_request (out, state, stack, eff) -> + begin + try + current_mode := Evaluation (Interpreter.default_effect_interp state eff) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run () end let rec run_steps n = @@ -158,6 +171,9 @@ let rec run_steps n = interactive_state := state; print_endline ("Result = " ^ Value.string_of_value v); current_mode := Normal + | Fail (_, _, _, _, msg) -> + print_endline ("Error: " ^ msg); + current_mode := Normal | Step (out, state, _, stack) -> begin try @@ -169,6 +185,14 @@ let rec run_steps n = | Break frame -> print_endline "Breakpoint"; current_mode := Evaluation frame + | Effect_request (out, state, stack, eff) -> + begin + try + current_mode := Evaluation (Interpreter.default_effect_interp state eff) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run_steps (n - 1) end let help = @@ -208,7 +232,9 @@ let help = (color yellow "<command>") (color green ":help :type") | ":elf" -> sprintf ":elf %s - Load an ELF file." - (color yellow "<file>") + (color yellow "<file>") + | ":bin" -> + ":bin <address> <file> - Load a binary file at the given address." | ":r" | ":run" -> "(:r | :run) - Completely evaluate the currently evaluating expression." | ":s" | ":step" -> @@ -402,7 +428,7 @@ let handle_input' input = let ast, env = Specialize.(specialize' 1 int_specialization !Interactive.ast !Interactive.env) in Interactive.ast := ast; Interactive.env := env; - interactive_state := initial_state !Interactive.ast Value.primops + interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops | ":pretty" -> print_endline (Pretty_print_sail.to_string (Latex.defs !Interactive.ast)) | ":ir" -> @@ -441,13 +467,23 @@ let handle_input' input = let files = Util.split_on_char ' ' arg in let (_, ast, env) = load_files !Interactive.env files in Interactive.ast := append_ast !Interactive.ast ast; - interactive_state := initial_state !Interactive.ast Value.primops; + interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops; Interactive.env := env; vs_ids := val_spec_ids !Interactive.ast + | ":bin" -> + begin + let args = Util.split_on_char ' ' arg in + match args with + | [addr_s; filename] -> + let addr = Big_int.of_string addr_s in + Elf_loader.load_binary addr filename + | _ -> + print_endline "Invalid argument for :bin, expected <addr> <filename>" + end | ":u" | ":unload" -> Interactive.ast := Ast.Defs []; Interactive.env := Type_check.initial_env; - interactive_state := initial_state !Interactive.ast Value.primops; + interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops; vs_ids := val_spec_ids !Interactive.ast; (* See initial_check.mli for an explanation of why we need this. *) Initial_check.have_undefined_builtins := false; @@ -469,7 +505,7 @@ let handle_input' input = let ast, env = Type_check.check !Interactive.env (Defs [DEF_val (mk_letbind (mk_pat (P_id (mk_id v))) exp)]) in Interactive.ast := append_ast !Interactive.ast ast; Interactive.env := env; - interactive_state := initial_state !Interactive.ast Value.primops; + interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops; | _ -> print_endline "Invalid arguments for :let" end | ":def" -> @@ -477,7 +513,7 @@ let handle_input' input = let ast, env = Type_check.check !Interactive.env ast in Interactive.ast := append_ast !Interactive.ast ast; Interactive.env := env; - interactive_state := initial_state !Interactive.ast Value.primops; + interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops; | ":graph" -> let format = if arg = "" then "svg" else arg in let dotfile, out_chan = Filename.open_temp_file "sail_graph_" ".gz" in @@ -538,17 +574,17 @@ let handle_input' input = end | ":rewrites" -> Interactive.ast := Process_file.rewrite_ast_target arg !Interactive.env !Interactive.ast; - interactive_state := initial_state !Interactive.ast Value.primops + interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops | ":prover_regstate" -> let env, ast = prover_regstate (Some arg) !Interactive.ast !Interactive.env in Interactive.env := env; Interactive.ast := ast; - interactive_state := initial_state !Interactive.ast Value.primops + interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops | ":recheck" -> let ast, env = Type_check.check Type_check.initial_env !Interactive.ast in Interactive.env := env; Interactive.ast := ast; - interactive_state := initial_state !Interactive.ast Value.primops; + interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops; vs_ids := val_spec_ids !Interactive.ast | ":compile" -> let out_name = match !opt_file_out with @@ -577,7 +613,7 @@ let handle_input' input = load_into_session arg; let (_, ast, env) = load_files ~check:true !Interactive.env [arg] in Interactive.ast := append_ast !Interactive.ast ast; - interactive_state := initial_state !Interactive.ast Value.primops; + interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops; Interactive.env := env; vs_ids := val_spec_ids !Interactive.ast; print_endline ("(message \"Checked " ^ arg ^ " done\")\n"); @@ -588,7 +624,7 @@ let handle_input' input = | ":unload" -> Interactive.ast := Ast.Defs []; Interactive.env := Type_check.initial_env; - interactive_state := initial_state !Interactive.ast Value.primops; + interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops; vs_ids := val_spec_ids !Interactive.ast; Initial_check.have_undefined_builtins := false; Process_file.clear_symbols () @@ -644,6 +680,9 @@ let handle_input' input = interactive_state := state; print_endline ("Result = " ^ Value.string_of_value v); current_mode := Normal + | Fail (_, _, _, _, msg) -> + print_endline ("Error: " ^ msg); + current_mode := Normal | Step (out, state, _, stack) -> begin try @@ -656,6 +695,15 @@ let handle_input' input = | Break frame -> print_endline "Breakpoint"; current_mode := Evaluation frame + | Effect_request (out, state, stack, eff) -> + begin + try + interactive_state := state; + current_mode := Evaluation (Interpreter.default_effect_interp state eff); + print_program () + with + | Failure str -> print_endline str; current_mode := Normal + end end end diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 787d5b17..bd4813ed 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -578,7 +578,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = raise (Reporting.err_unreachable l __POS__ ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF")) - | E_loop (loop_typ, cond, exp) -> + | E_loop (loop_typ, _, cond, exp) -> let acond = anf cond in let aexp = anf exp in mk_aexp (AE_loop (loop_typ, acond, aexp)) diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index fbc97f85..40bb0456 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -281,8 +281,18 @@ let rec compile_aval l ctx = function V_id (gs, ctyp), [iclear ctyp gs] - | AV_vector ([], _) -> - raise (Reporting.err_general l "Encountered empty vector literal") + | AV_vector ([], typ) -> + let vector_ctyp = ctyp_of_typ ctx typ in + begin match ctyp_of_typ ctx typ with + | CT_fbits (0, ord) -> + [], V_lit (VL_bits ([], ord), vector_ctyp), [] + | _ -> + let gs = ngensym () in + [idecl vector_ctyp gs; + iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [V_lit (VL_int Big_int.zero, CT_fint 64)]], + V_id (gs, vector_ctyp), + [iclear vector_ctyp gs] + end (* Convert a small bitvector to a uint64_t literal. *) | AV_vector (avals, typ) when is_bitvector avals && (List.length avals <= 64 || ctx.ignore_64) -> @@ -1309,7 +1319,8 @@ and compile_def' n total ctx = function (* Termination measures only needed for Coq, and other theorem prover output *) | DEF_measure _ -> [], ctx - + | DEF_loop_measures _ -> [], ctx + | DEF_internal_mutrec fundefs -> let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def n total ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs diff --git a/src/libsail.mllib b/src/libsail.mllib new file mode 100644 index 00000000..1a992391 --- /dev/null +++ b/src/libsail.mllib @@ -0,0 +1,58 @@ +Anf +Ast +Ast_util +Bitfield +C_backend +Cgen_backend +Constant_fold +Constraint +Elf_loader +Error_format +Graph +Initial_check +Interactive +Interpreter +Isail +Jib +Jib_compile +Jib_optimize +Jib_ssa +Jib_util +Latex +Lexer +Manifest +Monomorphise +Nl_flow +Ocaml_backend +Optimize +Parse_ast +Parser +Pattern_completeness +PPrint +PPrintCombinators +PPrintEngine +PPrintRenderer +PPrintOCaml +Pretty_print +Pretty_print_common +Pretty_print_coq +Pretty_print_lem +Pretty_print_sail +Process_file +Profile +Reporting +Rewriter +Rewrites +Sail +Sail2_values +Sail_lib +Scattered +Spec_analysis +Specialize +State +ToFromInterp_backend +ToFromInterp_lib +Type_check +Type_error +Util +Value diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4d7119d7..0c63e020 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -165,11 +165,13 @@ let rec split_insts = function | (k,None)::t -> let l1,l2 = split_insts t in l1,k::l2 | (k,Some v)::t -> let l1,l2 = split_insts t in (k,v)::l1,l2 -let apply_kid_insts kid_insts t = +let apply_kid_insts kid_insts nc t = let kid_insts, kids' = split_insts kid_insts in - let kid_insts = List.map (fun (v,i) -> (v,Nexp_aux (Nexp_constant i,Generated Unknown))) kid_insts in + let kid_insts = List.map + (fun (v,i) -> (kopt_kid v,Nexp_aux (Nexp_constant i,Generated Unknown))) + kid_insts in let subst = kbindings_from_list kid_insts in - kids', subst_kids_typ subst t + kids', subst_kids_nc subst nc, subst_kids_typ subst t let rec inst_src_type insts (Typ_aux (ty,l) as typ) = match ty with @@ -193,14 +195,11 @@ let rec inst_src_type insts (Typ_aux (ty,l) as typ) = args (insts,[]) in insts, Typ_aux (Typ_app (id,ts),l) | Typ_exist (kopts, nc, t) -> begin - (* TODO handle non-integer existentials *) - let kids = List.map kopt_kid kopts in - let kid_insts, insts' = peel (kids,insts) in - let kids', t' = apply_kid_insts kid_insts t in - (* TODO: subst in nc *) - match kids' with + let kid_insts, insts' = peel (kopts,insts) in + let kopts', nc', t' = apply_kid_insts kid_insts nc t in + match kopts' with | [] -> insts', t' - | _ -> insts', Typ_aux (Typ_exist (List.map (mk_kopt K_int) kids', nc, t'), l) + | _ -> insts', Typ_aux (Typ_exist (kopts', nc', t'), l) end | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" and inst_src_typ_arg insts (A_aux (ta,l) as tyarg) = @@ -249,19 +248,31 @@ let rec size_nvars_nexp (Nexp_aux (ne,_)) = (* Given a type for a constructor, work out which refinements we ought to produce *) (* TODO collision avoidance *) -let split_src_type id ty (TypQ_aux (q,ql)) = +let split_src_type all_errors env id ty (TypQ_aux (q,ql)) = + let cannot l msg default = + let open Reporting in + let error = Err_general (l, msg) in + match all_errors with + | None -> raise (Fatal_error error) + | Some flag -> begin + flag := false; + print_error error; + default + end + in let i = string_of_id id in (* This was originally written for the general case, but I cut it down to the more manageable prenex-form below *) - let rec size_nvars_ty (Typ_aux (ty,l) as typ) = + let rec size_nvars_ty typ = + let Typ_aux (ty,l) = Env.expand_synonyms env typ in match ty with | Typ_id _ | Typ_var _ -> (KidSet.empty,[[],typ]) | Typ_fn _ -> - raise (Reporting.err_general l ("Function type in constructor " ^ i)) + cannot l ("Function type in constructor " ^ i) (KidSet.empty,[[],typ]) | Typ_bidir _ -> - raise (Reporting.err_general l ("Mapping type in constructor " ^ i)) + cannot l ("Mapping type in constructor " ^ i) (KidSet.empty,[[],typ]) | Typ_tup ts -> let (vars,tys) = List.split (List.map size_nvars_ty ts) in let insttys = List.map (fun x -> let (insts,tys) = List.split x in @@ -275,54 +286,41 @@ let split_src_type id ty (TypQ_aux (q,ql)) = (KidSet.empty,[[],typ]) (* We only support sizes for bitvectors mentioned explicitly, not any buried inside another type *) | Typ_exist (kopts, nc, t) -> - (* TODO handle non integer existentials *) - let kids = List.map kopt_kid kopts in let (vars,tys) = size_nvars_ty t in let find_insts k (insts,nc) = let inst,nc' = - if KidSet.mem k vars then - let is,nc' = extract_set_nc l k nc in + if KidSet.mem (kopt_kid k) vars then + let is,nc' = extract_set_nc l (kopt_kid k) nc in Some is,nc' else None,nc in (k,inst)::insts,nc' in - let (insts,nc') = List.fold_right find_insts kids ([],nc) in + let (insts,nc') = List.fold_right find_insts kopts ([],nc) in let insts = cross'' insts in let ty_and_inst (inst0,ty) inst = - let kids, ty = apply_kid_insts inst ty in + let kopts, nc', ty = apply_kid_insts inst nc' ty in let ty = (* Typ_exist is not allowed an empty list of kids *) - match kids with + match kopts with | [] -> ty - | _ -> Typ_aux (Typ_exist (List.map (mk_kopt K_int) kids, nc', ty),l) + | _ -> Typ_aux (Typ_exist (kopts, nc', ty),l) in inst@inst0, ty in let tys = List.concat (List.map (fun instty -> List.map (ty_and_inst instty) insts) tys) in - let free = List.fold_left (fun vars k -> KidSet.remove k vars) vars kids in + let free = List.fold_left (fun vars k -> KidSet.remove (kopt_kid k) vars) vars kopts in (free,tys) | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" in - (* Only single-variable prenex-form for now *) let size_nvars_ty (Typ_aux (ty,l) as typ) = match ty with | Typ_exist (kids,_,t) -> begin match snd (size_nvars_ty typ) with | [] -> [] + | [[],_] -> [] | tys -> - (* One level of tuple type is stripped off by the type checker, so - add another here *) - let tys = - List.map (fun (x,ty) -> - x, match ty with - | Typ_aux (Typ_tup _,_) -> Typ_aux (Typ_tup [ty],Unknown) - | _ -> ty) tys in if contains_exist t then - raise (Reporting.err_general l - "Only prenex types in unions are supported by monomorphisation") - else if List.length kids > 1 then - raise (Reporting.err_general l - "Only single-variable existential types in unions are currently supported by monomorphisation") + cannot l "Only prenex types in unions are supported by monomorphisation" [] else tys end | _ -> [] @@ -331,19 +329,19 @@ let split_src_type id ty (TypQ_aux (q,ql)) = let variants = size_nvars_ty ty in match variants with | [] -> None - | sample::__ -> - let () = if List.length variants > size_set_limit then - raise (Reporting.err_general ql - (string_of_int (List.length variants) ^ "variants for constructor " ^ i ^ - "bigger than limit " ^ string_of_int size_set_limit)) else () - in + | sample::_ -> + if List.length variants > size_set_limit then + cannot ql + (string_of_int (List.length variants) ^ "variants for constructor " ^ i ^ + "bigger than limit " ^ string_of_int size_set_limit) None + else let wrap = match id with | Id_aux (Id i,l) -> (fun f -> Id_aux (Id (f i),Generated l)) | Id_aux (Operator i,l) -> (fun f -> Id_aux (Operator (f i),l)) in let name_seg = function | (_,None) -> "" - | (k,Some i) -> string_of_kid k ^ Big_int.to_string i + | (k,Some i) -> string_of_kid (kopt_kid k) ^ Big_int.to_string i in let name l i = String.concat "_" (i::(List.map name_seg l)) in Some (List.map (fun (l,ty) -> (l, wrap (name l),ty)) variants) @@ -385,7 +383,7 @@ let typ_of_args args = let refine_constructor refinements l env id args = match List.find (fun (id',_) -> Id.compare id id' = 0) refinements with | (_,irefinements) -> begin - let (_,constr_ty) = Env.get_val_spec id env in + let (_,constr_ty) = Env.get_union_id id env in match constr_ty with (* A constructor should always have a single argument. *) | Typ_aux (Typ_fn ([constr_ty],_,_),_) -> begin @@ -393,11 +391,9 @@ let refine_constructor refinements l env id args = match Type_check.destruct_exist (Type_check.Env.expand_synonyms env constr_ty) with | None -> None | Some (kopts,nc,constr_ty) -> - (* TODO: Handle non-integer existentials *) - let kids = List.map kopt_kid kopts in let bindings = Type_check.unify l env (tyvars_of_typ constr_ty) constr_ty arg_ty in - let find_kid kid = try Some (KBindings.find kid bindings) with Not_found -> None in - let bindings = List.map find_kid kids in + let find_kopt kopt = try Some (KBindings.find (kopt_kid kopt) bindings) with Not_found -> None in + let bindings = List.map find_kopt kopts in let matches_refinement (mapping,_,_) = List.for_all2 (fun v (_,w) -> @@ -614,11 +610,12 @@ let apply_pat_choices choices = e_assert = rewrite_assert; e_case = rewrite_case } -let split_defs all_errors splits defs = +let split_defs all_errors splits env defs = let no_errors_happened = ref true in + let error_opt = if all_errors then Some no_errors_happened else None in let split_constructors (Defs defs) = let sc_type_union q (Tu_aux (Tu_ty_id (ty, id), l)) = - match split_src_type id ty q with + match split_src_type error_opt env id ty q with | None -> ([],[Tu_aux (Tu_ty_id (ty,id),l)]) | Some variants -> ([(id,variants)], @@ -897,12 +894,14 @@ let split_defs all_errors splits defs = begin match List.find (fun (id',_) -> Id.compare id id' = 0) refinements with | (_,variants) -> +(* TODO: what changes to the pattern and what substitutions do we need in general? let kid,kid_annot = match args with | [P_aux (P_var (_, TP_aux (TP_var kid, _)),ann)] -> kid,ann | _ -> raise (Reporting.err_general l - "Pattern match not currently supported by monomorphisation") + ("Pattern match not currently supported by monomorphisation: " + ^ string_of_pat pat)) in let map_inst (insts,id',_) = let insts = @@ -920,6 +919,11 @@ let split_defs all_errors splits defs = P_aux (P_app (id',[P_aux (P_id (id_of_kid kid),kid_annot)]),(Generated l,tannot)), kbindings_from_list insts in +*) + let map_inst (insts,id',_) = + P_aux (P_app (id',args),(Generated l,tannot)), + KBindings.empty + in ConstrSplit (List.map map_inst variants) | exception Not_found -> NoSplit end @@ -980,7 +984,7 @@ let split_defs all_errors splits defs = | E_tuple es -> re (E_tuple (List.map map_exp es)) | E_if (e1,e2,e3) -> re (E_if (map_exp e1, map_exp e2, map_exp e3)) | E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,map_exp e1,map_exp e2,map_exp e3,ord,map_exp e4)) - | E_loop (loop,e1,e2) -> re (E_loop (loop,map_exp e1,map_exp e2)) + | E_loop (loop,m,e1,e2) -> re (E_loop (loop,m,map_exp e1,map_exp e2)) | E_vector es -> re (E_vector (List.map map_exp es)) | E_vector_access (e1,e2) -> re (E_vector_access (map_exp e1,map_exp e2)) | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (map_exp e1,map_exp e2,map_exp e3)) @@ -1007,9 +1011,9 @@ let split_defs all_errors splits defs = FE_aux (FE_Fexp (id,map_exp e),annot) and map_pexp = function | Pat_aux (Pat_exp (p,e),l) -> - let nosplit = [Pat_aux (Pat_exp (p,map_exp e),l)] in + let nosplit = lazy [Pat_aux (Pat_exp (p,map_exp e),l)] in (match map_pat p with - | NoSplit -> nosplit + | NoSplit -> Lazy.force nosplit | VarSplit patsubsts -> if check_split_size patsubsts (pat_loc p) then List.map (fun (pat',substs,pchoices,ksubsts) -> @@ -1020,7 +1024,7 @@ let split_defs all_errors splits defs = let exp' = stop_at_false_assertions exp' in Pat_aux (Pat_exp (pat', map_exp exp'),l)) patsubsts - else nosplit + else Lazy.force nosplit | ConstrSplit patnsubsts -> List.map (fun (pat',nsubst) -> let pat' = Spec_analysis.nexp_subst_pat nsubst pat' in @@ -1028,9 +1032,9 @@ let split_defs all_errors splits defs = Pat_aux (Pat_exp (pat', map_exp exp'),l) ) patnsubsts) | Pat_aux (Pat_when (p,e1,e2),l) -> - let nosplit = [Pat_aux (Pat_when (p,map_exp e1,map_exp e2),l)] in + let nosplit = lazy [Pat_aux (Pat_when (p,map_exp e1,map_exp e2),l)] in (match map_pat p with - | NoSplit -> nosplit + | NoSplit -> Lazy.force nosplit | VarSplit patsubsts -> if check_split_size patsubsts (pat_loc p) then List.map (fun (pat',substs,pchoices,ksubsts) -> @@ -1044,7 +1048,7 @@ let split_defs all_errors splits defs = let exp2' = stop_at_false_assertions exp2' in Pat_aux (Pat_when (pat', map_exp exp1', map_exp exp2'),l)) patsubsts - else nosplit + else Lazy.force nosplit | ConstrSplit patnsubsts -> List.map (fun (pat',nsubst) -> let pat' = Spec_analysis.nexp_subst_pat nsubst pat' in @@ -1115,10 +1119,14 @@ let split_defs all_errors splits defs = | DEF_internal_mutrec _ -> [d] | DEF_fundef fd -> [DEF_fundef (map_fundef fd)] - | DEF_mapdef (MD_aux (_, (l, _))) -> Reporting.unreachable l __POS__ "mappings should be gone by now" + | DEF_mapdef (MD_aux (_, (l, _))) -> + Reporting.unreachable l __POS__ "mappings should be gone by now" | DEF_val lb -> [DEF_val (map_letbind lb)] | DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd) | DEF_measure (id,pat,exp) -> [DEF_measure (id,pat,map_exp exp)] + | DEF_loop_measures (id,_) -> + Reporting.unreachable (id_loc id) __POS__ + "Loop termination measures should have been rewritten before now" in Defs (List.concat (List.map map_def defs)) in @@ -2065,7 +2073,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = let d3,a3,r3 = analyse_exp fn_id env assigns e3 in let assigns = add_dep_to_assigned d1 (dep_bindings_merge a2 a3) [e2;e3] in (dmerge d1 (dmerge d2 d3), assigns, merge r1 (merge r2 r3)) - | E_loop (_,e1,e2) -> + | E_loop (_,_,e1,e2) -> (* We remove all of the variables assigned in the loop, so we don't need to add control dependencies *) let assigns = remove_assigns [e1;e2] " assigned in a loop" in @@ -2207,30 +2215,34 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = (List.fold_left (fun tenv kopt -> Env.add_typ_var l kopt tenv) tenv kopts), typ in - if is_bitvector_typ typ then - let size,_,_ = vector_typ_args_of typ in - let Nexp_aux (size,_) as size_nexp = simplify_size_nexp env tenv size in - let is_tyvar_parameter v = - List.exists (fun k -> Kid.compare k v == 0) env.top_kids - in - match size with - | Nexp_constant _ -> r - | Nexp_var v when is_tyvar_parameter v -> - { r with kid_in_caller = CallerKidSet.add (fn_id,v) r.kid_in_caller } - | _ -> - match deps_of_nexp l env.kid_deps [] size_nexp with - | Have (args,extras) -> - { r with - split = ArgSplits.merge merge_detail r.split args; - extra_splits = merge_extras r.extra_splits extras - } - | Unknown (l,msg) -> - { r with - failures = - Failures.add l (StringSet.singleton ("Unable to monomorphise " ^ string_of_nexp size_nexp ^ ": " ^ msg)) - r.failures } - else - r + let rec check_typ typ = + if is_bitvector_typ typ then + let size,_,_ = vector_typ_args_of typ in + let Nexp_aux (size,_) as size_nexp = simplify_size_nexp env tenv size in + let is_tyvar_parameter v = + List.exists (fun k -> Kid.compare k v == 0) env.top_kids + in + match size with + | Nexp_constant _ -> r + | Nexp_var v when is_tyvar_parameter v -> + { r with kid_in_caller = CallerKidSet.add (fn_id,v) r.kid_in_caller } + | _ -> + match deps_of_nexp l env.kid_deps [] size_nexp with + | Have (args,extras) -> + { r with + split = ArgSplits.merge merge_detail r.split args; + extra_splits = merge_extras r.extra_splits extras + } + | Unknown (l,msg) -> + { r with + failures = + Failures.add l (StringSet.singleton ("Unable to monomorphise " ^ string_of_nexp size_nexp ^ ": " ^ msg)) + r.failures } + else match typ with + | Typ_aux (Typ_tup typs,_) -> + List.fold_left (fun r ty -> merge r (check_typ ty)) r typs + | _ -> r + in check_typ typ in (deps, assigns, r) @@ -3178,6 +3190,7 @@ let make_bitvector_env_casts env quant_kids (kid,i) exp = if mut = Immutable then mk_cast var typ exp else exp) locals exp let make_bitvector_cast_exp cast_name cast_env quant_kids typ target_typ exp = + if alpha_equivalent cast_env typ target_typ then exp else let infer_arg_typ env f l typ = let (typq, ctor_typ) = Env.get_union_id f env in let quants = quant_items typq in @@ -3194,6 +3207,7 @@ let make_bitvector_cast_exp cast_name cast_env quant_kids typ target_typ exp = in (* Push the cast down, including through constructors *) let rec aux exp (typ, target_typ) = + if alpha_equivalent cast_env typ target_typ then exp else let exp_env = env_of exp in match exp with | E_aux (E_let (lb,exp'),ann) -> @@ -3383,9 +3397,8 @@ let add_bitvector_casts (Defs defs) = let bitsn = vector_typ (nvar kid) dec_ord bit_typ in let ts = mk_typschm (mk_typquant [mk_qi_id K_int kid]) (function_typ [bitsn] bitsn no_effect) in - let extfn _ = Some "zeroExtend" in let mkfn name = - mk_val_spec (VS_val_spec (ts,name,extfn,false)) + mk_val_spec (VS_val_spec (ts,name,[("_", "zeroExtend")],false)) in let defs = List.map mkfn (IdSet.elements !specs_required) in check Env.empty (Defs defs) @@ -3650,7 +3663,7 @@ let monomorphise opts splits defs = then () else raise (Reporting.err_general Unknown "Unable to monomorphise program") in - let ok_split, defs = split_defs opts.all_split_errors splits defs in + let ok_split, defs = split_defs opts.all_split_errors splits env defs in let () = if (ok_analysis && ok_extras && ok_split) || opts.continue_anyway then () else raise (Reporting.err_general Unknown "Unable to monomorphise program") diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index c68a258d..1a77ea12 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -256,7 +256,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = separate space [string "let"; ocaml_atomic_lexp ctx lexp; equals; string "ref"; parens (ocaml_atomic_exp ctx exp1 ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (Rewrites.simple_typ (typ_of exp1))); string "in"] ^/^ ocaml_exp ctx exp2 - | E_loop (Until, cond, body) -> + | E_loop (Until, _, cond, body) -> let loop_body = (ocaml_atomic_exp ctx body ^^ semi) ^/^ @@ -267,7 +267,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = (string "let rec loop () =" ^//^ loop_body) ^/^ string "in" ^/^ string "loop ()" - | E_loop (While, cond, body) -> + | E_loop (While, _, cond, body) -> let loop_body = separate space [string "if"; ocaml_atomic_exp ctx cond; string "then"; parens (ocaml_atomic_exp ctx body ^^ semi ^^ space ^^ string "loop ()"); @@ -466,8 +466,8 @@ let ocaml_funcls ctx = | exception Not_found -> failwith ("No val spec found for " ^ string_of_id id) in (* Any remaining type variables after simple_typ rewrite should - ind icate Type-polymorphism. If we have it, we need to generate - explic it type signatures with universal quantification. *) + indicate Type-polymorphism. If we have it, we need to generate + explicit type signatures with universal quantification. *) let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in let pat_sym = gensym () in let pat, exp = @@ -625,8 +625,8 @@ let ocaml_typedef ctx (TD_aux (td_aux, (l, _))) = Reporting.unreachable l __POS__ "Bitfield should be re-written" let get_externs (Defs defs) = - let extern_id (VS_aux (VS_val_spec (typschm, id, ext, _), _)) = - match ext "ocaml" with + let extern_id (VS_aux (VS_val_spec (typschm, id, exts, _), _)) = + match Ast_util.extern_assoc "ocaml" exts with | None -> [] | Some ext -> [(id, mk_id ext)] in @@ -991,6 +991,8 @@ let ocaml_compile spec defs generator_types = let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/elf_loader.ml .") in let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/sail_lib.ml .") in let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/util.ml .") in + let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/value.ml .") in + let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/toFromInterp_lib.ml .") in let tags_file = if !opt_ocaml_coverage then "_tags_coverage" else "_tags" in let _ = Unix.system ("cp -r " ^ sail_dir ^ "/lib/" ^ tags_file ^ " _tags") in let out_chan = open_out (spec ^ ".ml") in diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 818c9340..91fb0610 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -238,7 +238,14 @@ and fpat = type loop = While | Until -type +type measure_aux = (* optional termination measure for a loop *) + | Measure_none + | Measure_some of exp + +and measure = + | Measure_aux of measure_aux * l + +and exp_aux = (* Expression *) E_block of (exp) list (* block (parsing conflict with structs?) *) | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *) @@ -251,7 +258,7 @@ exp_aux = (* Expression *) | E_app_infix of exp * id * exp (* infix function application *) | E_tuple of (exp) list (* tuple *) | E_if of exp * exp * exp (* conditional *) - | E_loop of loop * exp * exp + | E_loop of loop * measure * exp * exp | E_for of id * exp * exp * exp * atyp * exp (* loop *) | E_vector of (exp) list (* vector (indexed from 0) *) | E_vector_access of exp * exp (* vector access *) @@ -443,7 +450,7 @@ type_def_aux = (* Type definition body *) type val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id * (string -> string option) * bool + VS_val_spec of typschm * id * (string * string) list * bool type dec_spec_aux = (* Register declarations *) @@ -489,6 +496,10 @@ dec_spec = DEC_aux of dec_spec_aux * l +type loop_measure = + | Loop of loop * exp + + type scattered_def = SD_aux of scattered_def_aux * l @@ -509,6 +520,7 @@ def = (* Top-level definition *) | DEF_default of default_typing_spec (* default kind and type assumptions *) | DEF_scattered of scattered_def (* scattered definition *) | DEF_measure of id * pat * exp (* separate termination measure declaration *) + | DEF_loop_measures of id * loop_measure list (* separate termination measure declaration *) | DEF_reg_dec of dec_spec (* register declaration *) | DEF_pragma of string * string * l | DEF_internal_mutrec of fundef list diff --git a/src/parser.mly b/src/parser.mly index 39ca75ff..f764995a 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -92,6 +92,7 @@ let mk_typ t n m = ATyp_aux (t, loc n m) let mk_pat p n m = P_aux (p, loc n m) let mk_pexp p n m = Pat_aux (p, loc n m) let mk_exp e n m = E_aux (e, loc n m) +let mk_measure meas n m = Measure_aux (meas, loc n m) let mk_lit l n m = L_aux (l, loc n m) let mk_lit_exp l n m = mk_exp (E_lit (mk_lit l n m)) n m let mk_typschm tq t n m = TypSchm_aux (TypSchm_ts (tq, t), loc n m) @@ -748,6 +749,13 @@ exp_eof: | exp Eof { $1 } +/* Internal syntax for loop measures, rejected in normal code by initial_check */ +internal_loop_measure: + | + { mk_measure Measure_none $startpos $endpos } + | TerminationMeasure Lcurly exp Rcurly + { mk_measure (Measure_some $3) $startpos $endpos } + exp: | exp0 { $1 } @@ -802,10 +810,10 @@ exp: else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6)) in mk_exp (E_for ($3, $5, $7, step, ord, $9)) $startpos $endpos } - | Repeat exp Until exp - { mk_exp (E_loop (Until, $4, $2)) $startpos $endpos } - | While exp Do exp - { mk_exp (E_loop (While, $2, $4)) $startpos $endpos } + | Repeat internal_loop_measure exp Until exp + { mk_exp (E_loop (Until, $2, $5, $3)) $startpos $endpos } + | While internal_loop_measure exp Do exp + { mk_exp (E_loop (While, $2, $3, $5)) $startpos $endpos } /* Debugging only, will be rejected in initial_check if debugging isn't on */ | InternalPLet pat Eq exp In exp @@ -1056,6 +1064,8 @@ atomic_exp: { mk_exp (E_record $3) $startpos $endpos } | Lcurly exp With fexp_exp_list Rcurly { mk_exp (E_record_update ($2, $4)) $startpos $endpos } + | Lsquare Rsquare + { mk_exp (E_vector []) $startpos $endpos } | Lsquare exp_list Rsquare { mk_exp (E_vector $2) $startpos $endpos } | Lsquare exp With atomic_exp Eq exp Rsquare @@ -1341,31 +1351,31 @@ let_def: externs: | id Colon String - { ([(string_of_id $1, $3)], None) } + { [(string_of_id $1, $3)] } | Under Colon String - { ([], Some $3) } + { [("_", $3)] } | id Colon String Comma externs - { cons_fst (string_of_id $1, $3) $5 } + { (string_of_id $1, $3) :: $5 } val_spec_def: | Doc val_spec_def { doc_vs $1 $2 } | Val id Colon typschm - { mk_vs (VS_val_spec ($4, $2, (fun _ -> None), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($4, $2, [], false)) $startpos $endpos } | Val Cast id Colon typschm - { mk_vs (VS_val_spec ($5, $3, (fun _ -> None), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($5, $3, [], true)) $startpos $endpos } | Val id Eq String Colon typschm - { mk_vs (VS_val_spec ($6, $2, (fun _ -> Some $4), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($6, $2, [("_", $4)], false)) $startpos $endpos } | Val Cast id Eq String Colon typschm - { mk_vs (VS_val_spec ($7, $3, (fun _ -> Some $5), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($7, $3, [("_", $5)], true)) $startpos $endpos } | Val String Colon typschm - { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), (fun _ -> Some $2), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), [("_", $2)], false)) $startpos $endpos } | Val Cast String Colon typschm - { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), (fun _ -> Some $3), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), [("_", $3)], true)) $startpos $endpos } | Val id Eq Lcurly externs Rcurly Colon typschm - { mk_vs (VS_val_spec ($8, $2, (fun backend -> (assoc_opt backend $5)), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($8, $2, $5, false)) $startpos $endpos } | Val Cast id Eq Lcurly externs Rcurly Colon typschm - { mk_vs (VS_val_spec ($9, $3, (fun backend -> (assoc_opt backend $6)), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($9, $3, $6, true)) $startpos $endpos } register_def: | Register id Colon typ @@ -1401,6 +1411,19 @@ scattered_clause: | Function_ Clause funcl { mk_sd (SD_funcl $3) $startpos $endpos } +loop_measure: + | Until exp + { Loop (Until, $2) } + | Repeat exp + { Loop (Until, $2) } + | While exp + { Loop (While, $2) } + +loop_measures: + | loop_measure + { [$1] } + | loop_measure Comma loop_measures + { $1::$3 } def: | fun_def @@ -1439,6 +1462,8 @@ def: { DEF_pragma (fst $1, snd $1, loc $startpos $endpos) } | TerminationMeasure id pat Eq exp { DEF_measure ($2, $3, $5) } + | TerminationMeasure id loop_measures + { DEF_loop_measures ($2,$3) } defs_list: | def diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index b4f32dce..f26c74d7 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -58,6 +58,15 @@ open Pretty_print_common module StringSet = Set.Make(String) +let rec list_contains cmp l1 = function + | [] -> Some l1 + | h::t -> + let rec remove = function + | [] -> None + | h'::t' -> if cmp h h' = 0 then Some t' + else Util.option_map (List.cons h') (remove t') + in Util.option_bind (fun l1' -> list_contains cmp l1' t) (remove l1) + let opt_undef_axioms = ref false let opt_debug_on : string list ref = ref [] @@ -549,6 +558,11 @@ let classify_ex_type ctxt env ?binding ?(rawbools=false) (Typ_aux (t,l) as t0) = | Typ_exist (kopts,_,t1) -> ExGeneral,kopts,t1 | _ -> ExNone,[],t0 +let rec flatten_nc (NC_aux (nc,l) as nc_full) = + match nc with + | NC_and (nc1,nc2) -> flatten_nc nc1 @ flatten_nc nc2 + | _ -> [nc_full] + (* When making changes here, check whether they affect coq_nvars_of_typ *) let rec doc_typ_fns ctx env = (* following the structure of parser for precedence *) @@ -729,15 +743,19 @@ and doc_nc_prop ?(top = true) ctx env nc = (fun m (v,(_,Typ_aux (typ,_))) -> match typ with | Typ_app (id, [A_aux (A_bool nc,_)]) when string_of_id id = "atom_bool" -> - NCMap.add nc v m - | _ -> m) NCMap.empty locals + (flatten_nc nc, v)::m + | _ -> m) [] locals in - let newnc f nc = - match NCMap.find_opt nc nc_id_map with - | Some id -> parens (doc_op equals (doc_id id) (string "true")) - | None -> f nc - in - let rec l85 (NC_aux (nc,_) as nc_full) = + let rec newnc f nc = + let ncs = flatten_nc nc in + let candidates = + Util.map_filter (fun (ncs',id) -> Util.option_map (fun x -> x,id) (list_contains NC.compare ncs ncs')) nc_id_map + in + match List.sort (fun (l,_) (l',_) -> compare l l') candidates with + | ([],id)::_ -> parens (doc_op equals (doc_id id) (string "true")) + | ((h::t),id)::_ -> parens (doc_op (string "/\\") (doc_op equals (doc_id id) (string "true")) (l80 (List.fold_left nc_and h t))) + | [] -> f nc + and l85 (NC_aux (nc,_) as nc_full) = match nc with | NC_or (nc1, nc2) -> doc_op (string "\\/") (newnc l80 nc1) (newnc l85 nc2) | _ -> l80 nc_full @@ -779,21 +797,25 @@ and doc_nc_prop ?(top = true) ctx env nc = (* Follows Coq precedence levels *) let rec doc_nc_exp ctx env nc = let locals = Env.get_locals env |> Bindings.bindings in + let nc = Env.expand_constraint_synonyms env nc in let nc_id_map = List.fold_left (fun m (v,(_,Typ_aux (typ,_))) -> match typ with | Typ_app (id, [A_aux (A_bool nc,_)]) when string_of_id id = "atom_bool" -> - NCMap.add nc v m - | _ -> m) NCMap.empty locals - in - let newnc f nc = - match NCMap.find_opt nc nc_id_map with - | Some id -> doc_id id - | None -> f nc + (flatten_nc nc, v)::m + | _ -> m) [] locals in - let nc = Env.expand_constraint_synonyms env nc in - let rec l70 (NC_aux (nc,_) as nc_full) = + let rec newnc f nc = + let ncs = flatten_nc nc in + let candidates = + Util.map_filter (fun (ncs',id) -> Util.option_map (fun x -> x,id) (list_contains NC.compare ncs ncs')) nc_id_map + in + match List.sort (fun (l,_) (l',_) -> compare l l') candidates with + | ([],id)::_ -> doc_id id + | ((h::t),id)::_ -> parens (doc_op (string "&&") (doc_id id) (l10 (List.fold_left nc_and h t))) + | [] -> f nc + and l70 (NC_aux (nc,_) as nc_full) = match nc with | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) @@ -1504,43 +1526,70 @@ let doc_exp, doc_let = | _ -> raise (Reporting.err_unreachable l __POS__ "Unexpected number of arguments for loop combinator") end - | Id_aux (Id (("while#" | "until#") as combinator), _) -> - let combinator = String.sub combinator 0 (String.length combinator - 1) in + | Id_aux (Id (("while#" | "until#" | "while#t" | "until#t") as combinator), _) -> + let combinator = String.sub combinator 0 (String.index combinator '#') in begin - match args with - | [cond; varstuple; body] -> - let return (E_aux (e, a)) = E_aux (E_internal_return (E_aux (e, a)), a) in - let csuffix, cond, body = - match effectful (effect_of cond), effectful (effect_of body) with - | false, false -> "", cond, body - | false, true -> "M", return cond, body - | true, false -> "M", cond, return body - | true, true -> "M", cond, body - in - let used_vars_body = find_e_ids body in - let lambda = - (* Work around indentation issues in Lem when translating - tuple or literal unit patterns to Isabelle *) - match fst (uncast_exp varstuple) with - | E_aux (E_tuple _, _) - when not (IdSet.mem (mk_id "varstup") used_vars_body)-> - separate space [string "fun varstup"; bigarrow] ^^ break 1 ^^ - separate space [string "let"; squote ^^ expY varstuple; string ":= varstup in"] - | E_aux (E_lit (L_aux (L_unit, _)), _) - when not (IdSet.mem (mk_id "unit_var") used_vars_body) -> - separate space [string "fun unit_var"; bigarrow] - | _ -> - separate space [string "fun"; expY varstuple; bigarrow] - in - parens ( - (prefix 2 1) - ((separate space) [string (combinator ^ csuffix); expY varstuple]) - ((prefix 0 1) - (parens (prefix 2 1 (group lambda) (expN cond))) - (parens (prefix 2 1 (group lambda) (expN body)))) - ) - | _ -> raise (Reporting.err_unreachable l __POS__ - "Unexpected number of arguments for loop combinator") + let cond, varstuple, body, measure = + match args with + | [cond; varstuple; body] -> cond, varstuple, body, None + | [cond; varstuple; body; measure] -> cond, varstuple, body, Some measure + | _ -> raise (Reporting.err_unreachable l __POS__ + "Unexpected number of arguments for loop combinator") + in + let return (E_aux (e, (l,a))) = + let a' = mk_tannot (env_of_annot (l,a)) bool_typ no_effect in + E_aux (E_internal_return (E_aux (e, (l,a))), (l,a')) + in + let simple_bool (E_aux (_, (l,a)) as exp) = + let a' = mk_tannot (env_of_annot (l,a)) bool_typ no_effect in + E_aux (E_cast (bool_typ, exp), (l,a')) + in + let csuffix, cond, body = + match effectful (effect_of cond), effectful (effect_of body) with + | false, false -> "", cond, body + | false, true -> "M", return cond, body + | true, false -> "M", simple_bool cond, return body + | true, true -> "M", simple_bool cond, body + in + (* If rewrite_loops_with_escape_effect added a dummy assertion to + ensure that the loop can escape when it reaches the limit, omit + the dummy assert here. *) + let body = match body with + | E_aux (E_internal_plet + (P_aux ((P_wild | P_typ (_,P_aux (P_wild, _))),_), + E_aux (E_assert + (E_aux (E_lit (L_aux (L_true,_)),_), + E_aux (E_lit (L_aux (L_string "loop dummy assert",_)),_)) + ,_),body'),_) -> body' + | _ -> body + in + let msuffix, measure_pp = + match measure with + | None -> "", [] + | Some exp -> "T", [expY exp] + in + let used_vars_body = find_e_ids body in + let lambda = + (* Work around indentation issues in Lem when translating + tuple or literal unit patterns to Isabelle *) + match fst (uncast_exp varstuple) with + | E_aux (E_tuple _, _) + when not (IdSet.mem (mk_id "varstup") used_vars_body)-> + separate space [string "fun varstup"; bigarrow] ^^ break 1 ^^ + separate space [string "let"; squote ^^ expY varstuple; string ":= varstup in"] + | E_aux (E_lit (L_aux (L_unit, _)), _) + when not (IdSet.mem (mk_id "unit_var") used_vars_body) -> + separate space [string "fun unit_var"; bigarrow] + | _ -> + separate space [string "fun"; expY varstuple; bigarrow] + in + parens ( + (prefix 2 1) + ((separate space) (string (combinator ^ csuffix ^ msuffix)::measure_pp@[expY varstuple])) + ((prefix 0 1) + (parens (prefix 2 1 (group lambda) (expN cond))) + (parens (prefix 2 1 (group lambda) (expN body)))) + ) end | Id_aux (Id "early_return", _) -> begin @@ -1979,9 +2028,14 @@ let doc_exp, doc_let = match pat, e1, e2 with | (P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)), (E_aux (E_assert (assert_e1,assert_e2),_)), _ -> - let epp = liftR (separate space [string "assert_exp'"; expY assert_e1; expY assert_e2]) in - let epp = infix 0 1 (string ">>= fun _ =>") epp (top_exp new_ctxt false e2) in - if aexp_needed then parens (align epp) else align epp + let assert_fn, mid = + match assert_constraint outer_env true assert_e1 with + | Some _ -> "assert_exp'", ">>= fun _ =>" + | None -> "assert_exp", ">>" + in + let epp = liftR (separate space [string assert_fn; expY assert_e1; expY assert_e2]) in + let epp = infix 0 1 (string mid) epp (top_exp new_ctxt false e2) in + if aexp_needed then parens (align epp) else align epp | _ -> let epp = let middle = @@ -2191,7 +2245,9 @@ let types_used_with_generic_eq defs = | DEF_mapdef (MD_aux (_,(l,_))) | DEF_scattered (SD_aux (_,(l,_))) | DEF_measure (Id_aux (_,l),_,_) - -> unreachable l __POS__ "Internal definition found in the Coq back-end" + | DEF_loop_measures (Id_aux (_,l),_) + -> unreachable l __POS__ + "Definition found in the Coq back-end that should have been rewritten away" | DEF_internal_mutrec fds -> List.fold_left IdSet.union IdSet.empty (List.map typs_req_fundef fds) | DEF_val lb -> @@ -2925,6 +2981,10 @@ let rec doc_def unimplemented generic_eq_types def = | DEF_measure (id,_,_) -> unreachable (id_loc id) __POS__ ("Termination measure for " ^ string_of_id id ^ " should have been rewritten before backend") + | DEF_loop_measures (id,_) -> + unreachable (id_loc id) __POS__ + ("Loop termination measures for " ^ string_of_id id ^ + " should have been rewritten before backend") let find_exc_typ defs = let is_exc_typ_def = function @@ -2940,8 +3000,8 @@ let find_unimplemented defs = IdSet.remove id unimplemented in let adjust_def unimplemented = function - | DEF_spec (VS_aux (VS_val_spec (_,id,ext,_),_)) -> begin - match ext "coq" with + | DEF_spec (VS_aux (VS_val_spec (_,id,exts,_),_)) -> begin + match Ast_util.extern_assoc "coq" exts with | Some _ -> unimplemented | None -> IdSet.add id unimplemented end diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 6479a028..10441ed5 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -715,11 +715,12 @@ let doc_exp_lem, doc_let_lem = | _ -> raise (Reporting.err_unreachable l __POS__ "Unexpected number of arguments for loop combinator") end - | Id_aux (Id (("while#" | "until#") as combinator), _) -> - let combinator = String.sub combinator 0 (String.length combinator - 1) in + | Id_aux (Id (("while#" | "until#" | "while#t" | "until#t") as combinator), _) -> + let combinator = String.sub combinator 0 (String.index combinator '#') in begin match args with - | [cond; varstuple; body] -> + | [cond; varstuple; body] + | [cond; varstuple; body; _] -> (* Ignore termination measures - not used in Lem *) let return (E_aux (e, a)) = E_aux (E_internal_return (E_aux (e, a)), a) in let csuffix, cond, body = match effectful (effect_of cond), effectful (effect_of body) with @@ -1408,7 +1409,7 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = let doc_spec_lem env (VS_aux (valspec,annot)) = match valspec with - | VS_val_spec (typschm,id,ext,_) when ext "lem" = None -> + | VS_val_spec (typschm,id,exts,_) when Ast_util.extern_assoc "lem" exts = None -> (* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in if contains_t_pp_var typ then empty else *) doc_docstring_lem annot ^^ @@ -1485,6 +1486,7 @@ let rec doc_def_lem type_env def = | DEF_mapdef (MD_aux (_, (l, _))) -> unreachable l __POS__ "Lem doesn't support mappings" | DEF_pragma _ -> empty | DEF_measure _ -> empty (* we might use these in future *) + | DEF_loop_measures _ -> empty let find_exc_typ defs = let is_exc_typ_def = function diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 7f3a2b63..ad44f5b8 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -387,10 +387,10 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = | E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]" | E_cons (exp1, exp2) -> doc_atomic_exp exp1 ^^ space ^^ string "::" ^^ space ^^ doc_exp exp2 | E_record fexps -> separate space [string "struct"; string "{"; doc_fexps fexps; string "}"] - | E_loop (While, cond, exp) -> - separate space [string "while"; doc_exp cond; string "do"; doc_exp exp] - | E_loop (Until, cond, exp) -> - separate space [string "repeat"; doc_exp exp; string "until"; doc_exp cond] + | E_loop (While, measure, cond, exp) -> + separate space ([string "while"] @ doc_measure measure @ [doc_exp cond; string "do"; doc_exp exp]) + | E_loop (Until, measure, cond, exp) -> + separate space ([string "repeat"] @ doc_measure measure @ [doc_exp exp; string "until"; doc_exp cond]) | E_record_update (exp, fexps) -> separate space [string "{"; doc_exp exp; string "with"; doc_fexps fexps; string "}"] | E_vector_append (exp1, exp2) -> separate space [doc_atomic_exp exp1; string "@"; doc_atomic_exp exp2] @@ -429,6 +429,10 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 -> separate space [string "2"; string "^"; doc_atomic_exp exp] | _ -> doc_atomic_exp exp +and doc_measure (Measure_aux (m_aux, _)) = + match m_aux with + | Measure_none -> [] + | Measure_some exp -> [string "termination_measure"; braces (doc_exp exp)] and doc_infix n (E_aux (e_aux, _) as exp) = match e_aux with | E_app_infix (l, op, r) when n < 10 -> @@ -470,7 +474,7 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) = brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3]) | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4]) - | E_internal_value v -> string (Value.string_of_value v |> Util.green |> Util.clear) + | E_internal_value v -> string (Value.string_of_value v (* |> Util.green |> Util.clear *)) | _ -> parens (doc_exp exp) and doc_fexps fexps = separate_map (comma ^^ space) doc_fexp fexps @@ -623,9 +627,7 @@ let doc_typdef (TD_aux(td,_)) = match td with let doc_spec ?comment:(comment=false) (VS_aux (v, annot)) = let doc_extern ext = - let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^ - utf8string ("\"" ^ String.escaped id ^ "\"")) (ext b) in - let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"; "smt"; "interpreter"; "c"]) in + let docs = List.map (fun (backend, rep) -> string (backend ^ ":") ^^ space ^^ utf8string ("\"" ^ String.escaped rep ^ "\"")) ext in if docs = [] then empty else equals ^^ space ^^ braces (separate (comma ^^ space) docs) in match v with @@ -643,6 +645,13 @@ let doc_prec = function | InfixL -> string "infixl" | InfixR -> string "infixr" +let doc_loop_measures l = + separate_map (comma ^^ break 1) + (function (Loop (l,e)) -> + string (match l with While -> "while" | Until -> "until") ^^ + space ^^ doc_exp e) + l + let rec doc_scattered (SD_aux (sd_aux, _)) = match sd_aux with | SD_function (_, _, _, id) -> @@ -679,6 +688,8 @@ let rec doc_def def = group (match def with | DEF_measure (id,pat,exp) -> string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_pat pat ^^ space ^^ equals ^/^ doc_exp exp + | DEF_loop_measures (id,measures) -> + string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_loop_measures measures | DEF_pragma (pragma, arg, l) -> string ("$" ^ pragma ^ " " ^ arg) | DEF_fixity (prec, n, id) -> diff --git a/src/rewriter.ml b/src/rewriter.ml index edf0d4a5..2573a135 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -151,7 +151,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match destruct_tannot (snd annot) union_effects (fun_app_effects f env) (union_eff_exps [e1;e2]) | E_if (e1,e2,e3) -> union_eff_exps [e1;e2;e3] | E_for (_,e1,e2,e3,_,e4) -> union_eff_exps [e1;e2;e3;e4] - | E_loop (_,e1,e2) -> union_eff_exps [e1;e2] + | E_loop (_,_,e1,e2) -> union_eff_exps [e1;e2] | E_vector es -> union_eff_exps es | E_vector_access (e1,e2) -> union_eff_exps [e1;e2] | E_vector_subrange (e1,e2,e3) -> union_eff_exps [e1;e2;e3] @@ -280,8 +280,12 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) = | E_if (c,t,e) -> rewrap (E_if (rewrite c,rewrite t, rewrite e)) | E_for (id, e1, e2, e3, o, body) -> rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body)) - | E_loop (loop, e1, e2) -> - rewrap (E_loop (loop, rewrite e1, rewrite e2)) + | E_loop (loop, m, e1, e2) -> + let m = match m with + | Measure_aux (Measure_none,_) -> m + | Measure_aux (Measure_some exp,l) -> Measure_aux (Measure_some (rewrite exp),l) + in + rewrap (E_loop (loop, m, rewrite e1, rewrite e2)) | E_vector exps -> rewrap (E_vector (List.map rewrite exps)) | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index)) | E_vector_subrange (vec,i1,i2) -> @@ -362,8 +366,9 @@ let rewrite_def rewriters d = match d with | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs) | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind) | DEF_pragma (pragma, arg, l) -> DEF_pragma (pragma, arg, l) - | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter") + | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewriter") | DEF_measure (id,pat,exp) -> DEF_measure (id,rewriters.rewrite_pat rewriters pat, rewriters.rewrite_exp rewriters exp) + | DEF_loop_measures (id,_) -> raise (Reporting.err_unreachable (id_loc id) __POS__ "DEF_loop_measures survived to rewriter") let rewrite_defs_base rewriters (Defs defs) = let rec rewrite ds = match ds with @@ -539,7 +544,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, ; e_tuple : 'exp list -> 'exp_aux ; e_if : 'exp * 'exp * 'exp -> 'exp_aux ; e_for : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux - ; e_loop : loop * 'exp * 'exp -> 'exp_aux + ; e_loop : loop * ('exp option * Parse_ast.l) * 'exp * 'exp -> 'exp_aux ; e_vector : 'exp list -> 'exp_aux ; e_vector_access : 'exp * 'exp -> 'exp_aux ; e_vector_subrange : 'exp * 'exp * 'exp -> 'exp_aux @@ -602,8 +607,12 @@ let rec fold_exp_aux alg = function | E_if (e1,e2,e3) -> alg.e_if (fold_exp alg e1, fold_exp alg e2, fold_exp alg e3) | E_for (id,e1,e2,e3,order,e4) -> alg.e_for (id,fold_exp alg e1, fold_exp alg e2, fold_exp alg e3, order, fold_exp alg e4) - | E_loop (loop_type, e1, e2) -> - alg.e_loop (loop_type, fold_exp alg e1, fold_exp alg e2) + | E_loop (loop_type, m, e1, e2) -> + let m = match m with + | Measure_aux (Measure_none,l) -> None,l + | Measure_aux (Measure_some exp,l) -> Some (fold_exp alg exp),l + in + alg.e_loop (loop_type, m, fold_exp alg e1, fold_exp alg e2) | E_vector es -> alg.e_vector (List.map (fold_exp alg) es) | E_vector_access (e1,e2) -> alg.e_vector_access (fold_exp alg e1, fold_exp alg e2) | E_vector_subrange (e1,e2,e3) -> @@ -681,7 +690,9 @@ let id_exp_alg = ; e_tuple = (fun es -> E_tuple es) ; e_if = (fun (e1,e2,e3) -> E_if (e1,e2,e3)) ; e_for = (fun (id,e1,e2,e3,order,e4) -> E_for (id,e1,e2,e3,order,e4)) - ; e_loop = (fun (lt, e1, e2) -> E_loop (lt, e1, e2)) + ; e_loop = (fun (lt, (m,l), e1, e2) -> + let m = match m with None -> Measure_none | Some e -> Measure_some e in + E_loop (lt, Measure_aux (m,l), e1, e2)) ; e_vector = (fun es -> E_vector es) ; e_vector_access = (fun (e1,e2) -> E_vector_access (e1,e2)) ; e_vector_subrange = (fun (e1,e2,e3) -> E_vector_subrange (e1,e2,e3)) @@ -776,8 +787,12 @@ let compute_exp_alg bot join = ; e_if = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_if (e1,e2,e3))) ; e_for = (fun (id,(v1,e1),(v2,e2),(v3,e3),order,(v4,e4)) -> (join_list [v1;v2;v3;v4], E_for (id,e1,e2,e3,order,e4))) - ; e_loop = (fun (lt, (v1, e1), (v2, e2)) -> - (join_list [v1;v2], E_loop (lt, e1, e2))) + ; e_loop = (fun (lt, (m,l), (v1, e1), (v2, e2)) -> + let vs,m = match m with + | None -> [], Measure_none + | Some (v,e) -> [v], Measure_some e + in + (join_list (vs@[v1;v2]), E_loop (lt, Measure_aux (m,l), e1, e2))) ; e_vector = split_join (fun es -> E_vector es) ; e_vector_access = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_vector_access (e1,e2))) ; e_vector_subrange = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_vector_subrange (e1,e2,e3))) @@ -878,7 +893,8 @@ let pure_exp_alg bot join = ; e_tuple = join_list ; e_if = (fun (v1,v2,v3) -> join_list [v1;v2;v3]) ; e_for = (fun (id,v1,v2,v3,order,v4) -> join_list [v1;v2;v3;v4]) - ; e_loop = (fun (lt, v1, v2) -> join v1 v2) + ; e_loop = (fun (lt, (m,_), v1, v2) -> + let v = join v1 v2 in match m with None -> v | Some v' -> join v v') ; e_vector = join_list ; e_vector_access = (fun (v1,v2) -> join v1 v2) ; e_vector_subrange = (fun (v1,v2,v3) -> join_list [v1;v2;v3]) @@ -927,3 +943,200 @@ let pure_exp_alg bot join = ; lB_aux = (fun (vl,annot) -> vl) ; pat_alg = pure_pat_alg bot join } + +let default_fold_fexp f x (FE_aux (FE_Fexp (id,e),annot)) = + let x,e = f x e in + x, FE_aux (FE_Fexp (id,e),annot) + +let default_fold_pexp f x (Pat_aux (pe,ann)) = + let x,pe = match pe with + | Pat_exp (p,e) -> + let x,e = f x e in + x,Pat_exp (p,e) + | Pat_when (p,e1,e2) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + x,Pat_when (p,e1,e2) + in x, Pat_aux (pe,ann) + +let default_fold_letbind f x (LB_aux (LB_val (p,e),ann)) = + let x,e = f x e in + x, LB_aux (LB_val (p,e),ann) + +let rec default_fold_lexp f x (LEXP_aux (le,ann) as lexp) = + let re le = LEXP_aux (le,ann) in + match le with + | LEXP_id _ + | LEXP_cast _ + -> x, lexp + | LEXP_deref e -> + let x, e = f x e in + x, re (LEXP_deref e) + | LEXP_memory (id,es) -> + let x,es = List.fold_left (fun (x,es) e -> + let x,e' = f x e in x,e'::es) (x,[]) es in + x, re (LEXP_memory (id, List.rev es)) + | LEXP_tup les -> + let x,les = List.fold_left (fun (x,les) le -> + let x,le' = default_fold_lexp f x le in x,le'::les) (x,[]) les in + x, re (LEXP_tup (List.rev les)) + | LEXP_vector_concat les -> + let x,les = List.fold_left (fun (x,les) le -> + let x,le' = default_fold_lexp f x le in x,le'::les) (x,[]) les in + x, re (LEXP_vector_concat (List.rev les)) + | LEXP_vector (le,e) -> + let x, le = default_fold_lexp f x le in + let x, e = f x e in + x, re (LEXP_vector (le,e)) + | LEXP_vector_range (le,e1,e2) -> + let x, le = default_fold_lexp f x le in + let x, e1 = f x e1 in + let x, e2 = f x e2 in + x, re (LEXP_vector_range (le,e1,e2)) + | LEXP_field (le,id) -> + let x, le = default_fold_lexp f x le in + x, re (LEXP_field (le,id)) + +let default_fold_exp f x (E_aux (e,ann) as exp) = + let re e = E_aux (e,ann) in + match e with + | E_block es -> + let x,es = List.fold_left (fun (x,es) e -> + let x,e' = f x e in x,e'::es) (x,[]) es in + x, re (E_block (List.rev es)) + | E_nondet es -> + let x,es = List.fold_left (fun (x,es) e -> + let x,e' = f x e in x,e'::es) (x,[]) es in + x, re (E_nondet (List.rev es)) + | E_id _ + | E_ref _ + | E_lit _ -> x, exp + | E_cast (typ,e) -> + let x,e = f x e in + x, re (E_cast (typ,e)) + | E_app (id,es) -> + let x,es = List.fold_left (fun (x,es) e -> + let x,e' = f x e in x,e'::es) (x,[]) es in + x, re (E_app (id, List.rev es)) + | E_app_infix (e1,id,e2) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + x, re (E_app_infix (e1,id,e2)) + | E_tuple es -> + let x,es = List.fold_left (fun (x,es) e -> + let x,e' = f x e in x,e'::es) (x,[]) es in + x, re (E_tuple (List.rev es)) + | E_if (e1,e2,e3) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + let x,e3 = f x e3 in + x, re (E_if (e1,e2,e3)) + | E_for (id,e1,e2,e3,order,e4) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + let x,e3 = f x e3 in + let x,e4 = f x e4 in + x, re (E_for (id,e1,e2,e3,order,e4)) + | E_loop (loop_type, m, e1, e2) -> + let x,m = match m with + | Measure_aux (Measure_none,_) -> x,m + | Measure_aux (Measure_some exp,l) -> + let x, exp = f x exp in + x, Measure_aux (Measure_some exp,l) + in + let x,e1 = f x e1 in + let x,e2 = f x e2 in + x, re (E_loop (loop_type, m, e1, e2)) + | E_vector es -> + let x,es = List.fold_left (fun (x,es) e -> + let x,e' = f x e in x,e'::es) (x,[]) es in + x, re (E_vector (List.rev es)) + | E_vector_access (e1,e2) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + x, re (E_vector_access (e1,e2)) + | E_vector_subrange (e1,e2,e3) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + let x,e3 = f x e3 in + x, re (E_vector_subrange (e1,e2,e3)) + | E_vector_update (e1,e2,e3) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + let x,e3 = f x e3 in + x, re (E_vector_update (e1,e2,e3)) + | E_vector_update_subrange (e1,e2,e3,e4) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + let x,e3 = f x e3 in + let x,e4 = f x e4 in + x, re (E_vector_update_subrange (e1,e2,e3,e4)) + | E_vector_append (e1,e2) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + x, re (E_vector_append (e1,e2)) + | E_list es -> + let x,es = List.fold_left (fun (x,es) e -> + let x,e' = f x e in x,e'::es) (x,[]) es in + x, re (E_list (List.rev es)) + | E_cons (e1,e2) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + x, re (E_cons (e1,e2)) + | E_record fexps -> + let x,fexps = List.fold_left (fun (x,fes) fe -> + let x,fe' = default_fold_fexp f x fe in x,fe'::fes) (x,[]) fexps in + x, re (E_record (List.rev fexps)) + | E_record_update (e,fexps) -> + let x,e = f x e in + let x,fexps = List.fold_left (fun (x,fes) fe -> + let x,fe' = default_fold_fexp f x fe in x,fe'::fes) (x,[]) fexps in + x, re (E_record_update (e, List.rev fexps)) + | E_field (e,id) -> + let x,e = f x e in x, re (E_field (e,id)) + | E_case (e,pexps) -> + let x,e = f x e in + let x,pexps = List.fold_left (fun (x,pes) pe -> + let x,pe' = default_fold_pexp f x pe in x,pe'::pes) (x,[]) pexps in + x, re (E_case (e, List.rev pexps)) + | E_try (e,pexps) -> + let x,e = f x e in + let x,pexps = List.fold_left (fun (x,pes) pe -> + let x,pe' = default_fold_pexp f x pe in x,pe'::pes) (x,[]) pexps in + x, re (E_try (e, List.rev pexps)) + | E_let (letbind,e) -> + let x,letbind = default_fold_letbind f x letbind in + let x,e = f x e in + x, re (E_let (letbind,e)) + | E_assign (lexp,e) -> + let x,lexp = default_fold_lexp f x lexp in + let x,e = f x e in + x, re (E_assign (lexp,e)) + | E_sizeof _ + | E_constraint _ + -> x,exp + | E_exit e -> + let x,e = f x e in x, re (E_exit e) + | E_throw e -> + let x,e = f x e in x, re (E_throw e) + | E_return e -> + let x,e = f x e in x, re (E_return e) + | E_assert(e1,e2) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + x, re (E_assert (e1,e2)) + | E_var (lexp,e1,e2) -> + let x,lexp = default_fold_lexp f x lexp in + let x,e1 = f x e1 in + let x,e2 = f x e2 in + x, re (E_var (lexp,e1,e2)) + | E_internal_plet (pat,e1,e2) -> + let x,e1 = f x e1 in + let x,e2 = f x e2 in + x, re (E_internal_plet (pat,e1,e2)) + | E_internal_return e -> + let x,e = f x e in x, re (E_internal_return e) + | E_internal_value _ -> x,exp + +let rec foldin_exp f x e = f (default_fold_exp (foldin_exp f)) x e +let rec foldin_pexp f x e = default_fold_pexp (foldin_exp f) x e diff --git a/src/rewriter.mli b/src/rewriter.mli index ab29d1d9..878e0d15 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -128,7 +128,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, ; e_tuple : 'exp list -> 'exp_aux ; e_if : 'exp * 'exp * 'exp -> 'exp_aux ; e_for : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux - ; e_loop : loop * 'exp * 'exp -> 'exp_aux + ; e_loop : loop * ('exp option * Parse_ast.l) * 'exp * 'exp -> 'exp_aux ; e_vector : 'exp list -> 'exp_aux ; e_vector_access : 'exp * 'exp -> 'exp_aux ; e_vector_subrange : 'exp * 'exp * 'exp -> 'exp_aux @@ -254,3 +254,7 @@ val fix_eff_pexp : tannot pexp -> tannot pexp val fix_eff_fexp : tannot fexp -> tannot fexp val fix_eff_opt_default : tannot opt_default -> tannot opt_default + +(* In-order fold over expressions *) +val foldin_exp : (('a -> 'b exp -> 'a * 'b exp) -> 'a -> 'b exp -> 'a * 'b exp) -> 'a -> 'b exp -> 'a * 'b exp +val foldin_pexp : (('a -> 'b exp -> 'a * 'b exp) -> 'a -> 'b exp -> 'a * 'b exp) -> 'a -> 'b pexp -> 'a * 'b pexp diff --git a/src/rewrites.ml b/src/rewrites.ml index 2138207b..7ff500b9 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1772,7 +1772,7 @@ let rewrite_split_fun_ctor_pats fun_name env (Defs defs) = in let val_spec = VS_aux (VS_val_spec - (mk_typschm (mk_typquant quants) fun_typ, id, (fun _ -> None), false), + (mk_typschm (mk_typquant quants) fun_typ, id, [], false), (Parse_ast.Unknown, empty_tannot)) in let fundef = FD_aux (FD_function (r_o, t_o, e_o, funcls), fdannot) in @@ -2153,6 +2153,10 @@ let rewrite_simple_assignments env defs = let assign_e_aux e_aux annot = let env = env_of_annot annot in match e_aux with + | E_assign (LEXP_aux (LEXP_id _, _), _) -> + E_aux (e_aux, annot) + | E_assign (LEXP_aux (LEXP_cast (_, _), _), _) -> + E_aux (e_aux, annot) | E_assign (lexp, exp) -> let (lexp, rhs) = rewrite_lexp_to_rhs lexp in let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in @@ -2369,10 +2373,15 @@ let rewrite_defs_letbind_effects env = n_exp_name by (fun by -> let body = n_exp_term (effectful body) body in k (rewrap (E_for (id,start,stop,by,dir,body)))))) - | E_loop (loop, cond, body) -> + | E_loop (loop, measure, cond, body) -> + let measure = match measure with + | Measure_aux (Measure_none,_) -> measure + | Measure_aux (Measure_some exp,l) -> + Measure_aux (Measure_some (n_exp_term false exp),l) + in let cond = n_exp_term (effectful cond) cond in let body = n_exp_term (effectful body) body in - k (rewrap (E_loop (loop,cond,body))) + k (rewrap (E_loop (loop,measure,cond,body))) | E_vector exps -> n_exp_nameL exps (fun exps -> k (rewrap (E_vector exps))) @@ -2718,7 +2727,7 @@ let construct_toplevel_string_append_func env f_id pat = ), unk)] in let fun_typ = (mk_typ (Typ_fn ([string_typ], option_typ, no_effect))) in - let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, (fun _ -> None), false), unkt) in + let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, [], false), unkt) in let new_val_spec, env = Type_check.check_val_spec env new_val_spec in let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in @@ -3448,7 +3457,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = el env (typ_of exp4)))) el env (typ_of exp4)) in Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats)) - | E_loop(loop,cond,body) -> + | E_loop(loop,Measure_aux (measure,_),cond,body) -> (* Find variables that might be updated in the loop body and are used either after or within the loop. *) let vars, varpats = @@ -3458,11 +3467,14 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = in let body = rewrite_var_updates (add_vars overwrite body vars) in let (E_aux (_,(_,bannot))) = body in - let fname = match loop with - | While -> "while#" - | Until -> "until#" in + let fname, measure = match loop, measure with + | While, Measure_none -> "while#", [] + | Until, Measure_none -> "until#", [] + | While, Measure_some exp -> "while#t", [exp] + | Until, Measure_some exp -> "until#t", [exp] + in let funcl = Id_aux (Id fname,gen_loc el) in - let v = E_aux (E_app (funcl,[cond;tuple_exp vars;body]), (gen_loc el, bannot)) in + let v = E_aux (E_app (funcl,[cond;tuple_exp vars;body]@measure), (gen_loc el, bannot)) in Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats)) | E_if (c,e1,e2) -> let vars, varpats = @@ -3763,8 +3775,10 @@ let rewrite_defs_remove_e_assign env (Defs defs) = let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars"); ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars"); - ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in - let rewrite_exp _ e = + ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars"); + ("while#t", "forall ('vars : Type). (bool, 'vars, 'vars, int) -> 'vars"); + ("until#t", "forall ('vars : Type). (bool, 'vars, 'vars, int) -> 'vars")]))) in + let rewrite_exp _ e = replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in rewrite_defs_base { rewrite_exp = rewrite_exp @@ -3971,10 +3985,10 @@ let rewrite_defs_realise_mappings _ (Defs defs) = let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), l) in let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), l) in - let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in - let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in - let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in - let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, [], false), (Parse_ast.Unknown,())) in + let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, [], false), (Parse_ast.Unknown,())) in + let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, [], false), (Parse_ast.Unknown,())) in + let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, [], false), (Parse_ast.Unknown,())) in let forwards_spec, env = Type_check.check_val_spec env forwards_spec in let backwards_spec, env = Type_check.check_val_spec env backwards_spec in @@ -4008,7 +4022,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) = let string_defs = begin if subtype_check env typ1 string_typ && subtype_check env string_typ typ1 then let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in - let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in @@ -4018,7 +4032,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) = else if subtype_check env typ2 string_typ && subtype_check env string_typ typ2 then let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in - let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in @@ -4438,6 +4452,7 @@ let minimise_recursive_functions env (Defs defs) = | d -> d in Defs (List.map rewrite_def defs) +(* Move recursive function termination measures into the function definitions. *) let move_termination_measures env (Defs defs) = let scan_for id defs = let rec aux = function @@ -4568,15 +4583,16 @@ let rewrite_explicit_measure env (Defs defs) = | _, P_aux (P_tup ps,_) -> ps | _, _ -> [measure_pat] in - let mk_wrap i (P_aux (p,(l,_))) = + let mk_wrap i (P_aux (p,(l,_)) as p_full) = let id = match p with | P_id id | P_typ (_,(P_aux (P_id id,_))) -> id + | P_lit _ | P_wild | P_typ (_,(P_aux (P_wild,_))) -> mk_id ("_arg" ^ string_of_int i) - | _ -> raise (Reporting.err_todo l "Measure patterns can only be identifiers or wildcards") + | _ -> raise (Reporting.err_todo l ("Measure patterns can only be identifiers or wildcards, not " ^ string_of_pat p_full)) in P_aux (P_id id,(loc,empty_tannot)), E_aux (E_id id,(loc,empty_tannot)) @@ -4614,6 +4630,29 @@ let rewrite_explicit_measure env (Defs defs) = in Defs (List.flatten (List.map rewrite_def defs)) +(* Add a dummy assert to loops for backends that require loops to be able to + fail. Note that the Coq backend will spot the assert and omit it. *) +let rewrite_loops_with_escape_effect env defs = + let dummy_ann = Parse_ast.Unknown,empty_tannot in + let assert_exp = + E_aux (E_assert (E_aux (E_lit (L_aux (L_true,Unknown)),dummy_ann), + E_aux (E_lit (L_aux (L_string "loop dummy assert",Unknown)),dummy_ann)), + dummy_ann) + in + let rewrite_exp rws exp = + let (E_aux (e,ann) as exp) = Rewriter.rewrite_exp rws exp in + match e with + | E_loop (l,(Measure_aux (Measure_some _,_) as m),guard,body) -> + if has_effect (effect_of exp) BE_escape then exp else + let body = match body with + | E_aux (E_block es,ann) -> + E_aux (E_block (assert_exp::es),ann) + | _ -> E_aux (E_block [assert_exp;body],dummy_ann) + in E_aux (E_loop (l,m,guard,body),ann) + | _ -> exp + in + rewrite_defs_base { rewriters_base with rewrite_exp } defs + let recheck_defs env defs = fst (Type_error.check initial_env defs) let recheck_defs_without_effects env defs = let old = !opt_no_effects in @@ -4631,6 +4670,59 @@ let remove_mapping_valspecs env (Defs defs) = Defs (List.filter allowed_def defs) +(* Move loop termination measures into loop AST nodes. This is used before + type checking so that we avoid the complexity of type checking separate + measures. *) +let rec move_loop_measures (Defs defs) = + let loop_measures = + List.fold_left + (fun m d -> + match d with + | DEF_loop_measures (id, measures) -> + (* Allow multiple measure definitions, concatenating them *) + Bindings.add id + (match Bindings.find_opt id m with + | None -> measures + | Some m -> m @ measures) + m + | _ -> m) Bindings.empty defs + in + let do_exp exp_rec measures (E_aux (e,ann) as exp) = + match e, measures with + | E_loop (loop, _, e1, e2), (Loop (loop',exp))::t when loop = loop' -> + let t,e1 = exp_rec t e1 in + let t,e2 = exp_rec t e2 in + t,E_aux (E_loop (loop, Measure_aux (Measure_some exp, exp_loc exp), e1, e2),ann) + | _ -> exp_rec measures exp + in + let do_funcl (m,acc) (FCL_aux (FCL_Funcl (id, pexp),ann) as fcl) = + match Bindings.find_opt id m with + | Some measures -> + let measures,pexp = foldin_pexp do_exp measures pexp in + Bindings.add id measures m, (FCL_aux (FCL_Funcl (id, pexp),ann))::acc + | None -> m, fcl::acc + in + let unused,rev_defs = + List.fold_left + (fun (m,acc) d -> + match d with + | DEF_loop_measures _ -> m, acc + | DEF_fundef (FD_aux (FD_function (r,t,e,fcls),ann)) -> + let m,rfcls = List.fold_left do_funcl (m,[]) fcls in + m, (DEF_fundef (FD_aux (FD_function (r,t,e,List.rev rfcls),ann)))::acc + | _ -> m, d::acc) + (loop_measures,[]) defs + in let () = Bindings.iter + (fun id -> function + | [] -> () + | _::_ -> + Reporting.print_err (id_loc id) "Warning" + ("unused loop measure for function " ^ string_of_id id)) + unused + in Defs (List.rev rev_defs) + + + let opt_mono_rewrites = ref false let opt_mono_complex_nexps = ref true @@ -4750,6 +4842,7 @@ let all_rewrites = [ ("minimise_recursive_functions", Basic_rewriter minimise_recursive_functions); ("move_termination_measures", Basic_rewriter move_termination_measures); ("rewrite_explicit_measure", Basic_rewriter rewrite_explicit_measure); + ("rewrite_loops_with_escape_effect", Basic_rewriter rewrite_loops_with_escape_effect); ("simple_types", Basic_rewriter rewrite_simple_types); ("overload_cast", Basic_rewriter rewrite_overload_cast); ("top_sort_defs", Basic_rewriter (fun _ -> top_sort_defs)); @@ -4844,6 +4937,7 @@ let rewrites_coq = [ ("recheck_defs_without_effects", []); ("make_cases_exhaustive", []); ("rewrite_explicit_measure", []); + ("rewrite_loops_with_escape_effect", []); ("recheck_defs_without_effects", []); ("fix_val_specs", []); ("remove_blocks", []); @@ -4927,6 +5021,8 @@ let rewrites_target tgt = | "sail" -> [] | "latex" -> [] | "interpreter" -> rewrites_interpreter + | "tofrominterp" -> rewrites_interpreter + | "marshal" -> rewrites_interpreter | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Invalid target for rewriting: " ^ tgt)) diff --git a/src/rewrites.mli b/src/rewrites.mli index 330f10b4..e30a4206 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -63,6 +63,9 @@ val opt_dmono_continue : bool ref (* Generate a fresh id with the given prefix *) val fresh_id : string -> l -> id +(* Move loop termination measures into loop AST nodes *) +val move_loop_measures : 'a defs -> 'a defs + (* Re-write undefined to functions created by -undefined_gen flag *) val rewrite_undefined : bool -> Env.t -> tannot defs -> tannot defs diff --git a/src/sail.ml b/src/sail.ml index 4be5279d..14f24251 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -57,6 +57,7 @@ let opt_file_out : string option ref = ref None let opt_interactive_script : string option ref = ref None let opt_print_version = ref false let opt_target = ref None +let opt_tofrominterp_output_dir : string option ref = ref None let opt_memo_z3 = ref false let opt_sanity = ref false let opt_includes_c = ref ([]:string list) @@ -88,6 +89,15 @@ let options = Arg.align ([ ( "-no_warn", Arg.Clear Util.opt_warnings, " do not print warnings"); + ( "-tofrominterp", + set_target "tofrominterp", + " output OCaml functions to translate between shallow embedding and interpreter"); + ( "-tofrominterp_lem", + Arg.Tuple [set_target "tofrominterp"; Arg.Set ToFromInterp_backend.lem_mode], + " output embedding translation for the Lem backend rather than the OCaml backend, implies -tofrominterp"); + ( "-tofrominterp_output_dir", + Arg.String (fun dir -> opt_tofrominterp_output_dir := Some dir), + " set a custom directory to output embedding translation OCaml"); ( "-ocaml", Arg.Tuple [set_target "ocaml"; Arg.Set Initial_check.opt_undefined_gen], " output an OCaml translated version of the input"); @@ -121,6 +131,9 @@ let options = Arg.align ([ ( "-latex_full_valspecs", Arg.Clear Latex.opt_simple_val, " print full valspecs in LaTeX output"); + ( "-marshal", + Arg.Tuple [set_target "marshal"; Arg.Set Initial_check.opt_undefined_gen], + " OCaml-marshal out the rewritten AST to a file"); ( "-ir", set_target "ir", " print intermediate representation"); @@ -351,6 +364,9 @@ let load_files ?check:(check=false) type_envs files = -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in let ast = Process_file.preprocess_ast options ast in let ast = Initial_check.process_ast ~generate:(not check) ast in + (* The separate loop measures declarations would be awkward to type check, so + move them into the definitions beforehand. *) + let ast = Rewrites.move_loop_measures ast in Profile.finish "parsing" t; let t = Profile.start () in @@ -397,6 +413,24 @@ let target name out_name ast type_envs = let out = match !opt_file_out with None -> "out" | Some s -> s in Ocaml_backend.ocaml_compile out ast ocaml_generator_info + | Some "tofrominterp" -> + let out = match !opt_file_out with None -> "out" | Some s -> s in + ToFromInterp_backend.tofrominterp_output !opt_tofrominterp_output_dir out ast + + | Some "marshal" -> + let out_filename = match !opt_file_out with None -> "out" | Some s -> s in + let f = open_out_bin (out_filename ^ ".defs") in + let remove_prover (l, tannot) = + if Type_check.is_empty_tannot tannot then + (l, Type_check.empty_tannot) + else + (l, Type_check.replace_env (Type_check.Env.set_prover None (Type_check.env_of_tannot tannot)) tannot) + in + Marshal.to_string (Ast_util.map_defs_annot remove_prover ast, Type_check.Env.set_prover None type_envs) [Marshal.Compat_32] + |> B64.encode + |> output_string f; + close_out f + | Some "c" -> let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in let ast_c, type_envs = diff --git a/src/smtlib.ml b/src/smtlib.ml index 7748ae20..3ba85306 100644 --- a/src/smtlib.ml +++ b/src/smtlib.ml @@ -383,7 +383,7 @@ let check_counterexample ast env fname args arg_ctyps arg_smt_names = prerr_endline (sprintf "Solver found counterexample: %s" Util.("ok" |> green |> clear)); let counterexample = build_counterexample args arg_ctyps arg_smt_names model in List.iter (fun (id, v) -> prerr_endline (" " ^ string_of_id id ^ " -> " ^ string_of_value v)) counterexample; - let istate = initial_state ast primops in + let istate = initial_state ast env primops in let annot = (Parse_ast.Unknown, Type_check.mk_tannot env bool_typ no_effect) in let call = E_aux (E_app (mk_id "prop", List.map (fun (_, v) -> E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot))) counterexample), annot) in let result = run (Step (lazy "", istate, return call, [])) in diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 80bff0dd..8afc985d 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -205,7 +205,9 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset. | E_for(id,from,to_,by,_,body) -> let _,used,set = list_fv bound used set [from;to_;by] in fv_of_exp consider_var (Nameset.add (string_of_id id) bound) used set body - | E_loop(_, cond, body) -> list_fv bound used set [cond; body] + | E_loop(_, measure, cond, body) -> + let m = match measure with Measure_aux (Measure_some exp,_) -> [exp] | _ -> [] in + list_fv bound used set (m @ [cond; body]) | E_vector_access(v,i) -> list_fv bound used set [v;i] | E_vector_subrange(v,i1,i2) -> list_fv bound used set [v;i1;i2] | E_vector_update(v,i,e) -> list_fv bound used set [v;i;e] @@ -509,6 +511,8 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function ((fun (_,u,_) -> Nameset.singleton ("measure:"^i),u) (fv_of_pes consider_var mt used mt [Pat_aux(Pat_exp (pat,exp),(Unknown,Type_check.empty_tannot))])) + | DEF_loop_measures(id,_) -> + Reporting.unreachable (id_loc id) __POS__ "Loop termination measures should be rewritten before now" let group_defs consider_scatter_as_one (Ast.Defs defs) = @@ -823,7 +827,7 @@ let nexp_subst_fns substs = | E_tuple es -> re (E_tuple (List.map s_exp es)) | E_if (e1,e2,e3) -> re (E_if (s_exp e1, s_exp e2, s_exp e3)) | E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,s_exp e1,s_exp e2,s_exp e3,ord,s_exp e4)) - | E_loop (loop,e1,e2) -> re (E_loop (loop,s_exp e1,s_exp e2)) + | E_loop (loop,m,e1,e2) -> re (E_loop (loop,s_measure m,s_exp e1,s_exp e2)) | E_vector es -> re (E_vector (List.map s_exp es)) | E_vector_access (e1,e2) -> re (E_vector_access (s_exp e1,s_exp e2)) | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (s_exp e1,s_exp e2,s_exp e3)) @@ -846,6 +850,12 @@ let nexp_subst_fns substs = | E_internal_return e -> re (E_internal_return (s_exp e)) | E_throw e -> re (E_throw (s_exp e)) | E_try (e,cases) -> re (E_try (s_exp e, List.map s_pexp cases)) + and s_measure (Measure_aux (m,l)) = + let m = match m with + | Measure_none -> m + | Measure_some exp -> Measure_some (s_exp exp) + in + Measure_aux (m,l) and s_fexp (FE_aux (FE_Fexp (id,e), (l,annot))) = FE_aux (FE_Fexp (id,s_exp e),(l,s_tannot annot)) and s_pexp = function diff --git a/src/specialize.ml b/src/specialize.ml index 7aee3dd0..b2eb5314 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -62,7 +62,7 @@ let is_typ_ord_arg = function type specialization = { is_polymorphic : kinded_id -> bool; instantiation_filter : kid -> typ_arg -> bool; - extern_filter : (string -> string option) -> bool + extern_filter : (string * string) list -> bool } let typ_ord_specialization = { @@ -74,7 +74,7 @@ let typ_ord_specialization = { let int_specialization = { is_polymorphic = is_int_kopt; instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false); - extern_filter = (fun externs -> match externs "c" with Some _ -> true | None -> false) + extern_filter = (fun externs -> match Ast_util.extern_assoc "c" externs with Some _ -> true | None -> false) } let int_specialization_with_externs = { diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml new file mode 100644 index 00000000..d65aaf3b --- /dev/null +++ b/src/toFromInterp_backend.ml @@ -0,0 +1,361 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open PPrint +open Type_check +open Util +open Pretty_print_common +open Ocaml_backend + +let lem_mode = ref false + +let maybe_zencode s = if !lem_mode then String.uncapitalize_ascii s else zencode_string s +let maybe_zencode_upper s = if !lem_mode then String.capitalize_ascii s else zencode_upper_string s + +let frominterp_typedef (TD_aux (td_aux, (l, _))) = + let fromValueArgs (Typ_aux (typ_aux, _)) = match typ_aux with + | Typ_tup typs -> brackets (separate space [string "V_tuple"; brackets (separate (semi ^^ space) (List.mapi (fun i _ -> string ("v" ^ (string_of_int i))) typs))]) + | _ -> brackets (string "v0") + in + let fromValueKid (Kid_aux ((Var name), _)) = + string ("typq_" ^ name) + in + let fromValueNexp ((Nexp_aux (nexp_aux, annot)) as nexp) = match nexp_aux with + | Nexp_constant num -> parens (separate space [string "Big_int.of_string"; dquotes (string (Nat_big_num.to_string num))]) + | Nexp_var var -> fromValueKid var + | Nexp_id id -> string (string_of_id id ^ "FromInterpValue") + | _ -> string ("NEXP(" ^ string_of_nexp nexp ^ ")") + in + let rec fromValueTypArg (A_aux (a_aux, _)) = match a_aux with + | A_typ typ -> fromValueTyp typ "" + | A_nexp nexp -> fromValueNexp nexp + | A_order order -> string ("Order_" ^ (string_of_order order)) + | _ -> string "TYP_ARG" + and fromValueTyp ((Typ_aux (typ_aux, l)) as typ) arg_name = match typ_aux with + | Typ_id id -> parens (concat [string (maybe_zencode (string_of_id id)); string ("FromInterpValue"); space; string arg_name]) + (* special case bit vectors for lem *) + | Typ_app (Id_aux (Id "vector", _), [A_aux (A_nexp len_nexp, _); + A_aux (A_order (Ord_aux (Ord_dec, _)), _); + A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit", _)), _)), _)]) when !lem_mode -> + parens (separate space ([string (maybe_zencode "bitsFromInterpValue"); fromValueNexp len_nexp; string arg_name])) + | Typ_app (typ_id, typ_args) -> + assert (typ_args <> []); + parens (separate space ([string (maybe_zencode (string_of_id typ_id) ^ "FromInterpValue")] @ List.map fromValueTypArg typ_args @ [string arg_name])) + | Typ_var kid -> parens (separate space [fromValueKid kid; string arg_name]) + | Typ_fn _ -> parens (string "failwith \"fromValueTyp: Typ_fn arm unimplemented\"") + | _ -> parens (string "failwith \"fromValueTyp: type arm unimplemented\"") + in + let fromValueVals ((Typ_aux (typ_aux, l)) as typ) = match typ_aux with + | Typ_tup typs -> parens (separate comma_sp (List.mapi (fun i typ -> fromValueTyp typ ("v" ^ (string_of_int i))) typs)) + | _ -> fromValueTyp typ "v0" + in + let fromValueTypq (QI_aux (qi_aux, _)) = match qi_aux with + | QI_id (KOpt_aux (KOpt_kind (K_aux (kind_aux, _), kid), _)) -> fromValueKid kid + | QI_const _ -> empty + in + let fromValueTypqs (TypQ_aux (typq_aux, _)) = match typq_aux with + | TypQ_no_forall -> [empty] + | TypQ_tq quants -> List.map fromValueTypq quants + in + match td_aux with + | TD_variant (id, typq, arms, _) -> + begin match id with + | Id_aux ((Id "read_kind"),_) -> empty + | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "barrier_kind"),_) -> empty + | Id_aux ((Id "trans_kind"),_) -> empty + | Id_aux ((Id "instruction_kind"),_) -> empty + | Id_aux ((Id "cache_op_kind"),_) -> empty + | Id_aux ((Id "regfp"),_) -> empty + | Id_aux ((Id "regfps"),_) -> empty + | Id_aux ((Id "niafp"),_) -> empty + | Id_aux ((Id "niafps"),_) -> empty + | Id_aux ((Id "diafp"),_) -> empty + | Id_aux ((Id "diafps"),_) -> empty + (* | Id_aux ((Id "option"),_) -> empty *) + | Id_aux ((Id id_string), _) + | Id_aux ((Operator id_string), _) -> + if !lem_mode && id_string = "option" then empty else + let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in + let fromFallback = separate space [pipe; underscore; arrow; string "failwith"; + dquotes (string ("invalid interpreter value for " ^ (string_of_id id)))] in + let fromInterpValue = + prefix 2 1 + (separate space [string "let"; fromInterpValueName; separate space (fromValueTypqs typq @ [string "v"]); equals; string "match v with"]) + ((separate_map hardline + (fun (Tu_aux (Tu_ty_id (typ, ctor_id), _)) -> + separate space + [pipe; string "V_ctor"; parens (concat [dquotes (string (string_of_id ctor_id)); comma_sp; + fromValueArgs typ + ]); + arrow; string (maybe_zencode_upper (string_of_id ctor_id)); fromValueVals typ + ] + ) + arms) + ^^ hardline ^^ fromFallback) + in + fromInterpValue ^^ (twice hardline) + end + | TD_abbrev (Id_aux (Id "regfps", _), _, _) -> empty + | TD_abbrev (Id_aux (Id "niafps", _), _, _) -> empty + | TD_abbrev (id, typq, typ_arg) -> + begin + let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in + (* HACK: print a type annotation for abbrevs of unquantified types, to help cases ocaml can't type-infer on its own *) + let fromInterpValspec = + (* HACK because of lem renaming *) + if string_of_id id = "opcode" then empty else + match typ_arg with + | A_aux (A_typ _, _) -> begin match typq with + | TypQ_aux (TypQ_no_forall, _) -> separate space [colon; string "value"; arrow; string (maybe_zencode (string_of_id id))] + | _ -> empty + end + | _ -> empty + in + let fromInterpValue = + (separate space [string "let"; fromInterpValueName; separate space (fromValueTypqs typq); fromInterpValspec; equals; fromValueTypArg typ_arg]) + in + fromInterpValue ^^ (twice hardline) + end + | TD_enum (Id_aux (Id "read_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "write_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "barrier_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "trans_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "cache_op_kind", _), _, _) -> empty + | TD_enum (id, ids, _) -> + let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in + let fromFallback = separate space [pipe; underscore; arrow; string "failwith"; + dquotes (string ("invalid interpreter value for " ^ (string_of_id id)))] in + let fromInterpValue = + prefix 2 1 + (separate space [string "let"; fromInterpValueName; string "v"; equals; string "match v with"]) + ((separate_map hardline + (fun id -> + separate space + [pipe; string "V_ctor"; parens (concat [dquotes (string (string_of_id id)); comma_sp; string "[]"]); + arrow; string (maybe_zencode_upper (string_of_id id))] + ) + ids) + ^^ hardline ^^ fromFallback) + in + fromInterpValue ^^ (twice hardline) + | TD_record (record_id, typq, fields, _) -> + let fromInterpField (typ, id) = + separate space [string (maybe_zencode ((if !lem_mode then string_of_id record_id ^ "_" else "") ^ string_of_id id)); equals; fromValueTyp typ ("(StringMap.find \"" ^ (string_of_id id) ^ "\" fs)")] + in + let fromInterpValueName = concat [string (maybe_zencode (string_of_id record_id)); string "FromInterpValue"] in + let fromFallback = separate space [pipe; underscore; arrow; string "failwith"; + dquotes (string ("invalid interpreter value for " ^ (string_of_id record_id)))] in + let fromInterpValue = + prefix 2 1 + (separate space [string "let"; fromInterpValueName; separate space (fromValueTypqs typq @ [string "v"]); equals; string "match v with"]) + ((separate space [pipe; string "V_record fs"; arrow; braces (separate_map (semi ^^ space) fromInterpField fields)]) + ^^ hardline ^^ fromFallback) + in + fromInterpValue ^^ (twice hardline) + | _ -> empty + +let tointerp_typedef (TD_aux (td_aux, (l, _))) = + let toValueArgs (Typ_aux (typ_aux, _)) = match typ_aux with + | Typ_tup typs -> parens (separate comma_sp (List.mapi (fun i _ -> string ("v" ^ (string_of_int i))) typs)) + | _ -> parens (string "v0") + in + let toValueKid (Kid_aux ((Var name), _)) = + string ("typq_" ^ name) + in + let toValueNexp ((Nexp_aux (nexp_aux, _)) as nexp) = match nexp_aux with + | Nexp_constant num -> parens (separate space [string "Big_int.of_string"; dquotes (string (Nat_big_num.to_string num))]) + | Nexp_var var -> toValueKid var + | Nexp_id id -> string (string_of_id id ^ "ToInterpValue") + | _ -> string ("NEXP(" ^ string_of_nexp nexp ^ ")") + in + let rec toValueTypArg (A_aux (a_aux, _)) = match a_aux with + | A_typ typ -> toValueTyp typ "" + | A_nexp nexp -> toValueNexp nexp + | A_order order -> string ("Order_" ^ (string_of_order order)) + | _ -> string "TYP_ARG" + and toValueTyp ((Typ_aux (typ_aux, l)) as typ) arg_name = match typ_aux with + | Typ_id id -> parens (concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"; space; string arg_name]) + (* special case bit vectors for lem *) + | Typ_app (Id_aux (Id "vector", _), [A_aux (A_nexp len_nexp, _); + A_aux (A_order (Ord_aux (Ord_dec, _)), _); + A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit", _)), _)), _)]) when !lem_mode -> + parens (separate space ([string (maybe_zencode "bitsToInterpValue"); toValueNexp len_nexp; string arg_name])) + | Typ_app (typ_id, typ_args) -> + assert (typ_args <> []); + parens (separate space ([string ((maybe_zencode (string_of_id typ_id)) ^ "ToInterpValue")] @ List.map toValueTypArg typ_args @ [string arg_name])) + | Typ_var kid -> parens (separate space [toValueKid kid; string arg_name]) + | _ -> parens (string "failwith \"toValueTyp: type arm unimplemented\"") + in + let toValueVals ((Typ_aux (typ_aux, _)) as typ) = match typ_aux with + | Typ_tup typs -> brackets (separate space [string "V_tuple"; brackets (separate (semi ^^ space) (List.mapi (fun i typ -> toValueTyp typ ("v" ^ (string_of_int i))) typs))]) + | _ -> brackets (toValueTyp typ "v0") + in + let toValueTypq (QI_aux (qi_aux, _)) = match qi_aux with + | QI_id (KOpt_aux (KOpt_kind (K_aux (kind_aux, _), kid), _)) -> toValueKid kid + | QI_const _ -> empty + in + let toValueTypqs (TypQ_aux (typq_aux, _)) = match typq_aux with + | TypQ_no_forall -> [empty] + | TypQ_tq quants -> List.map toValueTypq quants + in + match td_aux with + | TD_variant (id, typq, arms, _) -> + begin match id with + | Id_aux ((Id "read_kind"),_) -> empty + | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "barrier_kind"),_) -> empty + | Id_aux ((Id "trans_kind"),_) -> empty + | Id_aux ((Id "instruction_kind"),_) -> empty + | Id_aux ((Id "cache_op_kind"),_) -> empty + | Id_aux ((Id "regfp"),_) -> empty + | Id_aux ((Id "regfps"),_) -> empty + | Id_aux ((Id "niafp"),_) -> empty + | Id_aux ((Id "niafps"),_) -> empty + | Id_aux ((Id "diafp"),_) -> empty + | Id_aux ((Id "diafps"),_) -> empty + (* | Id_aux ((Id "option"),_) -> empty *) + | Id_aux ((Id id_string), _) + | Id_aux ((Operator id_string), _) -> + if !lem_mode && id_string = "option" then empty else + let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in + let toInterpValue = + prefix 2 1 + (separate space [string "let"; toInterpValueName; separate space (toValueTypqs typq @ [string "v"]); equals; string "match v with"]) + ((separate_map hardline + (fun (Tu_aux (Tu_ty_id (typ, ctor_id), _)) -> + separate space + [pipe; string (maybe_zencode_upper (string_of_id ctor_id)); toValueArgs typ; + arrow; string "V_ctor"; parens (concat [dquotes (string (string_of_id ctor_id)); comma_sp; toValueVals typ]) + ] + ) + arms)) + in + toInterpValue ^^ (twice hardline) + end + | TD_abbrev (Id_aux (Id "regfps", _), _, _) -> empty + | TD_abbrev (Id_aux (Id "niafps", _), _, _) -> empty + | TD_abbrev (id, typq, typ_arg) -> + begin + let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in + (* HACK: print a type annotation for abbrevs of unquantified types, to help cases ocaml can't type-infer on its own *) + let toInterpValspec = + (* HACK because of lem renaming *) + if string_of_id id = "opcode" then empty else + match typ_arg with + | A_aux (A_typ _, _) -> begin match typq with + | TypQ_aux (TypQ_no_forall, _) -> separate space [colon; string (maybe_zencode (string_of_id id)); arrow; string "value"] + | _ -> empty + end + | _ -> empty + in + let toInterpValue = + (separate space [string "let"; toInterpValueName; separate space (toValueTypqs typq); toInterpValspec; equals; toValueTypArg typ_arg]) + in + toInterpValue ^^ (twice hardline) + end + | TD_enum (Id_aux (Id "read_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "write_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "barrier_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "trans_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "cache_op_kind", _), _, _) -> empty + | TD_enum (id, ids, _) -> + let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in + let toInterpValue = + prefix 2 1 + (separate space [string "let"; toInterpValueName; string "v"; equals; string "match v with"]) + ((separate_map hardline + (fun id -> + separate space + [pipe; string (maybe_zencode_upper (string_of_id id)); + arrow; string "V_ctor"; parens (concat [dquotes (string (string_of_id id)); comma_sp; string "[]"])] + ) + ids)) + in + toInterpValue ^^ (twice hardline) + | TD_record (record_id, typq, fields, _) -> + let toInterpField (typ, id) = + parens (separate comma_sp [dquotes (string (string_of_id id)); toValueTyp typ ("r." ^ (maybe_zencode ((if !lem_mode then string_of_id record_id ^ "_" else "") ^ string_of_id id)))]) + in + let toInterpValueName = concat [string (maybe_zencode (string_of_id record_id)); string "ToInterpValue"] in + let toInterpValue = + prefix 2 1 + (separate space [string "let"; toInterpValueName; separate space (toValueTypqs typq @ [string "r"]); equals]) + (separate space [string "V_record"; parens (separate space [string "List.fold_left (fun m (k, v) -> StringMap.add k v m) StringMap.empty"; (brackets (separate_map (semi ^^ space) toInterpField fields))])]) + in + toInterpValue ^^ (twice hardline) + | _ -> empty + + +let tofrominterp_def def = match def with + | DEF_type td -> group (frominterp_typedef td ^^ twice hardline ^^ tointerp_typedef td ^^ twice hardline) + | _ -> empty + +let tofrominterp_defs name (Defs defs) = + (string "open Sail_lib;;" ^^ hardline) + ^^ (string "open Value;;" ^^ hardline) + ^^ (string "open ToFromInterp_lib;;" ^^ hardline) + ^^ (if !lem_mode then (string "open Sail2_instr_kinds;;" ^^ hardline) else empty) + ^^ (string ("open " ^ String.capitalize_ascii name ^ ";;") ^^ hardline) + ^^ (if !lem_mode then (string ("open " ^ String.capitalize_ascii name ^ "_types;;") ^^ hardline) else empty) + ^^ (if !lem_mode then (string ("open " ^ String.capitalize_ascii name ^ "_extras;;") ^^ hardline) else empty) + ^^ (string "module Big_int = Nat_big_num" ^^ ocaml_def_end) + ^^ concat (List.map tofrominterp_def defs) + +let tofrominterp_pp_defs name f defs = + ToChannel.pretty 1. 80 f (tofrominterp_defs name defs) + +let tofrominterp_output maybe_dir name defs = + let dir = match maybe_dir with Some dir -> dir | None -> "." in + let out_chan = open_out (Filename.concat dir (name ^ "_toFromInterp2.ml")) in + tofrominterp_pp_defs name out_chan defs; + close_out out_chan diff --git a/src/toFromInterp_lib.ml b/src/toFromInterp_lib.ml new file mode 100644 index 00000000..c29fcd84 --- /dev/null +++ b/src/toFromInterp_lib.ml @@ -0,0 +1,126 @@ +(************************************************************) +(* Support for toFromInterp *) +(************************************************************) + +open Sail_lib;; +open Value;; + +type vector_order = + | Order_inc + | Order_dec + +(* zencoded variants are for the OCaml backend, non-zencoded are for the Lem backend compiled to OCaml. + Sometimes they're just aliased. *) + +let zunitFromInterpValue v = match v with + | V_unit -> () + | _ -> failwith "invalid interpreter value for unit" + +let zunitToInterpValue () = V_unit + +let unitFromInterpValue = zunitFromInterpValue +let unitToInterpValue = zunitToInterpValue + +let zatomFromInterpValue typq_'n v = match v with + | V_int i when typq_'n = i -> i + | _ -> failwith "invalid interpreter value for atom" + +let zatomToInterpValue typq_'n v = + assert (typq_'n = v); + V_int v + +let atomFromInterpValue = zatomFromInterpValue +let atomToInterpValue = zatomToInterpValue + +let zintFromInterpValue v = match v with + | V_int i -> i + | _ -> failwith "invalid interpreter value for int" + +let zintToInterpValue v = V_int v + +let intFromInterpValue = zintFromInterpValue +let intToInterpValue = zintToInterpValue + +let znatFromInterpValue v = match v with + | V_int i when i >= Big_int.zero -> i + | _ -> failwith "invalid interpreter value for nat" + +let znatToInterpValue v = + assert (v >= Big_int.zero); + V_int v + +let natFromInterpValue = znatFromInterpValue +let natToInterpValue = znatToInterpValue + + +let zboolFromInterpValue v = match v with + | V_bool b -> b + | _ -> failwith "invalid interpreter value for bool" + +let zboolToInterpValue v = V_bool v + +let boolFromInterpValue = zboolFromInterpValue +let boolToInterpValue = zboolToInterpValue + +let zstringFromInterpValue v = match v with + | V_string s -> s + | _ -> failwith "invalid interpreter value for string" + +let zstringToInterpValue v = V_string v + +let stringFromInterpValue = zstringFromInterpValue +let stringToInterpValue = zstringToInterpValue + +let zlistFromInterpValue typq_'a v = match v with + | V_list vs -> List.map typq_'a vs + | _ -> failwith "invalid interpreter value for list" + +let zlistToInterpValue typq_'a v = V_list (List.map typq_'a v) + +let listFromInterpValue = zlistFromInterpValue +let listToInterpValue = zlistToInterpValue + +let zvectorFromInterpValue typq_'n typq_'ord typq_'a v = match v with + | V_vector vs -> + assert (Big_int.of_int (List.length vs) = typq_'n); + List.map typq_'a vs + | _ -> failwith "invalid interpreter value for vector" + +let zvectorToInterpValue typq_'n typq_'ord typq_'a v = + assert (Big_int.of_int (List.length v) = typq_'n); + V_vector (List.map typq_'a v) + +let vectorFromInterpValue = zvectorFromInterpValue +let vectorToInterpValue = zvectorToInterpValue + +let zbitFromInterpValue v = match v with + | V_bit b -> b + | _ -> failwith "invalid interpreter value for bit" + +let zbitToInterpValue v = V_bit v + +let bitFromInterpValue = zbitFromInterpValue +let bitToInterpValue = zbitToInterpValue + +let optionFromInterpValue typq_'a v = match v with + | V_ctor ("None", [v0]) -> None + | V_ctor ("Some", [v0]) -> Some (typq_'a v0) + | _ -> failwith "invalid interpreter value for option" + +let optionToInterpValue typq_'a v = match v with + | None -> V_ctor ("None", [(unitToInterpValue ())]) + | Some (v0) -> V_ctor ("Some", [(typq_'a v0)]) + + +let bitsFromInterpValue typq_'n v = match v with + | V_vector vs -> + assert (Big_int.of_int (List.length vs) = typq_'n); + Lem.wordFromBitlist (List.map (fun b -> bitFromInterpValue b |> Sail_lib.bool_of_bit) vs) + | _ -> failwith "invalid interpreter value for bits" + +let bitsToInterpValue typq_'n v = + let bs = Lem.bitlistFromWord v in + assert (Big_int.of_int (List.length bs) = typq_'n); + V_vector (List.map (fun b -> Sail_lib.bit_of_bool b |> bitToInterpValue) bs) + + diff --git a/src/type_check.ml b/src/type_check.ml index d5d42316..ec5258d6 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -117,11 +117,10 @@ type env = shadow_vars : int KBindings.t; typ_synonyms : (typquant * typ_arg) Bindings.t; overloads : (id list) Bindings.t; - flow : (typ -> typ) Bindings.t; enums : IdSet.t Bindings.t; records : (typquant * (typ * id) list) Bindings.t; accessors : (typquant * typ) Bindings.t; - externs : (string -> string option) Bindings.t; + externs : (string * string) list Bindings.t; casts : id list; allow_casts : bool; allow_bindings : bool; @@ -129,7 +128,7 @@ type env = default_order : order option; ret_typ : typ option; poly_undefineds : bool; - prove : env -> n_constraint -> bool; + prove : (env -> n_constraint -> bool) option; allow_unknowns : bool; } @@ -422,9 +421,6 @@ module Env : sig val add_mapping : id -> typquant * typ * typ -> t -> t val add_union_id : id -> typquant * typ -> t -> t val get_union_id : id -> t -> typquant * typ - 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 -> effect * effect * typ val add_register : id -> effect -> effect -> typ -> t -> t @@ -444,7 +440,7 @@ module Env : sig val add_overloads : id -> id list -> t -> t val get_overloads : id -> t -> id list val is_extern : id -> t -> string -> bool - val add_extern : id -> (string -> string option) -> t -> t + val add_extern : id -> (string * string) list -> t -> t val get_extern : id -> t -> string -> string val get_default_order : t -> order val set_default_order : order_aux -> t -> t @@ -479,7 +475,7 @@ module Env : sig which is defined below. To break the circularity this would cause (as the prove code depends on the environment), we add a reference to the prover to the initial environment. *) - val add_prover : (t -> n_constraint -> bool) -> t -> t + val set_prover : (t -> n_constraint -> bool) option -> t -> t (* This must not be exported, initial_env sets up a correct initial environment. *) @@ -504,7 +500,6 @@ end = struct shadow_vars = KBindings.empty; typ_synonyms = Bindings.empty; overloads = Bindings.empty; - flow = Bindings.empty; enums = Bindings.empty; records = Bindings.empty; accessors = Bindings.empty; @@ -516,11 +511,11 @@ end = struct default_order = None; ret_typ = None; poly_undefineds = false; - prove = (fun _ _ -> false); + prove = None; allow_unknowns = false; } - let add_prover f env = { env with prove = f } + let set_prover f env = { env with prove = f } let allow_unknowns env = env.allow_unknowns let set_allow_unknowns b env = { env with allow_unknowns = b } @@ -614,7 +609,7 @@ end = struct | _, _ -> typ_error env Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq) in let ncs = subst_args kopts args in - if List.for_all (env.prove env) ncs + if (match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false) then () else typ_error env (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id) @@ -653,7 +648,7 @@ end = struct in fun l env args -> let typ_arg, ncs = subst_args env l kopts args in - if List.for_all (env.prove env) ncs + if (match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false) then typ_arg else typ_error env l ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs ^ " in type synonym " ^ string_of_typ_arg typ_arg @@ -1144,17 +1139,6 @@ end = struct match Bindings.find_opt id env.variants with | Some (typq, tus) -> typq, tus | None -> typ_error env (id_loc id) ("union " ^ string_of_id id ^ " not found") - let get_flow id env = - try Bindings.find id env.flow with - | Not_found -> fun typ -> typ - - let add_flow id f env = - 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 @@ -1164,7 +1148,7 @@ end = struct | Not_found -> typ_error env (id_loc id) ("No register binding found for " ^ string_of_id id) let is_extern id env backend = - try not (Bindings.find id env.externs backend = None) with + try not (Ast_util.extern_assoc backend (Bindings.find id env.externs) = None) with | Not_found -> false (* Bindings.mem id env.externs *) @@ -1173,7 +1157,7 @@ end = struct let get_extern id env backend = try - match Bindings.find id env.externs backend with + match Ast_util.extern_assoc backend (Bindings.find id env.externs) with | Some ext -> ext | None -> typ_error env (id_loc id) ("No extern binding found for " ^ string_of_id id) with @@ -1196,8 +1180,7 @@ end = struct 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, if raw then typ else flow typ) + Local (mut, typ) with | Not_found -> try @@ -2423,6 +2406,14 @@ let env_of_annot (l, tannot) = match tannot with | Some t -> t.env | None -> raise (Reporting.err_unreachable l __POS__ "no type annotation") +let env_of_tannot tannot = match tannot with + | Some t -> t.env + | None -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "no type annotation") + +let typ_of_tannot tannot = match tannot with + | Some t -> t.typ + | None -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "no type annotation") + let env_of (E_aux (_, (l, tannot))) = env_of_annot (l, tannot) let typ_of_annot (l, tannot) = match tannot with @@ -3475,7 +3466,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = begin match Env.lookup_id ~raw:true v env with | Local (Immutable, _) | Enum _ -> typ_error env 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.remove_flow v env + | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env | Register (_, weff, vtyp) -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ weff, env | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env end @@ -3696,10 +3687,15 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = in try_overload ([], Env.get_overloads f env) | E_app (f, xs) -> infer_funapp l env f xs None - | E_loop (loop_type, cond, body) -> + | E_loop (loop_type, measure, cond, body) -> let checked_cond = crule check_exp env cond bool_typ in + let checked_measure = match measure with + | Measure_aux (Measure_none,l) -> Measure_aux (Measure_none,l) + | Measure_aux (Measure_some exp,l) -> + Measure_aux (Measure_some (crule check_exp env exp int_typ),l) + in let checked_body = crule check_exp (add_opt_constraint (assert_constraint env true checked_cond) env) body unit_typ in - annot_exp (E_loop (loop_type, checked_cond, checked_body)) unit_typ + annot_exp (E_loop (loop_type, checked_measure, checked_cond, checked_body)) unit_typ | E_for (v, f, t, step, ord, body) -> begin let f, t, is_dec = match ord with @@ -4372,10 +4368,18 @@ and propagate_exp_effect_aux = function let p_body = propagate_exp_effect body in E_for (v, p_f, p_t, p_step, ord, p_body), collect_effects [p_f; p_t; p_step; p_body] - | E_loop (loop_type, cond, body) -> + | E_loop (loop_type, measure, cond, body) -> let p_cond = propagate_exp_effect cond in + let () = match measure with + | Measure_aux (Measure_some exp,l) -> + let eff = effect_of (propagate_exp_effect exp) in + if (BESet.is_empty (effect_set eff) || !opt_no_effects) + then () + else typ_error (env_of exp) l ("Loop termination measure with effects " ^ string_of_effect eff) + | _ -> () + in let p_body = propagate_exp_effect body in - E_loop (loop_type, p_cond, p_body), + E_loop (loop_type, measure, p_cond, p_body), union_effects (effect_of p_cond) (effect_of p_body) | E_let (letbind, exp) -> let p_lb, eff = propagate_letbind_effect letbind in @@ -4744,7 +4748,7 @@ let mk_val_spec env typq typ id = | Typ_aux (Typ_fn (_,_,eff),_) -> eff | _ -> no_effect in - DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, (fun _ -> None), false), (Parse_ast.Unknown, mk_tannot env typ eff))) + DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, [], false), (Parse_ast.Unknown, mk_tannot env typ eff))) let check_tannotopt env typq ret_typ = function | Typ_annot_opt_aux (Typ_annot_opt_none, _) -> () @@ -4864,9 +4868,9 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md let check_val_spec env (VS_aux (vs, (l, _))) = let annotate vs typ eff = DEF_spec (VS_aux (vs, (l, mk_tannot env typ eff))) in let vs, id, typq, typ, env = match vs with - | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, ext_opt, is_cast) -> + | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, exts, is_cast) -> typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm)); - let env = Env.add_extern id ext_opt env in + let env = Env.add_extern id exts env in let env = if is_cast then Env.add_cast id env else env in let typq', typ' = expand_bind_synonyms ts_l env (typq, typ) in (* !opt_expand_valspec controls whether the actual valspec in @@ -4878,7 +4882,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) = else (typq, typ) in - let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in + let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, exts, is_cast) in (vs, id, typq', typ', env) in let eff = @@ -5016,6 +5020,9 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err () | DEF_scattered sdef -> check_scattered env sdef | DEF_measure (id, pat, exp) -> [check_termination_measure_decl env (id, pat, exp)], env + | DEF_loop_measures (id, _) -> + Reporting.unreachable (id_loc id) __POS__ + "Loop termination measures should have been rewritten before type checking" and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot defs * Env.t = fun n total env defs -> @@ -5040,14 +5047,14 @@ and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list let initial_env = Env.empty - |> Env.add_prover (prove __POS__) - |> Env.add_extern (mk_id "size_itself_int") (fun _ -> Some "size_itself_int") + |> Env.set_prover (Some (prove __POS__)) + |> Env.add_extern (mk_id "size_itself_int") [("_", "size_itself_int")] |> Env.add_val_spec (mk_id "size_itself_int") (TypQ_aux (TypQ_tq [QI_aux (QI_id (mk_kopt K_int (mk_kid "n")), Parse_ast.Unknown)],Parse_ast.Unknown), function_typ [app_typ (mk_id "itself") [mk_typ_arg (A_nexp (nvar (mk_kid "n")))]] (atom_typ (nvar (mk_kid "n"))) no_effect) - |> Env.add_extern (mk_id "make_the_value") (fun _ -> Some "make_the_value") + |> Env.add_extern (mk_id "make_the_value") [("_", "make_the_value")] |> Env.add_val_spec (mk_id "make_the_value") (TypQ_aux (TypQ_tq [QI_aux (QI_id (mk_kopt K_int (mk_kid "n")), Parse_ast.Unknown)],Parse_ast.Unknown), diff --git a/src/type_check.mli b/src/type_check.mli index 737e714e..dcedcc90 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -221,6 +221,8 @@ module Env : sig val builtin_typs : typquant Bindings.t val get_union_id : id -> t -> typquant * typ + + val set_prover : (t -> n_constraint -> bool) option -> t -> t end (** {4 Environment helper functions} *) @@ -317,6 +319,8 @@ val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t +val assert_constraint : Env.t -> bool -> tannot exp -> n_constraint option + (** Attempt to prove a constraint using z3. Returns true if z3 can prove that the constraint is true, returns false if z3 cannot prove the constraint true. Note that this does not guarantee that the @@ -347,9 +351,11 @@ val typ_error : Env.t -> Ast.l -> string -> 'a val env_of : tannot exp -> Env.t val env_of_annot : Ast.l * tannot -> Env.t +val env_of_tannot : tannot -> Env.t val typ_of : tannot exp -> typ val typ_of_annot : Ast.l * tannot -> typ +val typ_of_tannot : tannot -> typ val typ_of_pat : tannot pat -> typ val env_of_pat : tannot pat -> Env.t @@ -424,6 +430,8 @@ val propagate_exp_effect : tannot exp -> tannot exp val propagate_pexp_effect : tannot pexp -> tannot pexp * effect +val big_int_of_nexp : nexp -> Big_int.num option + (** {2 Checking full ASTs} *) (** Fully type-check an AST diff --git a/src/value.ml b/src/value.ml index 6f5148e4..7a65f6ea 100644 --- a/src/value.ml +++ b/src/value.ml @@ -302,6 +302,10 @@ let value_or_vec = function | [v1; v2] -> mk_vector (Sail_lib.or_vec (coerce_bv v1, coerce_bv v2)) | _ -> failwith "value not_vec" +let value_xor_vec = function + | [v1; v2] -> mk_vector (Sail_lib.xor_vec (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value xor_vec" + let value_uint = function | [v] -> V_int (Sail_lib.uint (coerce_bv v)) | _ -> failwith "value uint" @@ -341,6 +345,14 @@ let value_negate = function | [v1] -> V_int (Sail_lib.negate (coerce_int v1)) | _ -> failwith "value negate" +let value_pow2 = function + | [v1] -> V_int (Sail_lib.pow2 (coerce_int v1)) + | _ -> failwith "value pow2" + +let value_int_power = function + | [v1; v2] -> V_int (Sail_lib.int_power (coerce_int v1, coerce_int v2)) + | _ -> failwith "value int_power" + let value_mult = function | [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2)) | _ -> failwith "value mult" @@ -363,7 +375,7 @@ let value_add_vec_int = function let value_sub_vec_int = function | [v1; v2] -> mk_vector (Sail_lib.sub_vec_int (coerce_bv v1, coerce_int v2)) - | _ -> failwith "value add_vec_int" + | _ -> failwith "value sub_vec_int" let value_add_vec = function | [v1; v2] -> mk_vector (Sail_lib.add_vec (coerce_bv v1, coerce_bv v2)) @@ -417,6 +429,14 @@ let value_shiftr = function | [v1; v2] -> mk_vector (Sail_lib.shiftr (coerce_bv v1, coerce_int v2)) | _ -> failwith "value shiftr" +let value_shift_bits_left = function + | [v1; v2] -> mk_vector (Sail_lib.shift_bits_left (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value shift_bits_left" + +let value_shift_bits_right = function + | [v1; v2] -> mk_vector (Sail_lib.shift_bits_right (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value shift_bits_right" + let value_vector_truncate = function | [v1; v2] -> mk_vector (Sail_lib.vector_truncate (coerce_bv v1, coerce_int v2)) | _ -> failwith "value vector_truncate" @@ -524,6 +544,14 @@ let value_round_down = function | [v] -> V_int (Sail_lib.round_down (coerce_real v)) | _ -> failwith "value round_down" +let value_quot_round_zero = function + | [v1; v2] -> V_int (Sail_lib.quot_round_zero (coerce_int v1, coerce_int v2)) + | _ -> failwith "value quot_round_zero" + +let value_rem_round_zero = function + | [v1; v2] -> V_int (Sail_lib.rem_round_zero (coerce_int v1, coerce_int v2)) + | _ -> failwith "value rem_round_zero" + let value_add_real = function | [v1; v2] -> V_real (Sail_lib.add_real (coerce_real v1, coerce_real v2)) | _ -> failwith "value add_real" @@ -568,6 +596,10 @@ let value_string_append = function | [v1; v2] -> V_string (Sail_lib.string_append (coerce_string v1, coerce_string v2)) | _ -> failwith "value string_append" +let value_decimal_string_of_bits = function + | [v] -> V_string (Sail_lib.decimal_string_of_bits (coerce_bv v)) + | _ -> failwith "value decimal_string_of_bits" + let primops = List.fold_left (fun r (x, y) -> StringMap.add x y r) @@ -582,6 +614,7 @@ let primops = ("putchar", value_putchar); ("string_of_int", fun vs -> V_string (string_of_value (List.hd vs))); ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs))); + ("decimal_string_of_bits", value_decimal_string_of_bits); ("print_bits", value_print_bits); ("print_int", value_print_int); ("print_string", value_print_string); @@ -614,6 +647,7 @@ let primops = ("not_vec", value_not_vec); ("and_vec", value_and_vec); ("or_vec", value_or_vec); + ("xor_vec", value_xor_vec); ("uint", value_uint); ("sint", value_sint); ("get_slice_int", value_get_slice_int); @@ -625,6 +659,8 @@ let primops = ("zeros", value_zeros); ("shiftr", value_shiftr); ("shiftl", value_shiftl); + ("shift_bits_left", value_shift_bits_left); + ("shift_bits_right", value_shift_bits_right); ("add_int", value_add_int); ("sub_int", value_sub_int); ("div_int", value_quotient); @@ -633,6 +669,8 @@ let primops = ("quotient", value_quotient); ("modulus", value_modulus); ("negate", value_negate); + ("pow2", value_pow2); + ("int_power", value_int_power); ("shr_int", value_shr_int); ("shl_int", value_shl_int); ("max_int", value_max_int); @@ -661,7 +699,9 @@ let primops = ("mult_real", value_mult_real); ("round_up", value_round_up); ("round_down", value_round_down); - ("quotient_real", value_div_real); + ("quot_round_zero", value_quot_round_zero); + ("rem_round_zero", value_rem_round_zero); + ("quotient_real", value_quotient_real); ("abs_real", value_abs_real); ("div_real", value_div_real); ("sqrt_real", value_sqrt_real); @@ -681,4 +721,5 @@ let primops = ("string_length", value_string_length); ("string_startswith", value_string_startswith); ("string_drop", value_string_drop); + ("skip", fun _ -> V_unit); ] |