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

[sledge] Refactor: Rename to use terminology for "sized sequences"

Browse Source 
Summary:
Logically there is nothing specific to memory contents (as
byte-arrays) or aggregate (struct/array) values, the theory is for
sequences of non-fixed sized elements.

Reviewed By: jvillard

Differential Revision: D21721019

fbshipit-source-id: b2b730a50
master
Josh Berdine 5 years ago committed by Facebook GitHub Bot
parent 52dec5f4da
commit 1214ab71b7
12 changed files with 219 additions and 221 deletions
Show Stats Download Patch File Download Diff File

14
sledge/src/domain_sh.ml
Unescape View File

@ -18,11 +18,11 @@ let simplify q = if !simplify_states then Sh.simplify q else q
let init globals = let init globals =
IArray.fold globals ~init:Sh.emp ~f:(fun q -> function IArray.fold globals ~init:Sh.emp ~f:(fun q -> function
| {Llair.Global.reg; init= Some (arr, siz)} -> | {Llair.Global.reg; init= Some (seq, 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) in let len = Term.integer (Z.of_int siz) in
let arr = Term.of_exp arr in let seq = Term.of_exp seq in
Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr}) Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; seq})
| _ -> q ) | _ -> q )
let join p q = let join p q =
@ -105,7 +105,7 @@ let garbage_collect (q : t) ~wrt =
let new_set = let new_set =
List.fold ~init:current q.heap ~f:(fun current seg -> List.fold ~init:current q.heap ~f:(fun current seg ->
if term_eq_class_has_only_vars_in current q.cong seg.loc then if term_eq_class_has_only_vars_in current q.cong seg.loc then
List.fold (Equality.class_of q.cong seg.arr) ~init:current List.fold (Equality.class_of q.cong seg.seq) ~init:current
~f:(fun c e -> Var.Set.union c (Term.fv e)) ~f:(fun c e -> Var.Set.union c (Term.fv e))
else current ) else current )
in in
@ -335,9 +335,9 @@ let%test_module _ =
let b = Term.var b_ let b = Term.var b_
let n = Term.var n_ let n = Term.var n_
let endV = Term.var end_ let endV = Term.var end_
let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; arr= a} let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; seq= a}
let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= endV} let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= endV}
let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= main} let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= main}
let%expect_test _ = let%expect_test _ =
pp (garbage_collect seg_main ~wrt:(Var.Set.of_list [])) ; pp (garbage_collect seg_main ~wrt:(Var.Set.of_list [])) ;

66
sledge/src/equality.ml
Unescape View File

@ -14,7 +14,7 @@ type kind = Interpreted | Atomic | Uninterpreted
let classify e = let classify e =
match (e : Term.t) with match (e : Term.t) with
| Add _ | Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) -> | Add _ | Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
Interpreted Interpreted
| Mul _ | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ | And _ | Or _ -> Uninterpreted | Mul _ | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ | And _ | Or _ -> Uninterpreted
| Var _ | Integer _ | Rational _ | Float _ | Label _ | RecRecord _ -> | Var _ | Integer _ | Rational _ | Float _ | Label _ | RecRecord _ ->
@ -178,13 +178,13 @@ end
(** Theory Solver *) (** Theory Solver *)
(** prefer representative terms that are minimal in the order s.t. Var < (** prefer representative terms that are minimal in the order s.t. Var <
Memory < Extract < Concat < others, then using height of aggregate Sized < Extract < Concat < others, then using height of sequence
nesting, and then using Term.compare *) nesting, and then using Term.compare *)
let prefer e f = let prefer e f =
let rank e = let rank e =
match (e : Term.t) with match (e : Term.t) with
| Var _ -> 0 | Var _ -> 0
| Ap2 (Memory, _, _) -> 1 | Ap2 (Sized, _, _) -> 1
| Ap3 (Extract, _, _, _) -> 2 | Ap3 (Extract, _, _, _) -> 2
| ApN (Concat, _) -> 3 | ApN (Concat, _) -> 3
| _ -> 4 | _ -> 4
@ -229,16 +229,16 @@ let solve_poly ?f p q s =
(* α[o,l) = β ==> l = |β| ∧ α = (⟨n,c⟩[0,o) ^ β ^ ⟨n,c⟩[o+l,n-o-l)) where n (* α[o,l) = β ==> l = |β| ∧ α = (⟨n,c⟩[0,o) ^ β ^ ⟨n,c⟩[o+l,n-o-l)) where n
= |α| and c fresh *) = |α| and c fresh *)
let rec solve_extract ?f a o l b s = let rec solve_extract ?f a o l b s =
let n = Term.agg_size_exn a in let n = Term.seq_size_exn a in
let c, s = fresh "c" s in let c, s = fresh "c" s in
let n_c = Term.memory ~siz:n ~arr:c in let n_c = Term.sized ~siz:n ~seq:c in
let o_l = Term.add o l in let o_l = Term.add o l in
let n_o_l = Term.sub n o_l in let n_o_l = Term.sub n o_l in
let c0 = Term.extract ~agg:n_c ~off:Term.zero ~len:o in let c0 = Term.extract ~seq:n_c ~off:Term.zero ~len:o in
let c1 = Term.extract ~agg:n_c ~off:o_l ~len:n_o_l in let c1 = Term.extract ~seq:n_c ~off:o_l ~len:n_o_l in
let b, s = let b, s =
match Term.agg_size b with match Term.seq_size b with
| None -> (Term.memory ~siz:l ~arr:b, Some s) | None -> (Term.sized ~siz:l ~seq:b, Some s)
| Some m -> (b, solve_ ?f l m s) | Some m -> (b, solve_ ?f l m s)
in in
s >>= solve_ ?f a (Term.concat [|c0; b; c1|]) s >>= solve_ ?f a (Term.concat [|c0; b; c1|])
@ -248,9 +248,9 @@ let rec solve_extract ?f a o l b s =
and solve_concat ?f a0V b m s = and solve_concat ?f a0V b m s =
IArray.fold_until a0V ~init:(s, Term.zero) IArray.fold_until a0V ~init:(s, Term.zero)
~f:(fun (s, oI) aJ -> ~f:(fun (s, oI) aJ ->
let nJ = Term.agg_size_exn aJ in let nJ = Term.seq_size_exn aJ in
let oJ = Term.add oI nJ in let oJ = Term.add oI nJ in
match solve_ ?f aJ (Term.extract ~agg:b ~off:oI ~len:nJ) s with match solve_ ?f aJ (Term.extract ~seq:b ~off:oI ~len:nJ) s with
| Some s -> Continue (s, oJ) | Some s -> Continue (s, oJ)
| None -> Stop None ) | None -> Stop None )
~finish:(fun (s, n0V) -> solve_ ?f n0V m s) ~finish:(fun (s, n0V) -> solve_ ?f n0V m s)
@ -266,18 +266,18 @@ and solve_ ?f d e s =
(* i = j ==> false when i ≠ j *) (* i = j ==> false when i ≠ j *)
| Some (Integer _, Integer _) | Some (Rational _, Rational _) -> None | Some (Integer _, Integer _) | Some (Rational _, Rational _) -> None
(* ⟨0,a⟩ = β ==> a = β = ⟨⟩ *) (* ⟨0,a⟩ = β ==> a = β = ⟨⟩ *)
| Some (Ap2 (Memory, n, a), b) when Term.equal n Term.zero -> | Some (Ap2 (Sized, n, a), b) when Term.equal n Term.zero ->
s |> solve_ ?f a (Term.concat [||]) >>= solve_ ?f b (Term.concat [||]) s |> solve_ ?f a (Term.concat [||]) >>= solve_ ?f b (Term.concat [||])
| Some (b, Ap2 (Memory, n, a)) when Term.equal n Term.zero -> | Some (b, Ap2 (Sized, n, a)) when Term.equal n Term.zero ->
s |> solve_ ?f a (Term.concat [||]) >>= solve_ ?f b (Term.concat [||]) s |> solve_ ?f a (Term.concat [||]) >>= solve_ ?f b (Term.concat [||])
(* v = ⟨n,a⟩ ==> v = a *) (* v = ⟨n,a⟩ ==> v = a *)
| Some ((Var _ as v), Ap2 (Memory, _, a)) -> s |> solve_ ?f v a | Some ((Var _ as v), Ap2 (Sized, _, a)) -> s |> solve_ ?f v a
(* ⟨n,a⟩ = ⟨m,b⟩ ==> n = m ∧ a = β *) (* ⟨n,a⟩ = ⟨m,b⟩ ==> n = m ∧ a = β *)
| Some (Ap2 (Memory, n, a), Ap2 (Memory, m, b)) -> | Some (Ap2 (Sized, n, a), Ap2 (Sized, m, b)) ->
s |> solve_ ?f n m >>= solve_ ?f a b s |> solve_ ?f n m >>= solve_ ?f a b
(* ⟨n,a⟩ = β ==> n = |β| ∧ a = β *) (* ⟨n,a⟩ = β ==> n = |β| ∧ a = β *)
| Some (Ap2 (Memory, n, a), b) -> | Some (Ap2 (Sized, n, a), b) ->
( match Term.agg_size b with ( match Term.seq_size b with
| None -> Some s | None -> Some s
| Some m -> solve_ ?f n m s ) | Some m -> solve_ ?f n m s )
>>= solve_ ?f a b >>= solve_ ?f a b
@ -287,19 +287,19 @@ and solve_ ?f d e s =
compose1 ?f ~var:v ~rep:e s compose1 ?f ~var:v ~rep:e s
else else
(* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *) (* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *)
compose1 ?f ~var:e ~rep:(Term.memory ~siz:l ~arr:v) s compose1 ?f ~var:e ~rep:(Term.sized ~siz:l ~seq:v) s
| Some ((Var _ as v), (ApN (Concat, a0V) as c)) -> | Some ((Var _ as v), (ApN (Concat, a0V) as c)) ->
if not (Var.Set.mem (Term.fv c) (Var.of_ v)) then if not (Var.Set.mem (Term.fv c) (Var.of_ v)) then
(* v = α₀^…^αᵥ ==> v ↦ α₀^…^αᵥ when v ∉ fv(α₀^…^αᵥ) *) (* v = α₀^…^αᵥ ==> v ↦ α₀^…^αᵥ when v ∉ fv(α₀^…^αᵥ) *)
compose1 ?f ~var:v ~rep:c s compose1 ?f ~var:v ~rep:c s
else else
(* v = α₀^…^αᵥ ==> ⟨|α₀^…^αᵥ|,v⟩ = α₀^…^αᵥ when v ∈ fv(α₀^…^αᵥ) *) (* v = α₀^…^αᵥ ==> ⟨|α₀^…^αᵥ|,v⟩ = α₀^…^αᵥ when v ∈ fv(α₀^…^αᵥ) *)
let m = Term.agg_size_exn c in let m = Term.seq_size_exn c in
solve_concat ?f a0V (Term.memory ~siz:m ~arr:v) m s solve_concat ?f a0V (Term.sized ~siz:m ~seq:v) m s
| Some ((Ap3 (Extract, _, _, l) as e), ApN (Concat, a0V)) -> | Some ((Ap3 (Extract, _, _, l) as e), ApN (Concat, a0V)) ->
solve_concat ?f a0V e l s solve_concat ?f a0V e l s
| Some (ApN (Concat, a0V), (ApN (Concat, _) as c)) -> | Some (ApN (Concat, a0V), (ApN (Concat, _) as c)) ->
solve_concat ?f a0V c (Term.agg_size_exn c) s solve_concat ?f a0V c (Term.seq_size_exn c) s
| Some (Ap3 (Extract, a, o, l), e) -> solve_extract ?f a o l e s | Some (Ap3 (Extract, a, o, l), e) -> solve_extract ?f a o l e s
(* p = q ==> p-q = 0 *) (* p = q ==> p-q = 0 *)
| Some | Some
@ -772,7 +772,7 @@ let solve_poly_eq us p' q' subst =
[%Trace.retn fun {pf} subst' -> [%Trace.retn fun {pf} subst' ->
pf "@[%a@]" Subst.pp_diff (subst, Option.value subst' ~default:subst)] pf "@[%a@]" Subst.pp_diff (subst, Option.value subst' ~default:subst)]
let solve_memory_eq us e' f' subst = let solve_seq_eq us e' f' subst =
[%Trace.call fun {pf} -> pf "%a = %a" Term.pp e' Term.pp f'] [%Trace.call fun {pf} -> pf "%a = %a" Term.pp e' Term.pp f']
; ;
let f x u = let f x u =
@ -781,9 +781,9 @@ let solve_memory_eq us e' f' subst =
in in
let solve_concat ms n a = let solve_concat ms n a =
let a, n = let a, n =
match Term.agg_size a with match Term.seq_size a with
| Some n -> (a, n) | Some n -> (a, n)
| None -> (Term.memory ~siz:n ~arr:a, n) | None -> (Term.sized ~siz:n ~seq:a, n)
in in
let+ _, xs, s = solve_concat ~f ms a n (us, Var.Set.empty, subst) in let+ _, xs, s = solve_concat ~f ms a n (us, Var.Set.empty, subst) in
assert (Var.Set.is_empty xs) ; assert (Var.Set.is_empty xs) ;
@ -791,12 +791,12 @@ let solve_memory_eq us e' f' subst =
in in
( match ((e' : Term.t), (f' : Term.t)) with ( match ((e' : Term.t), (f' : Term.t)) with
| (ApN (Concat, ms) as c), a when f c a -> | (ApN (Concat, ms) as c), a when f c a ->
solve_concat ms (Term.agg_size_exn c) a solve_concat ms (Term.seq_size_exn c) a
| a, (ApN (Concat, ms) as c) when f c a -> | a, (ApN (Concat, ms) as c) when f c a ->
solve_concat ms (Term.agg_size_exn c) a solve_concat ms (Term.seq_size_exn c) a
| (Ap2 (Memory, _, (Var _ as v)) as m), u when f m u -> | (Ap2 (Sized, _, (Var _ as v)) as m), u when f m u ->
Some (Subst.compose1 ~key:v ~data:u subst) Some (Subst.compose1 ~key:v ~data:u subst)
| u, (Ap2 (Memory, _, (Var _ as v)) as m) when f m u -> | u, (Ap2 (Sized, _, (Var _ as v)) as m) when f m u ->
Some (Subst.compose1 ~key:v ~data:u subst) Some (Subst.compose1 ~key:v ~data:u subst)
| _ -> None ) | _ -> None )
|> |>
@ -810,7 +810,7 @@ let solve_interp_eq us e' (cls, subst) =
; ;
List.find_map cls ~f:(fun f -> List.find_map cls ~f:(fun f ->
let f' = Subst.norm subst f in let f' = Subst.norm subst f in
match solve_memory_eq us e' f' subst with match solve_seq_eq us e' f' subst with
| Some subst -> Some subst | Some subst -> Some subst
| None -> solve_poly_eq us e' f' subst ) | None -> solve_poly_eq us e' f' subst )
|> |>
@ -853,7 +853,7 @@ type cls_solve_state =
let dom_trm e = let dom_trm e =
match (e : Term.t) with match (e : Term.t) with
| Ap2 (Memory, _, (Var _ as v)) -> Some v | Ap2 (Sized, _, (Var _ as v)) -> Some v
| _ when non_interpreted e -> Some e | _ when non_interpreted e -> Some e
| _ -> None | _ -> None
@ -960,7 +960,7 @@ let solve_concat_extracts_eq r x =
; ;
let uses = let uses =
fold_uses_of r x ~init:[] ~f:(fun uses -> function fold_uses_of r x ~init:[] ~f:(fun uses -> function
| Ap2 (Memory, _, _) as m -> | Ap2 (Sized, _, _) as m ->
fold_uses_of r m ~init:uses ~f:(fun uses -> function fold_uses_of r m ~init:uses ~f:(fun uses -> function
| Ap3 (Extract, _, _, _) as e -> e :: uses | _ -> uses ) | Ap3 (Extract, _, _, _) as e -> e :: uses | _ -> uses )
| _ -> uses ) | _ -> uses )
@ -975,7 +975,7 @@ let solve_concat_extracts_eq r x =
List.fold (find_extracts_at_off off) ~init:full_rev_extracts List.fold (find_extracts_at_off off) ~init:full_rev_extracts
~f:(fun full_rev_extracts e -> ~f:(fun full_rev_extracts e ->
match e with match e with
| Ap3 (Extract, Ap2 (Memory, n, _), o, l) -> | Ap3 (Extract, Ap2 (Sized, n, _), o, l) ->
let o_l = Term.add o l in let o_l = Term.add o l in
if entails_eq r n o_l then if entails_eq r n o_l then
(e :: rev_prefix) :: full_rev_extracts (e :: rev_prefix) :: full_rev_extracts
@ -999,7 +999,7 @@ let solve_concat_extracts r us x (classes, subst, us_xs) =
Some trm Some trm
| _ -> rep_ito_us ) | _ -> rep_ito_us )
in in
Term.memory ~siz:(Term.agg_size_exn e) ~arr:rep_ito_us :: suffix ) ) Term.sized ~siz:(Term.seq_size_exn e) ~seq:rep_ito_us :: suffix ) )
|> List.min_elt ~compare:[%compare: Term.t list] |> List.min_elt ~compare:[%compare: Term.t list]
with with
| Some extracts -> | Some extracts ->

80
sledge/src/exec.ml
Unescape View File

@ -19,7 +19,7 @@ let fresh_var nam us xs =
let var, us = Var.fresh nam ~wrt:us in let var, us = Var.fresh nam ~wrt:us in
(Term.var var, us, Var.Set.add xs var) (Term.var var, us, Var.Set.add xs var)
let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us = let fresh_seg ~loc ?bas ?len ?siz ?seq ?(xs = Var.Set.empty) us =
let freshen term nam us xs = let freshen term nam us xs =
match term with match term with
| Some term -> (term, us, xs) | Some term -> (term, us, xs)
@ -28,15 +28,15 @@ let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
let bas, us, xs = freshen bas "b" us xs in let bas, us, xs = freshen bas "b" us xs in
let len, us, xs = freshen len "m" us xs in let len, us, xs = freshen len "m" us xs in
let siz, us, xs = freshen siz "n" us xs in let siz, us, xs = freshen siz "n" us xs in
let arr, us, xs = freshen arr "a" us xs in let seq, us, xs = freshen seq "a" us xs in
{us; xs; seg= {loc; bas; len; siz; arr}} {us; xs; seg= {loc; bas; len; siz; seq}}
let null_eq ptr = Sh.pure (Term.eq Term.zero ptr) let null_eq ptr = Sh.pure (Term.eq Term.zero ptr)
let eq_concat (siz, arr) ms = let eq_concat (siz, seq) ms =
Term.( Term.(
eq (memory ~siz ~arr) eq (sized ~siz ~seq)
(concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms))) (concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
(* 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
@ -82,7 +82,7 @@ let load_spec us reg ptr len =
let sub, ms, _ = assign ~ws:(Var.Set.of_ reg) ~rs:foot.us ~us in let sub, ms, _ = assign ~ws:(Var.Set.of_ reg) ~rs:foot.us ~us in
let post = let post =
Sh.and_ Sh.and_
(Term.eq (Term.var reg) (Term.rename sub seg.arr)) (Term.eq (Term.var reg) (Term.rename sub seg.seq))
(Sh.rename sub foot) (Sh.rename sub foot)
in in
{xs; foot; sub; ms; post} {xs; foot; sub; ms; post}
@ -94,7 +94,7 @@ let load_spec us reg ptr len =
let store_spec us ptr exp len = let store_spec us ptr exp len =
let {us= _; xs; seg} = fresh_seg ~loc:ptr ~siz:len us in let {us= _; xs; seg} = fresh_seg ~loc:ptr ~siz:len us in
let foot = Sh.seg seg in let foot = Sh.seg seg in
let post = Sh.seg {seg with arr= exp} in let post = Sh.seg {seg with seq= exp} in
{xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
(* { d-[b;m)->⟨l,α⟩ } (* { d-[b;m)->⟨l,α⟩ }
@ -104,7 +104,7 @@ let store_spec us ptr exp len =
let memset_spec us dst byt len = let memset_spec us dst byt len =
let {us= _; xs; seg} = fresh_seg ~loc:dst ~siz:len us in let {us= _; xs; seg} = fresh_seg ~loc:dst ~siz:len us in
let foot = Sh.seg seg in let foot = Sh.seg seg in
let post = Sh.seg {seg with arr= Term.splat byt} in let post = Sh.seg {seg with seq= Term.splat byt} in
{xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
(* { d=s * l=0 * d-[b;m)->⟨l,α⟩ } (* { d=s * l=0 * d-[b;m)->⟨l,α⟩ }
@ -129,7 +129,7 @@ let memcpy_dj_spec us dst src len =
let dst_heap = Sh.seg dst_seg in let dst_heap = Sh.seg dst_seg in
let {us= _; xs; seg= src_seg} = fresh_seg ~loc:src ~siz:len ~xs us in let {us= _; xs; seg= src_seg} = fresh_seg ~loc:src ~siz:len ~xs us in
let src_heap = Sh.seg src_seg in let src_heap = Sh.seg src_seg in
let dst_seg' = {dst_seg with arr= src_seg.arr} in let dst_seg' = {dst_seg with seq= src_seg.seq} in
let dst_heap' = Sh.seg dst_seg' in let dst_heap' = Sh.seg dst_seg' in
let foot = Sh.star dst_heap src_heap in let foot = Sh.star dst_heap src_heap in
let post = Sh.star dst_heap' src_heap in let post = Sh.star dst_heap' src_heap in
@ -160,23 +160,23 @@ let memmov_foot us dst src len =
let xs = Var.Set.empty in let xs = Var.Set.empty in
let bas, us, xs = fresh_var "b" us xs in let bas, us, xs = fresh_var "b" us xs in
let siz, us, xs = fresh_var "m" us xs in let siz, us, xs = fresh_var "m" us xs in
let arr_dst, us, xs = fresh_var "a" us xs in let seq_dst, us, xs = fresh_var "a" us xs in
let arr_mid, us, xs = fresh_var "a" us xs in let seq_mid, us, xs = fresh_var "a" us xs in
let arr_src, us, xs = fresh_var "a" us xs in let seq_src, us, xs = fresh_var "a" us xs in
let src_dst = Term.sub src dst in let src_dst = Term.sub src dst in
let mem_dst = (src_dst, arr_dst) in let mem_dst = (src_dst, seq_dst) in
let siz_mid = Term.sub len src_dst in let siz_mid = Term.sub len src_dst in
let mem_mid = (siz_mid, arr_mid) in let mem_mid = (siz_mid, seq_mid) in
let mem_src = (src_dst, arr_src) in let mem_src = (src_dst, seq_src) in
let mem_dst_mid_src = [|mem_dst; mem_mid; mem_src|] in let mem_dst_mid_src = [|mem_dst; mem_mid; mem_src|] in
let siz_dst_mid_src, us, xs = fresh_var "m" us xs in let siz_dst_mid_src, us, xs = fresh_var "m" us xs in
let arr_dst_mid_src, us, xs = fresh_var "a" us xs in let seq_dst_mid_src, us, xs = fresh_var "a" us xs in
let eq_mem_dst_mid_src = let eq_mem_dst_mid_src =
eq_concat (siz_dst_mid_src, arr_dst_mid_src) mem_dst_mid_src eq_concat (siz_dst_mid_src, seq_dst_mid_src) mem_dst_mid_src
in in
let seg = let seg =
Sh.seg Sh.seg
{loc= dst; bas; len= siz; siz= siz_dst_mid_src; arr= arr_dst_mid_src} {loc= dst; bas; len= siz; siz= siz_dst_mid_src; seq= seq_dst_mid_src}
in in
let foot = let foot =
Sh.and_ eq_mem_dst_mid_src Sh.and_ eq_mem_dst_mid_src
@ -195,9 +195,9 @@ let memmov_dn_spec us dst src len =
in in
let mem_mid_src_src = [|mem_mid; mem_src; mem_src|] in let mem_mid_src_src = [|mem_mid; mem_src; mem_src|] in
let siz_mid_src_src, us, xs = fresh_var "m" us xs in let siz_mid_src_src, us, xs = fresh_var "m" us xs in
let arr_mid_src_src, _, xs = fresh_var "a" us xs in let seq_mid_src_src, _, xs = fresh_var "a" us xs in
let eq_mem_mid_src_src = let eq_mem_mid_src_src =
eq_concat (siz_mid_src_src, arr_mid_src_src) mem_mid_src_src eq_concat (siz_mid_src_src, seq_mid_src_src) mem_mid_src_src
in in
let post = let post =
Sh.and_ eq_mem_mid_src_src Sh.and_ eq_mem_mid_src_src
@ -206,7 +206,7 @@ let memmov_dn_spec us dst src len =
; bas ; bas
; len= siz ; len= siz
; siz= siz_mid_src_src ; siz= siz_mid_src_src
; arr= arr_mid_src_src }) ; seq= seq_mid_src_src })
in in
{xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -220,9 +220,9 @@ let memmov_up_spec us dst src len =
in in
let mem_src_src_mid = [|mem_src; mem_src; mem_mid|] in let mem_src_src_mid = [|mem_src; mem_src; mem_mid|] in
let siz_src_src_mid, us, xs = fresh_var "m" us xs in let siz_src_src_mid, us, xs = fresh_var "m" us xs in
let arr_src_src_mid, _, xs = fresh_var "a" us xs in let seq_src_src_mid, _, xs = fresh_var "a" us xs in
let eq_mem_src_src_mid = let eq_mem_src_src_mid =
eq_concat (siz_src_src_mid, arr_src_src_mid) mem_src_src_mid eq_concat (siz_src_src_mid, seq_src_src_mid) mem_src_src_mid
in in
let post = let post =
Sh.and_ eq_mem_src_src_mid Sh.and_ eq_mem_src_src_mid
@ -231,7 +231,7 @@ let memmov_up_spec us dst src len =
; bas ; bas
; len= siz ; len= siz
; siz= siz_src_src_mid ; siz= siz_src_src_mid
; arr= arr_src_src_mid }) ; seq= seq_src_src_mid })
in in
{xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -317,8 +317,8 @@ let calloc_spec us reg num len =
let sub, ms, us = assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) ~us in let sub, ms, us = assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) ~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 arr = Term.splat Term.zero in let seq = Term.splat Term.zero 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 ~seq 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}
@ -339,7 +339,7 @@ let posix_memalign_spec us reg ptr siz =
~us ~us
in in
let q, us, xs = fresh_var "q" us xs in let q, us, xs = fresh_var "q" us xs in
let pseg' = {pseg with arr= q} in let pseg' = {pseg with seq= q} in
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
@ -374,8 +374,8 @@ let realloc_spec us reg ptr siz =
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 {us; xs; seg= rseg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~xs us in let {us; xs; seg= rseg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~xs us in
let a0 = pseg.arr in let a0 = pseg.seq in
let a1 = rseg.arr in let a1 = rseg.seq in
let a2, _, xs = fresh_var "a" us xs in let a2, _, xs = fresh_var "a" us xs in
let post = let post =
Sh.or_ Sh.or_
@ -406,8 +406,8 @@ let rallocx_spec us reg ptr siz =
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 {us; xs; seg= rseg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~xs us in let {us; xs; seg= rseg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~xs us in
let a0 = pseg.arr in let a0 = pseg.seq in
let a1 = rseg.arr in let a1 = rseg.seq in
let a2, _, xs = fresh_var "a" us xs in let a2, _, xs = fresh_var "a" us xs in
let post = let post =
Sh.or_ Sh.or_
@ -442,8 +442,8 @@ let xallocx_spec us reg ptr siz ext =
let {us; xs; seg= seg'} = let {us; xs; seg= seg'} =
fresh_seg ~loc:ptr ~bas:ptr ~len:reg ~siz:reg ~xs us fresh_seg ~loc:ptr ~bas:ptr ~len:reg ~siz:reg ~xs us
in in
let a0 = seg.arr in let a0 = seg.seq in
let a1 = seg'.arr in let a1 = seg'.seq in
let a2, _, xs = fresh_var "a" us xs in let a2, _, xs = fresh_var "a" us xs in
let post = let post =
Sh.and_ Sh.and_
@ -502,14 +502,14 @@ let size_of_int_mul = Term.mulq (Q.of_int Llair.Typ.(size_of siz))
*) *)
let mallctl_read_spec us r i w n = let mallctl_read_spec us r i w n =
let {us; xs; seg= iseg} = fresh_seg ~loc:i us in let {us; xs; seg= iseg} = fresh_seg ~loc:i us in
let {us; xs; seg= rseg} = fresh_seg ~loc:r ~siz:iseg.arr ~xs us in let {us; xs; seg= rseg} = fresh_seg ~loc:r ~siz:iseg.seq ~xs us in
let a, _, xs = fresh_var "a" us xs in let a, _, xs = fresh_var "a" us xs in
let foot = let foot =
Sh.and_ Sh.and_
Term.(eq w zero) Term.(eq w zero)
(Sh.and_ Term.(eq n zero) (Sh.star (Sh.seg iseg) (Sh.seg rseg))) (Sh.and_ Term.(eq n zero) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
in in
let rseg' = {rseg with arr= a} in let rseg' = {rseg with seq= a} in
let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in
{xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -522,7 +522,7 @@ let mallctlbymib_read_spec us p l r i w n =
let wl = size_of_int_mul l in let wl = size_of_int_mul l in
let {us; xs; seg= pseg} = fresh_seg ~loc:p ~siz:wl us in let {us; xs; seg= pseg} = fresh_seg ~loc:p ~siz:wl us in
let {us; xs; seg= iseg} = fresh_seg ~loc:i ~xs us in let {us; xs; seg= iseg} = fresh_seg ~loc:i ~xs us in
let m = iseg.arr in let m = iseg.seq in
let {us; xs; seg= rseg} = fresh_seg ~loc:r ~siz:m ~xs us in let {us; xs; seg= rseg} = fresh_seg ~loc:r ~siz:m ~xs us in
let const = Sh.star (Sh.seg pseg) (Sh.seg iseg) in let const = Sh.star (Sh.seg pseg) (Sh.seg iseg) in
let a, _, xs = fresh_var "a" us xs in let a, _, xs = fresh_var "a" us xs in
@ -531,7 +531,7 @@ let mallctlbymib_read_spec us p l r i w n =
Term.(eq w zero) Term.(eq w zero)
(Sh.and_ Term.(eq n zero) (Sh.star const (Sh.seg rseg))) (Sh.and_ Term.(eq n zero) (Sh.star const (Sh.seg rseg)))
in in
let rseg' = {rseg with arr= a} in let rseg' = {rseg with seq= a} in
let post = Sh.star (Sh.seg rseg') const in let post = Sh.star (Sh.seg rseg') const in
{xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -577,12 +577,12 @@ let mallctlbymib_specs us p j r i w n =
*) *)
let mallctlnametomib_spec us p o = let mallctlnametomib_spec us p o =
let {us; xs; seg= oseg} = fresh_seg ~loc:o us in let {us; xs; seg= oseg} = fresh_seg ~loc:o us in
let n = oseg.arr in let n = oseg.seq in
let wn = size_of_int_mul n in let wn = size_of_int_mul n in
let {us; xs; seg= pseg} = fresh_seg ~loc:p ~siz:wn ~xs us in let {us; xs; seg= pseg} = fresh_seg ~loc:p ~siz:wn ~xs us in
let a, _, xs = fresh_var "a" us xs in let a, _, xs = fresh_var "a" us xs in
let foot = Sh.star (Sh.seg oseg) (Sh.seg pseg) in let foot = Sh.star (Sh.seg oseg) (Sh.seg pseg) in
let pseg' = {pseg with arr= a} in let pseg' = {pseg with seq= a} in
let post = Sh.star (Sh.seg pseg') (Sh.seg oseg) in let post = Sh.star (Sh.seg pseg') (Sh.seg oseg) in
{xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}

2
sledge/src/llair/exp.ml
Unescape View File

@ -389,7 +389,7 @@ let conditional ?typ ~cnd ~thn ~els =
let typ = match typ with Some typ -> typ | None -> typ_of thn in let typ = match typ with Some typ -> typ | None -> typ_of thn in
Ap3 (Conditional, typ, cnd, thn, els) |> check invariant Ap3 (Conditional, typ, cnd, thn, els) |> check invariant
(* memory *) (* sequences *)
let splat typ byt = Ap1 (Splat, typ, byt) |> check invariant let splat typ byt = Ap1 (Splat, typ, byt) |> check invariant

2
sledge/src/llair/exp.mli
Unescape View File

@ -172,7 +172,7 @@ val ashr : ?typ:Typ.t -> t -> t -> t
(* if-then-else *) (* if-then-else *)
val conditional : ?typ:Typ.t -> cnd:t -> thn:t -> els:t -> t val conditional : ?typ:Typ.t -> cnd:t -> thn:t -> els:t -> t
(* memory *) (* sequences *)
val splat : Typ.t -> t -> t val splat : Typ.t -> t -> t
(* records (struct / array values) *) (* records (struct / array values) *)

24
sledge/src/sh.ml
Unescape View File

@ -9,7 +9,7 @@
[@@@warning "+9"] [@@@warning "+9"]
type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; arr: Term.t} type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
[@@deriving compare, equal, sexp] [@@deriving compare, equal, sexp]
type starjunction = type starjunction =
@ -44,15 +44,15 @@ let map_seg ~f h =
let bas = f h.bas in let bas = f h.bas in
let len = f h.len in let len = f h.len in
let siz = f h.siz in let siz = f h.siz in
let arr = f h.arr in let seq = f h.seq in
if if
loc == h.loc loc == h.loc
&& bas == h.bas && bas == h.bas
&& len == h.len && len == h.len
&& siz == h.siz && siz == h.siz
&& arr == h.arr && seq == h.seq
then h then h
else {loc; bas; len; siz; arr} else {loc; bas; len; siz; seq}
let map ~f_sjn ~f_cong ~f_trm ({us; xs= _; cong; pure; heap; djns} as q) = let map ~f_sjn ~f_cong ~f_trm ({us; xs= _; cong; pure; heap; djns} as q) =
let exception Unsat in let exception Unsat in
@ -72,9 +72,9 @@ let map ~f_sjn ~f_cong ~f_trm ({us; xs= _; cong; pure; heap; djns} as q) =
else {q with cong; pure; heap; djns} else {q with cong; pure; heap; djns}
with Unsat -> false_ us with Unsat -> false_ us
let fold_terms_seg {loc; bas; len; siz; arr} ~init ~f = let fold_terms_seg {loc; bas; len; siz; seq} ~init ~f =
let f b s = f s b in let f b s = f s b in
f loc (f bas (f len (f siz (f arr init)))) f loc (f bas (f len (f siz (f seq init))))
let fold_vars_seg seg ~init ~f = let fold_vars_seg seg ~init ~f =
fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init) fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init)
@ -130,15 +130,15 @@ let var_strength ?(xs = Var.Set.empty) q =
in in
var_strength_ xs m q var_strength_ xs m q
let pp_memory x fs (siz, arr) = Term.ppx x fs (Term.memory ~siz ~arr) let pp_chunk x fs (siz, seq) = Term.ppx x fs (Term.sized ~siz ~seq)
let pp_seg x fs {loc; bas; len; siz; arr} = let pp_seg x fs {loc; bas; len; siz; seq} =
let term_pp = Term.ppx x in let term_pp = Term.ppx x in
Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc
(fun fs (bas, len) -> (fun fs (bas, len) ->
if (not (Term.equal loc bas)) || not (Term.equal len siz) then if (not (Term.equal loc bas)) || not (Term.equal len siz) then
Format.fprintf fs " %a, %a " term_pp bas term_pp len ) Format.fprintf fs " %a, %a " term_pp bas term_pp len )
(bas, len) (pp_memory x) (siz, arr) (bas, len) (pp_chunk x) (siz, seq)
let pp_seg_norm cong fs seg = let pp_seg_norm cong fs seg =
let x _ = None in let x _ = None in
@ -164,8 +164,8 @@ let pp_block x fs segs =
| [] -> false | [] -> false
in in
let term_pp = Term.ppx x in let term_pp = Term.ppx x in
let pp_mems = let pp_chunks =
List.pp "@,^" (fun fs seg -> pp_memory x fs (seg.siz, seg.arr)) List.pp "@,^" (fun fs seg -> pp_chunk x fs (seg.siz, seg.seq))
in in
match segs with match segs with
| {loc; bas; len; _} :: _ -> | {loc; bas; len; _} :: _ ->
@ -173,7 +173,7 @@ let pp_block x fs segs =
(fun fs -> (fun fs ->
if not (is_full_alloc segs) then if not (is_full_alloc segs) then
Format.fprintf fs " %a, %a " term_pp bas term_pp len ) Format.fprintf fs " %a, %a " term_pp bas term_pp len )
pp_mems segs pp_chunks segs
| [] -> () | [] -> ()
let pp_heap x ?pre cong fs heap = let pp_heap x ?pre cong fs heap =

7
sledge/src/sh.mli
Unescape View File

@ -7,11 +7,10 @@
(** Symbolic Heap Formulas *) (** Symbolic Heap Formulas *)
(** Segment of memory starting at [loc] containing a byte-array [arr] of (** Segment of memory starting at [loc] containing [seq] (a byte-array) of
size [siz], contained in an enclosing allocation-block starting at [bas] size [siz], contained in an enclosing allocation-block starting at [bas]
of length [len]. Byte-array expressions are either [Var]iables or of length [len]. *)
[Splat] vectors. *) type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; arr: Term.t}
type starjunction = private type starjunction = private
{ us: Var.Set.t (** vocabulary / variable context of formula *) { us: Var.Set.t (** vocabulary / variable context of formula *)

6
sledge/src/sh_test.ml
Unescape View File

@ -41,10 +41,10 @@ let%test_module _ =
let x = Term.var x_ let x = Term.var x_
let y = Term.var y_ let y = Term.var y_
let eq_concat (siz, arr) ms = let eq_concat (siz, seq) ms =
Term.( Term.(
eq (memory ~siz ~arr) eq (sized ~siz ~seq)
(concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms))) (concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
let of_eqs l = let of_eqs l =
List.fold ~init:emp ~f:(fun q (a, b) -> and_ (Term.eq a b) q) l List.fold ~init:emp ~f:(fun q (a, b) -> and_ (Term.eq a b) q) l

76
sledge/src/solver.ml
Unescape View File

@ -132,10 +132,10 @@ end
open Goal open Goal
let eq_concat (siz, arr) ms = let eq_concat (siz, seq) ms =
Term.( Term.(
eq (memory ~siz ~arr) eq (sized ~siz ~seq)
(concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms))) (concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
let fresh_var name vs zs ~wrt = let fresh_var name vs zs ~wrt =
let v, wrt = Var.fresh name ~wrt in let v, wrt = Var.fresh name ~wrt in
@ -212,8 +212,8 @@ let excise_seg_same ({com; min; sub} as goal) msg ssg =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.cong) pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.cong)
msg (Sh.pp_seg_norm sub.cong) ssg ) ; msg (Sh.pp_seg_norm sub.cong) ssg ) ;
let {Sh.bas= b; len= m; arr= a} = msg in let {Sh.bas= b; len= m; seq= a} = msg in
let {Sh.bas= b'; len= m'; arr= a'} = ssg in let {Sh.bas= b'; len= m'; seq= a'} = ssg 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 sub = let sub =
@ -240,18 +240,18 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_prefix@ %a@ \\- %a@]" pf "@[<hv 2>excise_seg_sub_prefix@ %a@ \\- %a@]"
(Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.bas= b'; len= m'; siz= n; seq= a'} = ssg in
let o_n = Term.integer o_n in let o_n = Term.integer o_n in
let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.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 xs = Var.Set.diff xs (Term.fv n) in let xs = Var.Set.diff xs (Term.fv n) 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; seq= a0}) com in
let min = let min =
Sh.and_ Sh.and_
(eq_concat (o, a) [|(n, a0); (o_n, a1)|]) (eq_concat (o, a) [|(n, a0); (o_n, a1)|])
(Sh.star (Sh.star
(Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; arr= a1}) (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; seq= a1})
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
@ -280,8 +280,8 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_prefix@ %a@ \\- %a@]" pf "@[<hv 2>excise_seg_min_prefix@ %a@ \\- %a@]"
(Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
let {Sh.bas= b; len= m; siz= o; arr= a} = msg in let {Sh.bas= b; len= m; siz= o; seq= 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; seq= a'} = ssg in
let n_o = Term.integer n_o 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
@ -293,7 +293,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
(eq_concat (n, a') [|(o, a); (n_o, a1')|]) (eq_concat (n, a') [|(o, a); (n_o, a1')|])
(Sh.star (Sh.star
(Sh.seg (Sh.seg
{loc= Term.add l o; bas= b'; len= m'; siz= n_o; arr= a1'}) {loc= Term.add l o; bas= b'; len= m'; siz= n_o; seq= a1'})
(Sh.rem_seg ssg sub)))) (Sh.rem_seg ssg sub))))
in in
goal |> with_ ~com ~min ~xs ~sub ~zs goal |> with_ ~com ~min ~xs ~sub ~zs
@ -316,20 +316,20 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_suffix@ %a@ \\- %a@]" pf "@[<hv 2>excise_seg_sub_suffix@ %a@ \\- %a@]"
(Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; seq= 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; seq= a'} = ssg in
let l_k = Term.integer l_k in let l_k = Term.integer l_k in
let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.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 xs = Var.Set.diff xs (Term.fv n) in let xs = Var.Set.diff xs (Term.fv n) in
let com = let com =
Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a1}) com
in in
let min = let min =
Sh.and_ Sh.and_
(eq_concat (o, a) [|(l_k, a0); (n, a1)|]) (eq_concat (o, a) [|(l_k, a0); (n, a1)|])
(Sh.star (Sh.star
(Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0}) (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
@ -358,8 +358,8 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_infix@ %a@ \\- %a@]" pf "@[<hv 2>excise_seg_sub_infix@ %a@ \\- %a@]"
(Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; seq= 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; seq= a'} = ssg in
let l_k = Term.integer l_k in let l_k = Term.integer l_k in
let ko_ln = Term.integer ko_ln in let ko_ln = Term.integer ko_ln in
let ln = Term.add l n in let ln = Term.add l n in
@ -368,15 +368,15 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
let xs = Var.Set.diff xs (Var.Set.union (Term.fv l) (Term.fv n)) in let xs = Var.Set.diff xs (Var.Set.union (Term.fv l) (Term.fv n)) in
let com = let com =
Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a1}) com
in in
let min = let min =
Sh.and_ Sh.and_
(eq_concat (o, a) [|(l_k, a0); (n, a1); (ko_ln, a2)|]) (eq_concat (o, a) [|(l_k, a0); (n, a1); (ko_ln, a2)|])
(Sh.star (Sh.star
(Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0}) (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
(Sh.star (Sh.star
(Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; arr= a2}) (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; seq= a2})
(Sh.rem_seg msg min))) (Sh.rem_seg msg min)))
in in
let sub = let sub =
@ -405,8 +405,8 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_skew@ %a@ \\- %a@]" pf "@[<hv 2>excise_seg_min_skew@ %a@ \\- %a@]"
(Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; seq= 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; seq= a'} = ssg in
let l_k = Term.integer l_k in let l_k = Term.integer l_k in
let ko_l = Term.integer ko_l in let ko_l = Term.integer ko_l in
let ln_ko = Term.integer ln_ko in let ln_ko = Term.integer ln_ko in
@ -416,13 +416,13 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
let xs = Var.Set.diff xs (Term.fv l) in let xs = Var.Set.diff xs (Term.fv l) in
let com = let com =
Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; arr= a1}) com Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; seq= a1}) com
in in
let min = let min =
Sh.and_ Sh.and_
(eq_concat (o, a) [|(l_k, a0); (ko_l, a1)|]) (eq_concat (o, a) [|(l_k, a0); (ko_l, a1)|])
(Sh.star (Sh.star
(Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0}) (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
@ -431,7 +431,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
(Sh.and_ (Sh.and_
(eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|]) (eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|])
(Sh.star (Sh.star
(Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'}) (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; seq= a2'})
(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
@ -455,8 +455,8 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_suffix@ %a@ \\- %a@]" pf "@[<hv 2>excise_seg_min_suffix@ %a@ \\- %a@]"
(Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
let {Sh.bas= b; len= m; siz= o; arr= a} = msg in let {Sh.bas= b; len= m; siz= o; seq= 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; seq= a'} = ssg in
let k_l = Term.integer k_l in let k_l = Term.integer k_l in
let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in
let com = Sh.star (Sh.seg msg) com in let com = Sh.star (Sh.seg msg) com in
@ -467,7 +467,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
(Sh.and_ (Sh.and_
(eq_concat (n, a') [|(k_l, a0'); (o, a)|]) (eq_concat (n, a') [|(k_l, a0'); (o, a)|])
(Sh.star (Sh.star
(Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'}) (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
(Sh.rem_seg ssg sub)))) (Sh.rem_seg ssg sub))))
in in
goal |> with_ ~com ~min ~xs ~sub ~zs goal |> with_ ~com ~min ~xs ~sub ~zs
@ -492,8 +492,8 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_infix@ %a@ \\- %a@]" pf "@[<hv 2>excise_seg_min_infix@ %a@ \\- %a@]"
(Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; seq= 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; seq= a'} = ssg in
let k_l = Term.integer k_l in let k_l = Term.integer k_l in
let ln_ko = Term.integer ln_ko in let ln_ko = Term.integer ln_ko in
let ko = Term.add k o in let ko = Term.add k o in
@ -507,9 +507,9 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
(Sh.and_ (Sh.and_
(eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|]) (eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|])
(Sh.star (Sh.star
(Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'}) (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
(Sh.star (Sh.star
(Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'}) (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; seq= a2'})
(Sh.rem_seg ssg sub))))) (Sh.rem_seg ssg sub)))))
in in
goal |> with_ ~com ~min ~xs ~sub ~zs goal |> with_ ~com ~min ~xs ~sub ~zs
@ -533,8 +533,8 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_skew@ %a@ \\- %a@]" pf "@[<hv 2>excise_seg_sub_skew@ %a@ \\- %a@]"
(Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; seq= 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; seq= a'} = ssg in
let k_l = Term.integer k_l in let k_l = Term.integer k_l in
let ln_k = Term.integer ln_k in let ln_k = Term.integer ln_k in
let ko_ln = Term.integer ko_ln in let ko_ln = Term.integer ko_ln in
@ -543,13 +543,13 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
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
let com = let com =
Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= ln_k; arr= a1}) com Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= ln_k; seq= a1}) com
in in
let min = let min =
Sh.and_ Sh.and_
(eq_concat (o, a) [|(ln_k, a1); (ko_ln, a2)|]) (eq_concat (o, a) [|(ln_k, a1); (ko_ln, a2)|])
(Sh.star (Sh.star
(Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; arr= a2}) (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; seq= a2})
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
@ -558,7 +558,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
(Sh.and_ (Sh.and_
(eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|]) (eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|])
(Sh.star (Sh.star
(Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'}) (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
(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

58
sledge/src/solver_test.ml
Unescape View File

@ -75,7 +75,7 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
check_frame check_frame
(Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a}) (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
[] Sh.emp ; [] Sh.emp ;
[%expect [%expect
{| {|
@ -84,9 +84,9 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
check_frame check_frame
(Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a}) (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
[] []
(Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a}) ; (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -95,8 +95,8 @@ let%test_module _ =
) infer_frame: emp |}] ) infer_frame: emp |}]
let%expect_test _ = let%expect_test _ =
let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; arr= a2} in let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; seq= a2} in
let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; arr= a} in let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; seq= a} in
let minued = Sh.star common seg1 in let minued = Sh.star common seg1 in
let subtrahend = let subtrahend =
Sh.and_ (Term.eq m n) Sh.and_ (Term.eq m n)
@ -117,10 +117,10 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
check_frame check_frame
(Sh.star (Sh.star
(Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a}) (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
(Sh.seg {loc= l2; bas= b; len= m; siz= n; arr= a2})) (Sh.seg {loc= l2; bas= b; len= m; siz= n; seq= a2}))
[] []
(Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a}) ; (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -132,10 +132,10 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
check_frame check_frame
(Sh.star (Sh.star
(Sh.seg {loc= l; bas= l; len= !16; siz= !8; arr= a}) (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
(Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; arr= a2})) (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
[a3_] [a3_]
(Sh.seg {loc= l; bas= l; len= !16; siz= !16; arr= a3}) ; (Sh.seg {loc= l; bas= l; len= !16; siz= !16; seq= a3}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -145,10 +145,10 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
check_frame check_frame
(Sh.star (Sh.star
(Sh.seg {loc= l; bas= l; len= !16; siz= !8; arr= a}) (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
(Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; arr= a2})) (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
[a3_; m_] [a3_; m_]
(Sh.seg {loc= l; bas= l; len= m; siz= !16; arr= a3}) ; (Sh.seg {loc= l; bas= l; len= m; siz= !16; seq= a3}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -161,10 +161,10 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
check_frame check_frame
(Sh.star (Sh.star
(Sh.seg {loc= l; bas= l; len= !16; siz= !8; arr= a}) (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
(Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; arr= a2})) (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
[a3_; m_] [a3_; m_]
(Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a3}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a3}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -177,12 +177,12 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
check_frame check_frame
(Sh.star (Sh.star
(Sh.seg {loc= k; bas= k; len= !16; siz= !32; arr= a}) (Sh.seg {loc= k; bas= k; len= !16; siz= !32; seq= a})
(Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= !16})) (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= !16}))
[a2_; m_; n_] [a2_; m_; n_]
(Sh.star (Sh.star
(Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= n}) (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= n})
(Sh.seg {loc= k; bas= k; len= m; siz= n; arr= a2})) ; (Sh.seg {loc= k; bas= k; len= m; siz= n; seq= a2})) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -199,12 +199,12 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
infer_frame infer_frame
(Sh.star (Sh.star
(Sh.seg {loc= k; bas= k; len= !16; siz= !32; arr= a}) (Sh.seg {loc= k; bas= k; len= !16; siz= !32; seq= a})
(Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= !16})) (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= !16}))
[a2_; m_; n_] [a2_; m_; n_]
(Sh.star (Sh.star
(Sh.seg {loc= k; bas= k; len= m; siz= n; arr= a2}) (Sh.seg {loc= k; bas= k; len= m; siz= n; seq= a2})
(Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= n})) ; (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= n})) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -220,9 +220,9 @@ let%test_module _ =
let seg_split_symbolically = let seg_split_symbolically =
Sh.star Sh.star
(Sh.seg {loc= l; bas= l; len= !16; siz= 8 * n; arr= a2}) (Sh.seg {loc= l; bas= l; len= !16; siz= 8 * n; seq= a2})
(Sh.seg (Sh.seg
{loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); arr= a3}) {loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); seq= a3})
let%expect_test _ = let%expect_test _ =
check_frame check_frame
@ -230,7 +230,7 @@ let%test_module _ =
Term.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2)) Term.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2))
seg_split_symbolically) seg_split_symbolically)
[m_; a_] [m_; a_]
(Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -263,7 +263,7 @@ let%test_module _ =
infer_frame infer_frame
(Sh.and_ (Term.le n !2) seg_split_symbolically) (Sh.and_ (Term.le n !2) seg_split_symbolically)
[m_; a_] [m_; a_]
(Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:

89
sledge/src/term.ml
Unescape View File

@ -30,7 +30,7 @@ type op2 =
| Shl | Shl
| Lshr | Lshr
| Ashr | Ashr
| Memory | Sized
| Update of int | Update of int
[@@deriving compare, equal, hash, sexp] [@@deriving compare, equal, hash, sexp]
@ -186,9 +186,9 @@ let rec ppx strength fs term =
| Ap2 (Ashr, x, y) -> pf "(%a@ ashr %a)" pp x pp y | Ap2 (Ashr, x, y) -> pf "(%a@ ashr %a)" pp x pp y
| Ap3 (Conditional, cnd, thn, els) -> | Ap3 (Conditional, cnd, thn, els) ->
pf "(%a@ ? %a@ : %a)" pp cnd pp thn pp els pf "(%a@ ? %a@ : %a)" pp cnd pp thn pp els
| Ap3 (Extract, agg, off, len) -> pf "%a[%a,%a)" pp agg pp off pp len | Ap3 (Extract, seq, off, len) -> pf "%a[%a,%a)" pp seq pp off pp len
| Ap1 (Splat, byt) -> pf "%a^" pp byt | Ap1 (Splat, byt) -> pf "%a^" pp byt
| Ap2 (Memory, siz, arr) -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr | Ap2 (Sized, siz, arr) -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
| ApN (Concat, args) when IArray.is_empty args -> pf "@<2>⟨⟩" | ApN (Concat, args) when IArray.is_empty args -> pf "@<2>⟨⟩"
| ApN (Concat, args) -> pf "(%a)" (IArray.pp "@,^" pp) args | ApN (Concat, args) -> pf "(%a)" (IArray.pp "@,^" pp) args
| ApN (Record, elts) -> pf "{%a}" (pp_record strength) elts | ApN (Record, elts) -> pf "{%a}" (pp_record strength) elts
@ -285,14 +285,14 @@ let assert_polynomial poly =
Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fn.id) Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fn.id)
| _ -> assert false | _ -> assert false
(* aggregate args of Extract and Concat must be aggregate terms, in (* sequence args of Extract and Concat must be sequence terms, in
particular, not variables *) particular, not variables *)
let rec assert_aggregate = function let rec assert_sequence = function
| Ap2 (Memory, _, _) -> () | Ap2 (Sized, _, _) -> ()
| Ap3 (Extract, a, _, _) -> assert_aggregate a | Ap3 (Extract, a, _, _) -> assert_sequence a
| ApN (Concat, a0N) -> | ApN (Concat, a0N) ->
assert (IArray.length a0N <> 1) ; assert (IArray.length a0N <> 1) ;
IArray.iter ~f:assert_aggregate a0N IArray.iter ~f:assert_sequence a0N
| _ -> assert false | _ -> assert false
let invariant e = let invariant e =
@ -302,8 +302,8 @@ let invariant e =
| Or _ -> assert_disjunction e |> Fn.id | Or _ -> assert_disjunction e |> Fn.id
| Add _ -> assert_polynomial e |> Fn.id | Add _ -> assert_polynomial e |> Fn.id
| Mul _ -> assert_monomial e |> Fn.id | Mul _ -> assert_monomial e |> Fn.id
| Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) -> | Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
assert_aggregate e assert_sequence e
| ApN (Record, elts) -> assert (not (IArray.is_empty elts)) | ApN (Record, elts) -> assert (not (IArray.is_empty elts))
| Ap1 (Convert {src= Integer _; dst= Integer _}, _) -> assert false | Ap1 (Convert {src= Integer _; dst= Integer _}, _) -> assert false
| Ap1 (Convert {src; dst}, _) -> | Ap1 (Convert {src; dst}, _) ->
@ -595,27 +595,27 @@ let rec simp_or2 x y =
let simp_or xs = Set.fold xs ~init:false_ ~f:simp_or2 let simp_or xs = Set.fold xs ~init:false_ ~f:simp_or2
(* aggregate sizes *) (* sequence sizes *)
let rec agg_size_exn = function let rec seq_size_exn = function
| Ap2 (Memory, n, _) | Ap3 (Extract, _, _, n) -> n | Ap2 (Sized, n, _) | Ap3 (Extract, _, _, n) -> n
| ApN (Concat, a0U) -> | ApN (Concat, a0U) ->
IArray.fold a0U ~init:zero ~f:(fun a0I aJ -> IArray.fold a0U ~init:zero ~f:(fun a0I aJ ->
simp_add2 a0I (agg_size_exn aJ) ) simp_add2 a0I (seq_size_exn aJ) )
| _ -> invalid_arg "agg_size_exn" | _ -> invalid_arg "seq_size_exn"
let agg_size e = try Some (agg_size_exn e) with Invalid_argument _ -> None let seq_size e = try Some (seq_size_exn e) with Invalid_argument _ -> None
(* memory *) (* sequences *)
let empty_agg = ApN (Concat, IArray.of_array [||]) let empty_seq = ApN (Concat, IArray.of_array [||])
let simp_splat byt = Ap1 (Splat, byt) let simp_splat byt = Ap1 (Splat, byt)
let simp_memory siz arr = let simp_sized siz arr =
(* ⟨n,α⟩ ==> α when n ≡ |α| *) (* ⟨n,α⟩ ==> α when n ≡ |α| *)
match agg_size arr with match seq_size arr with
| Some n when equal siz n -> arr | Some n when equal siz n -> arr
| _ -> Ap2 (Memory, siz, arr) | _ -> Ap2 (Sized, siz, arr)
type pcmp = Lt | Eq | Gt | Unknown type pcmp = Lt | Eq | Gt | Unknown
@ -630,22 +630,22 @@ let partial_compare x y : pcmp =
let partial_ge x y = let partial_ge x y =
match partial_compare x y with Gt | Eq -> true | Lt | Unknown -> false match partial_compare x y with Gt | Eq -> true | Lt | Unknown -> false
let rec simp_extract agg off len = let rec simp_extract seq off len =
[%Trace.call fun {pf} -> pf "%a" pp (Ap3 (Extract, agg, off, len))] [%Trace.call fun {pf} -> pf "%a" pp (Ap3 (Extract, seq, off, len))]
; ;
(* _[_,0) ==> ⟨⟩ *) (* _[_,0) ==> ⟨⟩ *)
( if equal len zero then empty_agg ( if equal len zero then empty_seq
else else
let o_l = simp_add2 off len in let o_l = simp_add2 off len in
match agg with match seq with
(* α[m,k)[o,l) ==> α[m+o,l) when k ≥ o+l *) (* α[m,k)[o,l) ==> α[m+o,l) when k ≥ o+l *)
| Ap3 (Extract, a, m, k) when partial_ge k o_l -> | Ap3 (Extract, a, m, k) when partial_ge k o_l ->
simp_extract a (simp_add2 m off) len simp_extract a (simp_add2 m off) len
(* ⟨n,E^⟩[o,l) ==> ⟨l,E^⟩ when n ≥ o+l *) (* ⟨n,E^⟩[o,l) ==> ⟨l,E^⟩ when n ≥ o+l *)
| Ap2 (Memory, n, (Ap1 (Splat, _) as e)) when partial_ge n o_l -> | Ap2 (Sized, n, (Ap1 (Splat, _) as e)) when partial_ge n o_l ->
simp_memory len e simp_sized len e
(* ⟨n,a⟩[0,n) ==> ⟨n,a⟩ *) (* ⟨n,a⟩[0,n) ==> ⟨n,a⟩ *)
| Ap2 (Memory, n, _) when equal off zero && equal n len -> agg | Ap2 (Sized, n, _) when equal off zero && equal n len -> seq
(* For (α₀^α₁)[o,l) there are 3 cases: (* For (α₀^α₁)[o,l) there are 3 cases:
* *
* ⟨...⟩^⟨...⟩ * ⟨...⟩^⟨...⟩
@ -671,7 +671,7 @@ let rec simp_extract agg off len =
| Integer {data= l} -> | Integer {data= l} ->
IArray.fold_map_until na1N ~init:(l, off) IArray.fold_map_until na1N ~init:(l, off)
~f:(fun (l, oI) naI -> ~f:(fun (l, oI) naI ->
let nI = agg_size_exn naI in let nI = seq_size_exn naI in
if Z.equal Z.zero l then if Z.equal Z.zero l then
Continue ((l, oI), simp_extract naI oI zero) Continue ((l, oI), simp_extract naI oI zero)
else else
@ -682,11 +682,11 @@ let rec simp_extract agg off len =
let lI = Z.(max zero (min l (neg data))) in let lI = Z.(max zero (min l (neg data))) in
let l = Z.(l - lI) in let l = Z.(l - lI) in
Continue ((l, oJ), simp_extract naI oI (integer lI)) Continue ((l, oJ), simp_extract naI oI (integer lI))
| _ -> Stop (Ap3 (Extract, agg, off, len)) ) | _ -> Stop (Ap3 (Extract, seq, off, len)) )
~finish:(fun (_, e1N) -> simp_concat e1N) ~finish:(fun (_, e1N) -> simp_concat e1N)
| _ -> Ap3 (Extract, agg, off, len) ) | _ -> Ap3 (Extract, seq, off, len) )
(* α[o,l) *) (* α[o,l) *)
| _ -> Ap3 (Extract, agg, off, len) ) | _ -> Ap3 (Extract, seq, off, len) )
|> |>
[%Trace.retn fun {pf} -> pf "%a" pp] [%Trace.retn fun {pf} -> pf "%a" pp]
@ -710,16 +710,16 @@ and simp_concat xs =
let simp_adjacent e f = let simp_adjacent e f =
match (e, f) with match (e, f) with
(* ⟨n,a⟩[o,k)^⟨n,a⟩[o+k,l) ==> ⟨n,a⟩[o,k+l) when n ≥ o+k+l *) (* ⟨n,a⟩[o,k)^⟨n,a⟩[o+k,l) ==> ⟨n,a⟩[o,k+l) when n ≥ o+k+l *)
| ( Ap3 (Extract, (Ap2 (Memory, n, _) as na), o, k) | ( Ap3 (Extract, (Ap2 (Sized, n, _) as na), o, k)
, Ap3 (Extract, na', o_k, l) ) , Ap3 (Extract, na', o_k, l) )
when equal na na' when equal na na'
&& equal o_k (simp_add2 o k) && equal o_k (simp_add2 o k)
&& partial_ge n (simp_add2 o_k l) -> && partial_ge n (simp_add2 o_k l) ->
Some (simp_extract na o (simp_add2 k l)) Some (simp_extract na o (simp_add2 k l))
(* ⟨m,E^⟩^⟨n,E^⟩ ==> ⟨m+n,E^⟩ *) (* ⟨m,E^⟩^⟨n,E^⟩ ==> ⟨m+n,E^⟩ *)
| Ap2 (Memory, m, (Ap1 (Splat, _) as a)), Ap2 (Memory, n, a') | Ap2 (Sized, m, (Ap1 (Splat, _) as a)), Ap2 (Sized, n, a')
when equal a a' -> when equal a a' ->
Some (simp_memory (simp_add2 m n) a) Some (simp_sized (simp_add2 m n) a)
| _ -> None | _ -> None
in in
let xs = flatten xs in let xs = flatten xs in
@ -791,17 +791,16 @@ let rec simp_eq x y =
let a = IArray.sub ~pos ~len:(m - length_common) a in let a = IArray.sub ~pos ~len:(m - length_common) a in
let b = IArray.sub ~pos ~len:(n - length_common) b in let b = IArray.sub ~pos ~len:(n - length_common) b in
simp_eq (simp_concat a) (simp_concat b) simp_eq (simp_concat a) (simp_concat b)
| ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) | ( (Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _))
, (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) ) -> , (Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) ) ->
Ap2 (Eq, x, y) Ap2 (Eq, x, y)
(* x = α ==> ⟨x,|α|⟩ = α *) (* x = α ==> ⟨x,|α|⟩ = α *)
| ( x | ( x
, ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as , ((Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as a)
a ) ) )
|( ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as |( ((Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as a)
a )
, x ) -> , x ) ->
simp_eq (Ap2 (Memory, agg_size_exn a, x)) a simp_eq (Ap2 (Sized, seq_size_exn a, x)) a
| x, y -> Ap2 (Eq, x, y) ) | x, y -> Ap2 (Eq, x, y) )
and simp_dq x y = and simp_dq x y =
@ -904,7 +903,7 @@ let norm1 op x =
let norm2 op x y = let norm2 op x y =
( match op with ( match op with
| Memory -> simp_memory x y | Sized -> simp_sized x y
| Eq -> simp_eq x y | Eq -> simp_eq x y
| Dq -> simp_dq x y | Dq -> simp_dq x y
| Lt -> simp_lt x y | Lt -> simp_lt x y
@ -965,8 +964,8 @@ let lshr = norm2 Lshr
let ashr = norm2 Ashr let ashr = norm2 Ashr
let conditional ~cnd ~thn ~els = norm3 Conditional cnd thn els let conditional ~cnd ~thn ~els = norm3 Conditional cnd thn els
let splat byt = norm1 Splat byt let splat byt = norm1 Splat byt
let memory ~siz ~arr = norm2 Memory siz arr let sized ~seq ~siz = norm2 Sized siz seq
let extract ~agg ~off ~len = norm3 Extract agg off len let extract ~seq ~off ~len = norm3 Extract seq off len
let concat xs = normN Concat (IArray.of_array xs) let concat xs = normN Concat (IArray.of_array xs)
let record elts = normN Record elts let record elts = normN Record elts
let select ~rcd ~idx = norm1 (Select idx) rcd let select ~rcd ~idx = norm1 (Select idx) rcd

16
sledge/src/term.mli
Unescape View File

@ -43,13 +43,13 @@ type op2 =
| Shl (** Shift left, bitwise *) | Shl (** Shift left, bitwise *)
| Lshr (** Logical shift right, bitwise *) | Lshr (** Logical shift right, bitwise *)
| Ashr (** Arithmetic shift right, bitwise *) | Ashr (** Arithmetic shift right, bitwise *)
| Memory (** Size-tagged byte-array *) | Sized (** Size-tagged sequence *)
| Update of int (** Constant record with updated index *) | Update of int (** Constant record with updated index *)
[@@deriving compare, equal, hash, sexp] [@@deriving compare, equal, hash, sexp]
type op3 = type op3 =
| Conditional (** If-then-else *) | Conditional (** If-then-else *)
| Extract (** Extract a slice of an aggregate value *) | Extract (** Extract a slice of an sequence value *)
[@@deriving compare, equal, hash, sexp] [@@deriving compare, equal, hash, sexp]
type opN = type opN =
@ -217,14 +217,14 @@ val ashr : t -> t -> t
(* if-then-else *) (* if-then-else *)
val conditional : cnd:t -> thn:t -> els:t -> t val conditional : cnd:t -> thn:t -> els:t -> t
(* aggregate sizes *) (* sequence sizes *)
val agg_size_exn : t -> t val seq_size_exn : t -> t
val agg_size : t -> t option val seq_size : t -> t option
(* aggregates (memory contents) *) (* sequences *)
val splat : t -> t val splat : t -> t
val memory : siz:t -> arr:t -> t val sized : seq:t -> siz:t -> t
val extract : agg:t -> off:t -> len:t -> t val extract : seq:t -> off:t -> len:t -> t
val concat : t array -> t val concat : t array -> t
(* records (struct / array values) *) (* records (struct / array values) *)

Write Preview
Loading…
Cancel
Save