From 3ec7f6d6373b6b8b5011daecbcf712f5a9d2dc7c Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 27 Mar 2020 01:19:40 +0000 Subject: Be more careful when flow-typing loops Asserting constraints from the loop condition in the body is fine for while-loops, but doesn't make sense for until-loops. --- src/type_check.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index 82bc92d8..08b6eb5a 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -3882,7 +3882,11 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | 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 + let nc = match loop_type with + | While -> assert_constraint env true checked_cond + | Until -> None + in + let checked_body = crule check_exp (add_opt_constraint nc env) body unit_typ in annot_exp (E_loop (loop_type, checked_measure, checked_cond, checked_body)) unit_typ | E_for (v, f, t, step, ord, body) -> begin -- cgit v1.2.3 From 6e717ac9c733b06eae6ed1717f11e8d00c21c8c0 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 26 Mar 2020 21:08:05 +0000 Subject: Implement hex_str for Lem --- src/gen_lib/sail2_values.lem | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) (limited to 'src') diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem index 69bf0852..7bd950d7 100644 --- a/src/gen_lib/sail2_values.lem +++ b/src/gen_lib/sail2_values.lem @@ -464,6 +464,44 @@ let show_bitlist_prefix c bs = let show_bitlist bs = show_bitlist_prefix #'0' bs +val hex_char : natural -> char + +let hex_char n = + match n with + | 0 -> #'0' + | 1 -> #'1' + | 2 -> #'2' + | 3 -> #'3' + | 4 -> #'4' + | 5 -> #'5' + | 6 -> #'6' + | 7 -> #'7' + | 8 -> #'8' + | 9 -> #'9' + | 10 -> #'A' + | 11 -> #'B' + | 12 -> #'C' + | 13 -> #'D' + | 14 -> #'E' + | 15 -> #'F' + | _ -> failwith "hex_char: not a hexadecimal digit" + end + +val hex_str_aux : natural -> list char -> list char + +let rec hex_str_aux n acc = + if n = 0 then acc else + hex_str_aux (n div 16) (hex_char (n mod 16) :: acc) + +declare {isabelle} termination_argument hex_str_aux = automatic + +val hex_str : integer -> string + +let hex_str i = + if i < 0 then failwith "hex_str: negative" else + if i = 0 then "0x0" else + "0x" ^ toString (hex_str_aux (naturalFromInteger (abs i)) []) + (*** List operations *) let inline (^^) = append_list -- cgit v1.2.3 From 319c382fe396886fd2b1bd8295c55aa0d9dd0acd Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 28 Mar 2020 13:28:52 +0000 Subject: Make bounds check for vector subrange assignments stricter Check that indices are within bounds, not just in the right (increasing/decreasing) order. --- src/type_check.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index 08b6eb5a..9b70f645 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -3663,18 +3663,18 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) = let inferred_exp2 = infer_exp env exp2 in let nexp1, env = bind_numeric l (typ_of inferred_exp1) env in let nexp2, env = bind_numeric l (typ_of inferred_exp2) env in - let (len, check) = match ord with + let (slice_len, check) = match ord with | Ord_aux (Ord_inc, _) -> (nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)), - nc_lteq nexp1 nexp2) + nc_and (nc_and (nc_lteq (nint 0) nexp1) (nc_lteq nexp1 nexp2)) (nc_lt nexp2 len)) | Ord_aux (Ord_dec, _) -> (nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)), - nc_gteq nexp1 nexp2) + nc_and (nc_and (nc_lteq (nint 0) nexp2) (nc_lteq nexp2 nexp1)) (nc_lt nexp1 len)) | Ord_aux (Ord_var _, _) -> typ_error env l "Slice assignment to bitvector with variable indexing order unsupported" in if !opt_no_lexp_bounds_check || prove __POS__ env check then - annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (bitvector_typ len ord) + annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (bitvector_typ slice_len ord) else typ_raise env l (Err_lexp_bounds (check, Env.get_locals env, Env.get_constraints env)) | _ -> typ_error env l "Cannot assign slice of non vector type" -- cgit v1.2.3 From 7bf9b460d3b2c324b4fae8e14e0a54e354002f54 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 25 Mar 2020 20:40:59 +0000 Subject: Add Lem builtins for operations on reals ... that match the names in lib/real.sail. Also fix the lem mapping for abs_int_atom and a Lem syntax error with nested record updates. --- src/gen_lib/sail2_values.lem | 30 +++++++++++++++++++++--------- src/pretty_print_lem.ml | 2 +- 2 files changed, 22 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem index 7bd950d7..9e1f20c0 100644 --- a/src/gen_lib/sail2_values.lem +++ b/src/gen_lib/sail2_values.lem @@ -35,15 +35,27 @@ let power_int_nat l r = integerPow l r let power_int_int l r = integerPow l (nat_of_int r) let negate_int i = integerNegate i let min_int l r = integerMin l r -let max_int l r = integerMax l r - -let add_real l r = realAdd l r -let sub_real l r = realMinus l r -let mult_real l r = realMult l r -let div_real l r = realDiv l r -let negate_real r = realNegate r -let abs_real r = realAbs r -let power_real b e = realPowInteger b e*) +let max_int l r = integerMax l r*) + +let inline add_real l r = realAdd l r +let inline sub_real l r = realMinus l r +let inline mult_real l r = realMult l r +let inline div_real l r = realDiv l r +let inline neg_real r = realNegate r +let inline abs_real r = realAbs r +let inline real_power b e = realPowInteger b e +let inline sqrt_real r = realSqrt r + +let inline eq_real l r = realEq l r +let inline lt_real l r = realLess l r +let inline gt_real l r = realLessEqual l r +let inline lteq_real l r = realGreater l r +let inline gteq_real l r = realGreaterEqual l r + +let inline to_real i = realFromInteger i + +let inline round_down r = realFloor r +let inline round_up r = realCeiling r val print_endline : string -> unit let print_endline _ = () diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 993934f5..34ccc5ba 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -901,7 +901,7 @@ let doc_exp_lem, doc_let_lem = when Env.is_record tid env -> tid | _ -> raise (report l __POS__ ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in - anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) + anglebars (space ^^ doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps) ^^ space) | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let start, (len, order, etyp) = -- cgit v1.2.3 From 4a04aec7e5ef23137c7dfbf5e655e183582c9769 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 28 Mar 2020 13:41:42 +0000 Subject: Allow empty Sail source files ... instead of dying with "Syntax error". --- src/parser.mly | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') diff --git a/src/parser.mly b/src/parser.mly index 6a579b7a..70f6f225 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -1493,3 +1493,5 @@ defs: file: | defs Eof { $1 } + | Eof + { (Defs []) } -- cgit v1.2.3 From 3d895704db4689f832180782ab30f1805804e2b3 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 28 Mar 2020 13:08:48 +0000 Subject: Check more types in monomorphisation rewrites In the new version of the ASL-generated Sail, some vector operators are also overloaded for integers to match idioms of ASL (e.g. i[31:0], where i is an integer), so check in the monomorphisation rewrites that we use bitvector helper functions only for actual bitvectors. --- src/monomorphise.ml | 38 +++++++++++++++++++++++--------------- 1 file changed, 23 insertions(+), 15 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index e328cce1..8279f83d 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2754,6 +2754,7 @@ let rec rewrite_app env typ (id,args) = [vector2; start2; end2]),_)] when is_append append && is_subrange subrange1 && is_subrange subrange2 && is_constant_vec_typ env (typ_of e1) && + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in @@ -2782,6 +2783,7 @@ let rec rewrite_app env typ (id,args) = [vector2; start2; length2]),_)] when is_append append && is_slice slice1 && is_slice slice2 && is_constant_vec_typ env (typ_of e1) && + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && not (is_constant length1 || is_constant length2) -> let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in @@ -2806,7 +2808,7 @@ let rec rewrite_app env typ (id,args) = (* variable-slice @ zeros *) | [E_aux (E_app (slice1, [vector1; start1; len1]),_); E_aux (E_app (zeros2, [len2]),_)] - when is_slice slice1 && is_zeros zeros2 && + when is_slice slice1 && is_zeros zeros2 && is_bitvector_typ (typ_of vector1) && not (is_constant start1 && is_constant len1 && is_constant len2) -> try_cast_to_typ (mk_exp (E_app (mk_id "place_slice", [vector1; start1; len1; len2]))) @@ -2825,6 +2827,7 @@ let rec rewrite_app env typ (id,args) = E_aux (E_app (subrange2, [vector2; start2; end2]),_)] when is_subrange subrange1 && is_subrange subrange2 && + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> try_cast_to_typ (E_aux (E_app (mk_id "subrange_subrange_concat", @@ -2837,6 +2840,7 @@ let rec rewrite_app env typ (id,args) = E_aux (E_app (slice2, [vector2; start2; length2]),_)] when is_slice slice1 && is_slice slice2 && + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && not (is_constant length1 || is_constant length2) -> try_cast_to_typ (E_aux (E_app (mk_id "slice_slice_concat", @@ -2846,7 +2850,8 @@ let rec rewrite_app env typ (id,args) = | [E_aux (E_app (slice1, [vector1; start1; length1]),_); (E_aux (E_id _,_) as vector2)] - when is_slice slice1 && not (is_constant length1) -> + when is_slice slice1 && is_bitvector_typ (typ_of vector1) && + not (is_constant length1) -> let start2 = mk_exp (E_lit (mk_lit (L_num Big_int.zero))) in let length2 = mk_exp (E_app (mk_id "length", [vector2])) in try_cast_to_typ @@ -2858,7 +2863,7 @@ let rec rewrite_app env typ (id,args) = E_aux (E_app (slice1, [vector1; start1; length1]),_)]),_); E_aux (E_app (zeros1, [length2]),_)] when is_append append1 && is_slice slice1 && is_zeros zeros1 && - is_constant_vec_typ env (typ_of e1) && + is_constant_vec_typ env (typ_of e1) && is_bitvector_typ (typ_of vector1) && not (is_constant length1 || is_constant length2) -> let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in @@ -2908,6 +2913,7 @@ let rec rewrite_app env typ (id,args) = E_aux (E_app (subrange2, [vector2; start2; end2]),_)] when is_subrange subrange1 && is_subrange subrange2 && + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> wrap (E_app (mk_id "subrange_subrange_eq", [vector1; start1; end1; vector2; start2; end2])) @@ -2916,6 +2922,7 @@ let rec rewrite_app env typ (id,args) = E_aux (E_app (slice2, [vector2; len2; start2]),_)] when is_slice slice1 && is_slice slice2 && + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && not (is_constant len1 && is_constant start1 && is_constant len2 && is_constant start2) -> let upper start len = mk_exp (E_app_infix (start, mk_id "+", @@ -2926,18 +2933,19 @@ let rec rewrite_app env typ (id,args) = [vector1; upper start1 len1; start1; vector2; upper start2 len2; start2])) | [E_aux (E_app (slice1, [vector1; start1; len1]), _); E_aux (E_app (zeros2, _), _)] - when is_slice slice1 && is_zeros zeros2 && not (is_constant len1) -> + when is_slice slice1 && is_zeros zeros2 && not (is_constant len1) && + is_bitvector_typ (typ_of vector1) -> wrap (E_app (mk_id "is_zeros_slice", [vector1; start1; len1])) | _ -> E_app (id,args) else if is_id env (Id "IsZero") id then match args with | [E_aux (E_app (subrange1, [vector1; start1; end1]),_)] - when (is_id env (Id "vector_subrange") subrange1) && + when (is_id env (Id "vector_subrange") subrange1) && is_bitvector_typ (typ_of vector1) && not (is_constant_range (start1,end1)) -> E_app (mk_id "is_zero_subrange", [vector1; start1; end1]) | [E_aux (E_app (slice1, [vector1; start1; len1]),_)] - when (is_slice slice1) && + when (is_slice slice1) && is_bitvector_typ (typ_of vector1) && not (is_constant len1) -> E_app (mk_id "is_zeros_slice", [vector1; start1; len1]) | _ -> E_app (id,args) @@ -2945,12 +2953,12 @@ let rec rewrite_app env typ (id,args) = else if is_id env (Id "IsOnes") id then match args with | [E_aux (E_app (subrange1, [vector1; start1; end1]),_)] - when is_id env (Id "vector_subrange") subrange1 && + when is_id env (Id "vector_subrange") subrange1 && is_bitvector_typ (typ_of vector1) && not (is_constant_range (start1,end1)) -> E_app (mk_id "is_ones_subrange", [vector1; start1; end1]) | [E_aux (E_app (slice1, [vector1; start1; len1]),_)] - when is_slice slice1 && not (is_constant len1) -> + when is_slice slice1 && not (is_constant len1) && is_bitvector_typ (typ_of vector1) -> E_app (mk_id "is_ones_slice", [vector1; start1; len1]) | _ -> E_app (id,args) @@ -2962,7 +2970,7 @@ let rec rewrite_app env typ (id,args) = (E_aux (E_app (zeros1, [len1]),_) | E_aux (E_cast (_,E_aux (E_app (zeros1, [len1]),_)),_)) ]),_)] - when is_subrange subrange1 && is_zeros zeros1 && is_append append1 + when is_subrange subrange1 && is_zeros zeros1 && is_append append1 && is_bitvector_typ (typ_of vector1) -> try_cast_to_typ (rewrap (E_app (mk_id "place_subrange", length_arg @ [vector1; start1; end1; len1]))) | [E_aux (E_app (append1, @@ -3013,7 +3021,7 @@ let rec rewrite_app env typ (id,args) = let length_arg = List.filter (fun arg -> is_number (typ_of arg)) args in match List.filter (fun arg -> not (is_number (typ_of arg))) args with | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] - when is_slice slice1 && not (is_constant length1) -> + when is_slice slice1 && not (is_constant length1) && is_bitvector_typ (typ_of vector1) -> try_cast_to_typ (rewrap (E_app (mk_id "sext_slice", length_arg @ [vector1; start1; length1]))) | [E_aux (E_app (append, @@ -3022,7 +3030,7 @@ let rec rewrite_app env typ (id,args) = E_aux (E_cast (_, E_aux (E_app (zeros2, [len2]), _)),_)) ]), _)] when is_append append && is_subrange subrange1 && is_zeros zeros2 && - not (is_constant len2) -> + not (is_constant len2) && is_bitvector_typ (typ_of vector1) -> E_app (mk_id "place_subrange_signed", length_arg @ [vector1; start1; end1; len2]) | [E_aux (E_app (append, @@ -3030,7 +3038,7 @@ let rec rewrite_app env typ (id,args) = (E_aux (E_app (zeros2, [len2]), _) | E_aux (E_cast (_, E_aux (E_app (zeros2, [len2]), _)),_)) ]), _)] - when is_append append && is_slice slice1 && is_zeros zeros2 && + when is_append append && is_slice slice1 && is_zeros zeros2 && is_bitvector_typ (typ_of vector1) && not (is_constant len1 && is_constant len2) -> E_app (mk_id "place_slice_signed", length_arg @ [vector1; start1; len1; len2]) @@ -3064,10 +3072,10 @@ let rec rewrite_app env typ (id,args) = else if is_id env (Id "UInt") id || is_id env (Id "unsigned") id then match args with | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] - when is_slice slice1 && not (is_constant length1) -> + when is_slice slice1 && not (is_constant length1) && is_bitvector_typ (typ_of vector1) -> E_app (mk_id "unsigned_slice", [vector1; start1; length1]) | [E_aux (E_app (subrange1, [vector1; start1; end1]),_)] - when is_subrange subrange1 && not (is_constant_range (start1,end1)) -> + when is_subrange subrange1 && not (is_constant_range (start1,end1)) && is_bitvector_typ (typ_of vector1) -> E_app (mk_id "unsigned_subrange", [vector1; start1; end1]) | _ -> E_app (id,args) @@ -3075,7 +3083,7 @@ let rec rewrite_app env typ (id,args) = else if is_id env (Id "__SetSlice_bits") id then match args with | [len; slice_len; vector; start; E_aux (E_app (zeros, _), _)] - when is_zeros zeros -> + when is_zeros zeros && is_bitvector_typ (typ_of vector) -> E_app (mk_id "set_slice_zeros", [len; vector; start; slice_len]) | _ -> E_app (id, args) -- cgit v1.2.3 From 4b6ffe96896f56d538dc9115c1d1b04156ab34a5 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sun, 22 Mar 2020 18:21:57 +0000 Subject: Be more careful about type annotations in rewrites to Lem In particular, don't add annotations for types with existentially quantified variables that only occur in constraints, not in the type, e.g. {'i1 'i2, 'i1 == div('i2, 8). int('i1)}. These seem to confuse the type checker when pulled out into the source AST. --- src/pretty_print_lem.ml | 4 +- src/rewriter.ml | 41 ++++++++++++++----- src/rewriter.mli | 6 ++- src/rewrites.ml | 102 +++++++++++++++++++++++++++++------------------- 4 files changed, 99 insertions(+), 54 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 34ccc5ba..0994a821 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -529,8 +529,8 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with | P_typ(Typ_aux (Typ_tup typs, _), P_aux (P_tup pats, _)) -> (* Isabelle does not seem to like type-annotated tuple patterns; it gives a syntax error. Avoid this by annotating the tuple elements instead *) - let doc_elem typ pat = - doc_pat_lem ctxt true (add_p_typ typ pat) in + let env = env_of_pat pa in + let doc_elem typ pat = doc_pat_lem ctxt true (add_p_typ env typ pat) in parens (separate comma_sp (List.map2 doc_elem typs pats)) | P_typ(typ,p) -> let doc_p = doc_pat_lem ctxt true p in diff --git a/src/rewriter.ml b/src/rewriter.ml index 62870083..3b68f493 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -91,6 +91,17 @@ let lookup_generated_kid env kid = let generated_kids typ = KidSet.filter is_kid_generated (tyvars_of_typ typ) +let rec is_src_typ typ = + match typ with + | Typ_aux (Typ_tup typs, l) -> List.for_all is_src_typ typs + | _ -> + match destruct_exist typ with + | Some (kopts, nc, typ') -> + let declared_kids = KidSet.of_list (List.map kopt_kid kopts) in + let unused_kids = KidSet.diff declared_kids (tyvars_of_typ typ') in + KidSet.is_empty unused_kids && KidSet.is_empty (generated_kids typ) + | None -> KidSet.is_empty (generated_kids typ) + let resolve_generated_kids env typ = let subst_kid kid typ = subst_kid typ_subst kid (lookup_generated_kid env kid) typ in KidSet.fold subst_kid (generated_kids typ) typ @@ -99,21 +110,31 @@ let rec remove_p_typ = function | P_aux (P_typ (typ, pat), _) -> remove_p_typ pat | pat -> pat -let add_p_typ typ (P_aux (paux, annot) as pat) = - let typ' = resolve_generated_kids (env_of_pat pat) typ in - if KidSet.is_empty (generated_kids typ') then - P_aux (P_typ (typ', remove_p_typ pat), annot) - else pat +let add_p_typ env typ (P_aux (paux, annot) as pat) = + let typ' = resolve_generated_kids env typ in + if is_src_typ typ' then P_aux (P_typ (typ', remove_p_typ pat), annot) else pat let rec remove_e_cast = function | E_aux (E_cast (_, exp), _) -> remove_e_cast exp | exp -> exp -let add_e_cast typ (E_aux (eaux, annot) as exp) = - let typ' = resolve_generated_kids (env_of exp) typ in - if KidSet.is_empty (generated_kids typ') then - E_aux (E_cast (typ', remove_e_cast exp), annot) - else exp +let add_e_cast env typ (E_aux (eaux, annot) as exp) = + let typ' = resolve_generated_kids env typ in + if is_src_typ typ' then E_aux (E_cast (typ', remove_e_cast exp), annot) else exp + +let add_typs_let env ltyp rtyp exp = + let aux pat lhs rhs = + let pat' = add_p_typ env ltyp pat in + (pat', lhs, rhs) + in + match exp with + | E_aux (E_let (LB_aux (LB_val (pat, lhs), lba), rhs), a) -> + let (pat', lhs', rhs') = aux pat lhs rhs in + E_aux (E_let (LB_aux (LB_val (pat', lhs'), lba), rhs'), a) + | E_aux (E_internal_plet (pat, lhs, rhs), a) -> + let (pat', lhs', rhs') = aux pat lhs rhs in + E_aux (E_internal_plet (pat', lhs', rhs'), a) + | _ -> exp let rec small (E_aux (exp,_)) = match exp with | E_id _ diff --git a/src/rewriter.mli b/src/rewriter.mli index 85f00453..f61bcc66 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -231,9 +231,11 @@ val pure_exp_alg : 'b -> ('b -> 'b -> 'b) -> val simple_annot : Parse_ast.l -> typ -> Parse_ast.l * tannot -val add_p_typ : typ -> tannot pat -> tannot pat +val add_p_typ : Env.t -> typ -> 'a pat -> 'a pat -val add_e_cast : typ -> tannot exp -> tannot exp +val add_e_cast : Env.t -> typ -> 'a exp -> 'a exp + +val add_typs_let : Env.t -> typ -> typ -> 'a exp -> 'a exp val effect_of_pexp : tannot pexp -> effect diff --git a/src/rewrites.ml b/src/rewrites.ml index 863f8115..063bbadb 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -385,7 +385,7 @@ let remove_vector_concat_pat pat = let id_pat = match typ_opt with - | Some typ -> add_p_typ typ (P_aux (P_id child,cannot)) + | Some typ -> add_p_typ env typ (P_aux (P_id child,cannot)) | None -> P_aux (P_id child,cannot) in let letbind = fix_eff_lb (LB_aux (LB_val (id_pat,subv),cannot)) in (letbind, @@ -1552,7 +1552,7 @@ let rewrite_defs_early_return env (Defs defs) = let eff = effect_of_annot tannot in let tannot' = mk_tannot env typ (union_effects eff (mk_effect [BE_escape])) in let exp' = match Env.get_ret_typ env with - | Some typ -> add_e_cast typ exp + | Some typ -> add_e_cast env typ exp | None -> exp in E_aux (E_app (mk_id "early_return", [exp']), (l, tannot')) | _ -> full_exp in @@ -2110,15 +2110,12 @@ let rewrite_tuple_assignments env defs = let env = env_of_annot annot in match e_aux with | E_assign (LEXP_aux (LEXP_tup lexps, _), exp) -> - (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *) let (_, ids) = List.fold_left (fun (n, ids) _ -> (n + 1, ids @ [mk_id ("tup__" ^ string_of_int n)])) (0, []) lexps in let block_assign i lexp = mk_exp (E_assign (strip_lexp lexp, mk_exp (E_id (mk_id ("tup__" ^ string_of_int i))))) in let block = mk_exp (E_block (List.mapi block_assign lexps)) in - let letbind = mk_letbind (mk_pat (P_typ (Type_check.typ_of exp, - mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))))) - (strip_exp exp) - in - let let_exp = mk_exp (E_let (letbind, block)) in + let pat = mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids)) in + let exp' = add_e_cast env (typ_of exp) exp in + let let_exp = mk_exp (E_let (mk_letbind pat (strip_exp exp'), block)) in begin try check_exp env let_exp unit_typ with | Type_error (_, l, err) -> @@ -2159,9 +2156,11 @@ let rewrite_defs_remove_blocks env = let l = get_loc_exp v in let env = env_of v in let typ = typ_of v in - let wild = add_p_typ typ (annot_pat P_wild l env typ) in + let wild = annot_pat P_wild l env typ in let e_aux = E_let (annot_letbind (unaux_pat wild, v) l env typ, body) in - fix_eff_exp (annot_exp e_aux l env (typ_of body)) in + fix_eff_exp (annot_exp e_aux l env (typ_of body)) + |> add_typs_let env typ (typ_of body) + in let rec f l = function | [] -> E_aux (E_lit (L_aux (L_unit,gen_loc l)), (simple_annot l unit_typ)) @@ -2192,19 +2191,20 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp = | Some (env, typ, eff) when is_unit_typ typ -> let body = body (annot_exp (E_lit (mk_lit L_unit)) l env unit_typ) in let body_typ = try typ_of body with _ -> unit_typ in - let wild = add_p_typ (typ_of v) (annot_pat P_wild l env (typ_of v)) in + let wild = annot_pat P_wild l env typ in let lb = fix_eff_lb (annot_letbind (unaux_pat wild, v) l env unit_typ) in fix_eff_exp (annot_exp (E_let (lb, body)) l env body_typ) + |> add_typs_let env typ body_typ | Some (env, typ, eff) -> let id = fresh_id "w__" l in - let pat = add_p_typ (typ_of v) (annot_pat (P_id id) l env (typ_of v)) in + let pat = annot_pat (P_id id) l env typ in let lb = fix_eff_lb (annot_letbind (unaux_pat pat, v) l env typ) in let body = body (annot_exp (E_id id) l env typ) in fix_eff_exp (annot_exp (E_let (lb, body)) l env (typ_of body)) + |> add_typs_let env typ (typ_of body) | None -> raise (Reporting.err_unreachable l __POS__ "no type information") - let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list -> 'a exp) : 'a exp = match l with | [] -> k [] @@ -2241,9 +2241,9 @@ let rewrite_defs_letbind_effects env = and n_pexp : 'b. bool -> 'a pexp -> ('a pexp -> 'b) -> 'b = fun newreturn pexp k -> match pexp with | Pat_aux (Pat_exp (pat,exp),annot) -> - k (fix_eff_pexp (Pat_aux (Pat_exp (pat,n_exp_term newreturn exp), annot))) + k (fix_eff_pexp (Pat_aux (Pat_exp (pat, n_exp_term newreturn exp), annot))) | Pat_aux (Pat_when (pat,guard,exp),annot) -> - k (fix_eff_pexp (Pat_aux (Pat_when (pat,n_exp_term newreturn guard,n_exp_term newreturn exp), annot))) + k (fix_eff_pexp (Pat_aux (Pat_when (pat, n_exp_term newreturn guard, n_exp_term newreturn exp), annot))) and n_pexpL (newreturn : bool) (pexps : 'a pexp list) (k : 'a pexp list -> 'a exp) : 'a exp = mapCont (n_pexp newreturn) pexps k @@ -2297,15 +2297,15 @@ let rewrite_defs_letbind_effects env = and n_lexpL (lexps : 'a lexp list) (k : 'a lexp list -> 'a exp) : 'a exp = mapCont n_lexp lexps k - and n_exp_term (newreturn : bool) (exp : 'a exp) : 'a exp = + and n_exp_term ?cast:(cast=false) (newreturn : bool) (exp : 'a exp) : 'a exp = let (E_aux (_,(l,tannot))) = exp in let exp = if newreturn then (* let typ = try typ_of exp with _ -> unit_typ in *) - let exp = add_e_cast (typ_of exp) exp in + let exp = if cast then add_e_cast (env_of exp) (typ_of exp) exp else exp in annot_exp (E_internal_return exp) l (env_of exp) (typ_of exp) - else - exp in + else exp + in (* n_exp_term forces an expression to be translated into a form "let .. let .. let .. in EXP" where EXP has no effect and does not update variables *) @@ -2328,8 +2328,8 @@ let rewrite_defs_letbind_effects env = (* Leave effectful operands of Boolean "and"/"or" in place to allow short-circuiting. *) let newreturn = effectful l || effectful r in - let l = n_exp_term newreturn l in - let r = n_exp_term newreturn r in + let l = n_exp_term ~cast:true newreturn l in + let r = n_exp_term ~cast:true newreturn r in k (rewrap (E_app (op_bool, [l; r]))) | E_app (id,exps) -> n_exp_nameL exps (fun exps -> @@ -2348,7 +2348,8 @@ let rewrite_defs_letbind_effects env = let newreturn = effectful exp2 || effectful exp3 in let exp2 = n_exp_term newreturn exp2 in let exp3 = n_exp_term newreturn exp3 in - k (rewrap (E_if (exp1,exp2,exp3))) in + k (rewrap (E_if (exp1,exp2,exp3))) + in if value exp1 then e_if (n_exp_term false exp1) else n_exp_name exp1 e_if | E_for (id,start,stop,by,dir,body) -> n_exp_name start (fun start -> @@ -2362,7 +2363,7 @@ let rewrite_defs_letbind_effects env = | 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 cond = n_exp_term ~cast:true (effectful cond) cond in let body = n_exp_term (effectful body) body in k (rewrap (E_loop (loop,measure,cond,body))) | E_vector exps -> @@ -2434,7 +2435,7 @@ let rewrite_defs_letbind_effects env = | E_assert (exp1,exp2) -> n_exp_name exp1 (fun exp1 -> n_exp_name exp2 (fun exp2 -> - k (rewrap (E_assert (exp1,exp2))))) + k (rewrap (E_assert (exp1, exp2))))) | E_var (lexp,exp1,exp2) -> n_lexp lexp (fun lexp -> n_exp exp1 (fun exp1 -> @@ -2502,7 +2503,7 @@ let rewrite_defs_internal_lets env = let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with | LEXP_id id -> P_aux (P_id id, annot) - | LEXP_cast (typ, id) -> add_p_typ typ (P_aux (P_id id, annot)) + | LEXP_cast (typ, id) -> add_p_typ (env_of_annot annot) typ (P_aux (P_id id, annot)) | LEXP_tup lexps -> P_aux (P_tup (List.map pat_of_local_lexp lexps), annot) | _ -> raise (Reporting.err_unreachable l __POS__ "unexpected local lexp") in @@ -2521,7 +2522,7 @@ let rewrite_defs_internal_lets env = | LEXP_aux (_,lexp_annot') -> lexp_annot' | exception _ -> lannot) in - let rhs = add_e_cast ltyp (rhs exp) in + let rhs = add_e_cast (env_of exp) ltyp (rhs exp) in E_let (LB_aux (LB_val (pat_of_local_lexp lhs, rhs), annot), body) | LB_aux (LB_val (pat,exp'),annot') -> if effectful exp' @@ -2533,7 +2534,7 @@ let rewrite_defs_internal_lets env = | LEXP_aux (LEXP_id id, annot) -> (P_id id, annot) | LEXP_aux (LEXP_cast (typ, id), annot) -> - (unaux_pat (add_p_typ typ (P_aux (P_id id, annot))), annot) + (unaux_pat (add_p_typ (env_of_annot annot) typ (P_aux (P_id id, annot))), annot) | _ -> failwith "E_var with unexpected lexp" in if effectful exp1 then E_internal_plet (P_aux (paux, annot), exp1, exp2) @@ -3331,22 +3332,24 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let tuple_exp = function | [] -> annot_exp (E_lit (mk_lit L_unit)) l env unit_typ | [e] -> e - | es -> annot_exp (E_tuple es) l env (tuple_typ (List.map typ_of es)) in + | es -> annot_exp (E_tuple es) l env (tuple_typ (List.map typ_of es)) + in let tuple_pat = function | [] -> annot_pat P_wild l env unit_typ | [pat] -> let typ = typ_of_pat pat in - add_p_typ typ pat + add_p_typ env typ pat | pats -> let typ = tuple_typ (List.map typ_of_pat pats) in - add_p_typ typ (annot_pat (P_tup pats) l env typ) in + add_p_typ env typ (annot_pat (P_tup pats) l env typ) + in let rec add_vars overwrite ((E_aux (expaux,annot)) as exp) vars = match expaux with | E_let (lb,exp) -> let exp = add_vars overwrite exp vars in - E_aux (E_let (lb,exp),swaptyp (typ_of exp) annot) + E_aux (E_let (lb,exp), swaptyp (typ_of exp) annot) | E_var (lexp,exp1,exp2) -> let exp2 = add_vars overwrite exp2 vars in E_aux (E_var (lexp,exp1,exp2), swaptyp (typ_of exp2) annot) @@ -3355,7 +3358,11 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = E_aux (E_internal_plet (pat,exp1,exp2), swaptyp (typ_of exp2) annot) | E_internal_return exp2 -> let exp2 = add_vars overwrite exp2 vars in - E_aux (E_internal_return exp2,swaptyp (typ_of exp2) annot) + E_aux (E_internal_return exp2, swaptyp (typ_of exp2) annot) + | E_cast (typ, exp) -> + let (E_aux (expaux, annot) as exp) = add_vars overwrite exp vars in + let typ' = typ_of exp in + add_e_cast (env_of exp) typ' (E_aux (expaux, swaptyp typ' annot)) | _ -> (* after rewrite_defs_letbind_effects there cannot be terms that have effects/update local variables in "tail-position": check n_exp_term @@ -3364,6 +3371,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let lb = LB_aux (LB_val (P_aux (P_wild, annot), exp), annot) in let exp' = tuple_exp vars in E_aux (E_let (lb, exp'), swaptyp (typ_of exp') annot) + |> add_typs_let env (typ_of exp) (typ_of exp') else tuple_exp (exp :: vars) in let mk_var_exps_pats l env ids = @@ -3375,7 +3383,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = exp, P_aux (P_id id, a)) |> List.split in - let rewrite used_vars (E_aux (expaux,((el,_) as annot)) as full_exp) (P_aux (paux,(pl,pannot)) as pat) = + let rec rewrite used_vars (E_aux (expaux,((el,_) as annot)) as full_exp) (P_aux (paux,(pl,pannot)) as pat) = let env = env_of_annot annot in let overwrite = match paux with | P_wild | P_typ (_, P_aux (P_wild, _)) -> true @@ -3414,11 +3422,15 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = in let lvar_nc = nc_and (nc_lteq (nvar lower_kid) (nvar lvar_kid)) (nc_lteq (nvar lvar_kid) (nvar upper_kid)) in let lvar_typ = mk_typ (Typ_exist (List.map (mk_kopt K_int) [lvar_kid], lvar_nc, atom_typ (nvar lvar_kid))) in - let lvar_pat = unaux_pat (add_p_typ lvar_typ (annot_pat (P_var ( + let lvar_pat = unaux_pat (annot_pat (P_var ( annot_pat (P_id id) el env (atom_typ (nvar lvar_kid)), - TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ)) in + TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ) + in let lb = fix_eff_lb (annot_letbind (lvar_pat, exp1) el env lvar_typ) in - let body = fix_eff_exp (annot_exp (E_let (lb, exp4)) el env (typ_of exp4)) in + let body = + fix_eff_exp (annot_exp (E_let (lb, exp4)) el env (typ_of exp4)) + |> add_typs_let env lvar_typ (typ_of exp4) + in (* If lower > upper, the loop body never gets executed, and the type checker might not be able to prove that the initial value exp1 satisfies the constraints on the loop variable. @@ -3518,7 +3530,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | E_assign (lexp,vexp) -> let mk_id_pat id = let typ = lvar_typ (Env.lookup_id id env) in - add_p_typ typ (annot_pat (P_id id) pl env typ) + add_p_typ env typ (annot_pat (P_id id) pl env typ) in if effectful exp then Same_vars (E_aux (E_assign (lexp,vexp),annot)) @@ -3528,7 +3540,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let pat = annot_pat (P_id id) pl env (typ_of vexp) in Added_vars (vexp, mk_id_pat id) | LEXP_aux (LEXP_cast (typ,id),annot) -> - let pat = add_p_typ typ (annot_pat (P_id id) pl env (typ_of vexp)) in + let pat = add_p_typ env typ (annot_pat (P_id id) pl env (typ_of vexp)) in Added_vars (vexp,pat) | LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i),((l1,_) as annot)) -> let eid = annot_exp (E_id id) l2 env (typ_of_annot annot2) in @@ -3542,6 +3554,13 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let pat = annot_pat (P_id id) pl env (typ_of vexp) in Added_vars (vexp,pat) | _ -> Same_vars (E_aux (E_assign (lexp,vexp),annot))) + | E_cast (typ, exp) -> + begin match rewrite used_vars exp pat with + | Added_vars (exp', pat') -> + Added_vars (add_e_cast (env_of exp') (typ_of exp') exp', pat') + | Same_vars (exp') -> + Same_vars (E_aux (E_cast (typ, exp'), annot)) + end | _ -> (* after rewrite_defs_letbind_effects this expression is pure and updates no variables: check n_exp_term and where it's used. *) @@ -3562,7 +3581,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | LEXP_aux (LEXP_id id, _) -> P_id id, typ_of v | LEXP_aux (LEXP_cast (typ, id), _) -> - unaux_pat (add_p_typ typ (annot_pat (P_id id) l env (typ_of v))), typ + unaux_pat (add_p_typ env typ (annot_pat (P_id id) l env (typ_of v))), typ | _ -> raise (Reporting.err_unreachable l __POS__ "E_var with a lexp that is not a variable") in @@ -3576,6 +3595,9 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = rewrite_var_updates exp' | E_internal_plet (pat,v,body) -> failwith "rewrite_var_updates: E_internal_plet shouldn't be introduced yet" + | E_cast (typ, exp) -> + let exp' = rewrite_var_updates exp in + E_aux (E_cast (typ, exp'), annot) (* There are no other expressions that have effects or variable updates in "tail-position": check the definition nexp_term and where it is used. *) | _ -> exp @@ -3711,7 +3733,7 @@ let rewrite_defs_remove_superfluous_returns env = let add_opt_cast typopt1 typopt2 annot exp = match typopt1, typopt2 with - | Some typ, _ | _, Some typ -> add_e_cast typ exp + | Some typ, _ | _, Some typ -> add_e_cast (env_of exp) typ exp | None, None -> exp in -- cgit v1.2.3 From 3cf9b1daf8536c4cbbfe38e3e0e9d468b62cab3e Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 13 Apr 2020 17:48:27 +0100 Subject: Rewrite vector concat lexps to sequences of assignments ... instead of a tuple assignment. This makes the rewrite independent of the tuple assignment rewrite and allows it to be moved after the latter (nesting vector concat lexps into tuple lexps is an idiom in ASL, but the other way around doesn't make sense). --- src/rewrites.ml | 45 +++++++++++++++++++++++---------------------- 1 file changed, 23 insertions(+), 22 deletions(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index 063bbadb..ffa790f5 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2063,35 +2063,36 @@ let rewrite_vector_concat_assignments env defs = match nexp_simp len with | Nexp_aux (Nexp_constant len, _) -> len | _ -> (Big_int.of_int 1) - else (Big_int.of_int 1) in + else (Big_int.of_int 1) + in let next i step = if is_order_inc ord then (Big_int.sub (Big_int.add i step) (Big_int.of_int 1), Big_int.add i step) - else (Big_int.add (Big_int.sub i step) (Big_int.of_int 1), Big_int.sub i step) in + else (Big_int.add (Big_int.sub i step) (Big_int.of_int 1), Big_int.sub i step) + in let i = match nexp_simp start with - | (Nexp_aux (Nexp_constant i, _)) -> i - | _ -> if is_order_inc ord then Big_int.zero else Big_int.of_int (List.length lexps - 1) in + | (Nexp_aux (Nexp_constant i, _)) -> i + | _ -> if is_order_inc ord then Big_int.zero else Big_int.of_int (List.length lexps - 1) + in let l = gen_loc (fst annot) in - let exp' = - if small exp then strip_exp exp - else mk_exp (E_id (mk_id "split_vec")) in + let vec_id = mk_id "split_vec" in + let exp' = if small exp then strip_exp exp else mk_exp (E_id vec_id) in let lexp_to_exp (i, exps) lexp = let (j, i') = next i (len lexp) in let i_exp = mk_exp (E_lit (mk_lit (L_num i))) in let j_exp = mk_exp (E_lit (mk_lit (L_num j))) in let sub = mk_exp (E_vector_subrange (exp', i_exp, j_exp)) in - (i', exps @ [sub]) in + (i', exps @ [sub]) + in let (_, exps) = List.fold_left lexp_to_exp (i, []) lexps in - let tup = mk_exp (E_tuple exps) in - let lexp = LEXP_aux (LEXP_tup (List.map strip_lexp lexps), (l, ())) in - let e_aux = - if small exp then mk_exp (E_assign (lexp, tup)) - else mk_exp ( - E_let ( - mk_letbind (mk_pat (P_id (mk_id "split_vec"))) (strip_exp exp), - mk_exp (E_assign (lexp, tup)))) in + let assign lexp exp = mk_exp (E_assign (strip_lexp lexp, exp)) in + let block = mk_exp (E_block (List.map2 assign lexps exps)) in + let full_exp = + if small exp then block else + mk_exp (E_let (mk_letbind (mk_pat (P_id vec_id)) (strip_exp exp), block)) + in begin - try check_exp env e_aux unit_typ with + try check_exp env full_exp unit_typ with | Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) end @@ -4930,8 +4931,8 @@ let rewrites_lem = [ ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); ("remove_impossible_int_cases", []); - ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); ("simple_assignments", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); @@ -4972,8 +4973,8 @@ let rewrites_coq = [ ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); ("remove_impossible_int_cases", []); - ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); ("simple_assignments", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); @@ -5021,8 +5022,8 @@ let rewrites_ocaml = [ ("mapping_builtins", []); ("undefined", [Bool_arg false]); ("vector_string_pats_to_bit_list", []); - ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); ("simple_assignments", []); ("remove_not_pats", []); ("remove_vector_concat", []); @@ -5053,8 +5054,8 @@ let rewrites_c = [ ("remove_vector_concat", []); ("remove_bitvector_pats", []); ("pattern_literals", [Literal_arg "all"]); - ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); ("simple_assignments", []); ("exp_lift_assign", []); ("merge_function_clauses", []); @@ -5069,8 +5070,8 @@ let rewrites_interpreter = [ ("pat_string_append", []); ("mapping_builtins", []); ("undefined", [Bool_arg false]); - ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); ("simple_assignments", []) ] -- cgit v1.2.3 From 1dfbac50e4aa49a59286d2aaf51a6745fb4e5f60 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sun, 29 Mar 2020 00:34:21 +0000 Subject: Add more mono rewrites for bitvector subranges --- src/monomorphise.ml | 227 ++++++++++++++++++++++++++++++++++------------------ 1 file changed, 151 insertions(+), 76 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 8279f83d..1c6d0fd3 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2705,14 +2705,20 @@ let is_constant = function | E_aux (E_lit _,_) -> true | _ -> false -let is_constant_vec_typ env typ = +let get_constant_vec_len env typ = let typ = Env.base_typ_of env typ in match destruct_bitvector env typ with | Some (size,_) -> (match nexp_simp size with - | Nexp_aux (Nexp_constant _,_) -> true - | _ -> false) - | _ -> false + | Nexp_aux (Nexp_constant i,_) -> Some i + | _ -> None) + | _ -> None + +let is_constant_vec_typ env typ = (get_constant_vec_len env typ <> None) + +let is_zeros env id = + is_id env (Id "Zeros") id || is_id env (Id "zeros") id || + is_id env (Id "sail_zeros") id (* We have to add casts in here with appropriate length information so that the type checker knows the expected return types. *) @@ -2721,10 +2727,7 @@ let rec rewrite_app env typ (id,args) = let is_append = is_id env (Id "append") in let is_subrange = is_id env (Id "vector_subrange") in let is_slice = is_id env (Id "slice") in - let is_zeros id = - is_id env (Id "Zeros") id || is_id env (Id "zeros") id || - is_id env (Id "sail_zeros") id - in + let is_zeros id = is_zeros env id in let is_ones id = is_id env (Id "Ones") id || is_id env (Id "ones") id || is_id env (Id "sail_ones") id in let is_zero_extend = @@ -2734,6 +2737,21 @@ let rec rewrite_app env typ (id,args) = in let is_truncate = is_id env (Id "truncate") id in let mk_exp e = E_aux (e, (Unknown, empty_tannot)) in + let rec is_zeros_exp e = match unaux_exp e with + | E_app (zeros, [_]) when is_zeros zeros -> true + | E_lit (L_aux ((L_bin s | L_hex s), _)) -> + List.for_all (fun c -> c = '0') (Util.string_to_list s) + | E_cast (_, e) -> is_zeros_exp e + | _ -> false + in + let rec get_zeros_exp_len e = match unaux_exp e with + | E_app (zeros, [len]) when is_zeros zeros -> Some len + | E_cast (_, e) -> get_zeros_exp_len e + | _ -> + match get_constant_vec_len (env_of e) (typ_of e) with + | Some i -> Some (mk_exp (E_lit (L_aux (L_num i, Unknown)))) + | None -> None + in let try_cast_to_typ (E_aux (e,(l, _)) as exp) = let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in match size with @@ -2806,20 +2824,24 @@ let rec rewrite_app env typ (id,args) = end (* variable-slice @ zeros *) - | [E_aux (E_app (slice1, [vector1; start1; len1]),_); - E_aux (E_app (zeros2, [len2]),_)] - when is_slice slice1 && is_zeros zeros2 && is_bitvector_typ (typ_of vector1) && - not (is_constant start1 && is_constant len1 && is_constant len2) -> - try_cast_to_typ - (mk_exp (E_app (mk_id "place_slice", [vector1; start1; len1; len2]))) + | [E_aux (E_app (op, [vector1; start1; len1]),_); zeros_exp] + when (is_slice op || is_subrange op) && is_zeros_exp zeros_exp + && is_bitvector_typ (typ_of vector1) + && not (is_constant start1 && is_constant len1 && is_constant_vec_typ env (typ_of zeros_exp)) -> + let op' = if is_subrange op then "place_subrange" else "place_slice" in + begin match get_zeros_exp_len zeros_exp with + | Some zlen -> try_cast_to_typ (mk_exp (E_app (mk_id op', [vector1; start1; len1; zlen]))) + | None -> E_app (id, args) + end (* ones @ zeros *) - | [E_aux (E_app (ones1, [len1]), _); - E_aux (E_app (zeros2, [len2]), _)] - when is_ones ones1 && is_zeros zeros2 && - not (is_constant len1 && is_constant len2) -> - try_cast_to_typ - (mk_exp (E_app (mk_id "slice_mask", [len2; len1]))) + | [E_aux (E_app (ones1, [len1]), _); zeros_exp] + when is_ones ones1 && is_zeros_exp zeros_exp && + not (is_constant len1 && is_constant_vec_typ env (typ_of zeros_exp)) -> + begin match get_zeros_exp_len zeros_exp with + | Some zlen -> try_cast_to_typ (mk_exp (E_app (mk_id "slice_mask", [zlen; len1]))) + | None -> E_app (id, args) + end (* variable-range @ variable-range *) | [E_aux (E_app (subrange1, @@ -2847,24 +2869,33 @@ let rec rewrite_app env typ (id,args) = [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot))) (* variable-slice @ local-var *) - | [E_aux (E_app (slice1, + | [E_aux (E_app (op, [vector1; start1; length1]),_); (E_aux (E_id _,_) as vector2)] - when is_slice slice1 && is_bitvector_typ (typ_of vector1) && + when (is_slice op || is_subrange op) && is_bitvector_typ (typ_of vector1) && not (is_constant length1) -> - let start2 = mk_exp (E_lit (mk_lit (L_num Big_int.zero))) in + let op' = if is_subrange op then "subrange_subrange_concat" else "slice_slice_concat" in + let zero = mk_exp (E_lit (mk_lit (L_num Big_int.zero))) in + let one = mk_exp (E_lit (mk_lit (L_num (Big_int.of_int 1)))) in let length2 = mk_exp (E_app (mk_id "length", [vector2])) in + let indices2 = + if is_subrange op then + [mk_exp (E_app_infix (length2, mk_id "-", one)); zero] + else + [zero; length2] + in try_cast_to_typ - (E_aux (E_app (mk_id "slice_slice_concat", - [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot))) + (E_aux (E_app (mk_id op', + [vector1; start1; length1; vector2] @ indices2),(Unknown,empty_tannot))) | [E_aux (E_app (append1, [e1; - E_aux (E_app (slice1, [vector1; start1; length1]),_)]),_); + E_aux (E_app (op, [vector1; start1; length1]),_)]),_); E_aux (E_app (zeros1, [length2]),_)] - when is_append append1 && is_slice slice1 && is_zeros zeros1 && + when is_append append1 && (is_slice op || is_subrange op) && is_zeros zeros1 && is_constant_vec_typ env (typ_of e1) && is_bitvector_typ (typ_of vector1) && not (is_constant length1 || is_constant length2) -> + let op' = mk_id (if is_subrange op then "subrange_zeros_concat" else "slice_zeros_concat") in let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in let midsize = nminus size size1 in begin @@ -2875,14 +2906,14 @@ let rec rewrite_app env typ (id,args) = (E_aux (E_app (mk_id "append", [e1; E_aux (E_cast (midtyp, - E_aux (E_app (mk_id "slice_zeros_concat", + E_aux (E_app (op', [vector1; start1; length1; length2]),(Unknown,empty_tannot))),(Unknown,empty_tannot))]), (Unknown,empty_tannot))) | _ -> try_cast_to_typ (E_aux (E_app (mk_id "append", [e1; - E_aux (E_app (mk_id "slice_zeros_concat", + E_aux (E_app (op', [vector1; start1; length1; length2]),(Unknown,empty_tannot))]), (Unknown,empty_tannot))) end @@ -2900,6 +2931,22 @@ let rec rewrite_app env typ (id,args) = | _ -> E_app (id,args) + else if is_id env (Id "vector_update_subrange") id then + match args with + | [vec1; start1; end1; (E_aux (E_app (subrange2, [vec2; start2; end2]), _) as e2)] + when is_subrange subrange2 && not (is_constant_vec_typ env (typ_of e2)) -> + let op = + if is_number (typ_of vec2) then "vector_update_subrange_from_integer_subrange" else + "vector_update_subrange_from_subrange" + in + try_cast_to_typ (E_aux (E_app (mk_id op, [vec1; start1; end1; vec2; start2; end2]), (Unknown, empty_tannot))) + + | [vec1; start1; end1; (E_aux (E_app (zeros, _), _) as e2)] + when is_zeros zeros && not (is_constant_vec_typ env (typ_of e2)) -> + try_cast_to_typ (E_aux (E_app (mk_id "set_subrange_zeros", [vec1; start1; end1]), (Unknown, empty_tannot))) + + | _ -> E_app (id, args) + else if is_id env (Id "eq_bits") id || is_id env (Id "neq_bits") id then (* variable-range == variable_range *) let wrap e = @@ -2931,11 +2978,12 @@ let rec rewrite_app env typ (id,args) = in wrap (E_app (mk_id "subrange_subrange_eq", [vector1; upper start1 len1; start1; vector2; upper start2 len2; start2])) - | [E_aux (E_app (slice1, [vector1; start1; len1]), _); + | [(E_aux (E_app (op, [vector1; start1; len1]), _) as e1); E_aux (E_app (zeros2, _), _)] - when is_slice slice1 && is_zeros zeros2 && not (is_constant len1) && - is_bitvector_typ (typ_of vector1) -> - wrap (E_app (mk_id "is_zeros_slice", [vector1; start1; len1])) + when (is_slice op || is_subrange op) && is_zeros zeros2 + && not (is_constant_vec_typ env (typ_of e1)) && is_bitvector_typ (typ_of vector1) -> + let op' = if is_subrange op then "is_zero_subrange" else "is_zeros_slice" in + wrap (E_app (mk_id op', [vector1; start1; len1])) | _ -> E_app (id,args) else if is_id env (Id "IsZero") id then @@ -2965,43 +3013,47 @@ let rec rewrite_app env typ (id,args) = else if is_zero_extend || is_truncate then let length_arg = List.filter (fun arg -> is_number (typ_of arg)) args in match List.filter (fun arg -> not (is_number (typ_of arg))) args with - | [E_aux (E_app (append1, - [E_aux (E_app (subrange1, [vector1; start1; end1]), _); - (E_aux (E_app (zeros1, [len1]),_) | - E_aux (E_cast (_,E_aux (E_app (zeros1, [len1]),_)),_)) - ]),_)] - when is_subrange subrange1 && is_zeros zeros1 && is_append append1 && is_bitvector_typ (typ_of vector1) - -> try_cast_to_typ (rewrap (E_app (mk_id "place_subrange", length_arg @ [vector1; start1; end1; len1]))) + | [E_aux (E_app (append1, [E_aux (E_app (subrange1, [vector1; start1; end1]), _); zeros_exp]),_)] + when is_subrange subrange1 && is_zeros_exp zeros_exp && is_append append1 && is_bitvector_typ (typ_of vector1) -> + begin match get_zeros_exp_len zeros_exp with + | Some zlen -> + try_cast_to_typ (rewrap (E_app (mk_id "place_subrange", length_arg @ [vector1; start1; end1; zlen]))) + | None -> E_app (id, args) + end - | [E_aux (E_app (append1, - [vector1; - (E_aux (E_app (zeros1, [length2]),_) | - E_aux (E_cast (_, E_aux (E_app (zeros1, [length2]),_)),_)) - ]),_)] - when is_constant_vec_typ env (typ_of vector1) && is_zeros zeros1 && is_append append1 - -> let (vector1, start1, length1) = - match vector1 with - | E_aux (E_app (slice1, [vector1; start1; length1]), _) -> - (vector1, start1, length1) - | _ -> - let (length1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of vector1)) in - (vector1, mk_exp (E_lit (mk_lit (L_num (Big_int.zero)))), mk_exp (E_sizeof length1)) - in - try_cast_to_typ (rewrap (E_app (mk_id "place_slice", length_arg @ [vector1; start1; length1; length2]))) + | [E_aux (E_app (append1, [vector1; zeros_exp]),_)] + when is_constant_vec_typ env (typ_of vector1) && is_zeros_exp zeros_exp && is_append append1 -> + begin match get_zeros_exp_len zeros_exp with + | Some zlen -> + let (vector1, start1, length1) = + match vector1 with + | E_aux (E_app (slice1, [vector1; start1; length1]), _) -> + (vector1, start1, length1) + | _ -> + let (length1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of vector1)) in + (vector1, mk_exp (E_lit (mk_lit (L_num (Big_int.zero)))), mk_exp (E_sizeof length1)) + in + try_cast_to_typ (rewrap (E_app (mk_id "place_slice", length_arg @ [vector1; start1; length1; zlen]))) + | None -> E_app (id, args) + end (* If we've already rewritten to slice_slice_concat or subrange_subrange_concat, we can just drop the zero extension because those functions can do it themselves *) - | [E_aux (E_cast (_, (E_aux (E_app (Id_aux ((Id "slice_slice_concat" | Id "subrange_subrange_concat" | Id "place_slice"),_) as op, args),_))),_)] + | [E_aux (E_cast (_, (E_aux (E_app (Id_aux ((Id "slice_slice_concat" | Id "subrange_subrange_concat" | Id "place_slice" | Id "place_subrange"),_) as op, args),_))),_)] -> try_cast_to_typ (rewrap (E_app (op, length_arg @ args))) - | [E_aux (E_app (Id_aux ((Id "slice_slice_concat" | Id "subrange_subrange_concat" | Id "place_slice"),_) as op, args),_)] + | [E_aux (E_app (Id_aux ((Id "slice_slice_concat" | Id "subrange_subrange_concat" | Id "place_slice" | Id "place_subrange"),_) as op, args),_)] -> try_cast_to_typ (rewrap (E_app (op, length_arg @ args))) | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] - when is_slice slice1 && not (is_constant length1) -> + when is_slice slice1 && not (is_constant length1) && is_bitvector_typ (typ_of vector1) -> try_cast_to_typ (rewrap (E_app (mk_id "zext_slice", length_arg @ [vector1; start1; length1]))) + | [E_aux (E_app (subrange1, [vector1; hi1; lo1]),_)] + when is_subrange subrange1 && not (is_constant hi1 && is_constant lo1) && is_bitvector_typ (typ_of vector1) -> + try_cast_to_typ (rewrap (E_app (mk_id "zext_subrange", length_arg @ [vector1; hi1; lo1]))) + | [E_aux (E_app (ones, [len1]),_)] when is_ones ones -> try_cast_to_typ (rewrap (E_app (mk_id "zext_ones", length_arg @ [len1]))) @@ -3013,7 +3065,7 @@ let rec rewrite_app env typ (id,args) = | [E_aux (E_app (zeros, [len1]),_)] | [E_aux (E_cast (_, E_aux (E_app (zeros, [len1]),_)), _)] when is_zeros zeros -> - try_cast_to_typ (rewrap (E_app (id, length_arg))) + try_cast_to_typ (rewrap (E_app (zeros, length_arg))) | _ -> E_app (id,args) @@ -3024,28 +3076,28 @@ let rec rewrite_app env typ (id,args) = when is_slice slice1 && not (is_constant length1) && is_bitvector_typ (typ_of vector1) -> try_cast_to_typ (rewrap (E_app (mk_id "sext_slice", length_arg @ [vector1; start1; length1]))) - | [E_aux (E_app (append, - [E_aux (E_app (subrange1, [vector1; start1; end1]), _); - (E_aux (E_app (zeros2, [len2]), _) | - E_aux (E_cast (_, E_aux (E_app (zeros2, [len2]), _)),_)) - ]), _)] - when is_append append && is_subrange subrange1 && is_zeros zeros2 && - not (is_constant len2) && is_bitvector_typ (typ_of vector1) -> - E_app (mk_id "place_subrange_signed", length_arg @ [vector1; start1; end1; len2]) - - | [E_aux (E_app (append, - [E_aux (E_app (slice1, [vector1; start1; len1]), _); - (E_aux (E_app (zeros2, [len2]), _) | - E_aux (E_cast (_, E_aux (E_app (zeros2, [len2]), _)),_)) - ]), _)] - when is_append append && is_slice slice1 && is_zeros zeros2 && is_bitvector_typ (typ_of vector1) && - not (is_constant len1 && is_constant len2) -> - E_app (mk_id "place_slice_signed", length_arg @ [vector1; start1; len1; len2]) + | [E_aux (E_app (subrange1, [vector1; hi1; lo1]),_)] + when is_subrange subrange1 && not (is_constant hi1 && is_constant lo1) && is_bitvector_typ (typ_of vector1) -> + try_cast_to_typ (rewrap (E_app (mk_id "sext_subrange", length_arg @ [vector1; hi1; lo1]))) + + | [E_aux (E_app (append, [E_aux (E_app (op, [vector1; start1; len1]), _); zeros_exp]), _)] + when is_append append && (is_slice op || is_subrange op) && is_zeros_exp zeros_exp + && is_bitvector_typ (typ_of vector1) + && not (is_constant len1 && is_constant_vec_typ env (typ_of zeros_exp)) -> + let op' = if is_subrange op then "place_subrange_signed" else "place_slice_signed" in + begin match get_zeros_exp_len zeros_exp with + | Some zlen -> E_app (mk_id op', length_arg @ [vector1; start1; len1; zlen]) + | None -> E_app (id, args) + end | [E_aux (E_cast (_, (E_aux (E_app (Id_aux ((Id "place_slice"),_), args),_))),_)] | [E_aux (E_app (Id_aux ((Id "place_slice"),_), args),_)] -> try_cast_to_typ (rewrap (E_app (mk_id "place_slice_signed", length_arg @ args))) + | [E_aux (E_cast (_, (E_aux (E_app (Id_aux ((Id "place_subrange"),_), args),_))),_)] + | [E_aux (E_app (Id_aux ((Id "place_subrange"),_), args),_)] + -> try_cast_to_typ (rewrap (E_app (mk_id "place_subrange_signed", length_arg @ args))) + (* If the original had a length, keep it *) (* | [E_aux (E_app (slice1, [vector1; start1; length1]),_);length2] when is_slice slice1 && not (is_constant length1) -> @@ -3078,6 +3130,14 @@ let rec rewrite_app env typ (id,args) = when is_subrange subrange1 && not (is_constant_range (start1,end1)) && is_bitvector_typ (typ_of vector1) -> E_app (mk_id "unsigned_subrange", [vector1; start1; end1]) + | [E_aux (E_app (append, [vector1; zeros2]), _)] + when is_append append && is_zeros_exp zeros2 && not (is_constant_vec_typ env (typ_of zeros2)) -> + begin match get_zeros_exp_len zeros2 with + | Some len -> + E_app (mk_id "shl_int", [E_aux (E_app (id, [vector1]), (Unknown, empty_tannot)); len]) + | None -> E_app (id, args) + end + | _ -> E_app (id,args) else if is_id env (Id "__SetSlice_bits") id then @@ -3087,6 +3147,15 @@ let rec rewrite_app env typ (id,args) = E_app (mk_id "set_slice_zeros", [len; vector; start; slice_len]) | _ -> E_app (id, args) + else if is_id env (Id "Replicate") id then + let length_arg = List.filter (fun arg -> is_number (typ_of arg)) args in + match List.filter (fun arg -> not (is_number (typ_of arg))) args with + | [E_aux (E_lit (L_aux (L_bin "0", _)), _)] -> + E_app (mk_id "sail_zeros", length_arg) + | [E_aux (E_lit (L_aux (L_bin "1", _)), _)] -> + E_app (mk_id "sail_ones", length_arg) + | _ -> E_app (id, args) + else E_app (id,args) let rewrite_aux = function @@ -3108,6 +3177,12 @@ let rewrite_aux = function start1; end1; vector2; start2; end2]),(Unknown,empty_tannot))), (l_assign, empty_tannot)) + | E_assign (LEXP_aux (LEXP_vector_range (LEXP_aux (LEXP_id id1, annot1), start1, end1), _), + E_aux (E_app (zeros, _), _)), annot + when is_zeros (env_of_annot annot) zeros -> + let lhs = LEXP_aux (LEXP_id id1, annot1) in + let rhs = E_aux (E_app (mk_id "set_subrange_zeros", [E_aux (E_id id1, annot1); start1; end1]), annot1) in + E_aux (E_assign (lhs, rhs), annot) | exp,annot -> E_aux (exp,annot) let mono_rewrite defs = -- cgit v1.2.3 From 264ab693afa90a1e9fa842f5972f64dc7e06c492 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 4 Apr 2020 17:16:29 +0100 Subject: Save SMT cache when terminating with an exception --- src/sail.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'src') diff --git a/src/sail.ml b/src/sail.ml index ea642470..b2ca498a 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -597,4 +597,5 @@ let _ = try with Reporting.Fatal_error e -> Reporting.print_error e; Interactive.opt_suppress_banner := true; + if !opt_memo_z3 then Constraint.save_digests () else (); if !Interactive.opt_interactive then () else exit 1 -- cgit v1.2.3 From e1a2b0d2a88e4797d714ad0cb941c3cbf019720b Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 4 Apr 2020 17:20:06 +0100 Subject: Tweak types of loop combinators for prover combinators Split the variable (tuple) type into an input and output type. They are meant to be the same, but due to the way function types are instantiated, unification can fail in the case of existential types, as in the added test case (when trying to generate Lem definitions from it). The output of the loop will be checked against the expected type, though, due to a type annotation outside the loop added by the rewrite pass for variable updates. --- src/rewrites.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index ffa790f5..abb3e4ed 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3785,11 +3785,11 @@ let rewrite_defs_remove_superfluous_returns env = let rewrite_defs_remove_e_assign env (Defs defs) = let (Defs loop_specs) = fst (Type_error.check initial_env (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"); - ("while#t", "forall ('vars : Type). (bool, 'vars, 'vars, int) -> 'vars"); - ("until#t", "forall ('vars : Type). (bool, 'vars, 'vars, int) -> 'vars")]))) in + [("foreach#", "forall ('vars_in 'vars_out : Type). (int, int, int, bool, 'vars_in, 'vars_out) -> 'vars_out"); + ("while#", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out) -> 'vars_out"); + ("until#", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out) -> 'vars_out"); + ("while#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out"); + ("until#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out")]))) in let rewrite_exp _ e = replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in rewrite_defs_base -- cgit v1.2.3 From 253e41a36015036cf6331be44b0bd605afe8c109 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 4 Apr 2020 21:57:54 +0100 Subject: Add support for some ASL idioms in mono rewrites --- src/monomorphise.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 1c6d0fd3..9efacb7a 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -232,6 +232,10 @@ and contains_exist_arg (A_aux (arg,_)) = -> false | A_typ typ -> contains_exist typ +let is_number typ = match destruct_numeric typ with + | Some _ -> true + | None -> false + let rec size_nvars_nexp (Nexp_aux (ne,_)) = match ne with | Nexp_var v -> [v] @@ -3171,8 +3175,13 @@ let rewrite_aux = function annot when is_id (env_of_annot annot) (Id "vector_subrange") subrange2 && not (is_constant_range (start1, end1)) -> + let typ2 = Env.base_typ_of (env_of_annot annot) (typ_of vector2) in + let op = + if is_number typ2 then "vector_update_subrange_from_integer_subrange" else + "vector_update_subrange_from_subrange" + in E_aux (E_assign (LEXP_aux (LEXP_id id1,(l_id1,empty_tannot)), - E_aux (E_app (mk_id "vector_update_subrange_from_subrange", [ + E_aux (E_app (mk_id op, [ E_aux (E_id id1,(Generated l_id1,empty_tannot)); start1; end1; vector2; start2; end2]),(Unknown,empty_tannot))), -- cgit v1.2.3 From f656842b6344eb8489044619874d6e89ef7eb0a7 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 4 Apr 2020 22:21:30 +0100 Subject: Handle more cases in bitvector cast rewrite Add casts for function arguments using the constraints in the environment of the function clause (not just assertions within the function body). Also pass in the global typing environment for comparison with the environment within the function clause (and make a corresponding change in the Lem pretty-printer so that it uses the right environments). --- src/monomorphise.ml | 14 ++++++++++---- src/monomorphise.mli | 2 +- src/pretty_print_lem.ml | 20 ++++++++++---------- src/rewrites.ml | 2 +- 4 files changed, 22 insertions(+), 16 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 9efacb7a..4eea717a 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3479,7 +3479,7 @@ let rec extract (E_aux (e,_)) = provide some way for the Lem pretty printer to know what to use; currently we just use two names for the cast, bitvector_cast_in and bitvector_cast_out, to let the pretty printer know whether to use the top-level environment. *) -let add_bitvector_casts (Defs defs) = +let add_bitvector_casts global_env (Defs defs) = let rewrite_body id quant_kids top_env ret_typ exp = let rewrite_aux (e,ann) = match e with @@ -3568,9 +3568,8 @@ let add_bitvector_casts (Defs defs) = e_aux = rewrite_aux } exp in let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),((l,_) as fcl_ann))) = - let fcl_env = env_of_annot fcl_ann in - let (tq,typ) = Env.get_val_spec_orig id fcl_env in - let fun_env = add_typquant l tq fcl_env in + let (tq,typ) = Env.get_val_spec_orig id global_env in + let fun_env = List.fold_right (Env.add_typ_var l) (quant_kopts tq) global_env in let quant_kids = List.map kopt_kid (List.filter is_int_kopt (quant_kopts tq)) in let ret_typ = match typ with @@ -3582,6 +3581,13 @@ let add_bitvector_casts (Defs defs) = in let pat,guard,body,annot = destruct_pexp pexp in let body = rewrite_body id quant_kids fun_env ret_typ body in + (* Cast function arguments, if necessary *) + let add_constraint insts = function + | NC_aux (NC_equal (Nexp_aux (Nexp_var kid,_), nexp), _) -> KBindings.add kid nexp insts + | _ -> insts + in + let insts = List.fold_left add_constraint KBindings.empty (Env.get_constraints (env_of body)) in + let body = make_bitvector_env_casts fun_env (env_of body) quant_kids insts body in (* Also add a cast around the entire function clause body, if necessary *) let body = make_bitvector_cast_exp "bitvector_cast_out" fun_env quant_kids (fill_in_type (env_of body) (typ_of body)) ret_typ body diff --git a/src/monomorphise.mli b/src/monomorphise.mli index 39d89461..b4eb7ead 100644 --- a/src/monomorphise.mli +++ b/src/monomorphise.mli @@ -69,7 +69,7 @@ val mono_rewrites : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_toplevel_nexps : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs (* Add casts across case splits *) -val add_bitvector_casts : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs (* Replace atom arguments which are fixed by a type parameter for a size with a singleton type *) val rewrite_atoms_to_singletons : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 0994a821..581872ee 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1367,7 +1367,7 @@ let doc_fun_body_lem ctxt exp = then align (string "catch_early_return" ^//^ parens (doc_exp)) else doc_exp -let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) = +let doc_funcl_lem type_env (FCL_aux(FCL_Funcl(id, pexp), annot)) = let typ = typ_of_annot annot in let arg_typs = match typ with | Typ_aux (Typ_fn (arg_typs, typ_ret, _), _) -> arg_typs @@ -1377,7 +1377,7 @@ let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) = let ctxt = { early_ret = contains_early_return exp; bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ); - top_env = env_of_annot annot } in + top_env = type_env } in let pats, bind = untuple_args_pat pat arg_typs in let patspp = separate_map space (doc_pat_lem ctxt true) pats in let _ = match guard with @@ -1398,16 +1398,16 @@ module StringSet = Set.Make(String) (* Strictly speaking, Lem doesn't support multiple clauses for a single function joined by "and", although it has worked for Isabelle before. However, all the funcls should have been merged by the merge_funcls rewrite now. *) -let doc_fundef_rhs_lem (FD_aux(FD_function(r, typa, efa, funcls),fannot) as fd) = - separate_map (hardline ^^ string "and ") doc_funcl_lem funcls +let doc_fundef_rhs_lem type_env (FD_aux(FD_function(r, typa, efa, funcls),fannot) as fd) = + separate_map (hardline ^^ string "and ") (doc_funcl_lem type_env) funcls -let doc_mutrec_lem = function +let doc_mutrec_lem type_env = function | [] -> failwith "DEF_internal_mutrec with empty function list" | fundefs -> string "let rec " ^^ - separate_map (hardline ^^ string "and ") doc_fundef_rhs_lem fundefs + separate_map (hardline ^^ string "and ") (doc_fundef_rhs_lem type_env) fundefs -let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = +let rec doc_fundef_lem type_env (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = match fcls with | [] -> failwith "FD_function with empty function list" | FCL_aux (FCL_Funcl(id, pexp),annot) :: _ @@ -1422,7 +1422,7 @@ let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = pexp in let doc_rec = if is_funcl_rec then [string "rec"] else [] in - separate space ([string "let"] @ doc_rec @ [doc_fundef_rhs_lem fd]) + separate space ([string "let"] @ doc_rec @ [doc_fundef_rhs_lem type_env fd]) | _ -> empty @@ -1523,8 +1523,8 @@ let rec doc_def_lem type_env def = | DEF_reg_dec dec -> group (doc_dec_lem dec) | DEF_default df -> empty - | DEF_fundef fdef -> group (doc_fundef_lem fdef) ^/^ hardline - | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline + | DEF_fundef fdef -> group (doc_fundef_lem type_env fdef) ^/^ hardline + | DEF_internal_mutrec fundefs -> doc_mutrec_lem type_env fundefs ^/^ hardline | DEF_val (LB_aux (LB_val (pat, _), _) as lbind) -> group (doc_let_lem empty_ctxt lbind) ^/^ hardline | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point" diff --git a/src/rewrites.ml b/src/rewrites.ml index abb3e4ed..a3238cce 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4873,7 +4873,7 @@ let all_rewrites = [ ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps); ("monomorphise", String_rewriter (fun target -> Basic_rewriter (monomorphise target))); ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons)); - ("add_bitvector_casts", Basic_rewriter (fun _ -> Monomorphise.add_bitvector_casts)); + ("add_bitvector_casts", Basic_rewriter Monomorphise.add_bitvector_casts); ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons)); ("remove_impossible_int_cases", Basic_rewriter Constant_propagation.remove_impossible_int_cases); ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_defs target))); -- cgit v1.2.3 From 329dd65ddf65ee3edc858200571973c713165e08 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 4 Apr 2020 22:26:57 +0100 Subject: Mono: Extract set constraints from (in)equalities --- src/monomorphise.ml | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4eea717a..4b7ed20c 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -138,6 +138,29 @@ let extract_set_nc env l var nc = let re nc = NC_aux (nc,l) in match nc with | NC_set (id,is) when KidSet.mem id vars -> Some (is,re NC_true) + | NC_equal (Nexp_aux (Nexp_var id,_), Nexp_aux (Nexp_constant n,_)) + when KidSet.mem id vars -> + Some ([n], re NC_true) + (* Turn (i <= 'v & 'v <= j & ...) into set constraint ('v in {i..j}) *) + | NC_and (NC_aux (NC_bounded_le (Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_var kid, _)), _) as nc1, nc2) + when KidSet.mem kid vars -> + let aux2 () = match aux expanded nc2 with + | Some (is, nc2') -> Some (is, re (NC_and (nc1, nc2'))) + | None -> None + in + begin match constraint_conj nc2 with + | NC_aux (NC_bounded_le (Nexp_aux (Nexp_var kid', _), Nexp_aux (Nexp_constant n', _)), _) :: ncs + when KidSet.mem kid' vars -> + let len = Big_int.succ (Big_int.sub n' n) in + if Big_int.less_equal Big_int.zero len && Big_int.less_equal len (Big_int.of_int size_set_limit) then + let elem i = Big_int.add n (Big_int.of_int i) in + let is = List.init (Big_int.to_int len) elem in + if aux expanded (List.fold_left nc_and nc_true ncs) <> None then + raise (Reporting.err_general l ("Multiple set constraints for " ^ string_of_kid var)) + else Some (is, nc_full) + else aux2 () + | _ -> aux2 () + end | NC_and (nc1,nc2) -> (match aux expanded nc1, aux expanded nc2 with | None, None -> None @@ -2493,6 +2516,8 @@ let rec sets_from_assert e = match nc with | NC_and (nc1,nc2) -> merge_set_asserts_by_kid (sets_from_nc nc1) (sets_from_nc nc2) | NC_set (kid,is) -> KBindings.singleton kid (l,is) + | NC_equal (Nexp_aux (Nexp_var kid,_), Nexp_aux (Nexp_constant n,_)) -> + KBindings.singleton kid (l, [n]) | NC_or _ -> (match set_from_nc_or nc_full with | Some (kid, is) -> KBindings.singleton kid (l,is) -- cgit v1.2.3 From 42197879faa99536a58dc9b141f276f84c88f7cc Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 10 Apr 2020 13:21:07 +0100 Subject: Consider literals in pattern disjointness check This check is used in the guarded pattern rewrite step, which would previously generate some impossible matches (e.g. matching expression "true" against pattern "false"). --- src/rewrites.ml | 40 ++++++++++++++++++++++++++++++---------- 1 file changed, 30 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index a3238cce..7705c75b 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -709,6 +709,26 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = | _, P_wild -> if is_irrefutable_pattern pat1 then Some [] else None | _ -> None +let vector_string_to_bits_pat (L_aux (lit, _) as l_aux) (l, tannot) = + let bit_annot = match destruct_tannot tannot with + | Some (env, _, _) -> mk_tannot env bit_typ no_effect + | None -> empty_tannot + in + begin match lit with + | L_hex _ | L_bin _ -> P_aux (P_vector (List.map (fun p -> P_aux (P_lit p, (l, bit_annot))) (vector_string_to_bit_list l_aux)), (l, tannot)) + | lit -> P_aux (P_lit l_aux, (l, tannot)) + end + +let vector_string_to_bits_exp (L_aux (lit, _) as l_aux) (l, tannot) = + let bit_annot = match destruct_tannot tannot with + | Some (env, _, _) -> mk_tannot env bit_typ no_effect + | None -> empty_tannot + in + begin match lit with + | L_hex _ | L_bin _ -> E_aux (E_vector (List.map (fun p -> E_aux (E_lit p, (l, bit_annot))) (vector_string_to_bit_list l_aux)), (l, tannot)) + | lit -> E_aux (E_lit l_aux, (l, tannot)) + end + (* A simple check for pattern disjointness; used for optimisation in the guarded pattern rewrite step *) let rec disjoint_pat env (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = @@ -722,6 +742,14 @@ let rec disjoint_pat env (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) | P_id id, _ when id_is_unbound id env -> false | _, P_id id when id_is_unbound id env -> false | P_id id1, P_id id2 -> Id.compare id1 id2 <> 0 + | P_lit (L_aux ((L_bin _ | L_hex _), _) as lit), _ -> + disjoint_pat env (vector_string_to_bits_pat lit (Unknown, empty_tannot)) pat2 + | _, P_lit (L_aux ((L_bin _ | L_hex _), _) as lit) -> + disjoint_pat env pat1 (vector_string_to_bits_pat lit (Unknown, empty_tannot)) + | P_lit (L_aux (L_num n1, _)), P_lit (L_aux (L_num n2, _)) -> + not (Big_int.equal n1 n2) + | P_lit (L_aux (l1, _)), P_lit (L_aux (l2, _)) -> + l1 <> l2 | P_app (id1, args1), P_app (id2, args2) -> Id.compare id1 id2 <> 0 || List.exists2 (disjoint_pat env) args1 args2 | P_vector pats1, P_vector pats2 @@ -1214,21 +1242,13 @@ let rewrite_defs_vector_string_pats_to_bit_list env = let rewrite_p_aux (pat, (annot : tannot annot)) = let env = env_of_annot annot in match pat with - | P_lit (L_aux (lit, l) as l_aux) -> - begin match lit with - | L_hex _ | L_bin _ -> P_aux (P_vector (List.map (fun p -> P_aux (P_lit p, (l, mk_tannot env bit_typ no_effect))) (vector_string_to_bit_list l_aux)), annot) - | lit -> P_aux (P_lit l_aux, annot) - end + | P_lit lit -> vector_string_to_bits_pat lit annot | pat -> (P_aux (pat, annot)) in let rewrite_e_aux (exp, (annot : tannot annot)) = let env = env_of_annot annot in match exp with - | E_lit (L_aux (lit, l) as l_aux) -> - begin match lit with - | L_hex _ | L_bin _ -> E_aux (E_vector (List.map (fun e -> E_aux (E_lit e, (l, mk_tannot env bit_typ no_effect))) (vector_string_to_bit_list l_aux)), annot) - | lit -> E_aux (E_lit l_aux, annot) - end + | E_lit lit -> vector_string_to_bits_exp lit annot | exp -> (E_aux (exp, annot)) in let pat_alg = { id_pat_alg with p_aux = rewrite_p_aux } in -- cgit v1.2.3 From ab0fe3e7920d10d7f9ab74649df71deb47dfb97f Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 13 Apr 2020 17:26:02 +0100 Subject: Various monomorphisation fixes - Handle more combinations of patterns and expressions in constant propagation - Remove dead code after throw() in monomorphisation - Use correct val specs and environments when analysing and pretty-printing function clauses --- src/constant_propagation.ml | 13 +++++++++++++ src/monomorphise.ml | 35 ++++++++++++++++++++++++++++++++++- src/pretty_print_lem.ml | 9 ++++++--- 3 files changed, 53 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml index 00b3d192..e785aa93 100644 --- a/src/constant_propagation.ml +++ b/src/constant_propagation.ml @@ -663,6 +663,10 @@ let const_props target defs ref_vars = | "or_bool", ([E_aux (E_lit (L_aux (L_true, _)), _) as e_true; _] | [_; E_aux (E_lit (L_aux (L_true, _)), _) as e_true]) -> e_true + | _, [E_aux (E_vector [], _); e'] + | _, [e'; E_aux (E_vector [], _)] + when is_overload_of (mk_id "append") -> + e' | _, _ when List.for_all Constant_fold.is_constant args -> const_fold exp | _, [arg] when is_overload_of (mk_id "__size") -> @@ -733,6 +737,10 @@ let const_props target defs ref_vars = (Reporting.print_err lit_l "Monomorphisation" "Unexpected kind of literal for var match"; GiveUp) end + | E_lit ((L_aux ((L_bin _ | L_hex _), _) as lit)), P_vector _ -> + let mk_bitlit lit = E_aux (E_lit lit, (Generated l, mk_tannot env bit_typ no_effect)) in + let lits' = List.map mk_bitlit (vector_string_to_bit_list lit) in + check_exp_pat (E_aux (E_vector lits', (l, annot))) pat | E_lit _, _ -> (Reporting.print_err l' "Monomorphisation" "Unexpected kind of pattern for literal"; GiveUp) @@ -744,6 +752,7 @@ let const_props target defs ref_vars = 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],[]) + | _, P_aux (P_wild, _) -> DoesMatch ([],[]) | _ -> GiveUp) es ps in let final = List.fold_left (fun acc m -> match acc, m with | _, GiveUp -> GiveUp @@ -755,6 +764,10 @@ let const_props target defs ref_vars = (Reporting.print_err l "Monomorphisation" "Unexpected kind of pattern for vector literal"; GiveUp) | _ -> final) + | E_vector _, P_lit ((L_aux ((L_bin _ | L_hex _), _) as lit)) -> + let mk_bitlit lit = P_aux (P_lit lit, (Generated l, mk_tannot env bit_typ no_effect)) in + let lits' = List.map mk_bitlit (vector_string_to_bit_list lit) in + check_exp_pat exp (P_aux (P_vector lits', (l, annot))) | E_vector _, _ -> (Reporting.print_err l "Monomorphisation" "Unexpected kind of pattern for vector literal"; GiveUp) diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4b7ed20c..e49ef4f5 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -577,6 +577,8 @@ let stop_at_false_assertions e = end | E_assert (e1,_) when exp_false e1 -> ea, Some (typ_of_annot ann) + | E_throw e -> + ea, Some (typ_of_annot ann) | _ -> ea, None in fst (exp e) @@ -1969,6 +1971,37 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps = (match mk_subrange_pattern vannot vstart vend with | Some mk_pat -> check_dep id mk_pat | None -> None) + (* TODO: Aborted attempt at considering bitvector concatenations when + refining dependencies. Needs corresponding support in constant + propagation to work. *) + (* | E_app (append, [vec1; vec2]) + when is_id (env_of exp) (Id "append") append -> + (* If the expression is a concatenation resulting in a small enough bitvector, + perform a (total) case split on the sub-vectors *) + let vec_len v = try Util.option_map Big_int.to_int (get_constant_vec_len (env_of exp) v) with _ -> None in + let pow2 n = Big_int.pow_int (Big_int.of_int 2) n in + let size_set len1 len2 = Big_int.mul (pow2 len1) (pow2 len2) in + begin match (vec_len (typ_of exp), vec_len (typ_of vec1), vec_len (typ_of vec2)) with + | (Some len, Some len1, Some len2) + when Big_int.less_equal (size_set len1 len2) (Big_int.of_int size_set_limit) -> + let recur = refine_dependency env in + (* Create pexps with dummy bodies (ignored by the recursive call) *) + let mk_pexps len = + let mk_pexp lit = + let (_, ord, _) = vector_typ_args_of (typ_of exp) in + let tannot = mk_tannot (env_of exp) (bitvector_typ (nint len) ord) no_effect in + let pat = P_aux (P_lit lit, (Generated l, tannot)) in + let exp = E_aux (E_lit (mk_lit L_unit), (Generated l, empty_tannot)) in + Pat_aux (Pat_exp (pat, exp), (Generated l, empty_tannot)) + in + List.map mk_pexp (make_vectors len) + in + begin match (recur vec1 (mk_pexps len1), recur vec2 (mk_pexps len2)) with + | (Some deps1, Some deps2) -> Some (dmerge deps1 deps2) + | _ -> None + end + | _ -> None + end *) | _ -> None let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) = @@ -2586,7 +2619,7 @@ let print_result r = let analyse_funcl debug tenv constants (FCL_aux (FCL_Funcl (id,pexp),(l,_))) = let _ = if debug > 2 then print_endline (string_of_id id) else () in let pat,guard,body,_ = destruct_pexp pexp in - let (tq,_) = Env.get_val_spec id tenv in + let (tq,_) = Env.get_val_spec_orig id tenv in let set_assertions = find_set_assertions body in let _ = if debug > 2 then print_set_assertions set_assertions in let aenv = initial_env id l tq pat body set_assertions constants in diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 581872ee..3b53d466 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1367,8 +1367,11 @@ let doc_fun_body_lem ctxt exp = then align (string "catch_early_return" ^//^ parens (doc_exp)) else doc_exp -let doc_funcl_lem type_env (FCL_aux(FCL_Funcl(id, pexp), annot)) = - let typ = typ_of_annot annot in +let doc_funcl_lem type_env (FCL_aux(FCL_Funcl(id, pexp), ((l, _) as annot))) = + let (tq, typ) = + try Env.get_val_spec_orig id type_env with + | _ -> raise (unreachable l __POS__ ("Could not get val-spec of " ^ string_of_id id)) + in let arg_typs = match typ with | Typ_aux (Typ_fn (arg_typs, typ_ret, _), _) -> arg_typs | Typ_aux (_, l) -> raise (unreachable l __POS__ "Non-function type for funcl") @@ -1411,7 +1414,7 @@ let rec doc_fundef_lem type_env (FD_aux(FD_function(r, typa, efa, fcls),fannot) match fcls with | [] -> failwith "FD_function with empty function list" | FCL_aux (FCL_Funcl(id, pexp),annot) :: _ - when not (Env.is_extern id (env_of_annot annot) "lem") -> + when not (Env.is_extern id type_env "lem") -> (* Output "rec" modifier if function calls itself. Mutually recursive functions are handled separately by doc_mutrec_lem. *) let is_funcl_rec = -- cgit v1.2.3 From ba733dcb489ee6990bc0b5125cb5a99fc3e9b722 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sun, 12 Apr 2020 20:30:17 +0100 Subject: Add rewrite for constant-folding top-level letbindings This will constant-fold letbindings such as let LOG2_TAG_GRANULE : int(4) = 4 let TAG_GRANULE : int = (1 << LOG2_TAG_GRANULE) which is useful for the translation to Lem if TAG_GRANULE is used in bitvector lengths. --- src/rewrites.ml | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index 7705c75b..3779d4f2 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4792,6 +4792,36 @@ let rec move_loop_measures (Defs defs) = in Defs (List.rev rev_defs) +let rewrite_toplevel_consts target type_env (Defs defs) = + let istate = Constant_fold.initial_state (Defs defs) type_env in + let subst consts exp = + let open Rewriter in + let used_ids = fold_exp { (pure_exp_alg IdSet.empty IdSet.union) with e_id = IdSet.singleton } exp in + let subst_ids = IdSet.filter (fun id -> Bindings.mem id consts) used_ids in + IdSet.fold (fun id -> subst id (Bindings.find id consts)) subst_ids exp + in + let rewrite_def (revdefs, consts) = function + | DEF_val (LB_aux (LB_val (pat, exp), a) as lb) -> + begin match unaux_pat pat with + | P_id id | P_typ (_, P_aux (P_id id, _)) -> + let exp' = Constant_fold.rewrite_exp_once target istate (subst consts exp) in + if Constant_fold.is_constant exp' then + try + let exp' = infer_exp (env_of exp') (strip_exp exp') in + let pannot = (pat_loc pat, mk_tannot (env_of_pat pat) (typ_of exp') no_effect) in + let pat' = P_aux (P_typ (typ_of exp', P_aux (P_id id, pannot)), pannot) in + let consts' = Bindings.add id exp' consts in + (DEF_val (LB_aux (LB_val (pat', exp'), a)) :: revdefs, consts') + with + | _ -> (DEF_val lb :: revdefs, consts) + else (DEF_val lb :: revdefs, consts) + | _ -> (DEF_val lb :: revdefs, consts) + end + | def -> (def :: revdefs, consts) + in + let (revdefs, _) = List.fold_left rewrite_def ([], Bindings.empty) defs in + Defs (List.rev revdefs) + let opt_mono_rewrites = ref false let opt_mono_complex_nexps = ref true @@ -4891,6 +4921,7 @@ let all_rewrites = [ ("mapping_builtins", Basic_rewriter rewrite_defs_mapping_patterns); ("mono_rewrites", Basic_rewriter mono_rewrites); ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps); + ("toplevel_consts", String_rewriter (fun target -> Basic_rewriter (rewrite_toplevel_consts target))); ("monomorphise", String_rewriter (fun target -> Basic_rewriter (monomorphise target))); ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons)); ("add_bitvector_casts", Basic_rewriter Monomorphise.add_bitvector_casts); @@ -4942,6 +4973,7 @@ let rewrites_lem = [ ("mono_rewrites", []); ("recheck_defs", [If_mono_arg]); ("undefined", [Bool_arg false]); + ("toplevel_consts", [String_arg "lem"; If_mwords_arg]); ("toplevel_nexps", [If_mono_arg]); ("monomorphise", [String_arg "lem"; If_mono_arg]); ("recheck_defs", [If_mwords_arg]); -- cgit v1.2.3 From ce927d2003375e585fb814ac1f79d8c2dfac806c Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sun, 12 Apr 2020 20:47:06 +0100 Subject: Mono: Propagate constants after applying pattern choices This will propagate constant assignments in chosen branches of case expressions after applying pattern choices, e.g. the assignment to datasize in match size { [bitone, _] => datasize = 64, ... } when pattern [bitone, _] is chosen for size. --- src/monomorphise.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index e49ef4f5..9086d488 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1044,8 +1044,8 @@ let split_defs target all_errors splits env defs = if check_split_size patsubsts (pat_loc p) then List.map (fun (pat',substs,pchoices,ksubsts) -> let exp' = Spec_analysis.nexp_subst_exp ksubsts e in - let exp' = subst_exp ref_vars substs ksubsts exp' in let exp' = apply_pat_choices pchoices exp' in + let exp' = subst_exp ref_vars substs ksubsts exp' in let exp' = stop_at_false_assertions exp' in Pat_aux (Pat_exp (pat', map_exp exp'),l)) patsubsts @@ -1064,11 +1064,11 @@ let split_defs target all_errors splits env defs = if check_split_size patsubsts (pat_loc p) then List.map (fun (pat',substs,pchoices,ksubsts) -> let exp1' = Spec_analysis.nexp_subst_exp ksubsts e1 in - let exp1' = subst_exp ref_vars substs ksubsts exp1' in let exp1' = apply_pat_choices pchoices exp1' in + let exp1' = subst_exp ref_vars substs ksubsts exp1' in let exp2' = Spec_analysis.nexp_subst_exp ksubsts e2 in - let exp2' = subst_exp ref_vars substs ksubsts exp2' in let exp2' = apply_pat_choices pchoices exp2' in + let exp2' = subst_exp ref_vars substs ksubsts exp2' in let exp2' = stop_at_false_assertions exp2' in Pat_aux (Pat_when (pat', map_exp exp1', map_exp exp2'),l)) patsubsts -- cgit v1.2.3 From 5bc66aaca59084f2e9b276f0e9c2d4cb7325fef1 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sun, 12 Apr 2020 21:02:30 +0100 Subject: Mono: Extract more kid instantiations from assertions Ask the type checker instead of looking at the expression syntax. This also discovers implied instantiations, e.g. if we previously knew ('N in {32, 64}) and we have an assertion ('N != 32), then we know ('N == 64). --- src/monomorphise.ml | 53 +++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 39 insertions(+), 14 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 9086d488..c8ea22e5 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3601,20 +3601,45 @@ let add_bitvector_casts global_env (Defs defs) = let rec aux = function | [] -> [] | (E_aux (E_assert (assert_exp,msg),ann) as h)::t -> - let insts = extract assert_exp in - begin match insts with - | [] -> h::(aux t) - | _ -> - let t' = aux t in - let et = E_aux (E_block t',ann) in - let env = env_of h in - let insts = List.fold_left (fun insts (kid,i) -> - KBindings.add kid (nconstant i) insts) KBindings.empty insts in - let et = make_bitvector_env_casts env (env_of et) quant_kids insts et in - let src_typ = subst_kids_typ insts result_typ in - let et = make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ et in - - [h; et] + (* Check the assertion for constraints that instantiate kids *) + let is_known_kid kid = KBindings.mem kid (Env.get_typ_vars env) in + let is_int_kid kid = try Env.get_typ_var kid env = K_int with _ -> false in + begin match Type_check.assert_constraint env true assert_exp with + | Some nc when KidSet.for_all is_known_kid (tyvars_of_constraint nc) -> + (* If the type checker can extract constraints from the assertion + for pre-existing kids (not for those that are bound by the + assertion itself), then look at the environment after the + assertion to extract kid instantiations. *) + let env_post = Env.add_constraint nc env in + let check_inst kid insts = + (* First check if the given kid already had a fixed value previously. *) + let rec nc_fixes_kid nc = match unaux_constraint nc with + | NC_equal (Nexp_aux (Nexp_var kid', _), Nexp_aux (Nexp_constant _, _)) -> + Kid.compare kid kid' = 0 + | NC_and (_, _) -> List.exists nc_fixes_kid (constraint_conj nc) + | _ -> false + in + if List.exists nc_fixes_kid (Env.get_constraints env) then + insts + else + (* Otherwise ask the solver for a new, unique value *) + match solve_unique env_post (nvar kid) with + | Some n -> KBindings.add kid (nconstant n) insts + | None -> insts + | exception _ -> insts + in + let kids = KidSet.filter is_int_kid (tyvars_of_constraint nc) in + let insts = KidSet.fold check_inst (tyvars_of_constraint nc) KBindings.empty in + if KBindings.is_empty insts then h :: (aux t) else begin + (* Propagate new instantiations and insert casts *) + let t' = aux t in + let et = E_aux (E_block t',ann) in + let et = make_bitvector_env_casts env env_post quant_kids insts et in + let src_typ = subst_kids_typ insts result_typ in + let et = make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ et in + [h; et] + end + | _ -> h :: (aux t) end | h::t -> h::(aux t) in E_aux (E_block (aux es),ann) -- cgit v1.2.3 From dda95db0f6c2c739e2ba7c29150f8f4a1eb3f403 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sun, 12 Apr 2020 21:36:23 +0100 Subject: Mono: Check for non-constant calls to make_the_value ... and try to resolve them using constant propagation. --- src/monomorphise.ml | 87 ++++++++++++++++++++++++++++++++++++++++------------ src/monomorphise.mli | 2 +- src/rewrites.ml | 7 ++--- src/type_check.mli | 2 ++ 4 files changed, 74 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index c8ea22e5..ee1ea8cb 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1318,10 +1318,24 @@ let replace_type env typ = ("replace_type: Unsupported type " ^ string_of_typ typ)) -let rewrite_size_parameters env (Defs defs) = +let rewrite_size_parameters target type_env (Defs defs) = let open Rewriter in let open Util in + let const_prop_exp exp = + let ref_vars = Constant_propagation.referenced_vars exp in + let substs = (Bindings.empty, KBindings.empty) in + let assigns = Bindings.empty in + fst (Constant_propagation.const_prop target (Defs defs) ref_vars substs assigns exp) + in + let const_prop_pexp pexp = + let (pat, guard, exp, a) = destruct_pexp pexp in + construct_pexp (pat, guard, const_prop_exp exp, a) + in + let const_prop_funcl (FCL_aux (FCL_Funcl (id, pexp), a)) = + FCL_aux (FCL_Funcl (id, const_prop_pexp pexp), a) + in + let sizes_funcl fsizes (FCL_aux (FCL_Funcl (id,pexp),(l,ann))) = let pat,guard,exp,pannot = destruct_pexp pexp in let env = env_of_annot (l,ann) in @@ -1466,27 +1480,62 @@ in *) in let rewrite_letbind = fold_letbind { id_exp_alg with e_app = rewrite_e_app } in let rewrite_exp = fold_exp { id_exp_alg with e_app = rewrite_e_app } in + let replace_funtype id typ = + match Bindings.find id fn_sizes with + | to_change,_ when not (IntSet.is_empty to_change) -> + begin match typ with + | Typ_aux (Typ_fn (ts,t2,eff),l2) -> + Typ_aux (Typ_fn (mapat (replace_type type_env) to_change ts,t2,eff),l2) + | _ -> replace_type type_env typ + end + | _ -> typ + | exception Not_found -> typ + in + let type_env' = + let update_val_spec id _ env = + let (tq, typ) = Env.get_val_spec_orig id env in + Env.update_val_spec id (tq, replace_funtype id typ) env + in + Bindings.fold update_val_spec fn_sizes type_env + in let rewrite_def = function | DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,_))) -> + let funcls = List.map rewrite_funcl funcls in + (* Check whether we have ended up with itself('n) expressions where 'n + is not constant. If so, try and see if constant propagation can + resolve those variable expressions. In many cases the monomorphisation + pass will already have performed constant propagation, but it does not + for functions where it does not perform splits.*) + let check_funcl (FCL_aux (FCL_Funcl (id, pexp), (l, _)) as funcl) = + let has_nonconst_sizes = + let check_cast (typ, _) = + match unaux_typ typ with + | Typ_app (itself, [A_aux (A_nexp nexp, _)]) + | Typ_exist (_, _, Typ_aux (Typ_app (itself, [A_aux (A_nexp nexp, _)]), _)) + when string_of_id itself = "itself" -> + not (is_nexp_constant nexp) + | _ -> false + in + fold_pexp { (pure_exp_alg false (||)) with e_cast = check_cast } pexp + in + if has_nonconst_sizes then + (* Constant propagation requires a fully type-annotated AST, + so re-check the function clause *) + let (tq, typ) = Env.get_val_spec id type_env' in + let env = add_typquant l tq type_env' in + const_prop_funcl (Type_check.check_funcl env funcl typ) + else funcl + in + let funcls = List.map check_funcl funcls in (* TODO rewrite tannopt? *) - DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,empty_tannot))) + DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,empty_tannot))) | DEF_val lb -> DEF_val (rewrite_letbind lb) | DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) as spec -> - begin - match Bindings.find id fn_sizes with - | to_change,_ when not (IntSet.is_empty to_change) -> - let typschm = match typschm with - | TypSchm_aux (TypSchm_ts (tq,typ),l) -> - let typ = match typ with - | Typ_aux (Typ_fn (ts,t2,eff),l2) -> - Typ_aux (Typ_fn (mapat (replace_type env) to_change ts,t2,eff),l2) - | _ -> replace_type env typ - in TypSchm_aux (TypSchm_ts (tq,typ),l) - in - DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,empty_tannot))) - | _ -> spec - | exception Not_found -> spec - end + let typschm = match typschm with + | TypSchm_aux (TypSchm_ts (tq, typ),l) -> + TypSchm_aux (TypSchm_ts (tq, replace_funtype id typ), l) + in + DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), a)) -> DEF_reg_dec (DEC_aux (DEC_config (id, typ, rewrite_exp exp), a)) | def -> def @@ -3970,6 +4019,6 @@ let monomorphise target opts splits defs = in defs let add_bitvector_casts = BitvectorSizeCasts.add_bitvector_casts -let rewrite_atoms_to_singletons defs = +let rewrite_atoms_to_singletons target defs = let defs, env = Type_check.check Type_check.initial_env defs in - AtomToItself.rewrite_size_parameters env defs + AtomToItself.rewrite_size_parameters target env defs diff --git a/src/monomorphise.mli b/src/monomorphise.mli index b4eb7ead..f8a17494 100644 --- a/src/monomorphise.mli +++ b/src/monomorphise.mli @@ -72,4 +72,4 @@ val rewrite_toplevel_nexps : Type_check.tannot Ast.defs -> Type_check.tannot Ast val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs (* Replace atom arguments which are fixed by a type parameter for a size with a singleton type *) -val rewrite_atoms_to_singletons : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val rewrite_atoms_to_singletons : string -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs diff --git a/src/rewrites.ml b/src/rewrites.ml index 3779d4f2..f9ce4d84 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4923,9 +4923,8 @@ let all_rewrites = [ ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps); ("toplevel_consts", String_rewriter (fun target -> Basic_rewriter (rewrite_toplevel_consts target))); ("monomorphise", String_rewriter (fun target -> Basic_rewriter (monomorphise target))); - ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons)); + ("atoms_to_singletons", String_rewriter (fun target -> (Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons target)))); ("add_bitvector_casts", Basic_rewriter Monomorphise.add_bitvector_casts); - ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons)); ("remove_impossible_int_cases", Basic_rewriter Constant_propagation.remove_impossible_int_cases); ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_defs target))); ("make_cases_exhaustive", Basic_rewriter MakeExhaustive.rewrite); @@ -4978,7 +4977,7 @@ let rewrites_lem = [ ("monomorphise", [String_arg "lem"; If_mono_arg]); ("recheck_defs", [If_mwords_arg]); ("add_bitvector_casts", [If_mwords_arg]); - ("atoms_to_singletons", [If_mono_arg]); + ("atoms_to_singletons", [String_arg "lem"; If_mono_arg]); ("recheck_defs", [If_mwords_arg]); ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); @@ -5098,7 +5097,7 @@ let rewrites_c = [ ("recheck_defs", [If_mono_arg]); ("toplevel_nexps", [If_mono_arg]); ("monomorphise", [String_arg "c"; If_mono_arg]); - ("atoms_to_singletons", [If_mono_arg]); + ("atoms_to_singletons", [String_arg "c"; If_mono_arg]); ("recheck_defs", [If_mono_arg]); ("undefined", [Bool_arg false]); ("vector_string_pats_to_bit_list", []); diff --git a/src/type_check.mli b/src/type_check.mli index fba5575a..ff839f50 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -319,6 +319,8 @@ val infer_lexp : Env.t -> unit lexp -> tannot lexp val check_case : Env.t -> typ -> unit pexp -> typ -> tannot pexp +val check_funcl : Env.t -> 'a funcl -> typ -> tannot funcl + 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 -- cgit v1.2.3 From 5963b1fddba11309c8a3efa9efa866530473c42d Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sun, 12 Apr 2020 23:42:56 +0100 Subject: Take kid synonyms into account when propagating constants For example, in let datasize = e in ... the typechecker will generate a kid '_datasize if e has an existential type (with one kid), and in let 'datasize = e in ... the typechecker will bind both 'datasize and '_datasize. If we substitute one as part of constant propagation, this patch will make constant propagation also substitute the other. --- src/constant_propagation.ml | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml index e785aa93..c190cffc 100644 --- a/src/constant_propagation.ml +++ b/src/constant_propagation.ml @@ -792,6 +792,24 @@ let const_props target defs ref_vars = | _ -> GiveUp in let check_pat = check_exp_pat exp0 in + let add_ksubst_synonyms env' ksubst = + (* The type checker sometimes automatically generates kid synonyms, e.g. + in let 'datasize = ... in ... it binds both 'datasize and '_datasize. + If we subsitute one, we also want to substitute the other. + In order to find synonyms, we consult the environment after the + bind (see findpat_generic below). *) + let get_synonyms (kid, nexp) = + let rec synonyms_of_nc nc = match unaux_constraint nc with + | NC_equal (Nexp_aux (Nexp_var kid1, _), Nexp_aux (Nexp_var (kid2), _)) + when Kid.compare kid kid1 = 0 -> + [(kid2, nexp)] + | NC_and _ -> List.concat (List.map synonyms_of_nc (constraint_conj nc)) + | _ -> [] + in + List.concat (List.map synonyms_of_nc (Env.get_constraints env')) + in + ksubst @ List.concat (List.map get_synonyms ksubst) + in let rec findpat_generic description assigns = function | [] -> (Reporting.print_err l "Monomorphisation" ("Failed to find a case for " ^ description); None) @@ -804,7 +822,9 @@ let const_props target defs ref_vars = kbindings_union ksubsts (kbindings_from_list ksubst) in 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_true,_)) -> + let ksubst = add_ksubst_synonyms (env_of exp) ksubst in + Some (exp,vsubst,ksubst) | E_lit (L_aux (L_false,_)) -> findpat_generic description assigns tl | _ -> None end @@ -813,7 +833,9 @@ let const_props target defs ref_vars = | (Pat_aux (Pat_exp (p,exp),_))::tl -> match check_pat p with | DoesNotMatch -> findpat_generic description assigns tl - | DoesMatch (subst,ksubst) -> Some (exp,subst,ksubst) + | DoesMatch (subst,ksubst) -> + let ksubst = add_ksubst_synonyms (env_of exp) ksubst in + Some (exp,subst,ksubst) | GiveUp -> None in findpat_generic (string_of_exp exp0) assigns cases -- cgit v1.2.3 From b9860a9bc7c546bfab207c76d15e0f72e6047922 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 18 Apr 2020 20:56:34 +0100 Subject: Add more monomorphisation rewrites Supporting more ASL idioms --- src/monomorphise.ml | 99 ++++++++++++++++++++++++++++++++++++--------------- src/spec_analysis.ml | 18 +++++++--- src/spec_analysis.mli | 3 +- 3 files changed, 86 insertions(+), 34 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index ee1ea8cb..c3d03f8b 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -81,6 +81,16 @@ let kbindings_union s1 s2 = | (Some x), _ -> Some x | _, _ -> None) s1 s2 +let ids_in_exp exp = + let open Rewriter in + fold_exp { + (pure_exp_alg IdSet.empty IdSet.union) with + e_id = IdSet.singleton; + lEXP_id = IdSet.singleton; + lEXP_memory = (fun (id,s) -> List.fold_left IdSet.union (IdSet.singleton id) s); + lEXP_cast = (fun (_,id) -> IdSet.singleton id) + } exp + let make_vector_lit sz i = let f j = if Big_int.equal (Big_int.modulus (Big_int.shift_right i (sz-j-1)) (Big_int.of_int 2)) Big_int.zero then '0' else '1' in let s = String.init sz f in @@ -95,6 +105,12 @@ let tabulate f n = let make_vectors sz = tabulate (make_vector_lit sz) (Big_int.shift_left (Big_int.of_int 1) sz) +let is_inc_vec typ = + try + let (_, ord, _) = vector_typ_args_of typ in + is_order_inc ord + with _ -> false + let rec cross = function | [] -> failwith "cross" | [(x,l)] -> List.map (fun y -> [(x,y)]) l @@ -2816,13 +2832,15 @@ let is_constant = function | E_aux (E_lit _,_) -> true | _ -> false -let get_constant_vec_len env typ = +let get_constant_vec_len ?solve:(solve=false) env typ = let typ = Env.base_typ_of env typ in match destruct_bitvector env typ with | Some (size,_) -> - (match nexp_simp size with - | Nexp_aux (Nexp_constant i,_) -> Some i - | _ -> None) + begin match nexp_simp size with + | Nexp_aux (Nexp_constant i,_) -> Some i + | nexp when solve -> solve_unique env nexp + | _ -> None + end | _ -> None let is_constant_vec_typ env typ = (get_constant_vec_len env typ <> None) @@ -2878,13 +2896,13 @@ let rec rewrite_app env typ (id,args) = | [E_aux (E_app (append, [e1; E_aux (E_app (subrange1, - [vector1; start1; end1]),_)]),_); + [vector1; start1; end1]),_) as sub1]),_); E_aux (E_app (subrange2, - [vector2; start2; end2]),_)] + [vector2; start2; end2]),_) as sub2] when is_append append && is_subrange subrange1 && is_subrange subrange2 && is_constant_vec_typ env (typ_of e1) && is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && - not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> + not (is_constant_vec_typ env (typ_of sub1) || is_constant_vec_typ env (typ_of sub2)) -> let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in let midsize = nminus size size1 in begin @@ -2935,10 +2953,10 @@ let rec rewrite_app env typ (id,args) = end (* variable-slice @ zeros *) - | [E_aux (E_app (op, [vector1; start1; len1]),_); zeros_exp] + | [E_aux (E_app (op, [vector1; start1; len1]),_) as exp1; zeros_exp] when (is_slice op || is_subrange op) && is_zeros_exp zeros_exp && is_bitvector_typ (typ_of vector1) - && not (is_constant start1 && is_constant len1 && is_constant_vec_typ env (typ_of zeros_exp)) -> + && not (is_constant_vec_typ env (typ_of exp1) && is_constant_vec_typ env (typ_of zeros_exp)) -> let op' = if is_subrange op then "place_subrange" else "place_slice" in begin match get_zeros_exp_len zeros_exp with | Some zlen -> try_cast_to_typ (mk_exp (E_app (mk_id op', [vector1; start1; len1; zlen]))) @@ -2956,12 +2974,12 @@ let rec rewrite_app env typ (id,args) = (* variable-range @ variable-range *) | [E_aux (E_app (subrange1, - [vector1; start1; end1]),_); + [vector1; start1; end1]),_) as exp1; E_aux (E_app (subrange2, - [vector2; start2; end2]),_)] + [vector2; start2; end2]),_) as exp2] when is_subrange subrange1 && is_subrange subrange2 && is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && - not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> + not (is_constant_vec_typ env (typ_of exp1) || is_constant_vec_typ env (typ_of exp2)) -> try_cast_to_typ (E_aux (E_app (mk_id "subrange_subrange_concat", [vector1; start1; end1; vector2; start2; end2]), @@ -3184,11 +3202,12 @@ let rec rewrite_app env typ (id,args) = let length_arg = List.filter (fun arg -> is_number (typ_of arg)) args in match List.filter (fun arg -> not (is_number (typ_of arg))) args with | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] - when is_slice slice1 && not (is_constant length1) && is_bitvector_typ (typ_of vector1) -> + when is_slice slice1 && not (is_constant length1) && is_bitvector_typ (typ_of vector1) -> try_cast_to_typ (rewrap (E_app (mk_id "sext_slice", length_arg @ [vector1; start1; length1]))) - | [E_aux (E_app (subrange1, [vector1; hi1; lo1]),_)] - when is_subrange subrange1 && not (is_constant hi1 && is_constant lo1) && is_bitvector_typ (typ_of vector1) -> + | [E_aux (E_app (subrange1, [vector1; hi1; lo1]),_) as exp1] + when is_subrange subrange1 && not (is_constant_vec_typ env (typ_of exp1)) + && is_bitvector_typ (typ_of vector1) -> try_cast_to_typ (rewrap (E_app (mk_id "sext_subrange", length_arg @ [vector1; hi1; lo1]))) | [E_aux (E_app (append, [E_aux (E_app (op, [vector1; start1; len1]), _); zeros_exp]), _)] @@ -3251,7 +3270,7 @@ let rec rewrite_app env typ (id,args) = | _ -> E_app (id,args) - else if is_id env (Id "__SetSlice_bits") id then + else if is_id env (Id "__SetSlice_bits") id || is_id env (Id "SetSlice") id then match args with | [len; slice_len; vector; start; E_aux (E_app (zeros, _), _)] when is_zeros zeros && is_bitvector_typ (typ_of vector) -> @@ -3267,9 +3286,31 @@ let rec rewrite_app env typ (id,args) = E_app (mk_id "sail_ones", length_arg) | _ -> E_app (id, args) + (* Turn constant-length subranges into slices, making the constant length more explicit, + e.g. turning x[i+1 .. i] into slice(x, i, 2) *) + else if is_subrange id then + match get_constant_vec_len ~solve:true env typ, args with + | Some i, [vector1; start1; end1] + when is_bitvector_typ (typ_of vector1) && not (is_constant start1 && is_constant end1) -> + let low = if is_inc_vec (typ_of vector1) then start1 else end1 in + E_app (mk_id "slice", [vector1; low; mk_exp (E_lit (mk_lit (L_num i)))]) + | _, _ -> E_app (id, args) + + (* Rewrite (v[x .. y] + i) to (v + (i << y))[x .. y], which is more amenable to further rewriting *) + else if is_id env (Id "add_bits_int") id then + match args with + | [E_aux (E_app (subrange1, [vec1; start1; end1]), a) as exp1; exp2] + when is_subrange subrange1 && is_bitvector_typ (typ_of vec1) + && not (is_constant_vec_typ env (typ_of exp1)) -> + let low = if is_inc_vec (typ_of vec1) then start1 else end1 in + let exp2' = mk_exp (E_app (mk_id "shl_int", [exp2; low])) in + let vec1' = E_aux (E_app (id, [vec1; exp2']), a) in + E_app (subrange1, [vec1'; start1; end1]) + | _ -> E_app (id, args) + else E_app (id,args) -let rewrite_aux = function +let rec rewrite_aux = function | E_app (id,args), (l, tannot) -> begin match destruct_tannot tannot with | Some (env, ty, _) -> @@ -3299,7 +3340,19 @@ let rewrite_aux = function let lhs = LEXP_aux (LEXP_id id1, annot1) in let rhs = E_aux (E_app (mk_id "set_subrange_zeros", [E_aux (E_id id1, annot1); start1; end1]), annot1) in E_aux (E_assign (lhs, rhs), annot) - | exp,annot -> E_aux (exp,annot) + | (E_let (LB_aux (LB_val (P_aux ((P_id id | P_typ (_, P_aux (P_id id, _))), _), + (E_aux (E_app (subrange1, [vec1; start1; end1]), _) as exp1)), _), + exp2) as e_aux), annot + when is_id (env_of_annot annot) (Id "vector_subrange") subrange1 + && not (is_constant_vec_typ (env_of_annot annot) (typ_of exp1))-> + let open Spec_analysis in + let depends1 = ids_in_exp exp1 in + let assigned2 = IdSet.union (assigned_vars exp2) (bound_vars exp2) in + if IdSet.disjoint depends1 assigned2 then rewrite_exp (subst id exp1 exp2) else + E_aux (e_aux, annot) + | e_aux, annot -> E_aux (e_aux, annot) + +and rewrite_exp exp = Rewriter.fold_exp { Rewriter.id_exp_alg with e_aux = rewrite_aux } exp let mono_rewrite defs = let open Rewriter in @@ -3452,16 +3505,6 @@ let make_bitvector_cast_cast cast_name top_env env quant_kids src_typ target_typ let _,_,f = make_bitvector_cast_fns cast_name top_env env quant_kids src_typ target_typ in f -let ids_in_exp exp = - let open Rewriter in - fold_exp { - (pure_exp_alg IdSet.empty IdSet.union) with - e_id = IdSet.singleton; - lEXP_id = IdSet.singleton; - lEXP_memory = (fun (id,s) -> List.fold_left IdSet.union (IdSet.singleton id) s); - lEXP_cast = (fun (_,id) -> IdSet.singleton id) - } exp - let make_bitvector_env_casts top_env env quant_kids insts exp = let mk_cast var typ exp = (make_bitvector_cast_let "bitvector_cast_in" env top_env quant_kids typ (subst_kids_typ insts typ)) var exp in let mk_assign_in var typ = diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 4814554b..542ecaae 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -602,11 +602,11 @@ let top_sort_defs (Defs defs) = let assigned_vars exp = - fst (Rewriter.fold_exp - { (Rewriter.compute_exp_alg IdSet.empty IdSet.union) with - Rewriter.lEXP_id = (fun id -> IdSet.singleton id, LEXP_id id); - Rewriter.lEXP_cast = (fun (ty,id) -> IdSet.singleton id, LEXP_cast (ty,id)) } - exp) + (Rewriter.fold_exp + { (Rewriter.pure_exp_alg IdSet.empty IdSet.union) with + Rewriter.lEXP_id = (fun id -> IdSet.singleton id); + Rewriter.lEXP_cast = (fun (ty,id) -> IdSet.singleton id) } + exp) let assigned_vars_in_fexps fes = List.fold_left @@ -633,6 +633,14 @@ let rec assigned_vars_in_lexp (LEXP_aux (le,_)) = | LEXP_field (le,_) -> assigned_vars_in_lexp le | LEXP_deref e -> assigned_vars e +let bound_vars exp = + let open Rewriter in + let pat_alg = { + (pure_pat_alg IdSet.empty IdSet.union) with + p_id = IdSet.singleton; + p_as = (fun (ids, id) -> IdSet.add id ids) + } in + fold_exp { (pure_exp_alg IdSet.empty IdSet.union) with pat_alg = pat_alg } exp let pat_id_is_variable env id = match Type_check.Env.lookup_id id env with diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli index 8586ac15..41ab9b6c 100644 --- a/src/spec_analysis.mli +++ b/src/spec_analysis.mli @@ -84,9 +84,10 @@ val assigned_vars_in_fexps : 'a fexp list -> IdSet.t val assigned_vars_in_pexp : 'a pexp -> IdSet.t val assigned_vars_in_lexp : 'a lexp -> IdSet.t -(** Variable bindings in patterns *) +(** Variable bindings in patterns and expressions *) val pat_id_is_variable : env -> id -> bool val bindings_from_pat : tannot pat -> id list +val bound_vars : 'a exp -> IdSet.t val equal_kids_ncs : kid -> n_constraint list -> KidSet.t val equal_kids : env -> kid -> KidSet.t -- cgit v1.2.3 From f2dbac60d6c1a92956652a631280314bde3fd633 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 18 Apr 2020 21:27:24 +0100 Subject: Add more SMT builtins Also add support for intialising variables with an "undefined" literal; make the SMT solver treat the value as arbitrary but fixed. --- src/jib/jib_smt.ml | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 47f6ee49..310a38a5 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -287,6 +287,8 @@ let smt_conversion ctx from_ctyp to_ctyp x = force_size ctx n ctx.lint_size x | CT_lint, CT_lbits _ -> Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int ctx.lint_size); force_size ctx (lbits_size ctx) ctx.lint_size x]) + | CT_fint n, CT_lbits _ -> + Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int n); force_size ctx (lbits_size ctx) n x]) | CT_lbits _, CT_fbits (n, _) -> unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x])) | CT_fbits (n, _), CT_fbits (m, _) -> @@ -960,6 +962,11 @@ let builtin_add_bits_int ctx v1 v2 ret_ctyp = | CT_fbits (n, _), CT_lint, CT_fbits (o, _) when n = o -> Fn ("bvadd", [smt_cval ctx v1; force_size ctx o ctx.lint_size (smt_cval ctx v2)]) + | CT_lbits _, CT_fint n, CT_lbits _ when n < lbits_size ctx -> + let smt1 = smt_cval ctx v1 in + let smt2 = force_size ctx (lbits_size ctx) n (smt_cval ctx v2) in + Fn ("Bits", [Fn ("len", [smt1]); Fn ("bvadd", [Fn ("contents", [smt1]); smt2])]) + | _ -> builtin_type_error ctx "add_bits_int" [v1; v2] (Some ret_ctyp) let builtin_sub_bits_int ctx v1 v2 ret_ctyp = @@ -1129,6 +1136,20 @@ let builtin_set_slice_bits ctx v1 v2 v3 v4 v5 ret_ctyp = let smt5 = Fn ("concat", [bvzero (n - m - pos); Fn ("concat", [smt_cval ctx v5; bvzero pos])]) in Fn ("bvor", [Fn ("bvand", [smt_cval ctx v3; mask]); smt5]) + (* set_slice_bits(len, slen, x, pos, y) = + let mask = slice_mask(len, pos, slen) in + (x AND NOT(mask)) OR ((unsigned_size(len, y) << pos) AND mask) *) + | CT_constant n', _, CT_fbits (n, _), _, CT_lbits _, CT_fbits (n'', _) + when Big_int.to_int n' = n && n'' = n -> + let pos = bvzeint ctx (lbits_size ctx) v4 in + let slen = bvzeint ctx ctx.lbits_index v2 in + let mask = Fn ("bvshl", [bvmask ctx slen; pos]) in + let smt3 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v3) in + let smt3' = Fn ("bvand", [smt3; Fn ("bvnot", [mask])]) in + let smt5 = Fn ("contents", [smt_cval ctx v5]) in + let smt5' = Fn ("bvand", [Fn ("bvshl", [smt5; pos]); mask]) in + Extract (n - 1, 0, Fn ("bvor", [smt3'; smt5'])) + | _ -> builtin_type_error ctx "set_slice" [v1; v2; v3; v4; v5] (Some ret_ctyp) let builtin_compare_bits fn ctx v1 v2 ret_ctyp = @@ -1875,11 +1896,14 @@ let smt_instr ctx = Reporting.unreachable l __POS__ "Register reference write should be re-written by now" | I_aux (I_init (ctyp, id, cval), _) | I_aux (I_copy (CL_id (id, ctyp), cval), _) -> - begin match id with - | Name (id, _) when IdSet.mem id ctx.preserved -> + begin match id, cval with + | Name (id, _), _ when IdSet.mem id ctx.preserved -> [preserve_const ctx id ctyp (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))] - | _ -> + | _, V_lit (VL_undefined, _) -> + (* Declare undefined variables as arbitrary but fixed *) + [declare_const ctx id ctyp] + | _, _ -> [define_const ctx id ctyp (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))] end -- cgit v1.2.3 From 2882405391abb9facc0b0019fdd265c2855f2f35 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sun, 19 Apr 2020 21:48:13 +0100 Subject: Lem: Print more type annotations In particular tuple types containing bitvectors. --- src/pretty_print_lem.ml | 79 ++++++++++++++++++++++++++++++------------------- 1 file changed, 48 insertions(+), 31 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 3b53d466..9e636b59 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -362,46 +362,63 @@ let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) = lem_nexps_of_typ typ |> NexpSet.exists (fun nexp -> not (is_nexp_constant nexp)) -let replace_typ_size ctxt env (Typ_aux (t,a)) = +let rec replace_typ_size ctxt env (Typ_aux (t, a) as typ) = + let rewrap t = Typ_aux (t, a) in + let recur = replace_typ_size ctxt env in match t with - | Typ_app (Id_aux (Id "bitvector",_) as id, [A_aux (A_nexp size,_);ord]) -> - begin - let mk_typ nexp = - Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord]),a)) - in - match Type_check.solve_unique env size with - | Some n -> mk_typ (nconstant n) - | None -> - let is_equal nexp = - prove __POS__ env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) - in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with - | nexp -> mk_typ nexp - | exception Not_found -> None + | Typ_tup typs -> + begin match Util.option_all (List.map recur typs) with + | Some typs' -> Some (rewrap (Typ_tup typs')) + | None -> None end - (* - | Typ_app (Id_aux (Id "vector",_) as id, [A_aux (A_nexp size,_);ord;typ']) -> - begin - let mk_typ nexp = - Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a)) - in - match Type_check.solve_unique env size with - | Some n -> mk_typ (nconstant n) + | Typ_app (id, args) when contains_t_pp_var ctxt typ -> + begin match Util.option_all (List.map (replace_typ_arg_size ctxt env) args) with + | Some args' -> Some (rewrap (Typ_app (id, args'))) + | None -> None + end + | Typ_app _ -> Some typ + | Typ_id _ -> Some typ + | Typ_fn (argtyps, rtyp, eff) -> + begin match (Util.option_all (List.map recur argtyps), recur rtyp) with + | (Some argtyps', Some rtyp') -> Some (rewrap (Typ_fn (argtyps', rtyp', eff))) + | _ -> None + end + | Typ_var kid -> + let is_kid nexp = Nexp.compare nexp (nvar kid) = 0 in + if NexpSet.exists is_kid ctxt.bound_nexps then Some typ else None + | Typ_exist (kids, nc, typ) -> + begin match recur typ with + | Some typ' -> Some (rewrap (Typ_exist (kids, nc, typ'))) + | None -> None + end + | Typ_internal_unknown + | Typ_bidir (_, _, _) -> None +and replace_typ_arg_size ctxt env (A_aux (ta, a) as targ) = + let rewrap ta = A_aux (ta, a) in + match ta with + | A_nexp nexp -> + begin match Type_check.solve_unique env nexp with + | Some n -> Some (rewrap (A_nexp (nconstant n))) | None -> - let is_equal nexp = - prove __POS__ env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) - in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with - | nexp -> mk_typ nexp + let is_equal nexp' = + prove __POS__ env (NC_aux (NC_equal (nexp,nexp'),Parse_ast.Unknown)) + in + match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with + | nexp' -> Some (rewrap (A_nexp nexp')) | exception Not_found -> None end - *) - | _ -> None + | A_typ typ -> + begin match replace_typ_size ctxt env typ with + | Some typ' -> Some (rewrap (A_typ typ')) + | None -> None + end + | A_order _ | A_bool _ -> Some targ let make_printable_type ctxt env typ = if contains_t_pp_var ctxt typ then - match replace_typ_size ctxt env typ with - | None -> None - | Some typ -> Some typ + try replace_typ_size ctxt env (Env.expand_synonyms env typ) with + | _ -> None else Some typ let doc_tannot_lem ctxt env eff typ = -- cgit v1.2.3 From 3311b7d4c5aeebacdbcd14602d7a8a75a9c1b258 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 21 Apr 2020 16:21:12 +0100 Subject: Fix build with OCaml 4.06.1 --- src/monomorphise.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index c3d03f8b..8c10b63f 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3348,7 +3348,7 @@ let rec rewrite_aux = function let open Spec_analysis in let depends1 = ids_in_exp exp1 in let assigned2 = IdSet.union (assigned_vars exp2) (bound_vars exp2) in - if IdSet.disjoint depends1 assigned2 then rewrite_exp (subst id exp1 exp2) else + if IdSet.is_empty (IdSet.inter depends1 assigned2) then rewrite_exp (subst id exp1 exp2) else E_aux (e_aux, annot) | e_aux, annot -> E_aux (e_aux, annot) -- cgit v1.2.3 From a1d7dc8a237dbbc5eacbec71ca2a258bc48b4234 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 29 Apr 2020 20:32:40 +0100 Subject: Add progress reporting to monomorphisation --- src/monomorphise.ml | 31 +++++++++++++++++++++---------- 1 file changed, 21 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 8c10b63f..5fce15f7 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1147,7 +1147,9 @@ let split_defs target all_errors splits env defs = List.map (fun fcl' -> SD_aux (SD_funcl fcl', annot)) (map_funcl fcl) | _ -> [sd] in - let map_def d = + let num_defs = List.length defs in + let map_def idx d = + Util.progress "Monomorphising " (string_of_int idx ^ "/" ^ string_of_int num_defs) idx num_defs; match d with | DEF_type _ | DEF_spec _ @@ -1168,10 +1170,11 @@ let split_defs target all_errors splits env defs = Reporting.unreachable (id_loc id) __POS__ "Loop termination measures should have been rewritten before now" in - Defs (List.concat (List.map map_def defs)) + Defs (List.concat (List.mapi map_def defs)) in - let defs'' = map_locs splits defs' in - !no_errors_happened, defs'' + let (Defs defs'') = map_locs splits defs' in + Util.progress "Monomorphising " "done" (List.length defs'') (List.length defs''); + !no_errors_happened, (Defs defs'') @@ -2725,11 +2728,17 @@ let argset_to_list splits = List.map argelt l let analyse_defs debug env (Defs defs) = - let def (globals,r) d = + let def (idx,globals,r) d = + begin match d with + | DEF_fundef fd -> + Util.progress "Analysing " (string_of_id (id_of_fundef fd)) idx (List.length defs) + | _ -> () + end; let globals,r' = analyse_def debug env globals d in - globals, merge r r' + idx + 1, globals, merge r r' in - let _,r = List.fold_left def (Bindings.empty,empty) defs in + let _,_,r = List.fold_left def (0,Bindings.empty,empty) defs in + let _ = Util.progress "Analysing " "done" (List.length defs) (List.length defs) in (* Resolve the interprocedural dependencies *) @@ -3770,13 +3779,15 @@ let add_bitvector_casts global_env (Defs defs) = let pexp = construct_pexp (pat,guard,body,annot) in FCL_aux (FCL_Funcl (id,pexp),fcl_ann) in - let rewrite_def = function - | DEF_fundef (FD_aux (FD_function (r,t,e,fcls),fd_ann)) -> + let rewrite_def idx = function + | DEF_fundef (FD_aux (FD_function (r,t,e,fcls),fd_ann) as fd) -> + Util.progress "Adding casts " (string_of_id (id_of_fundef fd)) idx (List.length defs); DEF_fundef (FD_aux (FD_function (r,t,e,List.map rewrite_funcl fcls),fd_ann)) | d -> d in specs_required := IdSet.empty; - let defs = List.map rewrite_def defs in + let defs = List.mapi rewrite_def defs in + let _ = Util.progress "Adding casts " "done" (List.length defs) (List.length defs) in let l = Generated Unknown in let Defs cast_specs,_ = (* TODO: use default/relevant order *) -- cgit v1.2.3 From 929469c81d863703aa5817bbbd92c697eca3af26 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 4 May 2020 17:53:12 +0100 Subject: Try to fix bug in size parameter rewriting If we call a function where some arguments need to be rewritten, we might need to rewrite those parameters in the caller as well. --- src/monomorphise.ml | 61 +++++++++++++++++++++++++++++++++++------------------ 1 file changed, 41 insertions(+), 20 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 5fce15f7..4d2ade50 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1394,31 +1394,52 @@ let rewrite_size_parameters target type_env (Defs defs) = print_endline ("Nexp map for " ^ string_of_id id); List.iter (fun (nexp, i) -> print_endline (" " ^ string_of_nexp nexp ^ " -> " ^ string_of_int i)) nexp_list in *) - let parameters_for tannot = - match destruct_tannot tannot with - | Some (env,typ,_) -> - begin match Env.base_typ_of env typ with - | Typ_aux (Typ_app (Id_aux (Id "bitvector",_), [A_aux (A_nexp size,_);_]),_) - when not (is_nexp_constant size) -> - begin - match NexpMap.find size nexp_map with - | i -> IntSet.singleton i - | exception Not_found -> - (* Look for equivalent nexps, but only in consistent type env *) - if prove __POS__ env (NC_aux (NC_false,Unknown)) then IntSet.empty else - match List.find (fun (nexp,i) -> - prove __POS__ env (NC_aux (NC_equal (nexp,size),Unknown))) nexp_list with - | _, i -> IntSet.singleton i - | exception Not_found -> IntSet.empty + let parameters_for e tannot = + let parameters_for_nexp env size = + match solve_unique env size with + | Some _ -> IntSet.empty + | None -> + match NexpMap.find size nexp_map with + | i -> IntSet.singleton i + | exception Not_found -> + (* Look for equivalent nexps, but only in consistent type env *) + if prove __POS__ env (NC_aux (NC_false,Unknown)) then IntSet.empty else + match List.find (fun (nexp,i) -> + prove __POS__ env (NC_aux (NC_equal (nexp,size),Unknown))) nexp_list with + | _, i -> IntSet.singleton i + | exception Not_found -> IntSet.empty + in + let parameters_for_typ = + match destruct_tannot tannot with + | Some (env,typ,_) -> + begin match Env.base_typ_of env typ with + | Typ_aux (Typ_app (Id_aux (Id "bitvector",_), [A_aux (A_nexp size,_);_]),_) + when not (is_nexp_constant size) -> + parameters_for_nexp env size + | _ -> IntSet.empty end - | _ -> IntSet.empty - end - | None -> IntSet.empty + | None -> IntSet.empty + in + let parameters_for_exp = match e with + | E_app (id, args) when Bindings.mem id fsizes -> + let add_arg (i, s) arg = + if IntSet.mem i (fst (Bindings.find id fsizes)) then + try match destruct_numeric (typ_of arg) with + | Some ([], _, nexp) -> + (i + 1, IntSet.union s (parameters_for_nexp env nexp)) + | _ -> (i + 1, s) + with _ -> (i + 1, s) + else (i + 1, s) + in + snd (List.fold_left add_arg (0, IntSet.empty) args) + | _ -> IntSet.empty + in + IntSet.union parameters_for_typ parameters_for_exp in let parameters_to_rewrite = fst (fold_pexp { (compute_exp_alg IntSet.empty IntSet.union) with - e_aux = (fun ((s,e),(l,annot)) -> IntSet.union s (parameters_for annot),E_aux (e,(l,annot))) + e_aux = (fun ((s,e),(l,annot)) -> IntSet.union s (parameters_for e annot),E_aux (e,(l,annot))) } pexp) in let new_nexps = NexpSet.of_list (List.map fst -- cgit v1.2.3 From dc674a7320e4684e4dbe3ccf618c644bd83796ca Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 4 May 2020 17:57:49 +0100 Subject: Mono: Try to fix bug in inter-procedural analysis The monomorphisation analysis decides whether to split function arguments in the callee or in callers. The code previously used a datastructure that can hold results of either the one case or the other, but there might be functions that are called in different contexts leading to different decisions. This patch changes the datastructure to support storing all instances of either case. --- src/monomorphise.ml | 58 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 36 insertions(+), 22 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4d2ade50..465ed30f 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1749,9 +1749,19 @@ let string_of_dep = function (* If a callee uses a type variable as a size, does it need to be split in the current function, or is it also a parameter? (Note that there may be multiple calls, so more than one parameter can be involved) *) -type call_dep = - | InFun of dependencies - | Parents of CallerKidSet.t +type call_dep = { + in_fun : dependencies option; + parents : CallerKidSet.t; +} + +let empty_call_dep = { + in_fun = None; + parents = CallerKidSet.empty; +} + +let in_fun_call_dep deps = { in_fun = Some deps; parents = CallerKidSet.empty } + +let parents_call_dep cks = { in_fun = None; parents = cks } (* Result of analysing the body of a function. The split field gives the arguments to split based on the body alone, the extra_splits @@ -1811,17 +1821,16 @@ let dep_bindings_merge a1 a2 = let dep_kbindings_merge a1 a2 = KBindings.merge (opt_merge dmerge) a1 a2 +let call_dep_merge k d1 d2 = { + in_fun = opt_merge dmerge k d1.in_fun d2.in_fun; + parents = CallerKidSet.union d1.parents d2.parents +} + let call_kid_merge k x y = match x, y with | None, x -> x | x, None -> x - | Some (InFun deps), Some (Parents _) - | Some (Parents _), Some (InFun deps) - -> Some (InFun deps) - | Some (InFun deps), Some (InFun deps') - -> Some (InFun (dmerge deps deps')) - | Some (Parents fns), Some (Parents fns') - -> Some (Parents (CallerKidSet.union fns fns')) + | Some d1, Some d2 -> Some (call_dep_merge k d1 d2) let call_arg_merge k args args' = match args, args' with @@ -1989,11 +1998,11 @@ and deps_of_typ_arg l fn_id env arg_deps (A_aux (aux, _)) = match aux with | A_nexp (Nexp_aux (Nexp_var kid,_)) when List.exists (fun k -> Kid.compare kid k == 0) env.top_kids -> - Parents (CallerKidSet.singleton (fn_id,kid)) - | A_nexp nexp -> InFun (deps_of_nexp l env.kid_deps arg_deps nexp) - | A_order _ -> InFun dempty - | A_typ typ -> InFun (deps_of_typ l env.kid_deps arg_deps typ) - | A_bool nc -> InFun (deps_of_nc env.kid_deps nc) + parents_call_dep (CallerKidSet.singleton (fn_id,kid)) + | A_nexp nexp -> in_fun_call_dep (deps_of_nexp l env.kid_deps arg_deps nexp) + | A_order _ -> in_fun_call_dep dempty + | A_typ typ -> in_fun_call_dep (deps_of_typ l env.kid_deps arg_deps typ) + | A_bool nc -> in_fun_call_dep (deps_of_nc env.kid_deps nc) let mk_subrange_pattern vannot vstart vend = let (len,ord,typ) = vector_typ_args_of (Env.base_typ_of (env_of_annot vannot) (typ_of_annot vannot)) in @@ -2221,7 +2230,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = let rdep,r' = if Id.compare fn_id id == 0 then let bad = Unknown (l,"Recursive call of " ^ string_of_id id) in - let kid_deps = KBindings.map (fun _ -> InFun bad) kid_deps in + let kid_deps = KBindings.map (fun _ -> in_fun_call_dep bad) kid_deps in bad, { empty with split_on_call = Bindings.singleton id kid_deps } else dempty, { empty with split_on_call = Bindings.singleton id kid_deps } in @@ -2683,11 +2692,12 @@ let print_set_assertions set_assertions = let print_result r = let _ = print_endline (" splits: " ^ string_of_argsplits r.split) in let print_kbinding kid dep = - let s = match dep with - | InFun dep -> "InFun " ^ string_of_dep dep - | Parents cks -> string_of_callerkidset cks + let s1 = match dep.in_fun with + | Some dep -> "InFun " ^ string_of_dep dep + | None -> "" in - let _ = print_endline (" " ^ string_of_kid kid ^ ": " ^ s) in + let s2 = string_of_callerkidset dep.parents in + let _ = print_endline (" " ^ string_of_kid kid ^ ": " ^ s1 ^ "; " ^ s2) in () in let print_binding id kdep = @@ -2773,8 +2783,12 @@ let analyse_defs debug env (Defs defs) = match Bindings.find id r.split_on_call with | kid_deps -> begin match KBindings.find kid kid_deps with - | InFun deps -> separate_deps deps - | Parents fns -> CallerKidSet.fold add_kid fns (ArgSplits.empty, ExtraSplits.empty, Failures.empty) + | call_dep -> + let (splits, extras, fails) = match call_dep.in_fun with + | Some deps -> separate_deps deps + | None -> (ArgSplits.empty, ExtraSplits.empty, Failures.empty) + in + CallerKidSet.fold add_kid call_dep.parents (splits, extras, fails) | exception Not_found -> ArgSplits.empty,ExtraSplits.empty,Failures.empty end | exception Not_found -> ArgSplits.empty,ExtraSplits.empty,Failures.empty -- cgit v1.2.3 From 01d1586f3dea234609b68f332646882e6474c6da Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 4 May 2020 17:59:20 +0100 Subject: Add some more cases in mono rewrites --- src/monomorphise.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 465ed30f..149162d8 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3042,11 +3042,11 @@ let rec rewrite_app env typ (id,args) = [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot))) (* variable-slice @ local-var *) - | [E_aux (E_app (op, - [vector1; start1; length1]),_); + | [(E_aux (E_app (op, + [vector1; start1; length1]),_) as exp1); (E_aux (E_id _,_) as vector2)] when (is_slice op || is_subrange op) && is_bitvector_typ (typ_of vector1) && - not (is_constant length1) -> + not (is_constant_vec_typ env (typ_of exp1)) -> let op' = if is_subrange op then "subrange_subrange_concat" else "slice_slice_concat" in let zero = mk_exp (E_lit (mk_lit (L_num Big_int.zero))) in let one = mk_exp (E_lit (mk_lit (L_num (Big_int.of_int 1)))) in @@ -3063,11 +3063,11 @@ let rec rewrite_app env typ (id,args) = | [E_aux (E_app (append1, [e1; - E_aux (E_app (op, [vector1; start1; length1]),_)]),_); + (E_aux (E_app (op, [vector1; start1; length1]),_) as slice1)]),_); E_aux (E_app (zeros1, [length2]),_)] when is_append append1 && (is_slice op || is_subrange op) && is_zeros zeros1 && is_constant_vec_typ env (typ_of e1) && is_bitvector_typ (typ_of vector1) && - not (is_constant length1 || is_constant length2) -> + not (is_constant_vec_typ env (typ_of slice1) || is_constant length2) -> let op' = mk_id (if is_subrange op then "subrange_zeros_concat" else "slice_zeros_concat") in let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in -- cgit v1.2.3 From 87db18e7d1736f168491b49b7b339039260d7ac6 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 4 May 2020 17:59:39 +0100 Subject: Lem: Add some reserved identifiers --- src/pretty_print_lem.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 9e636b59..b18541a3 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -95,9 +95,9 @@ let rec fix_id remove_tick name = match name with | "with" | "check" | "field" - | "LT" - | "GT" - | "EQ" + | "LT" | "lt" | "lteq" + | "GT" | "gt" | "gteq" + | "EQ" | "eq" | "neq" | "integer" -> name ^ "'" | _ -> -- cgit v1.2.3 From b8f99df745e03ca5805110f52f5263c2ee2813fe Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 7 May 2020 20:07:00 +0100 Subject: Add another type annotation in bitvector cast rewrite --- src/monomorphise.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 149162d8..0e946f96 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3336,8 +3336,10 @@ let rec rewrite_app env typ (id,args) = match get_constant_vec_len ~solve:true env typ, args with | Some i, [vector1; start1; end1] when is_bitvector_typ (typ_of vector1) && not (is_constant start1 && is_constant end1) -> - let low = if is_inc_vec (typ_of vector1) then start1 else end1 in - E_app (mk_id "slice", [vector1; low; mk_exp (E_lit (mk_lit (L_num i)))]) + let inc = is_inc_vec (typ_of vector1) in + let low = if inc then start1 else end1 in + let exp' = rewrap (E_app (mk_id "slice", [vector1; low; mk_exp (E_lit (mk_lit (L_num i)))])) in + E_cast (bitvector_typ (nconstant i) (if inc then inc_ord else dec_ord), exp') | _, _ -> E_app (id, args) (* Rewrite (v[x .. y] + i) to (v + (i << y))[x .. y], which is more amenable to further rewriting *) -- cgit v1.2.3 From bed9f2f05813afec446a26e441e1df3d08d9c251 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 8 May 2020 13:37:25 +0100 Subject: Only check int kids when simplifying nexps --- src/monomorphise.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 0e946f96..f4d0aa56 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2108,7 +2108,9 @@ let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) = | None -> let is_equal kid = try - prove __POS__ typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown)) + if Env.get_typ_var kid typ_env = K_int then + prove __POS__ typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown)) + else false with _ -> false in match ne with -- cgit v1.2.3 From 336522767a1c3b564fd4798851993afef9f629ed Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 9 May 2020 22:10:49 +0100 Subject: Make Isabelle lemma generation work with grouped regstate --- src/state.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/state.ml b/src/state.ml index 478a3fd5..8d487d3e 100644 --- a/src/state.ml +++ b/src/state.ml @@ -410,12 +410,12 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) = let id' = remove_trailing_underscores id in separate_map hardline string [ "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:"; - " \"\\read_reg " ^ id ^ "_ref\\\\<^sub>S = readS (" ^ id' ^ " \\ regstate)\""; - " by (auto simp: liftState_read_reg_readS register_defs)"; + " \"\\read_reg " ^ id ^ "_ref\\\\<^sub>S = read_regS " ^ id ^ "_ref\""; + " by (intro liftState_read_reg) (auto simp: register_defs)"; ""; "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:"; - " \"\\write_reg " ^ id ^ "_ref v\\\\<^sub>S = updateS (regstate_update (" ^ id' ^ "_update (\\_. v)))\""; - " by (auto simp: liftState_write_reg_updateS register_defs)" + " \"\\write_reg " ^ id ^ "_ref v\\\\<^sub>S = write_regS " ^ id ^ "_ref v\""; + " by (intro liftState_write_reg) (auto simp: register_defs)" ] in string "abbreviation liftS (\"\\_\\\\<^sub>S\") where \"liftS \\ liftState (get_regval, set_regval)\"" ^^ -- cgit v1.2.3 From 33be6201fa34557a46652658445f9c48c819ad34 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 11 May 2020 21:57:39 +0100 Subject: Add caching of calls to solve_unique --- src/constraint.ml | 55 +++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 43 insertions(+), 12 deletions(-) (limited to 'src') diff --git a/src/constraint.ml b/src/constraint.ml index 74f3ec69..3ceb0aae 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -230,6 +230,7 @@ type smt_result = Unknown | Sat | Unsat module DigestMap = Map.Make(Digest) let known_problems = ref (DigestMap.empty) +let known_uniques = ref (DigestMap.empty) let load_digests_err () = let in_chan = open_in_bin "z3_problems" in @@ -241,6 +242,10 @@ let load_digests_err () = | 0 -> known_problems := DigestMap.add digest Unknown !known_problems | 1 -> known_problems := DigestMap.add digest Sat !known_problems | 2 -> known_problems := DigestMap.add digest Unsat !known_problems + | 3 -> known_uniques := DigestMap.add digest None !known_uniques + | 4 -> + let solution = input_binary_int in_chan in + known_uniques := DigestMap.add digest (Some solution) !known_uniques | _ -> assert false end; load () @@ -254,14 +259,21 @@ let load_digests () = let save_digests () = let out_chan = open_out_bin "z3_problems" in - let output digest result = + let output_problem digest result = Digest.output out_chan digest; match result with | Unknown -> output_byte out_chan 0 | Sat -> output_byte out_chan 1 | Unsat -> output_byte out_chan 2 in - DigestMap.iter output !known_problems; + DigestMap.iter output_problem !known_problems; + let output_solution digest result = + Digest.output out_chan digest; + match result with + | None -> output_byte out_chan 3 + | Some i -> output_byte out_chan 4; output_binary_int out_chan i + in + DigestMap.iter output_solution !known_uniques; close_out out_chan let kopt_pair kopt = (kopt_kid kopt, unaux_kind (kopt_kind kopt)) @@ -344,16 +356,17 @@ let call_smt l constraints = Profile.finish_smt t; result -let solve_smt l constraints var = +let solve_smt_file l constraints = let vars = kopts_of_constraint constraints |> KOptSet.elements |> List.map kopt_pair |> List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty in - let smt_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in - let smt_var = pp_sexpr (smt_var var) in + smtlib_of_constraints ~get_model:true l vars constraints +let call_smt_solve l smt_file smt_vars var = + let smt_var = pp_sexpr (smt_vars var) in if !opt_smt_verbose then prerr_endline (Printf.sprintf "SMTLIB2 constraints are (solve for %s): \n%s%!" smt_var smt_file) else (); @@ -389,6 +402,10 @@ let solve_smt l constraints var = with | Not_found -> None +let solve_smt l constraints var = + let smt_file, smt_vars = solve_smt_file l constraints in + call_smt_solve l smt_file smt_vars var + let solve_all_smt l constraints var = let rec aux results = let constraints = List.fold_left (fun ncs r -> (nc_and ncs (nc_neq (nconstant r) (nvar var)))) constraints results in @@ -402,10 +419,24 @@ let solve_all_smt l constraints var = aux [] let solve_unique_smt l constraints var = - match solve_smt l constraints var with - | Some result -> - begin match call_smt l (nc_and constraints (nc_neq (nconstant result) (nvar var))) with - | Unsat -> Some result - | _ -> None - end - | None -> None + let smt_file, smt_vars = solve_smt_file l constraints in + let digest = Digest.string (smt_file ^ pp_sexpr (smt_vars var)) in + match DigestMap.find_opt digest !known_uniques with + | Some (Some result) -> Some (Big_int.of_int result) + | Some (None) -> None + | None -> + match call_smt_solve l smt_file smt_vars var with + | Some result -> + begin match call_smt l (nc_and constraints (nc_neq (nconstant result) (nvar var))) with + | Unsat -> + if Big_int.less_equal Big_int.zero result && Big_int.less result (Big_int.pow_int_positive 2 30) then + known_uniques := DigestMap.add digest (Some (Big_int.to_int result)) !known_uniques + else (); + Some result + | _ -> + known_uniques := DigestMap.add digest None !known_uniques; + None + end + | None -> + known_uniques := DigestMap.add digest None !known_uniques; + None -- cgit v1.2.3