diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/anf.ml | 2 | ||||
| -rw-r--r-- | src/jib/c_backend.ml | 74 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 32 | ||||
| -rw-r--r-- | src/jib/jib_optimize.ml | 8 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 24 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 8 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 133 | ||||
| -rw-r--r-- | src/property.ml | 2 | ||||
| -rw-r--r-- | src/smtlib.ml | 14 | ||||
| -rw-r--r-- | src/type_check.ml | 2 |
10 files changed, 168 insertions, 131 deletions
diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 331fed83..7c6eee3e 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -663,7 +663,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (mk_aexp (AE_app (mk_id "__assert", [aval1; aval2], unit_typ)))) + wrap1 (wrap2 (mk_aexp (AE_app (mk_id "sail_assert", [aval1; aval2], unit_typ)))) | E_cons (exp1, exp2) -> let aexp1 = anf exp1 in diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 1b9fa1dd..6b264a48 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -407,7 +407,7 @@ let analyze_primop' ctx id args typ = c_debug (lazy ("Analyzing primop " ^ extern ^ "(" ^ Util.string_of_list ", " (fun aval -> Pretty_print_sail.to_string (pp_aval aval)) args ^ ")")); match extern, args with - (* + (* | "eq_bits", [AV_cval (v1, _); AV_cval (v2, _)] -> begin match cval_ctyp v1 with | CT_fbits _ -> @@ -444,9 +444,9 @@ let analyze_primop' ctx id args typ = when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> begin match cval_ctyp v1 with | CT_fbits _ -> - AE_val (AV_C_fragment (v1, typ, CT_fbits (Big_int.to_int n, true))) + AE_val (AV_cval (v1, typ, CT_fbits (Big_int.to_int n, true))) | CT_sbits _ -> - AE_val (AV_C_fragment (F_call ("fast_zero_extend", [v1; v_int (Big_int.to_int n)]), typ, CT_fbits (Big_int.to_int n, true))) + AE_val (AV_cval (F_call ("fast_zero_extend", [v1; v_int (Big_int.to_int n)]), typ, CT_fbits (Big_int.to_int n, true))) end | _ -> no_change end @@ -1142,18 +1142,76 @@ let rec sgen_ctyp_name = function | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *) | CT_constant _ -> "CONSTANT" -let sgen_cval cval = string_of_cval cval +let rec sgen_cval = function + | V_id (id, ctyp) -> string_of_name id + | V_ref (id, _) -> "&" ^ string_of_name id + | V_lit (vl, ctyp) -> string_of_value vl + | V_call (op, cvals) -> sgen_call op cvals + | V_field (f, field) -> + Printf.sprintf "%s.%s" (sgen_cval f) field + | V_tuple_member (f, _, n) -> + Printf.sprintf "%s.ztup%d" (sgen_cval f) n + | V_ctor_kind (f, ctor, [], _) -> + sgen_cval f ^ ".kind" + ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor) + | V_ctor_kind (f, ctor, unifiers, _) -> + sgen_cval f ^ ".kind" + ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers) + | V_ctor_unwrap (ctor, f, [], _) -> + Printf.sprintf "%s.%s" (sgen_cval f) (Util.zencode_string (string_of_id ctor)) + | V_struct (fields, _) -> + Printf.sprintf "{%s}" + (Util.string_of_list ", " (fun (field, cval) -> string_of_id field ^ " = " ^ sgen_cval cval) fields) + | V_ctor_unwrap (ctor, f, unifiers, _) -> + Printf.sprintf "%s.%s" + (sgen_cval f) + (Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)) + | V_poly (f, _) -> sgen_cval f + +and sgen_call op cvals = + match op, cvals with + | Bnot, [v] -> "!(" ^ sgen_cval v ^ ")" + | List_hd, [v] -> + Printf.sprintf "(%s).hd" ("*" ^ sgen_cval v) + | List_tl, [v] -> + Printf.sprintf "(%s).tl" ("*" ^ sgen_cval v) + | Eq, [v1; v2] -> + Printf.sprintf "(%s == %s)" (sgen_cval v1) (sgen_cval v2) + | Neq, [v1; v2] -> + Printf.sprintf "(%s != %s)" (sgen_cval v1) (sgen_cval v2) + | Ilt, [v1; v2] -> + Printf.sprintf "(%s < %s)" (sgen_cval v1) (sgen_cval v2) + | Igt, [v1; v2] -> + Printf.sprintf "(%s > %s)" (sgen_cval v1) (sgen_cval v2) + | Ilteq, [v1; v2] -> + Printf.sprintf "(%s <= %s)" (sgen_cval v1) (sgen_cval v2) + | Igteq, [v1; v2] -> + Printf.sprintf "(%s >= %s)" (sgen_cval v1) (sgen_cval v2) + | Iadd, [v1; v2] -> + Printf.sprintf "(%s + %s)" (sgen_cval v1) (sgen_cval v2) + | Isub, [v1; v2] -> + Printf.sprintf "(%s - %s)" (sgen_cval v1) (sgen_cval v2) + | Bvand, [v1; v2] -> + Printf.sprintf "(%s & %s)" (sgen_cval v1) (sgen_cval v2) + | Bvor, [v1; v2] -> + Printf.sprintf "(%s | %s)" (sgen_cval v1) (sgen_cval v2) + | Zero_extend n, [v] -> + Printf.sprintf "fast_zero_extend(%d, %s)" n (sgen_cval v) + | Sign_extend n, [v] -> + Printf.sprintf "fast_sign_extend(%d, %s)" n (sgen_cval v) + | _, vs -> + Printf.sprintf "%s(%s)" (string_of_op op) (Util.string_of_list ", " sgen_cval cvals) let sgen_cval_param cval = match cval_ctyp cval with | CT_lbits direction -> - string_of_cval cval ^ ", " ^ string_of_bool direction + sgen_cval cval ^ ", " ^ string_of_bool direction | CT_sbits (_, direction) -> - string_of_cval cval ^ ", " ^ string_of_bool direction + sgen_cval cval ^ ", " ^ string_of_bool direction | CT_fbits (len, direction) -> - string_of_cval cval ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction + sgen_cval cval ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction | _ -> - string_of_cval cval + sgen_cval cval let rec sgen_clexp = function | CL_id (Have_exception _, _) -> "have_exception" diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index f7438b96..1a4b8b4b 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -342,10 +342,10 @@ let rec compile_aval l ctx = function match cval with | V_lit (VL_bit Sail2_values.B0, _) -> [] | V_lit (VL_bit Sail2_values.B1, _) -> - [icopy l (CL_id (gs, ctyp)) (V_op (V_id (gs, ctyp), "|", V_lit (mask i, ctyp)))] + [icopy l (CL_id (gs, ctyp)) (V_call (Bvor, [V_id (gs, ctyp); V_lit (mask i, ctyp)]))] | _ -> (* FIXME: Make this work in C *) - setup @ [iif (V_call ("bit_to_bool", [cval])) [icopy l (CL_id (gs, ctyp)) (V_op (V_id (gs, ctyp), "|", V_lit (mask i, ctyp)))] [] CT_unit] @ cleanup + setup @ [iif (V_call (Bit_to_bool, [cval])) [icopy l (CL_id (gs, ctyp)) (V_call (Bvor, [V_id (gs, ctyp); V_lit (mask i, ctyp)]))] [] CT_unit] @ cleanup in [idecl ctyp gs; icopy l (CL_id (gs, ctyp)) (V_lit (VL_bits (Util.list_init 64 (fun _ -> Sail2_values.B0), direction), ctyp))] @@ -472,7 +472,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = | AP_id (pid, _) when is_ct_enum ctyp -> begin match Env.lookup_id pid ctx.tc_env with | Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [], ctx - | _ -> [ijump (V_op (V_id (name pid, ctyp), "!=", cval)) case_label], [], ctx + | _ -> [ijump (V_call (Neq, [V_id (name pid, ctyp); cval])) case_label], [], ctx end | AP_id (pid, typ) -> @@ -525,7 +525,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = raise (Reporting.err_general l (Printf.sprintf "Variant constructor %s : %s matching against non-variant type %s : %s" (string_of_id ctor) (string_of_typ variant_typ) - (string_of_cval ~zencode:false cval) + (string_of_cval cval) (string_of_ctyp ctyp))) end @@ -534,14 +534,14 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = | AP_cons (hd_apat, tl_apat) -> begin match ctyp with | CT_list ctyp -> - let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_hd cval) case_label in - let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_tl cval) case_label in - [ijump (V_op (cval, "==", V_lit (VL_null, CT_list ctyp))) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx + let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_call (List_hd, [cval])) case_label in + let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_call (List_tl, [cval])) case_label in + [ijump (V_call (Eq, [cval; V_lit (VL_null, CT_list ctyp)])) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx | _ -> raise (Reporting.err_general l "Tried to pattern match cons on non list type") end - | AP_nil _ -> [ijump (V_op (cval, "!=", V_lit (VL_null, ctyp))) case_label], [], ctx + | AP_nil _ -> [ijump (V_call (Neq, [cval; V_lit (VL_null, ctyp)])) case_label], [], ctx let unit_cval = V_lit (VL_unit, CT_unit) @@ -588,7 +588,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = destructure @ (if not trivial_guard then guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup - @ [iif (V_unary ("!", V_id (gs, CT_bool))) (destructure_cleanup @ [igoto case_label]) [] CT_unit] + @ [iif (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit] else []) @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto finish_match_label] @@ -629,7 +629,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = destructure @ [icomment "end destructuring"] @ (if not trivial_guard then guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup - @ [ijump (V_unary ("!", V_id (gs, CT_bool))) try_label] + @ [ijump (V_call (Bnot, [V_id (gs, CT_bool)])) try_label] @ [icomment "end guard"] else []) @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @@ -640,7 +640,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); [idecl ctyp try_return_id; itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup); - ijump (V_unary ("!", V_id (have_exception, CT_bool))) handled_exception_label] + ijump (V_call (Bnot, [V_id (have_exception, CT_bool)])) handled_exception_label] @ List.concat (List.map compile_case cases) @ [igoto fallthrough_label; ilabel handled_exception_label; @@ -762,7 +762,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let body_setup, body_call, body_cleanup = compile_aexp ctx body in let gs = ngensym () in let unit_gs = ngensym () in - let loop_test = V_unary ("!", V_id (gs, CT_bool)) in + let loop_test = V_call (Bnot, [V_id (gs, CT_bool)]) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @ [iblock (cond_setup @@ -893,12 +893,12 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = icopy l (CL_id (loop_var, (CT_fint 64))) (V_id (from_gs, CT_fint 64)); idecl CT_unit body_gs; iblock ([ilabel loop_start_label] - @ [ijump (V_op (V_id (loop_var, CT_fint 64), (if is_inc then ">" else "<"), V_id (to_gs, CT_fint 64))) loop_end_label] + @ [ijump (V_call ((if is_inc then Igt else Ilt), [V_id (loop_var, CT_fint 64); V_id (to_gs, CT_fint 64)])) loop_end_label] @ body_setup @ [body_call (CL_id (body_gs, CT_unit))] @ body_cleanup @ [icopy l (CL_id (loop_var, (CT_fint 64))) - (V_op (V_id (loop_var, CT_fint 64), (if is_inc then "+" else "-"), V_id (step_gs, CT_fint 64)))] + (V_call ((if is_inc then Iadd else Isub), [V_id (loop_var, CT_fint 64); V_id (step_gs, CT_fint 64)]))] @ [igoto loop_start_label]); ilabel loop_end_label])], (fun clexp -> icopy l clexp unit_cval), @@ -1497,8 +1497,8 @@ let sort_ctype_defs cdefs = ctype_defs @ cdefs let compile_ast ctx (Defs defs) = - let assert_vs = Initial_check.extern_of_string (mk_id "__assert") "(bool, string) -> unit" in - let exit_vs = Initial_check.extern_of_string (mk_id "__exit") "unit -> unit" in + let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in + let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml index 331cf65e..0ec92b97 100644 --- a/src/jib/jib_optimize.ml +++ b/src/jib/jib_optimize.ml @@ -160,8 +160,6 @@ let rec cval_subst id subst = function | V_id (id', ctyp) -> if Name.compare id id' = 0 then subst else V_id (id', ctyp) | V_ref (reg_id, ctyp) -> V_ref (reg_id, ctyp) | V_lit (vl, ctyp) -> V_lit (vl, ctyp) - | V_op (cval1, op, cval2) -> V_op (cval_subst id subst cval1, op, cval_subst id subst cval2) - | V_unary (op, cval) -> V_unary (op, cval_subst id subst cval) | V_call (op, cvals) -> V_call (op, List.map (cval_subst id subst) cvals) | V_field (cval, field) -> V_field (cval_subst id subst cval, field) | V_tuple_member (cval, len, n) -> V_tuple_member (cval_subst id subst cval, len, n) @@ -169,22 +167,16 @@ let rec cval_subst id subst = function | V_ctor_unwrap (ctor, cval, unifiers, ctyp) -> V_ctor_unwrap (ctor, cval_subst id subst cval, unifiers, ctyp) | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> field, cval_subst id subst cval) fields, ctyp) | V_poly (cval, ctyp) -> V_poly (cval_subst id subst cval, ctyp) - | V_hd cval -> V_hd (cval_subst id subst cval) - | V_tl cval -> V_tl (cval_subst id subst cval) let rec cval_map_id f = function | V_id (id, ctyp) -> V_id (f id, ctyp) | V_ref (id, ctyp) -> V_ref (f id, ctyp) | V_lit (vl, ctyp) -> V_lit (vl, ctyp) | V_call (call, cvals) -> V_call (call, List.map (cval_map_id f) cvals) - | V_op (cval1, op, cval2) -> V_op (cval_map_id f cval1, op, cval_map_id f cval2) - | V_unary (op, cval) -> V_unary (op, cval_map_id f cval) | V_field (cval, field) -> V_field (cval_map_id f cval, field) | V_tuple_member (cval, len, n) -> V_tuple_member (cval_map_id f cval, len, n) | V_ctor_kind (cval, ctor, unifiers, ctyp) -> V_ctor_kind (cval_map_id f cval, ctor, unifiers, ctyp) | V_ctor_unwrap (ctor, cval, unifiers, ctyp) -> V_ctor_unwrap (ctor, cval_map_id f cval, unifiers, ctyp) - | V_hd cval -> V_hd (cval_map_id f cval) - | V_tl cval -> V_tl (cval_map_id f cval) | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> field, cval_map_id f cval) fields, ctyp) | V_poly (cval, ctyp) -> V_poly (cval_map_id f cval, ctyp) diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 719f0b53..c6fd9d8d 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -250,13 +250,13 @@ let rec smt_cval ctx cval = | _ -> Var (zencode_name ssa_id) end | V_id (ssa_id, _) -> Var (zencode_name ssa_id) - | V_op (frag1, "!=", frag2) -> - Fn ("not", [Fn ("=", [smt_cval ctx frag1; smt_cval ctx frag2])]) - | V_op (frag1, "|", frag2) -> - Fn ("bvor", [smt_cval ctx frag1; smt_cval ctx frag2]) - | V_call ("bit_to_bool", [cval]) -> + | V_call (Neq, [cval1; cval2]) -> + Fn ("not", [Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])]) + | V_call (Bvor, [cval1; cval2]) -> + Fn ("bvor", [smt_cval ctx cval1; smt_cval ctx cval2]) + | V_call (Bit_to_bool, [cval]) -> Fn ("=", [smt_cval ctx cval; Bin "1"]) - | V_unary ("!", cval) -> + | V_call (Bnot, [cval]) -> Fn ("not", [smt_cval ctx cval]) | V_ctor_kind (union, ctor_id, unifiers, _) -> Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval ctx union)]) @@ -296,7 +296,7 @@ let rec smt_cval ctx cval = end | _ -> assert false end - | cval -> failwith ("Unrecognised cval " ^ string_of_cval ~zencode:false cval) + | cval -> failwith ("Unrecognised cval " ^ string_of_cval cval) let add_event ctx ev smt = let stack = event_stack ctx ev in @@ -1301,7 +1301,7 @@ let smt_instr ctx = | _ -> Reporting.unreachable l __POS__ "Bad arguments for internal_vector_update" end - else if string_of_id function_id = "__assert" then + else if string_of_id function_id = "sail_assert" then begin match args with | [assertion; _] -> let smt = smt_cval ctx assertion in @@ -1310,7 +1310,7 @@ let smt_instr ctx = | _ -> Reporting.unreachable l __POS__ "Bad arguments for assertion" end - else if string_of_id function_id = "__assume" then + else if string_of_id function_id = "sail_assume" then begin match args with | [assumption] -> let smt = smt_cval ctx assumption in @@ -1489,7 +1489,7 @@ let expand_reg_deref ctx = function let end_label = label "end_reg_deref_" in let try_reg r = let next_label = label "next_reg_deref_" in - [ijump (V_op (V_ref (name r, reg_ctyp), "!=", reg_ref)) next_label; + [ijump (V_call (Neq, [V_ref (name r, reg_ctyp); reg_ref])) next_label; icopy l clexp (V_id (name r, reg_ctyp)); igoto end_label; ilabel next_label] @@ -1511,7 +1511,7 @@ let expand_reg_deref ctx = function let end_label = label "end_reg_write_" in let try_reg r = let next_label = label "next_reg_write_" in - [ijump (V_op (V_ref (name r, reg_ctyp), "!=", V_id (id, ctyp))) next_label; + [ijump (V_call (Neq, [V_ref (name r, reg_ctyp); V_id (id, ctyp)])) next_label; icopy l (CL_id (name r, reg_ctyp)) cval; igoto end_label; ilabel next_label] @@ -1634,7 +1634,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function | _ -> assert false ) arg_decls in - check_counterexample ctx.ast ctx.tc_env fname args arg_ctyps arg_smt_names + check_counterexample ctx.ast ctx.tc_env fname function_id args arg_ctyps arg_smt_names ); | _ -> failwith "Bad function body" diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml index ad2302de..19dff7b1 100644 --- a/src/jib/jib_ssa.ml +++ b/src/jib/jib_ssa.ml @@ -193,8 +193,6 @@ type cf_node = | CF_guard of cval | CF_start of ctyp NameMap.t -let cval_not cval = V_unary ("!", cval) - let control_flow_graph instrs = let module StringMap = Map.Make(String) in let labels = ref StringMap.empty in @@ -243,7 +241,7 @@ let control_flow_graph instrs = | I_aux (I_jump (cval, label), _) :: after -> let t = add_vertex ([], CF_guard cval) graph in - let f = add_vertex ([], CF_guard (cval_not cval)) graph in + let f = add_vertex ([], CF_guard (V_call (Bnot, [cval]))) graph in List.iter (fun p -> add_edge p t graph; add_edge p f graph) preds; add_edge t (StringMap.find label !labels) graph; cfg [f] after @@ -504,8 +502,6 @@ let rename_variables graph root children = let i = top_stack id in V_ref (ssa_name i id, ctyp) | V_lit (vl, ctyp) -> V_lit (vl, ctyp) - | V_op (f1, op, f2) -> V_op (fold_cval f1, op, fold_cval f2) - | V_unary (op, f) -> V_unary (op, fold_cval f) | V_call (id, fs) -> V_call (id, List.map fold_cval fs) | V_field (f, field) -> V_field (fold_cval f, field) | V_tuple_member (f, len, n) -> V_tuple_member (fold_cval f, len, n) @@ -685,7 +681,7 @@ let string_of_ssainstr = function | Phi (id, ctyp, args) -> string_of_name id ^ " : " ^ string_of_ctyp ctyp ^ " = φ(" ^ Util.string_of_list ", " string_of_name args ^ ")" | Pi cvals -> - "π(" ^ Util.string_of_list ", " (fun v -> String.escaped (string_of_cval ~zencode:false v)) cvals ^ ")" + "π(" ^ Util.string_of_list ", " (fun v -> String.escaped (string_of_cval v)) cvals ^ ")" let string_of_phis = function | [] -> "" diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 575e1352..2825d466 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -161,14 +161,10 @@ let rec cval_rename from_id to_id = function | V_ref (id, ctyp) -> V_ref (id, ctyp) | V_lit (vl, ctyp) -> V_lit (vl, ctyp) | V_call (call, cvals) -> V_call (call, List.map (cval_rename from_id to_id) cvals) - | V_op (f1, op, f2) -> V_op (cval_rename from_id to_id f1, op, cval_rename from_id to_id f2) - | V_unary (op, f) -> V_unary (op, cval_rename from_id to_id f) | V_field (f, field) -> V_field (cval_rename from_id to_id f, field) | V_tuple_member (f, len, n) -> V_tuple_member (cval_rename from_id to_id f, len, n) | V_ctor_kind (f, ctor, unifiers, ctyp) -> V_ctor_kind (cval_rename from_id to_id f, ctor, unifiers, ctyp) | V_ctor_unwrap (ctor, f, unifiers, ctyp) -> V_ctor_unwrap (ctor, cval_rename from_id to_id f, unifiers, ctyp) - | V_hd cval -> V_hd (cval_rename from_id to_id cval) - | V_tl cval -> V_tl (cval_rename from_id to_id cval) | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> field, cval_rename from_id to_id cval) fields, ctyp) | V_poly (f, ctyp) -> V_poly (cval_rename from_id to_id f, ctyp) @@ -279,46 +275,50 @@ let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) = | Current_exception n -> "current_exception" ^ ssa_num n -let rec string_of_cval ?zencode:(zencode=true) = function - | V_id (id, ctyp) -> string_of_name ~zencode:zencode id - | V_ref (id, _) -> "&" ^ string_of_name ~zencode:zencode id +let string_of_op = function + | Bnot -> "not" + | List_hd -> "hd" + | List_tl -> "tl" + | Bit_to_bool -> "bit_to_bool" + | Eq -> "eq" + | Neq -> "neq" + | Bvor -> "bvor" + | Bvand -> "bvand" + | Ilt -> "lt" + | Igt -> "gt" + | Ilteq -> "lteq" + | Igteq -> "gteq" + | Iadd -> "iadd" + | Isub -> "isub" + | Zero_extend n -> "zero_extend" ^ string_of_int n + | Sign_extend n -> "sign_extend" ^ string_of_int n + +let rec string_of_cval = function + | V_id (id, ctyp) -> string_of_name id + | V_ref (id, _) -> "&" ^ string_of_name id | V_lit (vl, ctyp) -> string_of_value vl - | V_call (str, cvals) -> - Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_cval ~zencode:zencode) cvals) + | V_call (op, cvals) -> + Printf.sprintf "%s(%s)" (string_of_op op) (Util.string_of_list ", " string_of_cval cvals) | V_field (f, field) -> - Printf.sprintf "%s.%s" (string_of_cval' ~zencode:zencode f) field + Printf.sprintf "%s.%s" (string_of_cval f) field | V_tuple_member (f, _, n) -> - Printf.sprintf "%s.ztup%d" (string_of_cval' ~zencode:zencode f) n - | V_op (f1, op, f2) -> - Printf.sprintf "%s %s %s" (string_of_cval' ~zencode:zencode f1) op (string_of_cval' ~zencode:zencode f2) - | V_unary (op, f) -> - op ^ string_of_cval' ~zencode:zencode f - | V_hd f -> - Printf.sprintf "(%s).hd" ("*" ^ string_of_cval' ~zencode:zencode f) - | V_tl f -> - Printf.sprintf "(%s).tl" ("*" ^ string_of_cval' ~zencode:zencode f) + Printf.sprintf "%s.ztup%d" (string_of_cval f) n | V_ctor_kind (f, ctor, [], _) -> - string_of_cval' ~zencode:zencode f ^ ".kind" + string_of_cval f ^ ".kind" ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor) | V_ctor_kind (f, ctor, unifiers, _) -> - string_of_cval' ~zencode:zencode f ^ ".kind" + string_of_cval f ^ ".kind" ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers) | V_ctor_unwrap (ctor, f, [], _) -> - Printf.sprintf "%s.%s" - (string_of_cval' ~zencode:zencode f) - (Util.zencode_string (string_of_id ctor)) + Printf.sprintf "%s.%s" (string_of_cval f) (string_of_id ctor) | V_struct (fields, _) -> Printf.sprintf "{%s}" - (Util.string_of_list ", " (fun (field, cval) -> string_of_id field ^ " = " ^ string_of_cval' ~zencode:zencode cval) fields) + (Util.string_of_list ", " (fun (field, cval) -> string_of_id field ^ " = " ^ string_of_cval cval) fields) | V_ctor_unwrap (ctor, f, unifiers, _) -> Printf.sprintf "%s.%s" - (string_of_cval' ~zencode:zencode f) + (string_of_cval f) (Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)) - | V_poly (f, _) -> string_of_cval ~zencode:zencode f -and string_of_cval' ?zencode:(zencode=true) f = - match f with - | V_op _ | V_unary _ -> "(" ^ string_of_cval ~zencode:zencode f ^ ")" - | _ -> string_of_cval ~zencode:zencode f + | V_poly (f, _) -> string_of_cval f (* String representation of ctyps here is only for debugging and intermediate language pretty-printer. *) @@ -535,8 +535,6 @@ let rec unpoly = function | V_poly (cval, _) -> unpoly cval | V_call (call, cvals) -> V_call (call, List.map unpoly cvals) | V_field (cval, field) -> V_field (unpoly cval, field) - | V_op (cval1, op, cval2) -> V_op (unpoly cval1, op, unpoly cval2) - | V_unary (op, cval) -> V_unary (op, unpoly cval) | cval -> cval let rec is_polymorphic = function @@ -560,7 +558,7 @@ let pp_keyword str = string ((str |> Util.red |> Util.clear) ^ " ") let pp_cval cval = - string (string_of_cval ~zencode:false cval) + string (string_of_cval cval) let rec pp_clexp = function | CL_id (id, ctyp) -> pp_name id ^^ string " : " ^^ pp_ctyp ctyp @@ -670,12 +668,10 @@ let pp_cdef = function let rec cval_deps = function | V_id (id, _) | V_ref (id, _) -> NameSet.singleton id | V_lit _ -> NameSet.empty - | V_field (cval, _) | V_unary (_, cval) | V_poly (cval, _) | V_tuple_member (cval, _, _) -> cval_deps cval + | V_field (cval, _) | V_poly (cval, _) | V_tuple_member (cval, _, _) -> cval_deps cval | V_call (_, cvals) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals) - | V_op (cval1, _, cval2) -> NameSet.union (cval_deps cval1) (cval_deps cval2) | V_ctor_kind (cval, _, _, _) -> cval_deps cval | V_ctor_unwrap (_, cval, _, _) -> cval_deps cval - | V_hd cval | V_tl cval -> cval_deps cval | V_struct (fields, ctyp) -> List.fold_left (fun ns (_, cval) -> NameSet.union ns (cval_deps cval)) NameSet.empty fields let rec clexp_deps = function @@ -750,22 +746,15 @@ let rec map_cval_ctyp f = function V_ctor_kind (map_cval_ctyp f cval, id, List.map f unifiers, f ctyp) | V_ctor_unwrap (id, cval, unifiers, ctyp) -> V_ctor_unwrap (id, map_cval_ctyp f cval, List.map f unifiers, f ctyp) - | V_op (cval1, op, cval2) -> - V_op (map_cval_ctyp f cval1, op, map_cval_ctyp f cval2) | V_tuple_member (cval, i, j) -> V_tuple_member (map_cval_ctyp f cval, i, j) - | V_unary (op, cval) -> - V_unary (op, map_cval_ctyp f cval) | V_call (op, cvals) -> V_call (op, List.map (map_cval_ctyp f) cvals) | V_field (cval, field) -> V_field (map_cval_ctyp f cval, field) - | V_hd cval -> V_hd (map_cval_ctyp f cval) - | V_tl cval -> V_tl (map_cval_ctyp f cval) | V_struct (fields, ctyp) -> V_struct (List.map (fun (id, cval) -> id, map_cval_ctyp f cval) fields, f ctyp) | V_poly (cval, ctyp) -> V_poly (map_cval_ctyp f cval, f ctyp) - let rec map_instr_ctyp f (I_aux (instr, aux)) = let instr = match instr with | I_decl (ctyp, id) -> I_decl (f ctyp, id) @@ -890,26 +879,32 @@ let label str = incr label_counter; str -let rec infer_unary v = function - | "!" -> CT_bool - | op -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Could not infer unary " ^ op) - -and infer_op v1 v2 = function - | "==" -> CT_bool - | "!=" -> CT_bool - | ">=" -> CT_bool - | "<=" -> CT_bool - | ">" -> CT_bool - | "<" -> CT_bool - | "+" -> cval_ctyp v1 - | "-" -> cval_ctyp v1 - | "|" -> cval_ctyp v1 - | "&" -> cval_ctyp v1 - | op -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Cannot infer binary op: " ^ op) - -and infer_call vs = function - | "bit_to_bool" -> CT_bool - | op -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Cannot infer call: " ^ op) +let rec infer_call op vs = + match op, vs with + | Bit_to_bool, _ -> CT_bool + | Bnot, _ -> CT_bool + | List_hd, [v] -> + begin match cval_ctyp v with + | CT_list ctyp -> ctyp + | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Invalid call to hd" + end + | List_tl, [v] -> + begin match cval_ctyp v with + | CT_list ctyp -> CT_list ctyp + | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Invalid call to tl" + end + | (Eq | Neq), _ -> CT_bool + | (Bvor | Bvand), [v; _] -> cval_ctyp v + | (Ilt | Igt | Ilteq | Igteq), _ -> CT_bool + | (Iadd | Isub), _ -> CT_fint 64 + | (Zero_extend n | Sign_extend n), [v] -> + begin match cval_ctyp v with + | CT_fbits (_, ord) | CT_sbits (_, ord) | CT_lbits ord -> + CT_fbits (n, ord) + | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Invalid type for zero/sign_extend argument" + end + | _, _ -> + Reporting.unreachable Parse_ast.Unknown __POS__ ("Invalid call to function " ^ string_of_op op) and cval_ctyp = function | V_id (_, ctyp) -> ctyp @@ -917,14 +912,6 @@ and cval_ctyp = function | V_lit (vl, ctyp) -> ctyp | V_ctor_kind _ -> CT_bool | V_ctor_unwrap (ctor, cval, unifiers, ctyp) -> ctyp - | V_hd v -> - begin match cval_ctyp v with - | CT_list ctyp -> ctyp - | ctyp -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Invalid list type " ^ full_string_of_ctyp ctyp) - end - | V_tl v -> cval_ctyp v - | V_op (v1, op, v2) -> infer_op v1 v2 op - | V_unary (op, v) -> infer_unary v op | V_poly (_, ctyp) -> ctyp | V_tuple_member (cval, _, n) -> begin match cval_ctyp cval with @@ -942,7 +929,7 @@ and cval_ctyp = function | ctyp -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Inavlid type for V_field " ^ full_string_of_ctyp ctyp) end | V_struct (fields, ctyp) -> ctyp - | V_call (op, vs) -> infer_call vs op + | V_call (op, vs) -> infer_call op vs let rec clexp_ctyp = function | CL_id (_, ctyp) -> ctyp diff --git a/src/property.ml b/src/property.ml index 84e9d734..9ef546a2 100644 --- a/src/property.ml +++ b/src/property.ml @@ -80,7 +80,7 @@ let add_property_guards props (Defs defs) = let add_constraints_to_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp, pexp_aux)), fcl_aux)) = let add_guard exp = (* FIXME: Use an assert *) - let exp' = mk_exp (E_block [mk_exp (E_app (mk_id "__assume", [mk_exp (E_constraint (List.fold_left nc_and nc_true constraints))])); + let exp' = mk_exp (E_block [mk_exp (E_app (mk_id "sail_assume", [mk_exp (E_constraint (List.fold_left nc_and nc_true constraints))])); strip_exp exp]) in try Type_check.check_exp (env_of exp) exp' (typ_of exp) with diff --git a/src/smtlib.ml b/src/smtlib.ml index d17cb4d9..65e73791 100644 --- a/src/smtlib.ml +++ b/src/smtlib.ml @@ -373,13 +373,17 @@ let build_counterexample args arg_ctyps arg_smt_names model = let rec run frame = match frame with - | Interpreter.Done (state, v) -> v + | Interpreter.Done (state, v) -> Some v | Interpreter.Step (lazy_str, _, _, _) -> run (Interpreter.eval_frame frame) | Interpreter.Break frame -> run (Interpreter.eval_frame frame) + | Interpreter.Fail (_, _, _, _, msg) -> + None + | Interpreter.Effect_request (out, state, stack, eff) -> + run (Interpreter.default_effect_interp state eff) -let check_counterexample ast env fname args arg_ctyps arg_smt_names = +let check_counterexample ast env fname function_id args arg_ctyps arg_smt_names = let open Printf in prerr_endline ("Checking counterexample: " ^ fname); let in_chan = ksprintf Unix.open_process_in "cvc4 --lang=smt2.6 %s" fname in @@ -402,15 +406,15 @@ let check_counterexample ast env fname args arg_ctyps arg_smt_names = List.iter (fun (id, v) -> prerr_endline (" " ^ string_of_id id ^ " -> " ^ string_of_value v)) counterexample; 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 call = E_aux (E_app (function_id, 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 begin match result with - | V_bool false -> + | Some (V_bool false) | None -> ksprintf prerr_endline "Replaying counterexample: %s" Util.("ok" |> green |> clear) | _ -> () end | _ -> - prerr_endline "failure" + prerr_endline "Solver could not find counterexample" end; let status = Unix.close_process_in in_chan in () diff --git a/src/type_check.ml b/src/type_check.ml index c0560a83..5fa2b377 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -5062,6 +5062,6 @@ let initial_env = (app_typ (mk_id "itself") [mk_typ_arg (A_nexp (nvar (mk_kid "n")))]) no_effect) (* __assume is used by property.ml to add guards for SMT generation, but which don't affect flow-typing. *) - |> Env.add_val_spec (mk_id "__assume") + |> Env.add_val_spec (mk_id "sail_assume") (TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), function_typ [bool_typ] unit_typ no_effect) |