diff --git a/lib/analysis/defuse_bool.ml b/lib/analysis/defuse_bool.ml index 2275f1e6..b4000e3d 100644 --- a/lib/analysis/defuse_bool.ml +++ b/lib/analysis/defuse_bool.ml @@ -66,7 +66,7 @@ module IsZeroValueAbstraction = struct | `FACCESS offset -> ( match a with Zero -> Zero | _ -> Top) | `Gamma | `Classification -> Top - let eval_binop (op : Lang.Ops.AllOps.binary) a b = + let eval_binary op a b = match (op, a, b) with | `BVSREM, _, _ -> Top | `BVSDIV, _, _ -> Top @@ -116,12 +116,15 @@ module IsZeroValueAbstraction = struct | `FSET _, _, _ -> Top | #Lang.Ops.Spec.binary, _, _ -> Top + let eval_binop op a b = eval_binary op a b + let eval_intrin (op : Lang.Ops.AllOps.intrin) (args : t list) = match op with - | `BVADD -> List.fold_left (eval_binop `BVADD) Bot args - | `BVOR -> List.fold_left (eval_binop `BVOR) Bot args - | `BVXOR -> List.fold_left (eval_binop `BVXOR) Bot args - | `BVAND -> List.fold_left (eval_binop `BVAND) Bot args + | `BVADD -> List.fold_left (eval_binary `BVADD) Bot args + | `BVOR -> List.fold_left (eval_binary `BVOR) Bot args + | `BVXOR -> List.fold_left (eval_binary `BVXOR) Bot args + | `BVMUL -> List.fold_left (eval_binary `BVXOR) Bot args + | `BVAND -> List.fold_left (eval_binary `BVAND) Bot args | `BVConcat -> List.fold_left join Bot args | `OR -> (* boolean or *) diff --git a/lib/analysis/known_bits.ml b/lib/analysis/known_bits.ml index 4721734f..3e0835db 100644 --- a/lib/analysis/known_bits.ml +++ b/lib/analysis/known_bits.ml @@ -219,27 +219,37 @@ module KnownBitsValueAbstraction = struct | `BVNEG -> tnum_neg a | _ -> ( match rt with Types.Bitvector width -> unknown ~width | _ -> Top) - let eval_binop (op : Lang.Ops.AllOps.binary) (a, _) (b, _) rt = + let eval_binary op (a, _) (b, _) rt = match op with - | `BVADD -> tnum_add a b + | #Lang.Ops.Spec.binary -> Top + | #Lang.Ops.PointerOps.binary -> Top + | #Lang.Ops.RecordOps.binary -> Top + | #Lang.Ops.IntOps.binary -> Top + | #Lang.Ops.LogicalOps.binary -> Top | `BVSUB -> tnum_sub a b - | `BVAND -> tnum_bitand a b | `BVNAND -> tnum_bitnot (tnum_bitand a b) - | `BVOR -> tnum_bitor a b - | `BVXOR -> tnum_bitxor a b | `BVSHL -> tnum_shl a b | `BVLSHR -> tnum_lshr a b | `BVASHR -> tnum_ashr a b + | `BVOR -> tnum_bitor a b + | `BVAND -> tnum_bitand a b + | `BVADD -> tnum_add a b + | `BVXOR -> tnum_bitxor a b | `BVMUL -> tnum_mul a b - | _ -> ( match rt with Types.Bitvector width -> unknown ~width | _ -> Top) + | `BVSDIV | `BVSLE | `BVSLT | `BVSMOD | `BVSREM | `BVUDIV | `BVULE | `BVULT + | `BVUREM -> + Top + + let eval_binop (op : Lang.Ops.AllOps.binary) a b rt = + match op with #Lang.Ops.AllOps.binary as op -> eval_binary op a b rt let eval_intrin (op : Lang.Ops.AllOps.intrin) (args : (t * Types.t) list) rt = let op a b = match op with - | `BVADD -> (eval_binop `BVADD a b rt, rt) - | `BVOR -> (eval_binop `BVOR a b rt, rt) - | `BVXOR -> (eval_binop `BVXOR a b rt, rt) - | `BVAND -> (eval_binop `BVAND a b rt, rt) + | `BVADD -> (eval_binary `BVADD a b rt, rt) + | `BVOR -> (eval_binary `BVOR a b rt, rt) + | `BVXOR -> (eval_binary `BVXOR a b rt, rt) + | `BVAND -> (eval_binary `BVAND a b rt, rt) | `BVConcat -> (tnum_concat (fst a) (fst b), rt) | _ -> ( match rt with diff --git a/lib/analysis/wrapped_intervals.ml b/lib/analysis/wrapped_intervals.ml index ae4f8e0b..8b995a11 100644 --- a/lib/analysis/wrapped_intervals.ml +++ b/lib/analysis/wrapped_intervals.ml @@ -714,10 +714,14 @@ module WrappedIntervalsValueAbstraction = struct | _ -> top) | _ -> top - let eval_binop (op : Lang.Ops.AllOps.binary) (a, ta) (b, tb) rt = + let eval_binary op (a, ta) (b, tb) rt = match (ta, ta) with | Types.Bitvector width, Types.Bitvector w2 when width = w2 -> ( match op with + | #Lang.Ops.Spec.binary -> Top + | #Lang.Ops.RecordOps.binary -> Top + | #Lang.Ops.IntOps.binary -> Top + | #Lang.Ops.LogicalOps.binary -> Top | `BVADD | `PTRADD -> add ~width a b | `BVSUB -> sub ~width a b | `BVMUL -> mul ~width a b @@ -730,16 +734,20 @@ module WrappedIntervalsValueAbstraction = struct | `BVASHR -> ashr ~width a b | `BVLSHR -> lshr ~width a b | `BVSHL -> shl ~width a b - | _ -> top) + | `BVSLE | `BVSLT | `BVSMOD | `BVSREM | `BVULE | `BVULT | `BVUREM -> top + ) | _ -> top + let eval_binop (op : Lang.Ops.AllOps.binary) a b rt = + match op with #Lang.Ops.AllOps.binary as op -> eval_binary op a b rt + let eval_intrin (op : Lang.Ops.AllOps.intrin) (args : (t * Types.t) list) rt = let op a b = match op with - | `BVADD -> (eval_binop `BVADD a b rt, rt) - | `BVOR -> (eval_binop `BVOR a b rt, rt) - | `BVXOR -> (eval_binop `BVXOR a b rt, rt) - | `BVAND -> (eval_binop `BVAND a b rt, rt) + | `BVADD -> (eval_binary `BVADD a b rt, rt) + | `BVOR -> (eval_binary `BVOR a b rt, rt) + | `BVXOR -> (eval_binary `BVXOR a b rt, rt) + | `BVAND -> (eval_binary `BVAND a b rt, rt) | `BVConcat -> ( (match (snd a, snd b) with | Types.Bitvector wa, Types.Bitvector wb -> diff --git a/lib/lang/algsimp.ml b/lib/lang/algsimp.ml index 025bb435..50ef4afc 100644 --- a/lib/lang/algsimp.ml +++ b/lib/lang/algsimp.ml @@ -4,16 +4,23 @@ open Bincaml_util.Common open Expr open Ops -let to_steady equal f x = - let rec loop x = - let n = f x in - if equal n x then n else loop n - in - loop x +module Comb = struct + let to_steady equal f x = + let rec loop x = + let n = f x in + if equal n x then n else loop n + in + loop x + + let sequence (a : 'a -> BasilExpr.rewrite) (b : 'a -> BasilExpr.rewrite) e = + match a e with Keep -> b e | e -> e -let apply_fun in_body args = - let args = args |> VarMap.of_list |> fun m v -> VarMap.find_opt v m in - BasilExpr.substitute args in_body + let apply_fun in_body args = + let args = args |> VarMap.of_list |> fun m v -> VarMap.find_opt v m in + BasilExpr.substitute args in_body +end + +open Comb let rec inline_let_rec e = let open AbstractExpr in @@ -134,131 +141,105 @@ let simplify_concat let simp_concat_fix e = to_steady BasilExpr.equal (BasilExpr.rewrite_typed_two simplify_concat) e -let algebraic_simplifications +(** Replace associative operators with empty or singleton argument lists with + the identity element for the operation, or the single argument, + respectively. + + Note we cannot infer the width of a bitvector operation with no arguments in + order to construct the identity, so such an expression should never be + constructed. + + Used by SMT encoding, so can't be tested by SMT*) +let drop_assoc (e : (BasilExpr.t BasilExpr.abstract_expr * Types.t) BasilExpr.abstract_expr) = let open AbstractExpr in let open BasilExpr in let open Bitvec in - (* trying to make views of abstract exprs simpler; but avoid disacarding the attribs. - There's probably too much to think about still with writing rewriters like this. - - We can build this into fold_with_type/rewrite_typed I guess. - *) - let orig_e (a, b, c) = a in - - (* orig expr, simplified view, expr type *) - let fix_s e = fix (AbstractExpr.of_simple_view e) in - let keep here a = replace here (fix (orig_e a)) in - let to_s (v, t) = (v, AbstractExpr.simple_view v, t) in - let s = AbstractExpr.simple_view (AbstractExpr.map to_s e) in - match s with - | Intrin (`BVConcat, (_, Intrin (`BVConcat, al), _) :: tl) -> - replace [%here] - (fix_s (Intrin (`BVConcat, al @ List.map (orig_e %> fix) tl))) - | Binary (`BVADD, a, (_, C (`Bitvector i), _)) when is_zero i -> - keep [%here] a - | Binary (`BVSUB, a, (_, C (`Bitvector i), _)) when is_zero i -> - keep [%here] a - | Binary (`BVMUL, a, (_, C (`Bitvector i), _)) - when equal i @@ of_int ~size:(size i) 1 -> - keep [%here] a - | Binary (`BVAND, a, (_, C (`Bitvector i), _)) when is_zero i -> - replace [%here] (bvconst (zero ~size:(size i))) - | Binary (`BVAND, a, (_, C (`Bitvector i), _)) - when equal i (ones ~size:(size i)) -> - keep [%here] a - | Binary (`BVOR, a, (_, C (`Bitvector i), _)) - when equal i (ones ~size:(size i)) -> - replace [%here] (bvconst @@ ones ~size:(size i)) - | Binary (`BVOR, a, (_, C (`Bitvector i), _)) when is_zero i -> keep [%here] a - | Unary (`ZeroExtend 0, a) -> keep [%here] a - | Unary (`SignExtend 0, a) -> keep [%here] a - | Unary (`Extract (hi, 0), ((_, _, Bitvector sz) as a)) when hi = sz -> - keep [%here] a - | Unary (`BVNOT, (_, Unary (`BVNOT, a), _)) -> replace [%here] a - | Unary (`BoolNOT, (_, Unary (`BoolNOT, a), _)) -> replace [%here] a + match e with + | ApplyIntrin + { + op = `BVADD | `BVMUL | `BVOR | `BVXOR | `BVAND | `AND | `OR | `BVConcat; + args = [ a ]; + } -> + replace [%here] (fix (fst a)) + | ApplyIntrin { op = `AND; args = [] } -> + replace [%here] (BasilExpr.boolconst true) + | ApplyIntrin { op = `OR; args = [] } -> + replace [%here] (BasilExpr.boolconst false) + | ApplyIntrin { op = `BVConcat; args = [] } -> + replace [%here] (BasilExpr.bvconst @@ Bitvec.zero ~size:0) | _ -> Keep -(* let algebraic_simplifications (e : (BasilExpr.t BasilExpr.abstract_expr * Types.t) BasilExpr.abstract_expr) = let open AbstractExpr in let open BasilExpr in let open Bitvec in - let keep a = Some (fix (fst a)) in + let keep a = fix (fst a) in + let is_bvzero = function + | Constant { const = `Bitvector i } when is_zero i -> true + | _ -> false + in + let is_ones = function + | Constant { const = `Bitvector i } when equal i (ones ~size:(size i)) -> + true + | _ -> false + in + let width_args args = + let size = + List.hd args |> snd |> Types.bit_width |> Option.get_exn_or "not a bv?" + in + size + in match e with | ApplyIntrin { op = `BVConcat; + attrib; args = (ApplyIntrin { op = `BVConcat; args = al }, _) :: tl; } -> - Some (BasilExpr.concatl @@ al @ List.map (fun i -> fix (fst i)) tl) - | BinaryExpr - { op = `BVADD; arg1; arg2 = Constant { const = `Bitvector i }, _ } - when is_zero i -> - keep arg1 + replace [%here] + (BasilExpr.concatl ?attrib @@ al @ List.map (fun i -> fix (fst i)) tl) + | ApplyIntrin { attrib; op = (`BVADD | `BVOR) as op; args } + when List.exists (fst %> is_bvzero) args -> + let size = width_args args in + let args = + args |> List.map fst |> List.filter (is_bvzero %> not) |> List.map fix + in + if List.is_empty args then + replace [%here] (BasilExpr.bvconst ?attrib (Bitvec.zero ~size)) + else replace [%here] (BasilExpr.applyintrin ?attrib ~op args) + | ApplyIntrin { attrib; op = `BVAND | `BVMUL; args } + when List.exists (fst %> is_bvzero) args -> + let size = width_args args in + replace [%here] (BasilExpr.bvconst ?attrib (Bitvec.zero ~size)) | BinaryExpr { op = `BVSUB; arg1; arg2 = Constant { const = `Bitvector i }, _ } when is_zero i -> - keep arg1 - | BinaryExpr - { op = `BVMUL; arg1; arg2 = Constant { const = `Bitvector i }, _ } - when equal i @@ of_int ~size:(size i) 1 -> - keep arg1 - | BinaryExpr { op = `BVAND; arg2 = Constant { const = `Bitvector i }, _ } - when is_zero i -> - Some (bvconst (zero ~size:(size i))) - | BinaryExpr { op = `BVAND; arg1 = Constant { const = `Bitvector i }, _ } - when is_zero i -> - Some (bvconst (zero ~size:(size i))) - | BinaryExpr - { op = `BVAND; arg1; arg2 = Constant { const = `Bitvector i }, _ } - when equal i (ones ~size:(size i)) -> - keep arg1 - | BinaryExpr - { op = `BVAND; arg2; arg1 = Constant { const = `Bitvector i }, _ } - when equal i (ones ~size:(size i)) -> - keep arg2 - | BinaryExpr { op = `BVOR; arg1; arg2 = Constant { const = `Bitvector i }, _ } - when equal i (ones ~size:(size i)) -> - Some (bvconst @@ ones ~size:(size i)) - | BinaryExpr { op = `BVOR; arg1; arg2 = Constant { const = `Bitvector i }, _ } - when is_zero i -> - keep arg1 - | UnaryExpr { op = `ZeroExtend 0; arg } -> keep arg - | UnaryExpr { op = `SignExtend 0; arg } -> keep arg + replace [%here] @@ keep arg1 + | ApplyIntrin { attrib; op = `BVAND; args } + when List.exists (fst %> is_ones) args -> + let args = + args |> List.map fst |> List.filter (is_ones %> not) |> List.map fix + in + replace [%here] (fix @@ ApplyIntrin { attrib; op = `BVAND; args }) + | ApplyIntrin { attrib; op = `BVOR; args } + when List.exists (fst %> is_ones) args -> + let size = width_args args in + replace [%here] (BasilExpr.bvconst ?attrib @@ Bitvec.ones ~size) + | UnaryExpr { op = `ZeroExtend 0; arg } -> replace [%here] @@ keep arg + | UnaryExpr { op = `SignExtend 0; arg } -> replace [%here] @@ keep arg | UnaryExpr { op = `Extract (hi, 0); arg = a, Bitvector sz } when hi = sz -> - Some (fix a) + replace [%here] (fix a) | UnaryExpr { op = `BVNOT; arg = UnaryExpr { op = `BVNOT; arg }, _ } -> - Some arg + replace [%here] arg | UnaryExpr { op = `BoolNOT; arg = UnaryExpr { op = `BoolNOT; arg }, _ } -> - Some arg - | _ -> None - -type 'e rewriter_expr = { - orig : 'e BasilExpr.abstract_expr BasilExpr.abstract_expr; - typ : Types.t; - e : - ( BasilExpr.const, - BasilExpr.var, - BasilExpr.unary, - BasilExpr.binary, - BasilExpr.intrin, - ( BasilExpr.const, - BasilExpr.var, - BasilExpr.unary, - BasilExpr.binary, - BasilExpr.intrin, - 'e ) - AbstractExpr.simple ) - AbstractExpr.simple; -} -*) + replace [%here] arg + | _ -> Keep -let sequence (a : 'a -> BasilExpr.rewrite) (b : 'a -> BasilExpr.rewrite) e = - match a e with Keep -> b e | e -> e +let algebraic_simplifications = sequence drop_assoc algebraic_simplifications let alg_simp_rewriter ?visit e = let partial_eval_expr e = @@ -268,8 +249,8 @@ let alg_simp_rewriter ?visit e = e |> ( to_steady BasilExpr.equal @@ fun e -> e |> partial_eval_expr |> simp_concat_fix ) - |> BasilExpr.rewrite_typed_two ?visit - (sequence simplify_concat algebraic_simplifications) + |> to_steady BasilExpr.equal + (BasilExpr.rewrite_typed_two ?visit algebraic_simplifications) |> to_steady BasilExpr.equal (BasilExpr.rewrite_typed_two ?visit normalise_bool) diff --git a/lib/lang/expr.ml b/lib/lang/expr.ml index 0e68f255..eecd1eac 100644 --- a/lib/lang/expr.ml +++ b/lib/lang/expr.ml @@ -745,6 +745,11 @@ module BasilExpr = struct include R.Constructors + let binexp ?attrib ~op arg1 arg2 = + match op with + | #Ops.AllOps.intrin as op -> applyintrin ?attrib ~op [ arg1; arg2 ] + | #Ops.AllOps.binary as op -> binexp ?attrib ~op arg1 arg2 + let zero_extend ?attrib ~n_prefix_bits (e : t) : t = unexp ?attrib ~op:(`ZeroExtend n_prefix_bits) e @@ -778,6 +783,12 @@ module BasilExpr = struct let bv_of_int ~(size : int) (v : int) : t = const (`Bitvector (Bitvec.of_int ~size v)) + let drop_attrib a = + let a = + rewrite ~rw_fun:(AbstractExpr.drop_attrib %> fix %> replace [%here]) a + in + a + (* module Memoiser = Fix.Memoize.ForHashedType (struct type expr = t diff --git a/lib/lang/expr_eval.ml b/lib/lang/expr_eval.ml index 3f862d55..bb0c0039 100644 --- a/lib/lang/expr_eval.ml +++ b/lib/lang/expr_eval.ml @@ -48,7 +48,7 @@ let eval_expr_alg (e : Ops.AllOps.const option BasilExpr.abstract_expr) = | BinaryExpr { op = `PTRADD; arg1 = a; arg2 = b } -> let* a, typ = get_pointer a in let* b = get_bv b in - pointer (BVOps.eval_binary_unif `BVADD a b, typ) + pointer (BVOps.eval_intrin `BVADD [ a; b ], typ) | BinaryExpr { op = #BVOps.binary_unif as op; arg1 = a; arg2 = b } -> let* a = get_bv a in let* b = get_bv b in @@ -120,7 +120,7 @@ let%expect_test _ = let ten = bv_of_int ~size:10 10 in let e = binexp ~op:`BVMUL - (binexp ~op:`BVADD ten ten) + (applyintrin ~op:`BVADD [ ten; ten ]) (BasilExpr.rvar (Var.create "beans" Types.(Bitvector 10))) in print_endline (to_string e); diff --git a/lib/lang/expr_smt.ml b/lib/lang/expr_smt.ml index d952534c..57cd5300 100644 --- a/lib/lang/expr_smt.ml +++ b/lib/lang/expr_smt.ml @@ -136,6 +136,94 @@ module SMTLib2 = struct in return v + open struct + let of_assoc a : Ops.AllOps.intrin option = + match a with + | "bvadd" -> Some `BVADD + | "bvor" -> Some `BVOR + | "bvand" -> Some `BVAND + | "bvxor" -> Some `BVXOR + | "bvmul" -> Some `BVMUL + | _ -> None + + let of_binop a : Ops.AllOps.binary option = + match a with + | "=" -> Some `EQ + | "bvsrem" -> Some `BVSREM + | "bvsdiv" -> Some `BVSDIV + | "bvashr" -> Some `BVASHR + | "bvsmod" -> Some `BVSMOD + | "bvshl" -> Some `BVSHL + | "bvnand" -> Some `BVNAND + | "bvurem" -> Some `BVUREM + | "bvsub" -> Some `BVSUB + | "bvudiv" -> Some `BVUDIV + | "bvlshr" -> Some `BVLSHR + | "bvsle" -> Some `BVSLE + | "bvule" -> Some `BVULE + | "bvult" -> Some `BVULT + | "bvslt" -> Some `BVSLT + | _ -> None + + let of_unop a : Ops.AllOps.unary option = + match a with + | "bvnot" -> Some `BVNOT + | "bvneg" -> Some `BVNEG + | "not" -> Some `BoolNOT + | _ -> None + end + + let rec expr_of_smt vardefs (e : Sexp.t) = + let open Option.Infix in + let module T = List.Traverse (Option) in + match e with + | `Atom "true" -> Some (BasilExpr.boolconst true) + | `Atom "false" -> Some (BasilExpr.boolconst false) + | `Atom e when Int.of_string e |> Option.is_some -> + Some (BasilExpr.intconst (Z.of_string e)) + | `Atom e -> StringMap.find_opt e vardefs + | `List [ `Atom "_"; `Atom bvalue; `Atom bsize ] -> + let* size = Int.of_string bsize in + let* b = String.chop_prefix ~pre:"bv" bvalue in + let v = Z.of_string b in + Some (BasilExpr.bvconst (Bitvec.create ~size v)) + (*| `List [ `Atom "ite"; c; t; e ] -> + let* c = expr_of_smt vardefs c in + let* t = expr_of_smt vardefs t in + let* e = expr_of_smt vardefs e in + Some (BasilExpr.ifthenelse c t e)*) + | `List (op :: args) -> ( + let* args = T.map_m (expr_of_smt vardefs) args in + match (op, args) with + | `Atom "and", _ -> Some (BasilExpr.applyintrin ~op:`AND args) + | `Atom "or", _ -> Some (BasilExpr.applyintrin ~op:`OR args) + | `Atom "concat", _ -> Some (BasilExpr.applyintrin ~op:`BVConcat args) + | `List [ `Atom "_"; `Atom "extract"; `Atom hi; `Atom lo ], [ a ] -> + let* hi = Int.of_string hi in + let* lo = Int.of_string lo in + Some (BasilExpr.extract ~hi_excl:(hi + 1) ~lo_incl:lo a) + | `List [ `Atom "_"; `Atom "sign_extend"; `Atom bits ], [ a ] -> + let* bits = Int.of_string bits in + Some (BasilExpr.sign_extend ~n_prefix_bits:bits a) + | `List [ `Atom "_"; `Atom "zero_extend"; `Atom bits ], [ a ] -> + let* bits = Int.of_string bits in + Some (BasilExpr.zero_extend ~n_prefix_bits:bits a) + | `Atom u, [ a ] when of_unop u |> Option.is_some -> + let* op = of_unop u in + Some (BasilExpr.unexp ~op a) + | `Atom u, [ a; b ] when of_binop u |> Option.is_some -> + let* op = of_binop u in + Some (BasilExpr.binexp ~op a b) + | `Atom op, args when Option.is_some (of_assoc op) -> + let* op = of_assoc op in + Some (BasilExpr.applyintrin ~op args) + | e, _ -> + print_endline ("unk op: " ^ Sexp.to_string e); + None) + | e -> + print_endline ("unk: " ^ Sexp.to_string e); + None + let decl_var (v : Var.t) s = VarMap.find_opt v s.var_decls |> function | Some { decl_cmd; var } -> (var, s) @@ -259,8 +347,11 @@ module SMTLib2 = struct let* func = func in return @@ list (func :: args) - let of_bexpr e = fst @@ (BasilExpr.cata smt_alg e) empty - let bind_of_bexpr e b = BasilExpr.cata smt_alg e b + let bind_of_bexpr e b = + let e = (BasilExpr.rewrite_typed_two Algsimp.drop_assoc) e in + BasilExpr.cata smt_alg e b + + let of_bexpr e = fst @@ (bind_of_bexpr e) empty let trans_decl (decl : Program.declaration) = let* x = return () in @@ -304,7 +395,7 @@ module SMTLib2 = struct | Variable v -> failwith "mutable" let assert_bexpr e = - let* s = BasilExpr.cata smt_alg e in + let* s = bind_of_bexpr e in add_assert s let push = add_command (list [ atom "push" ]) diff --git a/lib/lang/ops.ml b/lib/lang/ops.ml index 3113d190..5bc72aa5 100644 --- a/lib/lang/ops.ml +++ b/lib/lang/ops.ml @@ -125,16 +125,11 @@ module BVOps = struct | `BVSLT -> Bitvec.slt type binary_unif = - [ `BVAND - | `BVOR - | `BVADD - | `BVMUL - | `BVUDIV + [ `BVUDIV | `BVUREM | `BVSHL | `BVLSHR | `BVNAND - | `BVXOR | `BVSUB | `BVSDIV | `BVSREM @@ -148,24 +143,19 @@ module BVOps = struct match op with | `BVSREM -> srem | `BVSDIV -> sdiv - | `BVADD -> add | `BVASHR -> ashr | `BVSMOD -> smod | `BVSHL -> shl | `BVNAND -> fun a b -> bitnot (bitand a b) | `BVUREM -> urem - | `BVXOR -> bitxor - | `BVOR -> bitor | `BVSUB -> sub | `BVUDIV -> udiv | `BVLSHR -> lshr - | `BVAND -> bitand - | `BVMUL -> mul type binary = [ binary_pred | binary_unif ] [@@deriving show { with_path = false }, eq, ord] - type intrin = [ `BVAND | `BVOR | `BVADD | `BVXOR | `BVConcat ] + type intrin = [ `BVAND | `BVOR | `BVADD | `BVXOR | `BVConcat | `BVMUL ] [@@deriving show { with_path = false }, eq, ord] let eval_intrin (op : intrin) args = @@ -180,6 +170,7 @@ module BVOps = struct | `BVOR -> ev Bitvec.bitor | `BVAND -> ev Bitvec.bitand | `BVConcat -> ev Bitvec.concat + | `BVMUL -> ev Bitvec.mul let show = function | #const as c -> show_const c @@ -375,8 +366,8 @@ module AllOps = struct | `INTLE -> return Boolean | `INTDIV | `INTADD | `INTMUL | `INTSUB | `INTMOD -> return Integer - | `BVAND | `BVOR | `BVADD | `BVMUL | `BVUDIV | `BVUREM | `BVSHL | `BVLSHR - | `BVNAND | `BVXOR | `BVSUB | `BVSDIV | `BVSREM | `BVSMOD | `BVASHR -> + | `BVUDIV | `BVUREM | `BVSHL | `BVLSHR | `BVNAND | `BVSUB | `BVSDIV + | `BVSREM | `BVSMOD | `BVASHR -> return l | `FSET _ -> return r | `PTRADD -> return l @@ -392,6 +383,7 @@ module AllOps = struct match o with | `Cases -> return @@ List.hd @@ List.tl args | `BVADD -> return @@ List.hd args + | `BVMUL -> return @@ List.hd args | `BVOR -> return @@ List.hd args | `BVXOR -> return @@ List.hd args | `BVAND -> return @@ List.hd args diff --git a/lib/transforms/type_check.ml b/lib/transforms/type_check.ml index 19232ade..ee1caf24 100644 --- a/lib/transforms/type_check.ml +++ b/lib/transforms/type_check.ml @@ -134,9 +134,8 @@ let type_check stmt_id block_id expr = ] | _ -> []) | `IMPLIES -> binary_bool_types arg1 arg2 - | `BVSREM | `BVSDIV | `BVADD | `BVASHR | `BVMUL | `BVSHL | `BVNAND | `BVSLE - | `BVUREM | `BVXOR | `BVOR | `BVSUB | `BVUDIV | `BVLSHR | `BVAND | `BVSMOD - | `BVULT | `BVULE | `BVSLT -> ( + | `BVSREM | `BVSDIV | `BVASHR | `BVSHL | `BVNAND | `BVSLE | `BVUREM | `BVSUB + | `BVUDIV | `BVLSHR | `BVSMOD | `BVULT | `BVULE | `BVSLT -> ( match arg1 with | Bitvector sz as typ -> binary_same_types arg1 arg2 typ | _ -> @@ -153,7 +152,7 @@ let type_check stmt_id block_id expr = let check_intrin (op : Ops.AllOps.intrin) (args : Types.t list) : type_error list = match op with - | `BVADD | `BVXOR | `BVOR | `BVAND -> + | `BVADD | `BVXOR | `BVOR | `BVAND | `BVMUL -> let correct_type = List.hd args in List.fold_left (fun acc typ -> diff --git a/readme.md b/readme.md index fd61465d..f9cf1e8c 100644 --- a/readme.md +++ b/readme.md @@ -6,7 +6,7 @@ status: very early stages work-in progress. ### Setup -Supports Linux (at least amd64) and MacOS (arm64) with OCaml 5.3.0. +Supports Linux (at least amd64) and MacOS (arm64) with OCaml 5.4.1. Windows is explicitly not supported outside of WSL. - enable frame pointers on opam switch for performance recording @@ -15,7 +15,7 @@ Windows is explicitly not supported outside of WSL. - Tests requrie smt solver CVC5 installed. ```bash -opam switch create bincaml ocaml-variants.5.3.0+options ocaml-option-flambda ocaml-option-fp +opam switch create bincaml ocaml-variants.5.4.1+options ocaml-option-flambda ocaml-option-fp opam repository add pac https://github.com/uq-pac/opam-repository.git opam install --deps-only --with-doc --with-test . dune build diff --git a/test/analysis/wrapped_intervals.ml b/test/analysis/wrapped_intervals.ml index c9516ff9..314051f6 100644 --- a/test/analysis/wrapped_intervals.ml +++ b/test/analysis/wrapped_intervals.ml @@ -160,7 +160,7 @@ let%test "mul2" = in let t = Types.Bitvector 43 in let abstract = - eval_binop `BVMUL + eval_binary `BVMUL (iv ~w:43 0x48303bae5fb 0x48303bae5fb, t) ( eval_intrin `BVConcat [ diff --git a/test/cram/expr_smt.t b/test/cram/expr_smt.t index f257ff1d..73399269 100644 --- a/test/cram/expr_smt.t +++ b/test/cram/expr_smt.t @@ -7,7 +7,7 @@ Should output no errors Check concat rewrites work $ diff before.il after.il - 17,81c17,18 + 17,83c17,19 < $R28:bv64 := bvor(bvand(bvconcat(extract(1,0, bvlshr(var1_4206396_bv64:bv64, < 0x1f:bv64)), extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), @@ -73,8 +73,11 @@ Check concat rewrites work < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64))), < 0xffffffff00000000:bv64), + < bvand(bvor(0x0:bv64, bvand(var1_4206396_bv64:bv64, 0xffffffff:bv64)), + < 0xffffffff:bv64)); --- > $R28:bv64 := bvor(bvand(sign_extend(63, > extract(32,31, var1_4206396_bv64:bv64)), 0xffffffff00000000:bv64), + > bvand(bvand(var1_4206396_bv64:bv64, 0xffffffff:bv64), 0xffffffff:bv64)); [1] diff --git a/test/cram/typefail.t b/test/cram/typefail.t index 48860951..a9741acc 100644 --- a/test/cram/typefail.t +++ b/test/cram/typefail.t @@ -32,12 +32,12 @@ int is not of bitvector type in bvult at statement 23 in %main_entry int is not of bitvector type in bvule at statement 24 in %main_entry Paramters for the function has a type mismatch: type of bvand(1, 0x1:bv32) != type of $NF:bool (int != bool) at statement 25 in %main_entry - int is not of bitvector type in bvand at statement 25 in %main_entry - bool is not of bitvector type in bvor at statement 26 in %main_entry - bool is not of bitvector type in bvadd at statement 27 in %main_entry - bv32 is not the correct type of bv64 for bvadd at statement 28 in %main_entry - bool is not of bitvector type in bvmul at statement 29 in %main_entry - bv32 is not the correct type of bv64 for bvmul at statement 30 in %main_entry + bv32 is not a bitvector type in bvand at statement 25 in %main_entry + bv32 is not a bitvector type in bvor at statement 26 in %main_entry + bv32 is not a bitvector type in bvadd at statement 27 in %main_entry + bv32 is not a bitvector type in bvadd at statement 28 in %main_entry + bv32 is not a bitvector type in bvmul at statement 29 in %main_entry + bv32 is not a bitvector type in bvmul at statement 30 in %main_entry bool is not of bitvector type in bvudiv at statement 31 in %main_entry bv32 is not the correct type of bv64 for bvudiv at statement 32 in %main_entry bool is not of bitvector type in bvurem at statement 33 in %main_entry @@ -48,8 +48,8 @@ bv32 is not the correct type of bv64 for bvlshr at statement 38 in %main_entry bool is not of bitvector type in bvnand at statement 39 in %main_entry bv32 is not the correct type of bv64 for bvnand at statement 40 in %main_entry - bool is not of bitvector type in bvxor at statement 41 in %main_entry - bv32 is not the correct type of bv64 for bvxor at statement 42 in %main_entry + bv32 is not a bitvector type in bvxor at statement 41 in %main_entry + bv32 is not a bitvector type in bvxor at statement 42 in %main_entry bool is not of bitvector type in bvsub at statement 43 in %main_entry bv32 is not the correct type of bv64 for bvsub at statement 44 in %main_entry bool is not of bitvector type in bvsdiv at statement 45 in %main_entry diff --git a/test/lang/expr_eval_qcheck.ml b/test/lang/expr_eval_qcheck.ml index 2f2638b1..48067a86 100644 --- a/test/lang/expr_eval_qcheck.ml +++ b/test/lang/expr_eval_qcheck.ml @@ -1,5 +1,6 @@ open Lang open Containers +open Fun (** `Extract (hi, lo); `SignExtend n; `ZeroExtend n; `Integer i; `Bitvector z; `Forall; `Old; `INTNEG; `Exists; `IMPLIES; `INTLE; `AND; `OR; `INTLT; @@ -16,7 +17,7 @@ module EvalExprGen = struct let eval_expr = let open QCheck.Gen in let* wd = Expr_gen.gen_width in - Expr_gen.gen_bvexpr (2, wd) + Expr_gen.gen_bvexpr (1, wd) let arb_bvexpr = QCheck.make ~print:Expr.BasilExpr.to_string eval_expr @@ -32,16 +33,40 @@ module EvalExprGen = struct return (exp, partial) end +let check_success_smt query = + let stdout, stderr, _ = CCUnix.call ~stdin:(`Str query) "cvc5" in + match String.lines (String.trim stdout) |> List.rev with + | "success" :: _ -> true + | e :: _ + when CCString.mem ~sub:"invalid argument '0' for 'size'" + (String.lowercase_ascii e) -> + QCheck.assume_fail () + | o :: _ -> failwith ("smt error: " ^ o) + | o -> failwith stdout + let run_smt query = let stdout, stderr, _ = CCUnix.call ~stdin:(`Str query) "cvc5" in match String.trim stdout with | "unsat" -> `UNSAT | "sat" -> `SAT query - | e -> `UNKNOWN (e, stderr) + | e -> `UNKNOWN (e, stdout ^ stderr) + +let check_res res = + match res with + | `UNSAT -> true + | `SAT q -> + print_endline q; + print_endline ""; + false + | `UNKNOWN (e, stderr) + when CCString.mem ~sub:"invalid argument '0' for 'size'" + (String.lowercase_ascii e) -> + QCheck.assume_fail () + | `UNKNOWN (e, stderr) -> failwith (e ^ "\n" ^ stderr) let partial_eval_test = let open QCheck in - Test.make ~name:"partial eval test" ~count:1000 ~max_fail:3 + Test.make ~name:"partial eval matches smt" ~count:300 ~max_fail:3 EvalExprGen.arb_partial_eval_bvexpr @@ fun (exp, evaled) -> let evaled = @@ -59,22 +84,64 @@ let partial_eval_test = comparison |> Expr_smt.SMTLib2.check_sat_bexpr |> Iter.map Sexp.to_string |> String.concat_iter ~sep:"\n" in - let res = run_smt smt in - (*let smt = Lang.Expr_smt.*) - match res with - | `UNSAT -> true - | `SAT q -> - print_endline q; - print_endline ""; - false - | `UNKNOWN (e, stderr) - when CCString.mem ~sub:"invalid argument '0' for 'size'" - (String.lowercase_ascii e) -> - assume_fail () - | `UNKNOWN (e, stderr) -> failwith (e ^ "\n" ^ stderr) + check_res (run_smt (smt ^ "\n(exit)")) +(*let smt = Lang.Expr_smt.*) let () = Printexc.record_backtrace true +module StringMap = Map.Make (String) +module SMT = Bincaml_util.Smt.Solver + +let check_smt = + let gen = + let open QCheck.Gen in + let* e = Expr_gen.gen_expr in + let e = (Expr.BasilExpr.rewrite_typed_two Algsimp.drop_assoc) e in + let smt = Expr_smt.SMTLib2.of_bexpr e in + let parsed = Expr_smt.SMTLib2.expr_of_smt StringMap.empty smt in + return (e, smt, parsed) + in + + let arb = + QCheck.make + ~print:(fun (a, s, e) -> + Expr.BasilExpr.to_string a ^ " -> " ^ Sexp.to_string s ^ " -> " + ^ match e with None -> "none" | Some e -> Expr.BasilExpr.to_string e) + gen + in + + let valid_predicate (e, smt, p) = + let check_p = + Expr_smt.SMTLib2.of_bexpr + @@ Expr.BasilExpr.boolnot (Expr.BasilExpr.binexp ~op:`EQ e e) + in + let query = + "(set-logic QF_BV)\n(set-option :print-success true)\n" + ^ Sexp.to_string + (Expr_smt.SMTLib2.add_assert check_p Expr_smt.SMTLib2.empty |> fst) + ^ "\n(exit)" + in + check_success_smt query + in + + let roundtrip_predicate (e, smt, p) = + p + |> Option.exists + (Expr.BasilExpr.rewrite_typed_two Algsimp.drop_assoc + %> Expr.BasilExpr.equal e) + in + + [ + QCheck.Test.make ~name:"expr smt roundtrip" ~count:1000 ~max_fail:1 arb + roundtrip_predicate; + QCheck.Test.make ~name:"expr valid smt" ~count:30 ~max_fail:1 arb + valid_predicate; + ] + let _ = - let suite = List.map QCheck_alcotest.to_alcotest [ partial_eval_test ] in - Alcotest.run "smteval cvc qcheck" [ ("bv", suite) ] + let suite = + List.map + (QCheck_alcotest.to_alcotest ~long:true ~speed_level:`Slow ~verbose:true) + (partial_eval_test :: check_smt) + in + Alcotest.run "smtlib exprs" [ ("bv", suite) ] diff --git a/test/lang/expr_gen.ml b/test/lang/expr_gen.ml index 0e6f22f5..d8428d3d 100644 --- a/test/lang/expr_gen.ml +++ b/test/lang/expr_gen.ml @@ -8,23 +8,27 @@ type 'a gen = 'a QCheck.Gen.t let bv_unop = [ `BVNOT; `BVNEG ] let bv_ops_partial = [ `BVSREM; `BVSDIV; `BVUREM; `BVUDIV; `BVSMOD ] +let bv_binops_pred : Ops.BVOps.binary_pred list = + [ `EQ; `BVSLT; `BVSLE; `BVULT; `BVULE ] + let bv_ops_total = [ - `BVADD; `BVSUB; - `BVMUL; `BVSHL; `BVNAND; + `BVSUB; `BVXOR; `BVOR; `BVLSHR; `BVASHR; `BVAND; + `BVMUL; + `BVNAND; ] -let multi = [ `BVADD; `BVOR; `BVXOR; `BVAND ] +let multi = [ `BVMUL; `BVADD; `BVOR; `BVXOR; `BVAND ] let gen_width = int_range 1 62 -let arb_bv_op : Ops.BVOps.binary gen = oneof_list bv_ops_total +let arb_bv_op = oneof_list bv_ops_total let random_binary_string st length = (* 0b011101... *) @@ -111,3 +115,52 @@ let gen_bvexpr = let* r = self wd >|= ensure_nonzero wd in gen_binop_partial l r ); ]) + +let gen_bool = + let* b = bool in + return @@ Expr.BasilExpr.boolconst b + +let gen_not f = + let* u = f in + return @@ BasilExpr.unexp ~op:`BoolNOT u + +module LT = List.Traverse (QCheck.Gen) + +let gen_bv_pred = + let* w = int_range 2 32 in + let* a = gen_bvexpr (2, w) in + let* b = gen_bvexpr (2, w) in + let* op = oneof_list bv_binops_pred in + return @@ BasilExpr.binexp ~op a b + +let gen_pred f = + let* a = int_range 1 10 in + let* args = LT.map_m (fun _ -> f) (List.init a Fun.id) in + let* op = oneof_list [ `AND; `OR ] in + return @@ BasilExpr.applyintrin ~op args + +let gen_pred_expr = + fix (fun self size -> + let self = self (size / 2) in + match size with + | 0 -> gen_bool + | size -> + oneof_weighted + [ + (1, gen_bool); + (2, gen_bv_pred); + (2, gen_not self); + (2, gen_pred self); + ]) + +let gen_expr = + let gbv = + let* wd = int_range 2 65 in + let* c = int_bound 3 in + gen_bvexpr (wd, c) + in + let gpred = + let* c = int_bound 3 in + gen_pred_expr c + in + oneof_weighted [ (1, gpred); (1, gbv) ]