pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Simplify arithmetic terms due to not needing type

Browse Source 
Summary:
Now that terms operate over unbounded, signed, integers rather than
bounded integers, and Boolean operations are treated uniformly with
bitwise operations, it is not necessary to propagate types throughout
arithmetic term manipulation.

Reviewed By: bennostein

Differential Revision: D17665257

fbshipit-source-id: 5236b101d
master
Josh Berdine 5 years ago committed by Facebook Github Bot
parent 471d296266
commit a3506f995c
11 changed files with 236 additions and 325 deletions
Show Stats Download Patch File Download Diff File

5
sledge/src/symbheap/equality.ml
Unescape View File

@ -233,12 +233,9 @@ let difference r a b =
let b = canon r b in let b = canon r b in
( if Term.equal a b then Some Z.zero ( if Term.equal a b then Some Z.zero
else else
match (Term.typ a, Term.typ b) with match normalize r (Term.sub a b) with
| Some typ, _ | _, Some typ -> (
match normalize r (Term.sub typ a b) with
| Integer {data} -> Some data | Integer {data} -> Some data
| _ -> None ) | _ -> None )
| _ -> None )
|> |>
[%Trace.retn fun {pf} -> [%Trace.retn fun {pf} ->
function Some d -> pf "%a" Z.pp_print d | None -> pf ""] function Some d -> pf "%a" Z.pp_print d | None -> pf ""]

14
sledge/src/symbheap/equality_test.ml
Unescape View File

@ -18,10 +18,10 @@ let%test_module _ =
let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r) let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r)
let i8 = Typ.integer ~bits:8 let i8 = Typ.integer ~bits:8
let i64 = Typ.integer ~bits:64 let i64 = Typ.integer ~bits:64
let ( ! ) i = Term.integer (Z.of_int i) Typ.siz let ( ! ) i = Term.integer (Z.of_int i)
let ( + ) = Term.add Typ.siz let ( + ) = Term.add
let ( - ) = Term.sub Typ.siz let ( - ) = Term.sub
let ( * ) = Term.mul Typ.siz let ( * ) = Term.mul
let f = Term.convert ~dst:i64 ~src:i8 let f = Term.convert ~dst:i64 ~src:i8
let g = Term.rem let g = Term.rem
let wrt = Var.Set.empty let wrt = Var.Set.empty
@ -307,7 +307,7 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
pp r14 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}] pp r14 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}]
let%test _ = entails_eq r14 a (Term.bool true) let%test _ = entails_eq r14 a Term.true_
let b = Term.dq y !0 let b = Term.dq y !0
let r14 = of_eqs [(a, b); (x, !1)] let r14 = of_eqs [(a, b); (x, !1)]
@ -318,8 +318,8 @@ let%test_module _ =
{| {|
{sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}] {sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
let%test _ = entails_eq r14 a (Term.bool true) let%test _ = entails_eq r14 a Term.true_
let%test _ = entails_eq r14 b (Term.bool true) let%test _ = entails_eq r14 b Term.true_
let b = Term.dq x !0 let b = Term.dq x !0
let r15 = of_eqs [(b, b); (x, !1)] let r15 = of_eqs [(b, b); (x, !1)]

44
sledge/src/symbheap/exec.ml
Unescape View File

@ -32,7 +32,6 @@ let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
{us; xs; seg= {loc; bas; len; siz; arr}} {us; xs; seg= {loc; bas; len; siz; arr}}
let null_eq ptr = Sh.pure (Term.eq Term.null ptr) let null_eq ptr = Sh.pure (Term.eq Term.null ptr)
let zero = Term.integer Z.zero Typ.siz
(* Overwritten variables renaming and remaining modified variables. [ws] are (* Overwritten variables renaming and remaining modified variables. [ws] are
the written variables; [rs] are the variables read or in the the written variables; [rs] are the variables read or in the
@ -117,7 +116,7 @@ let memcpy_eq_spec us dst src len =
let {us= _; xs; seg} = fresh_seg ~loc:dst ~len us in let {us= _; xs; seg} = fresh_seg ~loc:dst ~len us in
let dst_heap = Sh.seg seg in let dst_heap = Sh.seg seg in
let foot = let foot =
Sh.and_ (Term.eq dst src) (Sh.and_ (Term.eq len zero) dst_heap) Sh.and_ (Term.eq dst src) (Sh.and_ (Term.eq len Term.zero) dst_heap)
in in
let post = dst_heap in let post = dst_heap in
{xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -165,9 +164,9 @@ let memmov_foot us dst src len =
let arr_dst, us, xs = fresh_var "a" us xs in let arr_dst, us, xs = fresh_var "a" us xs in
let arr_mid, us, xs = fresh_var "a" us xs in let arr_mid, us, xs = fresh_var "a" us xs in
let arr_src, us, xs = fresh_var "a" us xs in let arr_src, us, xs = fresh_var "a" us xs in
let src_dst = Term.sub Typ.siz src dst in let src_dst = Term.sub src dst in
let mem_dst = Term.memory ~siz:src_dst ~arr:arr_dst in let mem_dst = Term.memory ~siz:src_dst ~arr:arr_dst in
let siz_mid = Term.sub Typ.siz len src_dst in let siz_mid = Term.sub len src_dst in
let mem_mid = Term.memory ~siz:siz_mid ~arr:arr_mid in let mem_mid = Term.memory ~siz:siz_mid ~arr:arr_mid in
let mem_src = Term.memory ~siz:src_dst ~arr:arr_src in let mem_src = Term.memory ~siz:src_dst ~arr:arr_src in
let mem_dst_mid_src = Term.concat [|mem_dst; mem_mid; mem_src|] in let mem_dst_mid_src = Term.concat [|mem_dst; mem_mid; mem_src|] in
@ -184,7 +183,7 @@ let memmov_foot us dst src len =
let foot = let foot =
Sh.and_ eq_mem_dst_mid_src Sh.and_ eq_mem_dst_mid_src
(Sh.and_ (Term.lt dst src) (Sh.and_ (Term.lt dst src)
(Sh.and_ (Term.lt src (Term.add Typ.ptr dst len)) seg)) (Sh.and_ (Term.lt src (Term.add dst len)) seg))
in in
(xs, bas, siz, mem_dst, mem_mid, mem_src, foot) (xs, bas, siz, mem_dst, mem_mid, mem_src, foot)
@ -252,7 +251,7 @@ let memmov_specs us dst src len =
*) *)
let alloc_spec us reg num len = let alloc_spec us reg num len =
let foot = Sh.emp in let foot = Sh.emp in
let siz = Term.mul Typ.siz num len in let siz = Term.mul num len in
let sub, ms, us = let sub, ms, us =
assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us
in in
@ -324,13 +323,13 @@ let mallocx_spec us reg siz =
*) *)
let calloc_spec us reg num len = let calloc_spec us reg num len =
let foot = Sh.emp in let foot = Sh.emp in
let siz = Term.mul Typ.siz num len in let siz = Term.mul num len in
let sub, ms, us = let sub, ms, us =
assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us
in in
let loc = Term.var reg in let loc = Term.var reg in
let siz = Term.rename sub siz in let siz = Term.rename sub siz in
let arr = Term.splat ~byt:(Term.integer Z.zero Typ.byt) ~siz in let arr = Term.splat ~byt:Term.zero ~siz in
let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~arr us in let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~arr us in
let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
{xs; foot; sub; ms; post} {xs; foot; sub; ms; post}
@ -357,8 +356,8 @@ let posix_memalign_spec us reg ptr siz =
let {us= _; xs; seg= qseg} = let {us= _; xs; seg= qseg} =
fresh_seg ~loc:q ~bas:q ~len:siz ~siz ~xs us fresh_seg ~loc:q ~bas:q ~len:siz ~siz ~xs us
in in
let eok = Term.integer (Z.of_int 0) Typ.int in let eok = Term.zero in
let enomem = Term.integer (Z.of_int 12) Typ.int in let enomem = Term.integer (Z.of_int 12) in
let post = let post =
Sh.or_ Sh.or_
(Sh.and_ (Term.eq (Term.var reg) enomem) (Sh.rename sub foot)) (Sh.and_ (Term.eq (Term.var reg) enomem) (Sh.rename sub foot))
@ -402,12 +401,12 @@ let realloc_spec us reg ptr siz =
(eq (memory ~siz ~arr:a1) (eq (memory ~siz ~arr:a1)
(concat (concat
[| memory ~siz:len ~arr:a0 [| memory ~siz:len ~arr:a0
; memory ~siz:(sub Typ.siz siz len) ~arr:a2 |])) ; memory ~siz:(sub siz len) ~arr:a2 |]))
~els: ~els:
(eq (memory ~siz:len ~arr:a0) (eq (memory ~siz:len ~arr:a0)
(concat (concat
[| memory ~siz ~arr:a1 [| memory ~siz ~arr:a1
; memory ~siz:(sub Typ.siz len siz) ~arr:a2 |]))) ; memory ~siz:(sub len siz) ~arr:a2 |])))
(Sh.seg rseg)) (Sh.seg rseg))
in in
{xs; foot; sub; ms; post} {xs; foot; sub; ms; post}
@ -444,12 +443,12 @@ let rallocx_spec us reg ptr siz =
(eq (memory ~siz ~arr:a1) (eq (memory ~siz ~arr:a1)
(concat (concat
[| memory ~siz:len ~arr:a0 [| memory ~siz:len ~arr:a0
; memory ~siz:(sub Typ.siz siz len) ~arr:a2 |])) ; memory ~siz:(sub siz len) ~arr:a2 |]))
~els: ~els:
(eq (memory ~siz:len ~arr:a0) (eq (memory ~siz:len ~arr:a0)
(concat (concat
[| memory ~siz ~arr:a1 [| memory ~siz ~arr:a1
; memory ~siz:(sub Typ.siz len siz) ~arr:a2 |]))) ; memory ~siz:(sub len siz) ~arr:a2 |])))
(Sh.seg rseg)) (Sh.seg rseg))
in in
{xs; foot; sub; ms; post} {xs; foot; sub; ms; post}
@ -488,13 +487,13 @@ let xallocx_spec us reg ptr siz ext =
(eq (memory ~siz ~arr:a1) (eq (memory ~siz ~arr:a1)
(concat (concat
[| memory ~siz:len ~arr:a0 [| memory ~siz:len ~arr:a0
; memory ~siz:(sub Typ.siz siz len) ~arr:a2 |])) ; memory ~siz:(sub siz len) ~arr:a2 |]))
~els: ~els:
(eq (memory ~siz:len ~arr:a0) (eq (memory ~siz:len ~arr:a0)
(concat (concat
[| memory ~siz ~arr:a1 [| memory ~siz ~arr:a1
; memory ~siz:(sub Typ.siz len siz) ~arr:a2 |]))) ; memory ~siz:(sub len siz) ~arr:a2 |])))
(and_ (le siz reg) (le reg (add Typ.siz siz ext)))) (and_ (le siz reg) (le reg (add siz ext))))
(Sh.seg seg') (Sh.seg seg')
in in
{xs; foot; sub; ms; post} {xs; foot; sub; ms; post}
@ -529,15 +528,14 @@ let malloc_usable_size_spec us reg ptr =
*) *)
let nallocx_spec us reg siz = let nallocx_spec us reg siz =
let xs = Var.Set.empty in let xs = Var.Set.empty in
let foot = Sh.pure (Term.dq siz zero) in let foot = Sh.pure (Term.dq siz Term.zero) in
let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in
let loc = Term.var reg in let loc = Term.var reg in
let siz = Term.rename sub siz in let siz = Term.rename sub siz in
let post = Sh.or_ (null_eq loc) (Sh.pure (Term.eq loc siz)) in let post = Sh.or_ (null_eq loc) (Sh.pure (Term.eq loc siz)) in
{xs; foot; sub; ms; post} {xs; foot; sub; ms; post}
let size_of_int_mul n = let size_of_int_mul n = Term.mul (Option.value_exn (Term.size_of Typ.siz)) n
Term.mul Typ.siz (Option.value_exn (Term.size_of Typ.siz)) n
(* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 } (* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 }
* mallctl r i w n * mallctl r i w n
@ -642,11 +640,7 @@ let strlen_spec us reg ptr =
let foot = Sh.seg seg in let foot = Sh.seg seg in
let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in
let {Sh.loc= p; bas= b; len= m; _} = seg in let {Sh.loc= p; bas= b; len= m; _} = seg in
let ret = let ret = Term.sub (Term.sub (Term.add b m) p) Term.one in
Term.sub Typ.siz
(Term.sub Typ.siz (Term.add Typ.siz b m) p)
(Term.integer Z.one Typ.siz)
in
let post = let post =
Sh.and_ Sh.and_
(Term.eq (Term.var reg) (Term.rename sub ret)) (Term.eq (Term.var reg) (Term.rename sub ret))

16
sledge/src/symbheap/sh.ml
Unescape View File

@ -133,9 +133,7 @@ let rec fv_union init q =
let fv q = fv_union Var.Set.empty q let fv q = fv_union Var.Set.empty q
let invariant_pure = function let invariant_pure = function
| Term.Integer {data; typ} -> | Term.Integer {data} -> assert (not (Z.is_false data))
assert (Typ.equal Typ.bool typ) ;
assert (not (Z.is_false data))
| _ -> assert true | _ -> assert true
let invariant_seg _ = () let invariant_seg _ = ()
@ -381,17 +379,15 @@ let rec pure (e : Term.t) =
; ;
let us = Term.fv e in let us = Term.fv e in
let eq_false b = let eq_false b =
let cong = Equality.and_eq b (Term.bool false) Equality.true_ in let cong = Equality.and_eq b Term.false_ Equality.true_ in
{emp with us; cong; pure= [e]} {emp with us; cong; pure= [e]}
in in
( match e with ( match e with
| Integer {data; typ= _} -> if Z.is_false data then false_ us else emp | Integer {data} -> if Z.is_false data then false_ us else emp
(* ¬b ==> false = b *) (* ¬b ==> false = b *)
| App {op= App {op= Xor; arg= Integer {data; typ= _}}; arg} | App {op= App {op= Xor; arg= Integer {data}}; arg} when Z.is_true data ->
when Z.is_true data ->
eq_false arg eq_false arg
| App {op= App {op= Xor; arg}; arg= Integer {data; typ= _}} | App {op= App {op= Xor; arg}; arg= Integer {data}} when Z.is_true data ->
when Z.is_true data ->
eq_false arg eq_false arg
| App {op= App {op= And; arg= e1}; arg= e2} -> star (pure e1) (pure e2) | App {op= App {op= And; arg= e1}; arg= e2} -> star (pure e1) (pure e2)
| App {op= App {op= Or; arg= e1}; arg= e2} -> or_ (pure e1) (pure e2) | App {op= App {op= Or; arg= e1}; arg= e2} -> or_ (pure e1) (pure e2)
@ -399,7 +395,7 @@ let rec pure (e : Term.t) =
-> ->
or_ or_
(star (pure cnd) (pure thn)) (star (pure cnd) (pure thn))
(star (pure (Term.not_ Typ.bool cnd)) (pure els)) (star (pure (Term.not_ cnd)) (pure els))
| App {op= App {op= Eq; arg= e1}; arg= e2} -> | App {op= App {op= Eq; arg= e1}; arg= e2} ->
let cong = Equality.(and_eq e1 e2 true_) in let cong = Equality.(and_eq e1 e2 true_) in
if Equality.is_false cong then false_ us if Equality.is_false cong then false_ us

2
sledge/src/symbheap/sh_domain.ml
Unescape View File

@ -21,7 +21,7 @@ let init globals =
Vector.fold globals ~init:Sh.emp ~f:(fun q -> function Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
| {Global.reg; init= Some (arr, siz)} -> | {Global.reg; init= Some (arr, siz)} ->
let loc = Term.var (Var.of_reg reg) in let loc = Term.var (Var.of_reg reg) in
let len = Term.integer (Z.of_int siz) Typ.siz in let len = Term.integer (Z.of_int siz) in
let arr = Term.of_exp arr in let arr = Term.of_exp arr in
Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr}) Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
| _ -> q ) | _ -> q )

2
sledge/src/symbheap/sh_test.ml
Unescape View File

@ -13,7 +13,7 @@ let%test_module _ =
let pp = Format.printf "@\n%a@." Sh.pp let pp = Format.printf "@\n%a@." Sh.pp
let pp_djn = Format.printf "@\n%a@." Sh.pp_djn let pp_djn = Format.printf "@\n%a@." Sh.pp_djn
let ( ~$ ) = Var.Set.of_list let ( ~$ ) = Var.Set.of_list
let ( ! ) i = Term.integer (Z.of_int i) Typ.siz let ( ! ) i = Term.integer (Z.of_int i)
let ( = ) = Term.eq let ( = ) = Term.eq
let wrt = Var.Set.empty let wrt = Var.Set.empty
let x_, wrt = Var.fresh "x" ~wrt let x_, wrt = Var.fresh "x" ~wrt

55
sledge/src/symbheap/solver.ml
Unescape View File

@ -62,7 +62,7 @@ let single_existential_occurrence xs term =
let special_cases xs = function let special_cases xs = function
| Term.App {op= App {op= Eq; arg= Var _}; arg= Var _} as e -> | Term.App {op= App {op= Eq; arg= Var _}; arg= Var _} as e ->
if Set.is_subset (Term.fv e) ~of_:xs then Term.bool true else e if Set.is_subset (Term.fv e) ~of_:xs then Term.true_ else e
| e -> e | e -> e
let excise_term ({us; min; xs} as goal) pure term = let excise_term ({us; min; xs} as goal) pure term =
@ -136,7 +136,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in
let o_n = Term.integer o_n Typ.siz in let o_n = Term.integer o_n in
let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in
@ -147,8 +147,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
(Term.concat (Term.concat
[|Term.memory ~siz:n ~arr:a0; Term.memory ~siz:o_n ~arr:a1|])) [|Term.memory ~siz:n ~arr:a0; Term.memory ~siz:o_n ~arr:a1|]))
(Sh.star (Sh.star
(Sh.seg (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; arr= a1})
{loc= Term.add Typ.ptr k n; bas= b; len= m; siz= o_n; arr= a1})
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
@ -178,7 +177,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
let {Sh.bas= b; len= m; siz= o; arr= a} = msg in let {Sh.bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
let n_o = Term.integer n_o Typ.siz in let n_o = Term.integer n_o in
let com = Sh.star (Sh.seg msg) com in let com = Sh.star (Sh.seg msg) com in
let min = Sh.rem_seg msg min in let min = Sh.rem_seg msg min in
let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Set.union us xs) in let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Set.union us xs) in
@ -193,11 +192,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
(Term.memory ~siz:n ~arr:a')) (Term.memory ~siz:n ~arr:a'))
(Sh.star (Sh.star
(Sh.seg (Sh.seg
{ loc= Term.add Typ.ptr l o {loc= Term.add l o; bas= b'; len= m'; siz= n_o; arr= a1'})
; bas= b'
; len= m'
; siz= n_o
; arr= a1' })
(Sh.rem_seg ssg sub)))) (Sh.rem_seg ssg sub))))
in in
{goal with us; com; min; xs; sub; zs} {goal with us; com; min; xs; sub; zs}
@ -222,7 +217,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
let l_k = Term.integer l_k Typ.siz in let l_k = Term.integer l_k in
let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
let com = let com =
@ -265,9 +260,9 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
let l_k = Term.integer l_k Typ.siz let l_k = Term.integer l_k in
and ko_ln = Term.integer ko_ln Typ.siz in let ko_ln = Term.integer ko_ln in
let ln = Term.add Typ.ptr l n in let ln = Term.add l n in
let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
@ -315,10 +310,10 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
let l_k = Term.integer l_k Typ.siz in let l_k = Term.integer l_k in
let ko_l = Term.integer ko_l Typ.siz in let ko_l = Term.integer ko_l in
let ln_ko = Term.integer ln_ko Typ.siz in let ln_ko = Term.integer ln_ko in
let ko = Term.add Typ.ptr k o in let ko = Term.add k o in
let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
@ -371,7 +366,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
let {Sh.bas= b; len= m; siz= o; arr= a} = msg in let {Sh.bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
let k_l = Term.integer k_l Typ.siz in let k_l = Term.integer k_l in
let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
let com = Sh.star (Sh.seg msg) com in let com = Sh.star (Sh.seg msg) com in
let min = Sh.rem_seg msg min in let min = Sh.rem_seg msg min in
@ -412,9 +407,9 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
let k_l = Term.integer k_l Typ.siz in let k_l = Term.integer k_l in
let ln_ko = Term.integer ln_ko Typ.siz in let ln_ko = Term.integer ln_ko in
let ko = Term.add Typ.ptr k o in let ko = Term.add k o in
let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
let com = Sh.star (Sh.seg msg) com in let com = Sh.star (Sh.seg msg) com in
@ -458,10 +453,10 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
let k_l = Term.integer k_l Typ.siz in let k_l = Term.integer k_l in
let ln_k = Term.integer ln_k Typ.siz in let ln_k = Term.integer ln_k in
let ko_ln = Term.integer ko_ln Typ.siz in let ko_ln = Term.integer ko_ln in
let ln = Term.add Typ.ptr l n in let ln = Term.add l n in
let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
@ -513,8 +508,8 @@ let excise_seg ({sub} as goal) msg ssg =
match[@warning "-p"] Z.sign k_l with match[@warning "-p"] Z.sign k_l with
(* k-l < 0 so k < l *) (* k-l < 0 so k < l *)
| -1 -> ( | -1 -> (
let ko = Term.add Typ.ptr k o in let ko = Term.add k o in
let ln = Term.add Typ.ptr l n in let ln = Term.add l n in
Equality.difference sub.cong ko ln Equality.difference sub.cong ko ln
>>= fun ko_ln -> >>= fun ko_ln ->
match[@warning "-p"] Z.sign ko_ln with match[@warning "-p"] Z.sign ko_ln with
@ -553,8 +548,8 @@ let excise_seg ({sub} as goal) msg ssg =
| 1 -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) ) | 1 -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) )
(* k-l > 0 so k > l *) (* k-l > 0 so k > l *)
| 1 -> ( | 1 -> (
let ko = Term.add Typ.ptr k o in let ko = Term.add k o in
let ln = Term.add Typ.ptr l n in let ln = Term.add l n in
Equality.difference sub.cong ko ln Equality.difference sub.cong ko ln
>>= fun ko_ln -> >>= fun ko_ln ->
match[@warning "-p"] Z.sign ko_ln with match[@warning "-p"] Z.sign ko_ln with

8
sledge/src/symbheap/solver_test.ml
Unescape View File

@ -22,10 +22,10 @@ let%test_module _ =
Solver.infer_frame p (Var.Set.of_list xs) q Solver.infer_frame p (Var.Set.of_list xs) q
|> fun r -> assert (Option.is_some r) |> fun r -> assert (Option.is_some r)
let ( ! ) i = Term.integer (Z.of_int i) Typ.siz let ( ! ) i = Term.integer (Z.of_int i)
let ( + ) = Term.add Typ.ptr let ( + ) = Term.add
let ( - ) = Term.sub Typ.siz let ( - ) = Term.sub
let ( * ) = Term.mul Typ.siz let ( * ) = Term.mul
let wrt = Var.Set.empty let wrt = Var.Set.empty
let a_, wrt = Var.fresh "a" ~wrt let a_, wrt = Var.fresh "a" ~wrt
let a2_, wrt = Var.fresh "a" ~wrt let a2_, wrt = Var.fresh "a" ~wrt

338
sledge/src/symbheap/term.ml
Unescape View File

@ -20,8 +20,8 @@ module rec T : sig
type t = type t =
(* nary: arithmetic, numeric and pointer *) (* nary: arithmetic, numeric and pointer *)
| Add of {args: qset; typ: Typ.t} | Add of {args: qset}
| Mul of {args: qset; typ: Typ.t} | Mul of {args: qset}
(* pointer and memory constants and operations *) (* pointer and memory constants and operations *)
| Splat of {byt: t; siz: t} | Splat of {byt: t; siz: t}
| Memory of {siz: t; arr: t} | Memory of {siz: t; arr: t}
@ -62,7 +62,7 @@ module rec T : sig
| Extract of {unsigned: bool; bits: int} | Extract of {unsigned: bool; bits: int}
| Convert of {unsigned: bool; dst: Typ.t; src: Typ.t} | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
(* numeric constants *) (* numeric constants *)
| Integer of {data: Z.t; typ: Typ.t} | Integer of {data: Z.t}
| Float of {data: string} | Float of {data: string}
[@@deriving compare, equal, hash, sexp] [@@deriving compare, equal, hash, sexp]
@ -82,8 +82,8 @@ and T0 : sig
type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
type t = type t =
| Add of {args: qset; typ: Typ.t} | Add of {args: qset}
| Mul of {args: qset; typ: Typ.t} | Mul of {args: qset}
| Splat of {byt: t; siz: t} | Splat of {byt: t; siz: t}
| Memory of {siz: t; arr: t} | Memory of {siz: t; arr: t}
| Concat of {args: t vector} | Concat of {args: t vector}
@ -114,15 +114,15 @@ and T0 : sig
| Struct_rec of {elts: t vector} | Struct_rec of {elts: t vector}
| Extract of {unsigned: bool; bits: int} | Extract of {unsigned: bool; bits: int}
| Convert of {unsigned: bool; dst: Typ.t; src: Typ.t} | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
| Integer of {data: Z.t; typ: Typ.t} | Integer of {data: Z.t}
| Float of {data: string} | Float of {data: string}
[@@deriving compare, equal, hash, sexp] [@@deriving compare, equal, hash, sexp]
end = struct end = struct
type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
type t = type t =
| Add of {args: qset; typ: Typ.t} | Add of {args: qset}
| Mul of {args: qset; typ: Typ.t} | Mul of {args: qset}
| Splat of {byt: t; siz: t} | Splat of {byt: t; siz: t}
| Memory of {siz: t; arr: t} | Memory of {siz: t; arr: t}
| Concat of {args: t vector} | Concat of {args: t vector}
@ -153,7 +153,7 @@ end = struct
| Struct_rec of {elts: t vector} | Struct_rec of {elts: t vector}
| Extract of {unsigned: bool; bits: int} | Extract of {unsigned: bool; bits: int}
| Convert of {unsigned: bool; dst: Typ.t; src: Typ.t} | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
| Integer of {data: Z.t; typ: Typ.t} | Integer of {data: Z.t}
| Float of {data: string} | Float of {data: string}
[@@deriving compare, equal, hash, sexp] [@@deriving compare, equal, hash, sexp]
end end
@ -207,7 +207,6 @@ let rec pp ?is_x fs term =
Trace.pp_styled (get_var_style var) "%%%s_%d" fs name id Trace.pp_styled (get_var_style var) "%%%s_%d" fs name id
| Nondet {msg} -> pf "nondet \"%s\"" msg | Nondet {msg} -> pf "nondet \"%s\"" msg
| Label {name} -> pf "%s" name | Label {name} -> pf "%s" name
| Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
| Splat {byt; siz} -> pf "%a^%a" pp byt pp siz | Splat {byt; siz} -> pf "%a^%a" pp byt pp siz
| Memory {siz; arr} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr | Memory {siz; arr} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
| Concat {args} -> pf "%a" (Vector.pp "@,^" pp) args | Concat {args} -> pf "%a" (Vector.pp "@,^" pp) args
@ -308,30 +307,6 @@ let pp = pp_t
(** Invariant *) (** Invariant *)
let rec typ_of = function
| Add {typ} | Mul {typ} | Integer {typ} | App {op= Convert {dst= typ}} ->
Some typ
| App {op= App {op= Eq | Dq | Gt | Ge | Lt | Le}} -> Some Typ.bool
| App
{ op= App {op= Div | Rem | And | Or | Xor | Shl | Lshr | Ashr; arg= x}
; arg= y } -> (
match typ_of x with Some _ as t -> t | None -> typ_of y )
| App {op= App {op= App {op= Conditional}; arg= thn}; arg= els} -> (
match typ_of thn with Some _ as t -> t | None -> typ_of els )
| _ -> None
let typ = typ_of
let is_boolean e = Option.exists ~f:(Typ.equal Typ.bool) (typ_of e)
let type_check e typ =
assert (
Option.for_all ~f:(Typ.castable typ) (typ_of e)
|| fail "%a@ : %a not <:@ %a" pp e Typ.pp
(Option.value_exn (typ_of e))
Typ.pp typ )
let type_check2 e f typ = type_check e typ ; type_check f typ
(* an indeterminate (factor of a monomial) is any non-Add/Mul/Integer term *) (* an indeterminate (factor of a monomial) is any non-Add/Mul/Integer term *)
let rec assert_indeterminate = function let rec assert_indeterminate = function
| App {op} -> assert_indeterminate op | App {op} -> assert_indeterminate op
@ -342,11 +317,9 @@ let rec assert_indeterminate = function
* ∏ᵢ xᵢ^nᵢ * ∏ᵢ xᵢ^nᵢ
* for (non-constant) indeterminants xᵢ and positive integer exponents nᵢ * for (non-constant) indeterminants xᵢ and positive integer exponents nᵢ
*) *)
let assert_monomial add_typ mono = let assert_monomial mono =
match mono with match mono with
| Mul {typ; args} -> | Mul {args} ->
assert (Typ.castable add_typ typ) ;
assert (Option.is_some (Typ.prim_bit_size_of typ)) ;
Qset.iter args ~f:(fun factor exponent -> Qset.iter args ~f:(fun factor exponent ->
assert (Q.sign exponent > 0) ; assert (Q.sign exponent > 0) ;
assert_indeterminate factor |> Fn.id ) assert_indeterminate factor |> Fn.id )
@ -355,7 +328,7 @@ let assert_monomial add_typ mono =
(* a polynomial term is a monomial multiplied by a non-zero coefficient (* a polynomial term is a monomial multiplied by a non-zero coefficient
* c × ∏ᵢ xᵢ * c × ∏ᵢ xᵢ
*) *)
let assert_poly_term add_typ mono coeff = let assert_poly_term mono coeff =
assert (not (Q.equal Q.zero coeff)) ; assert (not (Q.equal Q.zero coeff)) ;
match mono with match mono with
| Integer {data} -> assert (Z.equal Z.one data) | Integer {data} -> assert (Z.equal Z.one data)
@ -364,8 +337,8 @@ let assert_poly_term add_typ mono coeff =
| None | Some (Integer _, _) -> assert false | None | Some (Integer _, _) -> assert false
| Some (_, n) -> assert (Qset.length args > 1 || not (Q.equal Q.one n)) | Some (_, n) -> assert (Qset.length args > 1 || not (Q.equal Q.one n))
) ; ) ;
assert_monomial add_typ mono |> Fn.id assert_monomial mono |> Fn.id
| _ -> assert_monomial add_typ mono |> Fn.id | _ -> assert_monomial mono |> Fn.id
(* a polynomial is a linear combination of monomials, e.g. (* a polynomial is a linear combination of monomials, e.g.
* ∑ᵢ cᵢ × ∏ⱼ xᵢⱼ * ∑ᵢ cᵢ × ∏ⱼ xᵢⱼ
@ -374,13 +347,12 @@ let assert_poly_term add_typ mono coeff =
*) *)
let assert_polynomial poly = let assert_polynomial poly =
match poly with match poly with
| Add {typ; args} -> | Add {args} ->
( match Qset.min_elt args with ( match Qset.min_elt args with
| None -> assert false | None | Some (Integer _, _) -> assert false
| Some (Integer _, _) -> assert false
| Some (_, k) -> assert (Qset.length args > 1 || not (Q.equal Q.one k)) | Some (_, k) -> assert (Qset.length args > 1 || not (Q.equal Q.one k))
) ; ) ;
Qset.iter args ~f:(fun m c -> assert_poly_term typ m c |> Fn.id) Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fn.id)
| _ -> assert false | _ -> assert false
let invariant ?(partial = false) e = let invariant ?(partial = false) e =
@ -393,41 +365,23 @@ let invariant ?(partial = false) e =
in in
match op with match op with
| App _ -> fail "uncurry cannot return App" () | App _ -> fail "uncurry cannot return App" ()
| Integer {data; typ= (Integer _ | Pointer _) as typ} -> ( | Integer _ -> assert_arity 0
match Typ.prim_bit_size_of typ with
| None -> assert false
| Some bits ->
assert_arity 0 ;
assert (Z.numbits data <= bits) )
| Integer _ -> assert false
| Var _ | Nondet _ | Label _ | Float _ -> assert_arity 0 | Var _ | Nondet _ | Label _ | Float _ -> assert_arity 0
| Extract _ -> assert_arity 1 | Extract _ -> assert_arity 1
| Convert {dst; src} -> | Convert {dst; src} ->
( match args with assert_arity 1 ;
| [Integer {typ= Integer _ as typ}] -> assert (Typ.equal src typ)
| [arg] ->
assert (Option.for_all ~f:(Typ.convertible src) (typ_of arg))
| _ -> assert_arity 1 ) ;
assert (Typ.convertible src dst) assert (Typ.convertible src dst)
| Add _ -> assert_polynomial e |> Fn.id | Add _ -> assert_polynomial e |> Fn.id
| Mul {typ} -> assert_monomial typ e |> Fn.id | Mul _ -> assert_monomial e |> Fn.id
| Eq | Dq | Gt | Ge | Lt | Le | Div | Rem | And | Or | Xor | Shl | Lshr | Eq | Dq | Gt | Ge | Lt | Le | Div | Rem | And | Or | Xor | Shl | Lshr
|Ashr -> ( |Ashr ->
match args with assert_arity 2
| [x; y] -> (
match (typ_of x, typ_of y) with
| Some typ, Some typ' -> assert (Typ.castable typ typ')
| _ -> assert true )
| _ -> assert_arity 2 )
| Concat {args} -> assert (Vector.length args <> 1) | Concat {args} -> assert (Vector.length args <> 1)
| Splat {byt; siz} -> ( | Splat {siz} -> (
assert (Option.exists ~f:(Typ.convertible Typ.byt) (typ_of byt)) ;
assert (Option.exists ~f:(Typ.convertible Typ.siz) (typ_of siz)) ;
match siz with match siz with
| Integer {data} -> assert (not (Z.equal Z.zero data)) | Integer {data} -> assert (not (Z.equal Z.zero data))
| _ -> () ) | _ -> () )
| Memory {siz} -> | Memory _ -> assert true
assert (Option.for_all ~f:(Typ.convertible Typ.siz) (typ_of siz))
| Ord | Uno | Select -> assert_arity 2 | Ord | Uno | Select -> assert_arity 2
| Conditional | Update -> assert_arity 3 | Conditional | Update -> assert_arity 3
| Record -> assert (partial || not (List.is_empty args)) | Record -> assert (partial || not (List.is_empty args))
@ -581,24 +535,19 @@ let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
let var x = x let var x = x
let nondet msg = Nondet {msg} |> check invariant let nondet msg = Nondet {msg} |> check invariant
let label ~parent ~name = Label {parent; name} |> check invariant let label ~parent ~name = Label {parent; name} |> check invariant
let integer data typ = Integer {data; typ} |> check invariant let integer data = Integer {data} |> check invariant
let null = integer Z.zero Typ.ptr let null = integer Z.zero
let bool b = integer (Z.of_bool b) Typ.bool let zero = integer Z.zero
let one = integer Z.one
let minus_one = integer Z.minus_one
let bool b = integer (Z.of_bool b)
let true_ = bool true
let false_ = bool false
let float data = Float {data} |> check invariant let float data = Float {data} |> check invariant
let zero (typ : Typ.t) =
match typ with Float _ -> float "0" | _ -> integer Z.zero typ
let one (typ : Typ.t) =
match typ with Float _ -> float "1" | _ -> integer Z.one typ
let minus_one (typ : Typ.t) =
match typ with Float _ -> float "-1" | _ -> integer Z.minus_one typ
let simp_extract ~unsigned bits arg = let simp_extract ~unsigned bits arg =
match arg with match arg with
| Integer {data} -> | Integer {data} -> integer (Z.extract ~unsigned bits data)
integer (Z.extract ~unsigned bits data) (Typ.integer ~bits)
| _ -> App {op= Extract {unsigned; bits}; arg} | _ -> App {op= Extract {unsigned; bits}; arg}
let simp_convert ~unsigned dst src arg = let simp_convert ~unsigned dst src arg =
@ -606,7 +555,7 @@ let simp_convert ~unsigned dst src arg =
else else
match (dst, src, arg) with match (dst, src, arg) with
| Integer {bits= m}, Integer {bits= n}, Integer {data} -> | Integer {bits= m}, Integer {bits= n}, Integer {data} ->
integer (Z.extract ~unsigned (min m n) data) dst integer (Z.extract ~unsigned (min m n) data)
| _ -> App {op= Convert {unsigned; dst; src}; arg} | _ -> App {op= Convert {unsigned; dst; src}; arg}
let simp_gt x y = let simp_gt x y =
@ -637,37 +586,37 @@ let sum_mul_const const sum =
if Q.equal Q.one const then sum if Q.equal Q.one const then sum
else Qset.map_counts ~f:(fun _ -> Q.mul const) sum else Qset.map_counts ~f:(fun _ -> Q.mul const) sum
let rec sum_to_term typ sum = let rec sum_to_term sum =
match Qset.length sum with match Qset.length sum with
| 0 -> zero typ | 0 -> zero
| 1 -> ( | 1 -> (
match Qset.min_elt sum with match Qset.min_elt sum with
| Some (Integer _, q) -> rational q typ | Some (Integer _, q) -> rational q
| Some (arg, q) when Q.equal Q.one q -> arg | Some (arg, q) when Q.equal Q.one q -> arg
| _ -> Add {typ; args= sum} ) | _ -> Add {args= sum} )
| _ -> Add {typ; args= sum} | _ -> Add {args= sum}
and rational Q.{num; den} typ = simp_div (integer num typ) (integer den typ) and rational Q.{num; den} = simp_div (integer num) (integer den)
and simp_div x y = and simp_div x y =
match (x, y) with match (x, y) with
(* i / j *) (* i / j *)
| Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) -> | Integer {data= i}, Integer {data= j} when not (Z.equal Z.zero j) ->
integer (Z.div i j) typ integer (Z.div i j)
(* e / 1 ==> e *) (* e / 1 ==> e *)
| e, Integer {data} when Z.equal Z.one data -> e | e, Integer {data} when Z.equal Z.one data -> e
(* (∑ᵢ cᵢ × Xᵢ) / z ==> ∑ᵢ cᵢ/z × Xᵢ *) (* (∑ᵢ cᵢ × Xᵢ) / z ==> ∑ᵢ cᵢ/z × Xᵢ *)
| Add {typ; args}, Integer {data} -> | Add {args}, Integer {data} ->
sum_to_term typ (sum_mul_const Q.(inv (of_z data)) args) sum_to_term (sum_mul_const Q.(inv (of_z data)) args)
| _ -> App {op= App {op= Div; arg= x}; arg= y} | _ -> App {op= App {op= Div; arg= x}; arg= y}
let simp_rem x y = let simp_rem x y =
match (x, y) with match (x, y) with
(* i % j *) (* i % j *)
| Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) -> | Integer {data= i}, Integer {data= j} when not (Z.equal Z.zero j) ->
integer (Z.rem i j) typ integer (Z.rem i j)
(* e % 1 ==> 0 *) (* e % 1 ==> 0 *)
| _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ | _, Integer {data} when Z.equal Z.one data -> zero
| _ -> App {op= App {op= Rem; arg= x}; arg= y} | _ -> App {op= App {op= Rem; arg= x}; arg= y}
(* Sums of polynomial terms represented by multisets. A sum ∑ᵢ cᵢ × Xᵢ of (* Sums of polynomial terms represented by multisets. A sum ∑ᵢ cᵢ × Xᵢ of
@ -681,8 +630,7 @@ module Sum = struct
assert (not (Q.equal Q.zero coeff)) ; assert (not (Q.equal Q.zero coeff)) ;
match term with match term with
| Integer {data} when Z.equal Z.zero data -> sum | Integer {data} when Z.equal Z.zero data -> sum
| Integer {data; typ} -> | Integer {data} -> Qset.add sum one Q.(coeff * of_z data)
Qset.add sum (integer Z.one typ) Q.(coeff * of_z data)
| _ -> Qset.add sum term coeff | _ -> Qset.add sum term coeff
let singleton ?(coeff = Q.one) term = add coeff term empty let singleton ?(coeff = Q.one) term = add coeff term empty
@ -694,7 +642,7 @@ module Sum = struct
let to_term = sum_to_term let to_term = sum_to_term
end end
let rec simp_add_ typ es poly = let rec simp_add_ es poly =
(* (coeff × term) + poly *) (* (coeff × term) + poly *)
let f term coeff poly = let f term coeff poly =
match (term, poly) with match (term, poly) with
@ -704,18 +652,18 @@ let rec simp_add_ typ es poly =
| Integer {data}, _ when Z.equal Z.zero data -> poly | Integer {data}, _ when Z.equal Z.zero data -> poly
(* (c × cᵢ) + cⱼ ==> c×cᵢ+cⱼ *) (* (c × cᵢ) + cⱼ ==> c×cᵢ+cⱼ *)
| Integer {data= i}, Integer {data= j} -> | Integer {data= i}, Integer {data= j} ->
rational Q.((coeff * of_z i) + of_z j) typ rational Q.((coeff * of_z i) + of_z j)
(* (c × ∑ᵢ cᵢ × Xᵢ) + s ==> (∑ᵢ (c × cᵢ) × Xᵢ) + s *) (* (c × ∑ᵢ cᵢ × Xᵢ) + s ==> (∑ᵢ (c × cᵢ) × Xᵢ) + s *)
| Add {args}, _ -> simp_add_ typ (Sum.mul_const coeff args) poly | Add {args}, _ -> simp_add_ (Sum.mul_const coeff args) poly
(* (c₀ × X₀) + (∑ᵢ₌₁ⁿ cᵢ × Xᵢ) ==> ∑ᵢ₌₀ⁿ cᵢ × Xᵢ *) (* (c₀ × X₀) + (∑ᵢ₌₁ⁿ cᵢ × Xᵢ) ==> ∑ᵢ₌₀ⁿ cᵢ × Xᵢ *)
| _, Add {args} -> Sum.to_term typ (Sum.add coeff term args) | _, Add {args} -> Sum.to_term (Sum.add coeff term args)
(* (c₁ × X₁) + X₂ ==> ∑ᵢ₌₁² cᵢ × Xᵢ for c₂ = 1 *) (* (c₁ × X₁) + X₂ ==> ∑ᵢ₌₁² cᵢ × Xᵢ for c₂ = 1 *)
| _ -> Sum.to_term typ (Sum.add coeff term (Sum.singleton poly)) | _ -> Sum.to_term (Sum.add coeff term (Sum.singleton poly))
in in
Qset.fold ~f es ~init:poly Qset.fold ~f es ~init:poly
let simp_add typ es = simp_add_ typ es (zero typ) let simp_add es = simp_add_ es zero
let simp_add2 typ e f = simp_add_ typ (Sum.singleton e) f let simp_add2 e f = simp_add_ (Sum.singleton e) f
(* Products of indeterminants represented by multisets. A product ∏ᵢ xᵢ^nᵢ (* Products of indeterminants represented by multisets. A product ∏ᵢ xᵢ^nᵢ
of indeterminates xᵢ is represented by a multiset where the elements are of indeterminates xᵢ is represented by a multiset where the elements are
@ -731,58 +679,56 @@ module Prod = struct
let union = Qset.union let union = Qset.union
end end
let rec simp_mul2 typ e f = let rec simp_mul2 e f =
match (e, f) with match (e, f) with
(* c₁ × c₂ ==> c₁×c₂ *) (* c₁ × c₂ ==> c₁×c₂ *)
| Integer {data= i}, Integer {data= j} -> integer (Z.mul i j) typ | Integer {data= i}, Integer {data= j} -> integer (Z.mul i j)
(* 0 × f ==> 0 *) (* 0 × f ==> 0 *)
| Integer {data}, _ when Z.equal Z.zero data -> e | Integer {data}, _ when Z.equal Z.zero data -> e
(* e × 0 ==> 0 *) (* e × 0 ==> 0 *)
| _, Integer {data} when Z.equal Z.zero data -> f | _, Integer {data} when Z.equal Z.zero data -> f
(* c × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ c × cᵤ × ∏ⱼ yᵤⱼ *) (* c × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ c × cᵤ × ∏ⱼ yᵤⱼ *)
| Integer {data}, Add {args} | Add {args}, Integer {data} -> | Integer {data}, Add {args} | Add {args}, Integer {data} ->
Sum.to_term typ (Sum.mul_const (Q.of_z data) args) Sum.to_term (Sum.mul_const (Q.of_z data) args)
(* c₁ × x₁ ==> ∑ᵢ₌₁ cᵢ × xᵢ *) (* c₁ × x₁ ==> ∑ᵢ₌₁ cᵢ × xᵢ *)
| Integer {data= c}, x | x, Integer {data= c} -> | Integer {data= c}, x | x, Integer {data= c} ->
Sum.to_term typ (Sum.singleton ~coeff:(Q.of_z c) x) Sum.to_term (Sum.singleton ~coeff:(Q.of_z c) x)
(* (∏ᵤ₌₀ⁱ xᵤ) × (∏ᵥ₌ᵢ₊₁ⁿ xᵥ) ==> ∏ⱼ₌₀ⁿ xⱼ *) (* (∏ᵤ₌₀ⁱ xᵤ) × (∏ᵥ₌ᵢ₊₁ⁿ xᵥ) ==> ∏ⱼ₌₀ⁿ xⱼ *)
| Mul {args= xs1}, Mul {args= xs2} -> Mul {typ; args= Prod.union xs1 xs2} | Mul {args= xs1}, Mul {args= xs2} -> Mul {args= Prod.union xs1 xs2}
(* (∏ᵢ xᵢ) × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ cᵤ × ∏ᵢ xᵢ × ∏ⱼ yᵤⱼ *) (* (∏ᵢ xᵢ) × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ cᵤ × ∏ᵢ xᵢ × ∏ⱼ yᵤⱼ *)
| (Mul {args= prod} as m), Add {args= sum} | (Mul {args= prod} as m), Add {args= sum}
|Add {args= sum}, (Mul {args= prod} as m) -> |Add {args= sum}, (Mul {args= prod} as m) ->
Sum.to_term typ Sum.to_term
(Sum.map sum ~f:(function (Sum.map sum ~f:(function
| Mul {args} -> Mul {typ; args= Prod.union prod args} | Mul {args} -> Mul {args= Prod.union prod args}
| Integer _ as c -> simp_mul2 typ c m | Integer _ as c -> simp_mul2 c m
| mono -> Mul {typ; args= Prod.add mono prod} )) | mono -> Mul {args= Prod.add mono prod} ))
(* x₀ × (∏ᵢ₌₁ⁿ xᵢ) ==> ∏ᵢ₌₀ⁿ xᵢ *) (* x₀ × (∏ᵢ₌₁ⁿ xᵢ) ==> ∏ᵢ₌₀ⁿ xᵢ *)
| Mul {args= xs1}, x | x, Mul {args= xs1} -> | Mul {args= xs1}, x | x, Mul {args= xs1} -> Mul {args= Prod.add x xs1}
Mul {typ; args= Prod.add x xs1}
(* e × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ e × cᵤ × ∏ⱼ yᵤⱼ *) (* e × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ e × cᵤ × ∏ⱼ yᵤⱼ *)
| Add {args}, e | e, Add {args} -> | Add {args}, e | e, Add {args} ->
simp_add typ (Sum.map ~f:(fun m -> simp_mul2 typ e m) args) simp_add (Sum.map ~f:(fun m -> simp_mul2 e m) args)
(* x₁ × x₂ ==> ∏ᵢ₌₁² xᵢ *) (* x₁ × x₂ ==> ∏ᵢ₌₁² xᵢ *)
| _ -> Mul {args= Prod.add e (Prod.singleton f); typ} | _ -> Mul {args= Prod.add e (Prod.singleton f)}
let simp_mul typ es = let simp_mul es =
(* (bas ^ pwr) × term *) (* (bas ^ pwr) × term *)
let rec mul_pwr bas pwr term = let rec mul_pwr bas pwr term =
if Q.equal Q.zero pwr then term if Q.equal Q.zero pwr then term
else mul_pwr bas Q.(pwr - one) (simp_mul2 typ bas term) else mul_pwr bas Q.(pwr - one) (simp_mul2 bas term)
in in
let one = one typ in
Qset.fold es ~init:one ~f:(fun bas pwr term -> Qset.fold es ~init:one ~f:(fun bas pwr term ->
if Q.sign pwr >= 0 then mul_pwr bas pwr term if Q.sign pwr >= 0 then mul_pwr bas pwr term
else simp_div term (mul_pwr bas (Q.neg pwr) one) ) else simp_div term (mul_pwr bas (Q.neg pwr) one) )
let simp_negate typ x = simp_mul2 typ (minus_one typ) x let simp_negate x = simp_mul2 minus_one x
let simp_sub typ x y = let simp_sub x y =
match (x, y) with match (x, y) with
(* i - j *) (* i - j *)
| Integer {data= i}, Integer {data= j} -> integer (Z.sub i j) typ | Integer {data= i}, Integer {data= j} -> integer (Z.sub i j)
(* x - y ==> x + (-1 * y) *) (* x - y ==> x + (-1 * y) *)
| _ -> simp_add2 typ x (simp_negate typ y) | _ -> simp_add2 x (simp_negate y)
let simp_cond cnd thn els = let simp_cond cnd thn els =
match cnd with match cnd with
@ -796,7 +742,7 @@ let simp_cond cnd thn els =
let rec simp_and x y = let rec simp_and x y =
match (x, y) with match (x, y) with
(* i && j *) (* i && j *)
| Integer {data= i; typ}, Integer {data= j} -> integer (Z.logand i j) typ | Integer {data= i}, Integer {data= j} -> integer (Z.logand i j)
(* e && true ==> e *) (* e && true ==> e *)
| (Integer {data}, e | e, Integer {data}) when Z.is_true data -> e | (Integer {data}, e | e, Integer {data}) when Z.is_true data -> e
(* e && false ==> 0 *) (* e && false ==> 0 *)
@ -814,7 +760,7 @@ let rec simp_and x y =
let rec simp_or x y = let rec simp_or x y =
match (x, y) with match (x, y) with
(* i || j *) (* i || j *)
| Integer {data= i; typ}, Integer {data= j} -> integer (Z.logor i j) typ | Integer {data= i}, Integer {data= j} -> integer (Z.logor i j)
(* e || true ==> true *) (* e || true ==> true *)
| ((Integer {data} as t), _ | _, (Integer {data} as t)) | ((Integer {data} as t), _ | _, (Integer {data} as t))
when Z.is_true data -> when Z.is_true data ->
@ -829,7 +775,18 @@ let rec simp_or x y =
| _ when equal x y -> x | _ when equal x y -> x
| _ -> App {op= App {op= Or; arg= x}; arg= y} | _ -> App {op= App {op= Or; arg= x}; arg= y}
let rec simp_not (typ : Typ.t) term = let rec is_boolean = function
| App {op= App {op= Eq | Dq | Gt | Ge | Lt | Le}}
|App {op= Convert {dst= Integer {bits= 1}}} ->
true
| App
{ op= App {op= Div | Rem | And | Or | Xor | Shl | Lshr | Ashr; arg= x}
; arg= y }
|App {op= App {op= App {op= Conditional}; arg= x}; arg= y} ->
is_boolean x || is_boolean y
| _ -> false
let rec simp_not term =
match term with match term with
(* ¬(x = y) ==> x ≠ y *) (* ¬(x = y) ==> x ≠ y *)
| App {op= App {op= Eq; arg= x}; arg= y} -> simp_dq x y | App {op= App {op= Eq; arg= x}; arg= y} -> simp_dq x y
@ -849,28 +806,26 @@ let rec simp_not (typ : Typ.t) term =
| App {op= App {op= Uno; arg= x}; arg= y} -> simp_ord x y | App {op= App {op= Uno; arg= x}; arg= y} -> simp_ord x y
(* ¬(a ∧ b) ==> ¬a ∨ ¬b *) (* ¬(a ∧ b) ==> ¬a ∨ ¬b *)
| App {op= App {op= And; arg= x}; arg= y} -> | App {op= App {op= And; arg= x}; arg= y} ->
simp_or (simp_not typ x) (simp_not typ y) simp_or (simp_not x) (simp_not y)
(* ¬(a ∨ b) ==> ¬a ∧ ¬b *) (* ¬(a ∨ b) ==> ¬a ∧ ¬b *)
| App {op= App {op= Or; arg= x}; arg= y} -> | App {op= App {op= Or; arg= x}; arg= y} ->
simp_and (simp_not typ x) (simp_not typ y) simp_and (simp_not x) (simp_not y)
(* ¬(c ? t : e) ==> c ? ¬t : ¬e *) (* ¬(c ? t : e) ==> c ? ¬t : ¬e *)
| App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els} | App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}
-> ->
simp_cond cnd (simp_not typ thn) (simp_not typ els) simp_cond cnd (simp_not thn) (simp_not els)
(* ¬i ==> -i-1 *) (* ¬i ==> -i-1 *)
| Integer {data; typ} -> integer (Z.lognot data) typ | Integer {data} -> integer (Z.lognot data)
(* ¬e ==> true xor e *) (* ¬e ==> true xor e *)
| e -> App {op= App {op= Xor; arg= integer (Z.of_bool true) typ}; arg= e} | e -> App {op= App {op= Xor; arg= true_}; arg= e}
and simp_eq x y = and simp_eq x y =
match (x, y) with match (x, y) with
(* i = j *) (* i = j *)
| Integer {data= i}, Integer {data= j} -> bool (Z.equal i j) | Integer {data= i}, Integer {data= j} -> bool (Z.equal i j)
(* b = false ==> ¬b *) (* b = false ==> ¬b *)
| b, Integer {data} when Z.is_false data && is_boolean b -> | b, Integer {data} when Z.is_false data && is_boolean b -> simp_not b
simp_not Typ.bool b | Integer {data}, b when Z.is_false data && is_boolean b -> simp_not b
| Integer {data}, b when Z.is_false data && is_boolean b ->
simp_not Typ.bool b
(* b = true ==> b *) (* b = true ==> b *)
| b, Integer {data} when Z.is_true data && is_boolean b -> b | b, Integer {data} when Z.is_true data && is_boolean b -> b
| Integer {data}, b when Z.is_true data && is_boolean b -> b | Integer {data}, b when Z.is_true data && is_boolean b -> b
@ -892,24 +847,22 @@ and simp_dq x y =
match simp_eq x y with match simp_eq x y with
| App {op= App {op= Eq; arg= x}; arg= y} -> | App {op= App {op= Eq; arg= x}; arg= y} ->
App {op= App {op= Dq; arg= x}; arg= y} App {op= App {op= Dq; arg= x}; arg= y}
| b -> simp_not Typ.bool b ) | b -> simp_not b )
let simp_xor x y = let simp_xor x y =
match (x, y) with match (x, y) with
(* i xor j *) (* i xor j *)
| Integer {data= i; typ}, Integer {data= j} -> integer (Z.logxor i j) typ | Integer {data= i}, Integer {data= j} -> integer (Z.logxor i j)
(* true xor b ==> ¬b *) (* true xor b ==> ¬b *)
| Integer {data}, b when Z.is_true data && is_boolean b -> | Integer {data}, b when Z.is_true data && is_boolean b -> simp_not b
simp_not Typ.bool b | b, Integer {data} when Z.is_true data && is_boolean b -> simp_not b
| b, Integer {data} when Z.is_true data && is_boolean b ->
simp_not Typ.bool b
| _ -> App {op= App {op= Xor; arg= x}; arg= y} | _ -> App {op= App {op= Xor; arg= x}; arg= y}
let simp_shl x y = let simp_shl x y =
match (x, y) with match (x, y) with
(* i shl j *) (* i shl j *)
| Integer {data= i; typ}, Integer {data= j} when Z.sign j >= 0 -> | Integer {data= i}, Integer {data= j} when Z.sign j >= 0 ->
integer (Z.shift_left i (Z.to_int j)) typ integer (Z.shift_left i (Z.to_int j))
(* e shl 0 ==> e *) (* e shl 0 ==> e *)
| e, Integer {data} when Z.equal Z.zero data -> e | e, Integer {data} when Z.equal Z.zero data -> e
| _ -> App {op= App {op= Shl; arg= x}; arg= y} | _ -> App {op= App {op= Shl; arg= x}; arg= y}
@ -917,8 +870,8 @@ let simp_shl x y =
let simp_lshr x y = let simp_lshr x y =
match (x, y) with match (x, y) with
(* i lshr j *) (* i lshr j *)
| Integer {data= i; typ}, Integer {data= j} when Z.sign j >= 0 -> | Integer {data= i}, Integer {data= j} when Z.sign j >= 0 ->
integer (Z.shift_right_trunc i (Z.to_int j)) typ integer (Z.shift_right_trunc i (Z.to_int j))
(* e lshr 0 ==> e *) (* e lshr 0 ==> e *)
| e, Integer {data} when Z.equal Z.zero data -> e | e, Integer {data} when Z.equal Z.zero data -> e
| _ -> App {op= App {op= Lshr; arg= x}; arg= y} | _ -> App {op= App {op= Lshr; arg= x}; arg= y}
@ -926,8 +879,8 @@ let simp_lshr x y =
let simp_ashr x y = let simp_ashr x y =
match (x, y) with match (x, y) with
(* i ashr j *) (* i ashr j *)
| Integer {data= i; typ}, Integer {data= j} when Z.sign j >= 0 -> | Integer {data= i}, Integer {data= j} when Z.sign j >= 0 ->
integer (Z.shift_right i (Z.to_int j)) typ integer (Z.shift_right i (Z.to_int j))
(* e ashr 0 ==> e *) (* e ashr 0 ==> e *)
| e, Integer {data} when Z.equal Z.zero data -> e | e, Integer {data} when Z.equal Z.zero data -> e
| _ -> App {op= App {op= Ashr; arg= x}; arg= y} | _ -> App {op= App {op= Ashr; arg= x}; arg= y}
@ -1005,22 +958,10 @@ let app1 ?(partial = false) op arg =
let app2 op x y = app1 (app1 ~partial:true op x) y let app2 op x y = app1 (app1 ~partial:true op x) y
let app3 op x y z = app1 (app1 ~partial:true (app1 ~partial:true op x) y) z let app3 op x y z = app1 (app1 ~partial:true (app1 ~partial:true op x) y) z
let addN typ args = simp_add typ args |> check invariant let addN args = simp_add args |> check invariant
let mulN typ args = simp_mul typ args |> check invariant let mulN args = simp_mul args |> check invariant
let check1 op typ x =
type_check x typ ;
op typ x |> check invariant
let check2 op typ x y =
type_check2 x y typ ;
op typ x y |> check invariant
let simp_memory siz arr = Memory {siz; arr} let simp_memory siz arr = Memory {siz; arr}
let memory ~siz ~arr = simp_memory siz arr |> check invariant
let memory ~siz ~arr =
type_check siz Typ.siz ;
simp_memory siz arr |> check invariant
let simp_concat xs = let simp_concat xs =
if Vector.length xs = 1 then Vector.get xs 0 if Vector.length xs = 1 then Vector.get xs 0
@ -1044,11 +985,7 @@ let simp_splat byt siz =
| Integer {data} when Z.equal Z.zero data -> concat [||] | Integer {data} when Z.equal Z.zero data -> concat [||]
| _ -> Splat {byt; siz} | _ -> Splat {byt; siz}
let splat ~byt ~siz = let splat ~byt ~siz = simp_splat byt siz |> check invariant
type_check byt Typ.byt ;
type_check siz Typ.siz ;
simp_splat byt siz |> check invariant
let eq = app2 Eq let eq = app2 Eq
let dq = app2 Dq let dq = app2 Dq
let gt = app2 Gt let gt = app2 Gt
@ -1057,16 +994,16 @@ let lt = app2 Lt
let le = app2 Le let le = app2 Le
let ord = app2 Ord let ord = app2 Ord
let uno = app2 Uno let uno = app2 Uno
let neg = check1 simp_negate let neg = simp_negate
let add = check2 simp_add2 let add = simp_add2
let sub = check2 simp_sub let sub = simp_sub
let mul = check2 simp_mul2 let mul = simp_mul2
let div = app2 Div let div = app2 Div
let rem = app2 Rem let rem = app2 Rem
let and_ = app2 And let and_ = app2 And
let or_ = app2 Or let or_ = app2 Or
let xor = app2 Xor let xor = app2 Xor
let not_ = check1 simp_not let not_ = simp_not
let shl = app2 Shl let shl = app2 Shl
let lshr = app2 Lshr let lshr = app2 Lshr
let ashr = app2 Ashr let ashr = app2 Ashr
@ -1103,6 +1040,10 @@ let extract ?(unsigned = false) ~bits term =
let convert ?(unsigned = false) ~dst ~src term = let convert ?(unsigned = false) ~dst ~src term =
app1 (Convert {unsigned; dst; src}) term app1 (Convert {unsigned; dst; src}) term
let size_of t =
Option.bind (Typ.prim_bit_size_of t) ~f:(fun n ->
if n % 8 = 0 then Some (integer (Z.of_int (n / 8))) else None )
let rec of_exp (e : Exp.t) = let rec of_exp (e : Exp.t) =
let unsigned op typ x y = let unsigned op typ x y =
match Typ.prim_bit_size_of typ with match Typ.prim_bit_size_of typ with
@ -1116,14 +1057,12 @@ let rec of_exp (e : Exp.t) =
| Reg {name} -> var (Var {id= 0; name}) | Reg {name} -> var (Var {id= 0; name})
| Nondet {msg} -> nondet msg | Nondet {msg} -> nondet msg
| Label {parent; name} -> label ~parent ~name | Label {parent; name} -> label ~parent ~name
| Integer {data; typ= Integer {bits} as typ} -> | Integer {data} -> integer data
integer (Z.signed_extract data 0 bits) typ
| Integer {data; typ} -> integer data typ
| Float {data} -> float data | Float {data} -> float data
| Ap1 (Convert {unsigned; dst}, src, arg) -> | Ap1 (Convert {unsigned; dst}, src, arg) ->
convert ~unsigned ~dst ~src (of_exp arg) convert ~unsigned ~dst ~src (of_exp arg)
| Ap1 (Select idx, _, arg) -> | Ap1 (Select idx, _, arg) ->
select ~rcd:(of_exp arg) ~idx:(integer (Z.of_int idx) Typ.siz) select ~rcd:(of_exp arg) ~idx:(integer (Z.of_int idx))
| Ap2 (Eq, _, x, y) -> eq (of_exp x) (of_exp y) | Ap2 (Eq, _, x, y) -> eq (of_exp x) (of_exp y)
| Ap2 (Dq, _, x, y) -> dq (of_exp x) (of_exp y) | Ap2 (Dq, _, x, y) -> dq (of_exp x) (of_exp y)
| Ap2 (Gt, _, x, y) -> gt (of_exp x) (of_exp y) | Ap2 (Gt, _, x, y) -> gt (of_exp x) (of_exp y)
@ -1136,9 +1075,9 @@ let rec of_exp (e : Exp.t) =
| Ap2 (Ule, typ, x, y) -> unsigned le typ x y | Ap2 (Ule, typ, x, y) -> unsigned le typ x y
| Ap2 (Ord, _, x, y) -> ord (of_exp x) (of_exp y) | Ap2 (Ord, _, x, y) -> ord (of_exp x) (of_exp y)
| Ap2 (Uno, _, x, y) -> uno (of_exp x) (of_exp y) | Ap2 (Uno, _, x, y) -> uno (of_exp x) (of_exp y)
| Ap2 (Add, typ, x, y) -> add typ (of_exp x) (of_exp y) | Ap2 (Add, _, x, y) -> add (of_exp x) (of_exp y)
| Ap2 (Sub, typ, x, y) -> sub typ (of_exp x) (of_exp y) | Ap2 (Sub, _, x, y) -> sub (of_exp x) (of_exp y)
| Ap2 (Mul, typ, x, y) -> mul typ (of_exp x) (of_exp y) | Ap2 (Mul, _, x, y) -> mul (of_exp x) (of_exp y)
| Ap2 (Div, _, x, y) -> div (of_exp x) (of_exp y) | Ap2 (Div, _, x, y) -> div (of_exp x) (of_exp y)
| Ap2 (Rem, _, x, y) -> rem (of_exp x) (of_exp y) | Ap2 (Rem, _, x, y) -> rem (of_exp x) (of_exp y)
| Ap2 (Udiv, typ, x, y) -> unsigned div typ x y | Ap2 (Udiv, typ, x, y) -> unsigned div typ x y
@ -1151,7 +1090,7 @@ let rec of_exp (e : Exp.t) =
| Ap2 (Ashr, _, x, y) -> ashr (of_exp x) (of_exp y) | Ap2 (Ashr, _, x, y) -> ashr (of_exp x) (of_exp y)
| Ap2 (Update idx, _, rcd, elt) -> | Ap2 (Update idx, _, rcd, elt) ->
update ~rcd:(of_exp rcd) ~elt:(of_exp elt) update ~rcd:(of_exp rcd) ~elt:(of_exp elt)
~idx:(integer (Z.of_int idx) Typ.siz) ~idx:(integer (Z.of_int idx))
| Ap3 (Conditional, _, cnd, thn, els) -> | Ap3 (Conditional, _, cnd, thn, els) ->
conditional ~cnd:(of_exp cnd) ~thn:(of_exp thn) ~els:(of_exp els) conditional ~cnd:(of_exp cnd) ~thn:(of_exp thn) ~els:(of_exp els)
| ApN (Record, _, elts) -> | ApN (Record, _, elts) ->
@ -1162,11 +1101,6 @@ let rec of_exp (e : Exp.t) =
~id:e ~id:e
(Vector.map elts ~f:(fun e -> lazy (of_exp e))) (Vector.map elts ~f:(fun e -> lazy (of_exp e)))
let size_of t =
Option.bind (Typ.prim_bit_size_of t) ~f:(fun n ->
if n % 8 = 0 then Some (integer (Z.of_int (n / 8)) Typ.siz) else None
)
(** Transform *) (** Transform *)
let map e ~f = let map e ~f =
@ -1181,14 +1115,14 @@ let map e ~f =
let args' = Vector.map_preserving_phys_equal ~f args in let args' = Vector.map_preserving_phys_equal ~f args in
if args' == args then e else mk args' if args' == args then e else mk args'
in in
let map_qset mk typ ~f args = let map_qset mk ~f args =
let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in
if args' == args then e else mk typ args' if args' == args then e else mk args'
in in
match e with match e with
| App {op; arg} -> map_bin (app1 ~partial:true) ~f op arg | App {op; arg} -> map_bin (app1 ~partial:true) ~f op arg
| Add {args; typ} -> map_qset addN typ ~f args | Add {args} -> map_qset addN ~f args
| Mul {args; typ} -> map_qset mulN typ ~f args | Mul {args} -> map_qset mulN ~f args
| Splat {byt; siz} -> map_bin simp_splat ~f byt siz | Splat {byt; siz} -> map_bin simp_splat ~f byt siz
| Memory {siz; arr} -> map_bin simp_memory ~f siz arr | Memory {siz; arr} -> map_bin simp_memory ~f siz arr
| Concat {args} -> map_vector simp_concat ~f args | Concat {args} -> map_vector simp_concat ~f args
@ -1246,23 +1180,21 @@ let solve e f =
Some (Map.add_exn s ~key ~data) Some (Map.add_exn s ~key ~data)
in in
let concat_size args = let concat_size args =
Vector.fold_until args ~init:(integer Z.zero Typ.siz) Vector.fold_until args ~init:zero
~f:(fun sum -> function ~f:(fun sum -> function Memory {siz} -> Continue (add siz sum)
| Memory {siz} -> Continue (add Typ.siz siz sum) | _ -> Stop None | _ -> Stop None )
)
~finish:(fun _ -> None) ~finish:(fun _ -> None)
in in
match (e, f) with match (e, f) with
| (Add {typ} | Mul {typ} | Integer {typ}), _ | (Add _ | Mul _ | Integer _), _ | _, (Add _ | Mul _ | Integer _) -> (
|_, (Add {typ} | Mul {typ} | Integer {typ}) -> ( match sub e f with
match sub typ e f with
| Add {args} -> | Add {args} ->
let c, q = Qset.min_elt_exn args in let c, q = Qset.min_elt_exn args in
let n = Sum.to_term typ (Qset.remove args c) in let n = Sum.to_term (Qset.remove args c) in
let d = rational (Q.neg q) typ in let d = rational (Q.neg q) in
let r = div n d in let r = div n d in
Some (Map.add_exn s ~key:c ~data:r) Some (Map.add_exn s ~key:c ~data:r)
| e_f -> solve_uninterp e_f (zero typ) ) | e_f -> solve_uninterp e_f zero )
| Concat {args= ms}, Concat {args= ns} -> ( | Concat {args= ms}, Concat {args= ns} -> (
match (concat_size ms, concat_size ns) with match (concat_size ms, concat_size ns) with
| Some p, Some q -> solve_uninterp e f >>= solve_ p q | Some p, Some q -> solve_uninterp e f >>= solve_ p q

28
sledge/src/symbheap/term.mli
Unescape View File

@ -21,8 +21,8 @@ type comparator_witness
type qset = (t, comparator_witness) Qset.t type qset = (t, comparator_witness) Qset.t
and t = private and t = private
| Add of {args: qset; typ: Typ.t} (** Addition *) | Add of {args: qset} (** Addition *)
| Mul of {args: qset; typ: Typ.t} (** Multiplication *) | Mul of {args: qset} (** Multiplication *)
| Splat of {byt: t; siz: t} | Splat of {byt: t; siz: t}
(** Iterated concatenation of a single byte *) (** Iterated concatenation of a single byte *)
| Memory of {siz: t; arr: t} (** Size-tagged byte-array *) | Memory of {siz: t; arr: t} (** Size-tagged byte-array *)
@ -67,7 +67,7 @@ and t = private
integer. If [src] is a [Float] type and [dst] is an [Integer] integer. If [src] is a [Float] type and [dst] is an [Integer]
type, then [unsigned] indidates that the result should be the type, then [unsigned] indidates that the result should be the
nearest non-negative value. *) nearest non-negative value. *)
| Integer of {data: Z.t; typ: Typ.t} | Integer of {data: Z.t}
(** Integer constant, or if [typ] is a [Pointer], null pointer value (** Integer constant, or if [typ] is a [Pointer], null pointer value
that never refers to an object *) that never refers to an object *)
| Float of {data: string} (** Floating-point constant *) | Float of {data: string} (** Floating-point constant *)
@ -127,17 +127,21 @@ end
(** Construct *) (** Construct *)
val of_exp : Exp.t -> t
val var : Var.t -> t val var : Var.t -> t
val nondet : string -> t val nondet : string -> t
val label : parent:string -> name:string -> t val label : parent:string -> name:string -> t
val true_ : t
val false_ : t
val null : t val null : t
val zero : t
val one : t
val minus_one : t
val splat : byt:t -> siz:t -> t val splat : byt:t -> siz:t -> t
val memory : siz:t -> arr:t -> t val memory : siz:t -> arr:t -> t
val concat : t array -> t val concat : t array -> t
val bool : bool -> t val bool : bool -> t
val integer : Z.t -> Typ.t -> t val integer : Z.t -> t
val rational : Q.t -> Typ.t -> t val rational : Q.t -> t
val float : string -> t val float : string -> t
val eq : t -> t -> t val eq : t -> t -> t
val dq : t -> t -> t val dq : t -> t -> t
@ -147,16 +151,16 @@ val lt : t -> t -> t
val le : t -> t -> t val le : t -> t -> t
val ord : t -> t -> t val ord : t -> t -> t
val uno : t -> t -> t val uno : t -> t -> t
val neg : Typ.t -> t -> t val neg : t -> t
val add : Typ.t -> t -> t -> t val add : t -> t -> t
val sub : Typ.t -> t -> t -> t val sub : t -> t -> t
val mul : Typ.t -> t -> t -> t val mul : t -> t -> t
val div : t -> t -> t val div : t -> t -> t
val rem : t -> t -> t val rem : t -> t -> t
val and_ : t -> t -> t val and_ : t -> t -> t
val or_ : t -> t -> t val or_ : t -> t -> t
val xor : t -> t -> t val xor : t -> t -> t
val not_ : Typ.t -> t -> t val not_ : t -> t
val shl : t -> t -> t val shl : t -> t -> t
val lshr : t -> t -> t val lshr : t -> t -> t
val ashr : t -> t -> t val ashr : t -> t -> t
@ -167,6 +171,7 @@ val update : rcd:t -> elt:t -> idx:t -> t
val extract : ?unsigned:bool -> bits:int -> t -> t val extract : ?unsigned:bool -> bits:int -> t -> t
val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t
val size_of : Typ.t -> t option val size_of : Typ.t -> t option
val of_exp : Exp.t -> t
(** Access *) (** Access *)
@ -185,6 +190,5 @@ val rename : Var.Subst.t -> t -> t
val fv : t -> Var.Set.t val fv : t -> Var.Set.t
val is_true : t -> bool val is_true : t -> bool
val is_false : t -> bool val is_false : t -> bool
val typ : t -> Typ.t option
val classify : t -> [> `Atomic | `Interpreted | `Simplified | `Uninterpreted] val classify : t -> [> `Atomic | `Interpreted | `Simplified | `Uninterpreted]
val solve : t -> t -> (t, t, comparator_witness) Map.t option val solve : t -> t -> (t, t, comparator_witness) Map.t option

41
sledge/src/symbheap/term_test.ml
Unescape View File

@ -10,11 +10,10 @@ let%test_module _ =
(* let () = Trace.init ~margin:68 ~config:all () *) (* let () = Trace.init ~margin:68 ~config:all () *)
let () = Trace.init ~margin:68 ~config:none () let () = Trace.init ~margin:68 ~config:none ()
let pp = Format.printf "@\n%a@." Term.pp let pp = Format.printf "@\n%a@." Term.pp
let char = Typ.integer ~bits:8 let ( ! ) i = Term.integer (Z.of_int i)
let ( ! ) i = Term.integer (Z.of_int i) char let ( + ) = Term.add
let ( + ) = Term.add char let ( - ) = Term.sub
let ( - ) = Term.sub char let ( * ) = Term.mul
let ( * ) = Term.mul char
let ( = ) = Term.eq let ( = ) = Term.eq
let ( != ) = Term.dq let ( != ) = Term.dq
let ( > ) = Term.gt let ( > ) = Term.gt
@ -23,7 +22,7 @@ let%test_module _ =
let ( <= ) = Term.le let ( <= ) = Term.le
let ( && ) = Term.and_ let ( && ) = Term.and_
let ( || ) = Term.or_ let ( || ) = Term.or_
let ( ~~ ) = Term.not_ Typ.bool let ( ~~ ) = Term.not_
let wrt = Var.Set.empty let wrt = Var.Set.empty
let y_, wrt = Var.fresh "y" ~wrt let y_, wrt = Var.fresh "y" ~wrt
let z_, _ = Var.fresh "z" ~wrt let z_, _ = Var.fresh "z" ~wrt
@ -31,16 +30,10 @@ let%test_module _ =
let z = Term.var z_ let z = Term.var z_
let%test "booleans distinct" = let%test "booleans distinct" =
Term.is_false Term.is_false (Term.eq Term.minus_one Term.zero)
(Term.eq
(Term.integer Z.minus_one Typ.bool)
(Term.integer Z.zero Typ.bool))
let%test "unsigned booleans distinct" = let%test "unsigned booleans distinct" =
Term.is_false Term.is_false (Term.eq Term.one Term.zero)
(Term.eq
(Term.integer Z.one Typ.bool)
(Term.integer Z.zero Typ.bool))
let%test "boolean overflow" = let%test "boolean overflow" =
Term.is_true Term.is_true
@ -182,19 +175,19 @@ let%test_module _ =
[%expect {| 0 |}] [%expect {| 0 |}]
let%expect_test _ = let%expect_test _ =
pp (!3 * y = z = Term.bool true) ; pp (!3 * y = z = Term.true_) ;
[%expect {| ((3 × %y_1) = %z_2) |}] [%expect {| ((3 × %y_1) = %z_2) |}]
let%expect_test _ = let%expect_test _ =
pp (Term.bool true = (!3 * y = z)) ; pp (Term.true_ = (!3 * y = z)) ;
[%expect {| ((3 × %y_1) = %z_2) |}] [%expect {| ((3 × %y_1) = %z_2) |}]
let%expect_test _ = let%expect_test _ =
pp (!3 * y = z = Term.bool false) ; pp (!3 * y = z = Term.false_) ;
[%expect {| ((3 × %y_1) ≠ %z_2) |}] [%expect {| ((3 × %y_1) ≠ %z_2) |}]
let%expect_test _ = let%expect_test _ =
pp (Term.bool false = (!3 * y = z)) ; pp (Term.false_ = (!3 * y = z)) ;
[%expect {| ((3 × %y_1) ≠ %z_2) |}] [%expect {| ((3 × %y_1) ≠ %z_2) |}]
let%expect_test _ = let%expect_test _ =
@ -214,11 +207,11 @@ let%test_module _ =
[%expect {| ((-3 × %y_1 + 4) = %y_1) |}] [%expect {| ((-3 × %y_1 + 4) = %y_1) |}]
let%expect_test _ = let%expect_test _ =
pp (Term.sub Typ.bool (Term.bool true) (z = !4)) ; pp (Term.sub Term.true_ (z = !4)) ;
[%expect {| (-1 × (%z_2 = 4) + -1) |}] [%expect {| (-1 × (%z_2 = 4) + -1) |}]
let%expect_test _ = let%expect_test _ =
pp (Term.add Typ.bool (Term.bool true) (z = !4) = (z = !4)) ; pp (Term.add Term.true_ (z = !4) = (z = !4)) ;
[%expect {| (((%z_2 = 4) + -1) = (%z_2 = 4)) |}] [%expect {| (((%z_2 = 4) + -1) = (%z_2 = 4)) |}]
let%expect_test _ = let%expect_test _ =
@ -252,14 +245,14 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
pp Term.(eq z null) ; pp Term.(eq z null) ;
pp Term.(eq null z) ; pp Term.(eq null z) ;
pp Term.(dq (eq null z) (bool false)) ; pp Term.(dq (eq null z) false_) ;
[%expect [%expect
{| {|
(%z_2 = null) (%z_2 = 0)
(null = %z_2) (0 = %z_2)
(null = %z_2) |}] (0 = %z_2) |}]
let%expect_test _ = let%expect_test _ =
let z1 = z + !1 in let z1 = z + !1 in

Write Preview
Loading…
Cancel
Save