Skip to content

convert smt to expr #103

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
agle wants to merge 6 commits into
base: main
Choose a base branch
from
Open

convert smt to expr #103

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
bb718e6
wip vbroken
agle Mar 24, 2026
78c7ceb
remove duplicate represntation of associative binops
agle Mar 25, 2026
49c5d6a
expand gen set for bvops
agle Mar 25, 2026
282a284
comment
agle Mar 25, 2026
ece9bb0
add predicate expr generator
agle Mar 25, 2026
8baac5e
update ocaml 5.4
agle Mar 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 8 additions & 5 deletions lib/analysis/defuse_bool.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
Expand Down
30 changes: 20 additions & 10 deletions lib/analysis/known_bits.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
20 changes: 14 additions & 6 deletions lib/analysis/wrapped_intervals.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 ->
Expand Down
201 changes: 91 additions & 110 deletions lib/lang/algsimp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand All @@ -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)

Expand Down
11 changes: 11 additions & 0 deletions lib/lang/expr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down
Loading
Loading