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

[sledge] Rename Sh.seg.seq to cnt

Browse Source 
Summary:
The `seq` name of this field refers to the expected sort of it's
value, where the others refer to the role they play. So rename
seq (for sequence) to cnt (for contents).

Reviewed By: ngorogiannis

Differential Revision: D24951507

fbshipit-source-id: fd6640517
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 79d65a83df
commit f02952c003
7 changed files with 132 additions and 127 deletions
Show Stats Download Patch File Download Diff File

12
sledge/src/domain_sh.ml
Unescape View File

@ -30,8 +30,8 @@ let init globals =
| _ -> violates Llair.GlobalDefn.invariant global | _ -> violates Llair.GlobalDefn.invariant global
in in
let len = Term.integer (Z.of_int siz) in let len = Term.integer (Z.of_int siz) in
let seq = X.term seq in let cnt = X.term seq in
Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; seq}) Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; cnt})
| _ -> q ) | _ -> q )
let join p q = let join p q =
@ -93,7 +93,7 @@ let garbage_collect (q : Sh.t) ~wrt =
let new_set = let new_set =
List.fold q.heap current ~f:(fun seg current -> List.fold q.heap current ~f:(fun seg current ->
if value_determined_by q.ctx current seg.loc then if value_determined_by q.ctx current seg.loc then
List.fold (Context.class_of q.ctx seg.seq) current List.fold (Context.class_of q.ctx seg.cnt) current
~f:(fun e c -> ~f:(fun e c ->
Term.Set.union c (Term.Set.of_iter (Term.atoms e)) ) Term.Set.union c (Term.Set.of_iter (Term.atoms e)) )
else current ) else current )
@ -324,9 +324,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; seq= a} let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; cnt= a}
let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= endV} let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; cnt= endV}
let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= main} let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; cnt= main}
let%expect_test _ = let%expect_test _ =
pp (garbage_collect seg_main ~wrt:(Term.Set.of_list [])) ; pp (garbage_collect seg_main ~wrt:(Term.Set.of_list [])) ;

84
sledge/src/exec.ml
Unescape View File

@ -28,7 +28,7 @@ module Fresh : sig
?bas:Term.t ?bas:Term.t
-> ?len:Term.t -> ?len:Term.t
-> ?siz:Term.t -> ?siz:Term.t
-> ?seq:Term.t -> ?cnt:Term.t
-> Term.t -> Term.t
-> Sh.seg t -> Sh.seg t
(** Segment with fresh variables for omitted arguments. *) (** Segment with fresh variables for omitted arguments. *)
@ -55,15 +55,15 @@ end = struct
let xs = Var.Set.add x xs in let xs = Var.Set.add x xs in
return (Term.var x) {wrt; xs} return (Term.var x) {wrt; xs}
let seg ?bas ?len ?siz ?seq loc = let seg ?bas ?len ?siz ?cnt loc =
let freshen term nam = let freshen term nam =
match term with Some term -> return term | None -> var nam match term with Some term -> return term | None -> var nam
in in
let* bas = freshen bas "b" in let* bas = freshen bas "b" in
let* len = freshen len "m" in let* len = freshen len "m" in
let* siz = freshen siz "n" in let* siz = freshen siz "n" in
let* seq = freshen seq "a" in let* cnt = freshen cnt "a" in
return Sh.{loc; bas; len; siz; seq} return Sh.{loc; bas; len; siz; cnt}
let assign ~ws ~rs {wrt; xs} = let assign ~ws ~rs {wrt; xs} =
let ovs = Var.Set.inter ws rs in let ovs = Var.Set.inter ws rs in
@ -89,9 +89,11 @@ let gen_spec us specm =
let null_eq ptr = Sh.pure (Formula.eq0 ptr) let null_eq ptr = Sh.pure (Formula.eq0 ptr)
let eq_concat (siz, seq) ms = let eq_concat (siz, cnt) ms =
Formula.eq (Term.sized ~siz ~seq) Formula.eq
(Term.concat (Array.map ~f:(fun (siz, seq) -> Term.sized ~siz ~seq) ms)) (Term.sized ~siz ~seq:cnt)
(Term.concat
(Array.map ~f:(fun (siz, cnt) -> Term.sized ~siz ~seq:cnt) ms))
open Fresh.Import open Fresh.Import
@ -123,7 +125,7 @@ let load_spec reg ptr len =
let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
let post = let post =
Sh.and_ Sh.and_
(Formula.eq (Term.var reg) (Term.rename sub seg.seq)) (Formula.eq (Term.var reg) (Term.rename sub seg.cnt))
(Sh.rename sub foot) (Sh.rename sub foot)
in in
{foot; sub; ms; post} {foot; sub; ms; post}
@ -135,7 +137,7 @@ let load_spec reg ptr len =
let store_spec ptr exp len = let store_spec ptr exp len =
let+ seg = Fresh.seg ptr ~siz:len in let+ seg = Fresh.seg ptr ~siz:len in
let foot = Sh.seg seg in let foot = Sh.seg seg in
let post = Sh.seg {seg with seq= exp} in let post = Sh.seg {seg with cnt= exp} in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
(* { d-[b;m)->⟨l,α⟩ } (* { d-[b;m)->⟨l,α⟩ }
@ -145,7 +147,7 @@ let store_spec ptr exp len =
let memset_spec dst byt len = let memset_spec dst byt len =
let+ seg = Fresh.seg dst ~siz:len in let+ seg = Fresh.seg dst ~siz:len in
let foot = Sh.seg seg in let foot = Sh.seg seg in
let post = Sh.seg {seg with seq= Term.splat byt} in let post = Sh.seg {seg with cnt= Term.splat byt} in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {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,α⟩ }
@ -170,7 +172,7 @@ let memcpy_dj_spec dst src len =
let dst_heap = Sh.seg dst_seg in let dst_heap = Sh.seg dst_seg in
let+ src_seg = Fresh.seg src ~siz:len in let+ src_seg = Fresh.seg src ~siz:len in
let src_heap = Sh.seg src_seg in let src_heap = Sh.seg src_seg in
let dst_seg' = {dst_seg with seq= src_seg.seq} in let dst_seg' = {dst_seg with cnt= src_seg.cnt} 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
@ -200,23 +202,23 @@ let memmov_dj_spec = memcpy_dj_spec
let memmov_foot dst src len = let memmov_foot dst src len =
let* bas = Fresh.var "b" in let* bas = Fresh.var "b" in
let* siz = Fresh.var "m" in let* siz = Fresh.var "m" in
let* seq_dst = Fresh.var "a" in let* cnt_dst = Fresh.var "a" in
let* seq_mid = Fresh.var "a" in let* cnt_mid = Fresh.var "a" in
let* seq_src = Fresh.var "a" in let* cnt_src = Fresh.var "a" in
let src_dst = Term.sub src dst in let src_dst = Term.sub src dst in
let mem_dst = (src_dst, seq_dst) in let mem_dst = (src_dst, cnt_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, seq_mid) in let mem_mid = (siz_mid, cnt_mid) in
let mem_src = (src_dst, seq_src) in let mem_src = (src_dst, cnt_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 = Fresh.var "m" in let* siz_dst_mid_src = Fresh.var "m" in
let+ seq_dst_mid_src = Fresh.var "a" in let+ cnt_dst_mid_src = Fresh.var "a" in
let eq_mem_dst_mid_src = let eq_mem_dst_mid_src =
eq_concat (siz_dst_mid_src, seq_dst_mid_src) mem_dst_mid_src eq_concat (siz_dst_mid_src, cnt_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; seq= seq_dst_mid_src} {loc= dst; bas; len= siz; siz= siz_dst_mid_src; cnt= cnt_dst_mid_src}
in in
let foot = let foot =
Sh.and_ eq_mem_dst_mid_src Sh.and_ eq_mem_dst_mid_src
@ -233,9 +235,9 @@ let memmov_dn_spec dst src len =
let* bas, siz, _, mem_mid, mem_src, foot = memmov_foot dst src len in let* bas, siz, _, mem_mid, mem_src, foot = memmov_foot dst src len 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 = Fresh.var "m" in let* siz_mid_src_src = Fresh.var "m" in
let+ seq_mid_src_src = Fresh.var "a" in let+ cnt_mid_src_src = Fresh.var "a" in
let eq_mem_mid_src_src = let eq_mem_mid_src_src =
eq_concat (siz_mid_src_src, seq_mid_src_src) mem_mid_src_src eq_concat (siz_mid_src_src, cnt_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
@ -244,7 +246,7 @@ let memmov_dn_spec dst src len =
; bas ; bas
; len= siz ; len= siz
; siz= siz_mid_src_src ; siz= siz_mid_src_src
; seq= seq_mid_src_src }) ; cnt= cnt_mid_src_src })
in in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -256,9 +258,9 @@ let memmov_up_spec dst src len =
let* bas, siz, mem_src, mem_mid, _, foot = memmov_foot src dst len in let* bas, siz, mem_src, mem_mid, _, foot = memmov_foot src dst len 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 = Fresh.var "m" in let* siz_src_src_mid = Fresh.var "m" in
let+ seq_src_src_mid = Fresh.var "a" in let+ cnt_src_src_mid = Fresh.var "a" in
let eq_mem_src_src_mid = let eq_mem_src_src_mid =
eq_concat (siz_src_src_mid, seq_src_src_mid) mem_src_src_mid eq_concat (siz_src_src_mid, cnt_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
@ -267,7 +269,7 @@ let memmov_up_spec dst src len =
; bas ; bas
; len= siz ; len= siz
; siz= siz_src_src_mid ; siz= siz_src_src_mid
; seq= seq_src_src_mid }) ; cnt= cnt_src_src_mid })
in in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -353,8 +355,8 @@ let calloc_spec reg num len =
let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) in let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) 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 seq = Term.splat Term.zero in let cnt = Term.splat Term.zero in
let+ seg = Fresh.seg loc ~bas:loc ~len:siz ~siz ~seq in let+ seg = Fresh.seg loc ~bas:loc ~len:siz ~siz ~cnt 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
{foot; sub; ms; post} {foot; sub; ms; post}
@ -374,7 +376,7 @@ let posix_memalign_spec reg ptr siz =
~rs:(Var.Set.union foot.us (Term.fv siz)) ~rs:(Var.Set.union foot.us (Term.fv siz))
in in
let* q = Fresh.var "q" in let* q = Fresh.var "q" in
let pseg' = {pseg with seq= q} in let pseg' = {pseg with cnt= q} in
let+ qseg = Fresh.seg q ~bas:q ~len:siz ~siz in let+ qseg = Fresh.seg q ~bas:q ~len:siz ~siz in
let eok = Term.zero in let eok = Term.zero in
let enomem = Term.integer (Z.of_int 12) in let enomem = Term.integer (Z.of_int 12) in
@ -404,8 +406,8 @@ let realloc_spec 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* rseg = Fresh.seg loc ~bas:loc ~len:siz ~siz in let* rseg = Fresh.seg loc ~bas:loc ~len:siz ~siz in
let a0 = pseg.seq in let a0 = pseg.cnt in
let a1 = rseg.seq in let a1 = rseg.cnt in
let+ a2 = Fresh.var "a" in let+ a2 = Fresh.var "a" in
let post = let post =
Sh.or_ Sh.or_
@ -433,8 +435,8 @@ let rallocx_spec 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* rseg = Fresh.seg loc ~bas:loc ~len:siz ~siz in let* rseg = Fresh.seg loc ~bas:loc ~len:siz ~siz in
let a0 = pseg.seq in let a0 = pseg.cnt in
let a1 = rseg.seq in let a1 = rseg.cnt in
let+ a2 = Fresh.var "a" in let+ a2 = Fresh.var "a" in
let post = let post =
Sh.or_ Sh.or_
@ -465,8 +467,8 @@ let xallocx_spec reg ptr siz ext =
let siz = Term.rename sub siz in let siz = Term.rename sub siz in
let ext = Term.rename sub ext in let ext = Term.rename sub ext in
let* seg' = Fresh.seg ptr ~bas:ptr ~len:reg ~siz:reg in let* seg' = Fresh.seg ptr ~bas:ptr ~len:reg ~siz:reg in
let a0 = seg.seq in let a0 = seg.cnt in
let a1 = seg'.seq in let a1 = seg'.cnt in
let+ a2 = Fresh.var "a" in let+ a2 = Fresh.var "a" in
let post = let post =
Sh.and_ Sh.and_
@ -524,13 +526,13 @@ let size_of_int_mul = Term.mulq (Q.of_int Llair.Typ.(size_of siz))
*) *)
let mallctl_read_spec r i w n = let mallctl_read_spec r i w n =
let* iseg = Fresh.seg i in let* iseg = Fresh.seg i in
let* rseg = Fresh.seg r ~siz:iseg.seq in let* rseg = Fresh.seg r ~siz:iseg.cnt in
let+ a = Fresh.var "a" in let+ a = Fresh.var "a" in
let foot = let foot =
Sh.and_ (Formula.eq0 w) Sh.and_ (Formula.eq0 w)
(Sh.and_ (Formula.eq0 n) (Sh.star (Sh.seg iseg) (Sh.seg rseg))) (Sh.and_ (Formula.eq0 n) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
in in
let rseg' = {rseg with seq= a} in let rseg' = {rseg with cnt= a} in
let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -543,7 +545,7 @@ let mallctlbymib_read_spec p l r i w n =
let wl = size_of_int_mul l in let wl = size_of_int_mul l in
let* pseg = Fresh.seg p ~siz:wl in let* pseg = Fresh.seg p ~siz:wl in
let* iseg = Fresh.seg i in let* iseg = Fresh.seg i in
let m = iseg.seq in let m = iseg.cnt in
let* rseg = Fresh.seg r ~siz:m in let* rseg = Fresh.seg r ~siz:m 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 = Fresh.var "a" in let+ a = Fresh.var "a" in
@ -551,7 +553,7 @@ let mallctlbymib_read_spec p l r i w n =
Sh.and_ (Formula.eq0 w) Sh.and_ (Formula.eq0 w)
(Sh.and_ (Formula.eq0 n) (Sh.star const (Sh.seg rseg))) (Sh.and_ (Formula.eq0 n) (Sh.star const (Sh.seg rseg)))
in in
let rseg' = {rseg with seq= a} in let rseg' = {rseg with cnt= a} in
let post = Sh.star (Sh.seg rseg') const in let post = Sh.star (Sh.seg rseg') const in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -596,12 +598,12 @@ let mallctlbymib_specs p j r i w n =
*) *)
let mallctlnametomib_spec p o = let mallctlnametomib_spec p o =
let* oseg = Fresh.seg o in let* oseg = Fresh.seg o in
let n = oseg.seq in let n = oseg.cnt in
let wn = size_of_int_mul n in let wn = size_of_int_mul n in
let* pseg = Fresh.seg p ~siz:wn in let* pseg = Fresh.seg p ~siz:wn in
let+ a = Fresh.var "a" in let+ a = Fresh.var "a" 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 seq= a} in let pseg' = {pseg with cnt= a} in
let post = Sh.star (Sh.seg pseg') (Sh.seg oseg) in let post = Sh.star (Sh.seg pseg') (Sh.seg oseg) in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}

20
sledge/src/sh.ml
Unescape View File

@ -11,7 +11,7 @@ open Fol
[@@@warning "+9"] [@@@warning "+9"]
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; cnt: Term.t}
[@@deriving compare, equal, sexp] [@@deriving compare, equal, sexp]
type starjunction = type starjunction =
@ -46,18 +46,18 @@ 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 seq = f h.seq in let cnt = f h.cnt 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
&& seq == h.seq && cnt == h.cnt
then h then h
else {loc; bas; len; siz; seq} else {loc; bas; len; siz; cnt}
let fold_terms_seg {loc; bas; len; siz; seq} s ~f = let fold_terms_seg {loc; bas; len; siz; cnt} s ~f =
f loc (f bas (f len (f siz (f seq s)))) f loc (f bas (f len (f siz (f cnt s))))
let fold_vars_seg seg s ~f = let fold_vars_seg seg s ~f =
fold_terms_seg ~f:(Iter.fold ~f << Term.vars) seg s fold_terms_seg ~f:(Iter.fold ~f << Term.vars) seg s
@ -109,15 +109,15 @@ let var_strength ?(xs = Var.Set.empty) q =
in in
var_strength_ xs m q var_strength_ xs m q
let pp_chunk x fs (siz, seq) = Term.ppx x fs (Term.sized ~siz ~seq) let pp_chunk x fs (siz, cnt) = Term.ppx x fs (Term.sized ~siz ~seq:cnt)
let pp_seg x fs {loc; bas; len; siz; seq} = let pp_seg x fs {loc; bas; len; siz; cnt} =
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_chunk x) (siz, seq) (bas, len) (pp_chunk x) (siz, cnt)
let pp_seg_norm ctx fs seg = let pp_seg_norm ctx fs seg =
let x _ = None in let x _ = None in
@ -144,7 +144,7 @@ let pp_block x fs segs =
in in
let term_pp = Term.ppx x in let term_pp = Term.ppx x in
let pp_chunks = let pp_chunks =
List.pp "@,^" (fun fs seg -> pp_chunk x fs (seg.siz, seg.seq)) List.pp "@,^" (fun fs seg -> pp_chunk x fs (seg.siz, seg.cnt))
in in
match segs with match segs with
| {loc; bas; len; _} :: _ -> | {loc; bas; len; _} :: _ ->

11
sledge/src/sh.mli
Unescape View File

@ -9,10 +9,13 @@
open Fol open Fol
(** Segment of memory starting at [loc] containing [seq] (a byte-array) of (** Segment of memory. *)
size [siz], contained in an enclosing allocation-block starting at [bas] type seg =
of length [len]. *) { loc: Term.t (** location (address) where segment starts *)
type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t} ; bas: Term.t (** base address of enclosing allocation-block *)
; len: Term.t (** length of enclosing allocation-block *)
; siz: Term.t (** size of segment / length of the contents *)
; cnt: Term.t (** contents of segment, a sequence / byte array *) }
type starjunction = private type starjunction = private
{ us: Var.Set.t (** vocabulary / variable context of formula *) { us: Var.Set.t (** vocabulary / variable context of formula *)

70
sledge/src/solver.ml
Unescape View File

@ -194,8 +194,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.ctx) pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.ctx)
msg (Sh.pp_seg_norm sub.ctx) ssg ) ; msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.bas= b; len= m; seq= a} = msg in let {Sh.bas= b; len= m; cnt= a} = msg in
let {Sh.bas= b'; len= m'; seq= a'} = ssg in let {Sh.bas= b'; len= m'; cnt= 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 =
@ -223,18 +223,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.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
let {Sh.bas= b'; len= m'; siz= n; seq= a'} = ssg in let {Sh.bas= b'; len= m'; siz= n; cnt= 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; seq= a0}) com in let com = Sh.star (Sh.seg {msg with siz= n; cnt= 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; seq= a1}) (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; cnt= a1})
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
@ -263,8 +263,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.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.bas= b; len= m; siz= o; seq= a} = msg in let {Sh.bas= b; len= m; siz= o; cnt= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= 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
@ -276,7 +276,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; seq= a1'}) {loc= Term.add l o; bas= b'; len= m'; siz= n_o; cnt= 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
@ -299,20 +299,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.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= 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; seq= a1}) com Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= 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; seq= a0}) (Sh.seg {loc= k; bas= b; len= m; siz= l_k; cnt= a0})
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
@ -341,8 +341,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.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= 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
@ -351,15 +351,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; seq= a1}) com Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= 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; seq= a0}) (Sh.seg {loc= k; bas= b; len= m; siz= l_k; cnt= a0})
(Sh.star (Sh.star
(Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; seq= a2}) (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; cnt= a2})
(Sh.rem_seg msg min))) (Sh.rem_seg msg min)))
in in
let sub = let sub =
@ -388,8 +388,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.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= 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
@ -399,13 +399,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; seq= a1}) com Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; cnt= 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; seq= a0}) (Sh.seg {loc= k; bas= b; len= m; siz= l_k; cnt= a0})
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
@ -414,7 +414,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; seq= a2'}) (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; cnt= 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
@ -438,8 +438,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.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.bas= b; len= m; siz= o; seq= a} = msg in let {Sh.bas= b; len= m; siz= o; cnt= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= 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
@ -450,7 +450,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; seq= a0'}) (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; cnt= 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
@ -475,8 +475,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.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= 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
@ -490,9 +490,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; seq= a0'}) (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; cnt= a0'})
(Sh.star (Sh.star
(Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; seq= a2'}) (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; cnt= 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
@ -516,8 +516,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.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= 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
@ -526,13 +526,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; seq= a1}) com Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= ln_k; cnt= 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; seq= a2}) (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; cnt= a2})
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
@ -541,7 +541,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; seq= a0'}) (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; cnt= 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

4
sledge/src/test/sh_test.ml
Unescape View File

@ -58,8 +58,8 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
pp pp
(star (star
(seg {loc= x; bas= x; len= !16; siz= !8; seq= a}) (seg {loc= x; bas= x; len= !16; siz= !8; cnt= a})
(seg {loc= x + !8; bas= x; len= !16; siz= !8; seq= b})) ; (seg {loc= x + !8; bas= x; len= !16; siz= !8; cnt= b})) ;
[%expect {| [%expect {|
%x_6 -[)-> ⟨8,%a_1⟩^⟨8,%b_2⟩ |}] %x_6 -[)-> ⟨8,%a_1⟩^⟨8,%b_2⟩ |}]

58
sledge/src/test/solver_test.ml
Unescape View File

@ -78,7 +78,7 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
check_frame check_frame
(Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a})
[] Sh.emp ; [] Sh.emp ;
[%expect [%expect
{| {|
@ -87,9 +87,9 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
check_frame check_frame
(Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a})
[] []
(Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) ; (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -98,8 +98,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; seq= a2} in let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; cnt= a2} in
let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; seq= a} in let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; cnt= a} in
let minued = Sh.star common seg1 in let minued = Sh.star common seg1 in
let subtrahend = let subtrahend =
Sh.and_ (Formula.eq m n) Sh.and_ (Formula.eq m n)
@ -120,10 +120,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; seq= a}) (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a})
(Sh.seg {loc= l2; bas= b; len= m; siz= n; seq= a2})) (Sh.seg {loc= l2; bas= b; len= m; siz= n; cnt= a2}))
[] []
(Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) ; (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -135,10 +135,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; seq= a}) (Sh.seg {loc= l; bas= l; len= !16; siz= !8; cnt= a})
(Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2})) (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; cnt= a2}))
[a3_] [a3_]
(Sh.seg {loc= l; bas= l; len= !16; siz= !16; seq= a3}) ; (Sh.seg {loc= l; bas= l; len= !16; siz= !16; cnt= a3}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -148,10 +148,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; seq= a}) (Sh.seg {loc= l; bas= l; len= !16; siz= !8; cnt= a})
(Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2})) (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; cnt= a2}))
[a3_; m_] [a3_; m_]
(Sh.seg {loc= l; bas= l; len= m; siz= !16; seq= a3}) ; (Sh.seg {loc= l; bas= l; len= m; siz= !16; cnt= a3}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -164,10 +164,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; seq= a}) (Sh.seg {loc= l; bas= l; len= !16; siz= !8; cnt= a})
(Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2})) (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; cnt= a2}))
[a3_; m_] [a3_; m_]
(Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a3}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a3}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -180,12 +180,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; seq= a}) (Sh.seg {loc= k; bas= k; len= !16; siz= !32; cnt= a})
(Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= !16})) (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= !16}))
[a2_; m_; n_] [a2_; m_; n_]
(Sh.star (Sh.star
(Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= n}) (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= n})
(Sh.seg {loc= k; bas= k; len= m; siz= n; seq= a2})) ; (Sh.seg {loc= k; bas= k; len= m; siz= n; cnt= a2})) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -202,12 +202,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; seq= a}) (Sh.seg {loc= k; bas= k; len= !16; siz= !32; cnt= a})
(Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= !16})) (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= !16}))
[a2_; m_; n_] [a2_; m_; n_]
(Sh.star (Sh.star
(Sh.seg {loc= k; bas= k; len= m; siz= n; seq= a2}) (Sh.seg {loc= k; bas= k; len= m; siz= n; cnt= a2})
(Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= n})) ; (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= n})) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -223,9 +223,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; seq= a2}) (Sh.seg {loc= l; bas= l; len= !16; siz= 8 * n; cnt= a2})
(Sh.seg (Sh.seg
{loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); seq= a3}) {loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); cnt= a3})
let%expect_test _ = let%expect_test _ =
check_frame check_frame
@ -233,7 +233,7 @@ let%test_module _ =
Formula.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2)) Formula.(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; seq= a}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:
@ -266,7 +266,7 @@ let%test_module _ =
infer_frame infer_frame
(Sh.and_ (Formula.le n !2) seg_split_symbolically) (Sh.and_ (Formula.le n !2) seg_split_symbolically)
[m_; a_] [m_; a_]
(Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ;
[%expect [%expect
{| {|
( infer_frame: ( infer_frame:

Write Preview
Loading…
Cancel
Save