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

[sledge] Some simplifications using let+

Browse Source 
Reviewed By: jvillard

Differential Revision: D18738850

fbshipit-source-id: dc3477fe7
master
Josh Berdine 5 years ago committed by Facebook Github Bot
parent f60ce32125
commit c9449cce77
5 changed files with 79 additions and 82 deletions
Show Stats Download Patch File Download Diff File

4
sledge/src/control.ml
Unescape View File

@ -271,8 +271,8 @@ module Make (Dom : Domain_sig.Dom) = struct
else else
let maybe_summary_post = let maybe_summary_post =
let state = fst (domain_call ~summaries:false state) in let state = fst (domain_call ~summaries:false state) in
Hashtbl.find summary_table name.reg let* summary = Hashtbl.find summary_table name.reg in
>>= List.find_map ~f:(Dom.apply_summary state) List.find_map ~f:(Dom.apply_summary state) summary
in in
[%Trace.info [%Trace.info
"Maybe summary post: %a" (Option.pp "%a" Dom.pp) "Maybe summary post: %a" (Option.pp "%a" Dom.pp)

21
sledge/src/domain/itv.ml
Unescape View File

@ -8,7 +8,6 @@
(** Interval abstract domain *) (** Interval abstract domain *)
open Apron open Apron
open Option.Let_syntax
let equal_apron_typ = let equal_apron_typ =
(* Apron.Texpr1.typ is a sum of nullary constructors *) (* Apron.Texpr1.typ is a sum of nullary constructors *)
@ -77,7 +76,7 @@ let rec pow base typ = function
let rec texpr_of_nary_term subtms typ q op = let rec texpr_of_nary_term subtms typ q op =
assert (Qset.length subtms >= 2) ; assert (Qset.length subtms >= 2) ;
let term_to_texpr (tm, coeff) = let term_to_texpr (tm, coeff) =
let%bind base = apron_texpr_of_llair_term tm q typ in let* base = apron_texpr_of_llair_term tm q typ in
match op with match op with
| Texpr1.Add -> | Texpr1.Add ->
Some Some
@ -91,8 +90,8 @@ let rec texpr_of_nary_term subtms typ q op =
match Qset.to_list subtms with match Qset.to_list subtms with
| hd :: tl -> | hd :: tl ->
List.fold tl ~init:(term_to_texpr hd) ~f:(fun acc curr -> List.fold tl ~init:(term_to_texpr hd) ~f:(fun acc curr ->
let%bind c = term_to_texpr curr in let* c = term_to_texpr curr in
let%map a = acc in let+ a = acc in
Texpr1.Binop (op, c, a, typ, Texpr0.Rnd) ) Texpr1.Binop (op, c, a, typ, Texpr0.Rnd) )
| _ -> assert false | _ -> assert false
@ -115,21 +114,21 @@ and apron_texpr_of_llair_term tm q typ =
let subtm = apron_texpr_of_llair_term t q src in let subtm = apron_texpr_of_llair_term t q src in
if equal_apron_typ src dst then subtm if equal_apron_typ src dst then subtm
else else
let%bind t = subtm in let+ t = subtm in
Some (Texpr1.Unop (Texpr1.Cast, t, dst, Texpr0.Rnd)) ) Texpr1.Unop (Texpr1.Cast, t, dst, Texpr0.Rnd) )
(* extraction to unsigned 1-bit int is llvm encoding of C boolean; (* extraction to unsigned 1-bit int is llvm encoding of C boolean;
restrict to [0,1] *) restrict to [0,1] *)
| Ap1 (Unsigned {bits= 1}, _t) -> Some (Texpr1.Cst (Coeff.i_of_int 0 1)) | Ap1 (Unsigned {bits= 1}, _t) -> Some (Texpr1.Cst (Coeff.i_of_int 0 1))
(* "t xor true" and "true xor t" are negation *) (* "t xor true" and "true xor t" are negation *)
| Ap2 (Xor, t, Integer {data}) when Z.is_true data -> | Ap2 (Xor, t, Integer {data}) when Z.is_true data ->
let%map t = apron_texpr_of_llair_term t q typ in let+ t = apron_texpr_of_llair_term t q typ in
Texpr1.Unop (Texpr1.Neg, t, typ, Texpr0.Rnd) Texpr1.Unop (Texpr1.Neg, t, typ, Texpr0.Rnd)
| Ap2 (Xor, Integer {data}, t) when Z.is_true data -> | Ap2 (Xor, Integer {data}, t) when Z.is_true data ->
let%map t = apron_texpr_of_llair_term t q typ in let+ t = apron_texpr_of_llair_term t q typ in
Texpr1.Unop (Texpr1.Neg, t, typ, Texpr0.Rnd) Texpr1.Unop (Texpr1.Neg, t, typ, Texpr0.Rnd)
(* query apron for abstract evaluation of binary operations*) (* query apron for abstract evaluation of binary operations*)
| Ap2 (op, t1, t2) -> | Ap2 (op, t1, t2) ->
let%bind f = let* f =
match op with match op with
| Rem -> Some (mk_arith_binop typ Texpr0.Mod) | Rem -> Some (mk_arith_binop typ Texpr0.Mod)
| Div -> Some (mk_arith_binop typ Texpr0.Div) | Div -> Some (mk_arith_binop typ Texpr0.Div)
@ -139,8 +138,8 @@ and apron_texpr_of_llair_term tm q typ =
| Le -> Some (Fn.flip (mk_bool_binop typ q Tcons0.SUPEQ)) | Le -> Some (Fn.flip (mk_bool_binop typ q Tcons0.SUPEQ))
| _ -> None | _ -> None
in in
let%bind te1 = apron_texpr_of_llair_term t1 q typ in let* te1 = apron_texpr_of_llair_term t1 q typ in
let%map te2 = apron_texpr_of_llair_term t2 q typ in let+ te2 = apron_texpr_of_llair_term t2 q typ in
f te1 te2 f te1 te2
| x -> | x ->
[%Trace.info [%Trace.info

42
sledge/src/domain/relation.ml
Unescape View File

@ -32,17 +32,16 @@ module Make (State_domain : State_domain_sig) = struct
let init globals = embed (State_domain.init globals) let init globals = embed (State_domain.init globals)
let join (entry_a, current_a) (entry_b, current_b) = let join (entry_a, current_a) (entry_b, current_b) =
if State_domain.equal entry_b entry_a then if State_domain.equal entry_a entry_b then
State_domain.join current_a current_b let+ next = State_domain.join current_a current_b in
>>= fun curr -> Some (entry_a, curr) (entry_a, next)
else None else None
let is_false (_, curr) = State_domain.is_false curr let is_false (_, curr) = State_domain.is_false curr
let exec_assume (entry, current) cnd = let exec_assume (entry, current) cnd =
match State_domain.exec_assume current cnd with let+ next = State_domain.exec_assume current cnd in
| Some current -> Some (entry, current) (entry, next)
| None -> None
let exec_kill (entry, current) reg = let exec_kill (entry, current) reg =
(entry, State_domain.exec_kill current reg) (entry, State_domain.exec_kill current reg)
@ -51,16 +50,17 @@ module Make (State_domain : State_domain_sig) = struct
(entry, State_domain.exec_move current reg_exps) (entry, State_domain.exec_move current reg_exps)
let exec_inst (entry, current) inst = let exec_inst (entry, current) inst =
State_domain.exec_inst current inst >>| fun current -> (entry, current) let+ next = State_domain.exec_inst current inst in
(entry, next)
let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals
= =
State_domain.exec_intrinsic ~skip_throw current areturn intrinsic let+ next_opt =
actuals State_domain.exec_intrinsic ~skip_throw current areturn intrinsic
|> function actuals
| Some (Some current) -> Some (Some (entry, current)) in
| Some None -> Some None let+ next = next_opt in
| None -> None (entry, next)
type from_call = type from_call =
{state_from_call: State_domain.from_call; caller_entry: State_domain.t} {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
@ -105,22 +105,20 @@ module Make (State_domain : State_domain_sig) = struct
List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current) List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current)
let resolve_callee f e (entry, current) = let resolve_callee f e (entry, current) =
let callees, current = State_domain.resolve_callee f e current in let callees, next = State_domain.resolve_callee f e current in
(callees, (entry, current)) (callees, (entry, next))
type summary = State_domain.summary type summary = State_domain.summary
let pp_summary = State_domain.pp_summary let pp_summary = State_domain.pp_summary
let create_summary ~locals ~formals (entry, current) = let create_summary ~locals ~formals (entry, current) =
let fs, current = let fs, next =
State_domain.create_summary ~locals ~formals ~entry ~current State_domain.create_summary ~locals ~formals ~entry ~current
in in
(fs, (entry, current)) (fs, (entry, next))
let apply_summary rel summ = let apply_summary (entry, current) summ =
let entry, current = rel in let+ next = State_domain.apply_summary current summ in
Option.map (entry, next)
~f:(fun c -> (entry, c))
(State_domain.apply_summary current summ)
end end

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

@ -635,31 +635,30 @@ let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) =
(* execute a command with given spec from pre *) (* execute a command with given spec from pre *)
let exec_spec pre0 {xs; foot; sub; ms; post} = let exec_spec pre0 {xs; foot; sub; ms; post} =
[%Trace.call fun {pf} -> ([%Trace.call fun {pf} ->
pf "@[%a@]@ @[<2>%a@,@[<hv>{%a %a}@;<1 -1>%a--@ {%a }@]@]" Sh.pp pre0 pf "@[%a@]@ @[<2>%a@,@[<hv>{%a %a}@;<1 -1>%a--@ {%a }@]@]" Sh.pp pre0
(Sh.pp_us ~pre:"@<2>∀ ") (Sh.pp_us ~pre:"@<2>∀ ")
xs Sh.pp foot xs Sh.pp foot
(fun fs sub -> (fun fs sub ->
if not (Var.Subst.is_empty sub) then if not (Var.Subst.is_empty sub) then
Format.fprintf fs "∧ %a" Var.Subst.pp sub ) Format.fprintf fs "∧ %a" Var.Subst.pp sub )
sub sub
(fun fs ms -> (fun fs ms ->
if not (Set.is_empty ms) then if not (Set.is_empty ms) then
Format.fprintf fs "%a := " Var.Set.pp ms ) Format.fprintf fs "%a := " Var.Set.pp ms )
ms Sh.pp post ; ms Sh.pp post ;
assert ( assert (
let vs = Set.diff (Set.diff foot.us xs) pre0.us in let vs = Set.diff (Set.diff foot.us xs) pre0.us in
Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ; Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ;
assert ( assert (
let vs = Set.diff (Set.diff post.us xs) pre0.us in let vs = Set.diff (Set.diff post.us xs) pre0.us in
Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )] Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )]
; ;
let foot = Sh.extend_us xs foot in let foot = Sh.extend_us xs foot in
let zs, pre = Sh.bind_exists pre0 ~wrt:xs in let zs, pre = Sh.bind_exists pre0 ~wrt:xs in
( Solver.infer_frame pre xs foot let+ frame = Solver.infer_frame pre xs foot in
>>| fun frame ->
Sh.exists (Set.union zs xs) Sh.exists (Set.union zs xs)
(Sh.star post (Sh.exists ms (Sh.rename sub frame))) ) (Sh.star post (Sh.exists ms (Sh.rename sub frame))))
|> |>
[%Trace.retn fun {pf} r -> [%Trace.retn fun {pf} r ->
pf "%a" (Option.pp "%a" Sh.pp) r ; pf "%a" (Option.pp "%a" Sh.pp) r ;
@ -671,9 +670,9 @@ let rec exec_specs pre = function
| ({xs; foot; _} as spec) :: specs -> | ({xs; foot; _} as spec) :: specs ->
let foot = Sh.extend_us xs foot in let foot = Sh.extend_us xs foot in
let pre_pure = Sh.star (Sh.exists xs (Sh.pure_approx foot)) pre in let pre_pure = Sh.star (Sh.exists xs (Sh.pure_approx foot)) pre in
exec_spec pre_pure spec let* post = exec_spec pre_pure spec in
>>= fun post -> let+ posts = exec_specs pre specs in
exec_specs pre specs >>| fun posts -> Sh.or_ post posts Sh.or_ post posts
| [] -> Some (Sh.false_ pre.us) | [] -> Some (Sh.false_ pre.us)
let exec_specs pre specs = let exec_specs pre specs =

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

@ -85,9 +85,11 @@ let excise_term ({us; min; xs} as goal) pure term =
let excise_pure ({sub} as goal) = let excise_pure ({sub} as goal) =
[%Trace.info "@[<2>excise_pure@ %a@]" pp goal] ; [%Trace.info "@[<2>excise_pure@ %a@]" pp goal] ;
List.fold_option sub.pure ~init:(goal, []) ~f:(fun (goal, pure) term -> let+ goal, pure =
excise_term goal pure term ) List.fold_option sub.pure ~init:(goal, []) ~f:(fun (goal, pure) term ->
>>| fun (goal, pure) -> {goal with sub= Sh.with_pure pure sub} excise_term goal pure term )
in
{goal with sub= Sh.with_pure pure sub}
(* [k; o) (* [k; o)
* ⊢ [l; n) * ⊢ [l; n)
@ -496,8 +498,7 @@ let excise_seg ({sub} as goal) msg ssg =
(Sh.pp_seg_norm sub.cong) ssg] ; (Sh.pp_seg_norm sub.cong) ssg] ;
let {Sh.loc= k; bas= b; len= m; siz= o} = msg in let {Sh.loc= k; bas= b; len= m; siz= o} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in
Equality.difference sub.cong k l let* k_l = Equality.difference sub.cong k l in
>>= fun k_l ->
if if
(not (Equality.entails_eq sub.cong b b')) (not (Equality.entails_eq sub.cong b b'))
|| not (Equality.entails_eq sub.cong m m') || not (Equality.entails_eq sub.cong m m')
@ -511,13 +512,11 @@ let excise_seg ({sub} as goal) msg ssg =
| -1 -> ( | -1 -> (
let ko = Term.add k o in let ko = Term.add k o in
let ln = Term.add l n in let ln = Term.add l n in
Equality.difference sub.cong ko ln let* ko_ln = Equality.difference sub.cong ko ln in
>>= fun ko_ln ->
match[@warning "-p"] Z.sign ko_ln with match[@warning "-p"] Z.sign ko_ln with
(* k+o-(l+n) < 0 so k+o < l+n *) (* k+o-(l+n) < 0 so k+o < l+n *)
| -1 -> ( | -1 -> (
Equality.difference sub.cong l ko let* l_ko = Equality.difference sub.cong l ko in
>>= fun l_ko ->
match[@warning "-p"] Z.sign l_ko with match[@warning "-p"] Z.sign l_ko with
(* l-(k+o) < 0 [k; o) (* l-(k+o) < 0 [k; o)
* so l < k+o ⊢ [l; n) *) * so l < k+o ⊢ [l; n) *)
@ -551,8 +550,7 @@ let excise_seg ({sub} as goal) msg ssg =
| 1 -> ( | 1 -> (
let ko = Term.add k o in let ko = Term.add k o in
let ln = Term.add l n in let ln = Term.add l n in
Equality.difference sub.cong ko ln let* ko_ln = Equality.difference sub.cong ko ln in
>>= fun ko_ln ->
match[@warning "-p"] Z.sign ko_ln with match[@warning "-p"] Z.sign ko_ln with
(* k+o-(l+n) < 0 [k; o) (* k+o-(l+n) < 0 [k; o)
* so k+o < l+n ⊢ [l; n) *) * so k+o < l+n ⊢ [l; n) *)
@ -562,8 +560,7 @@ let excise_seg ({sub} as goal) msg ssg =
| 0 -> Some (excise_seg_min_suffix goal msg ssg k_l) | 0 -> Some (excise_seg_min_suffix goal msg ssg k_l)
(* k+o-(l+n) > 0 so k+o > l+n *) (* k+o-(l+n) > 0 so k+o > l+n *)
| 1 -> ( | 1 -> (
Equality.difference sub.cong k ln let* k_ln = Equality.difference sub.cong k ln in
>>= fun k_ln ->
match[@warning "-p"] Z.sign k_ln with match[@warning "-p"] Z.sign k_ln with
(* k-(l+n) < 0 [k; o) (* k-(l+n) < 0 [k; o)
* so k < l+n ⊢ [l; n) *) * so k < l+n ⊢ [l; n) *)
@ -601,16 +598,20 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
let ys, min = Sh.bind_exists minuend ~wrt:xs in let ys, min = Sh.bind_exists minuend ~wrt:xs in
let us = min.us in let us = min.us in
let com = Sh.emp in let com = Sh.emp in
List.find_map dnf_subtrahend ~f:(fun sub -> let+ remainder =
[%Trace.info "@[<2>subtrahend@ %a@]" Sh.pp sub] ; List.find_map dnf_subtrahend ~f:(fun sub ->
let sub = Sh.extend_us us sub in [%Trace.info "@[<2>subtrahend@ %a@]" Sh.pp sub] ;
let ws, sub = Sh.bind_exists sub ~wrt:xs in let sub = Sh.extend_us us sub in
let xs = Set.union xs ws in let ws, sub = Sh.bind_exists sub ~wrt:xs in
let sub = Sh.and_cong min.cong sub in let xs = Set.union xs ws in
let zs = Var.Set.empty in let sub = Sh.and_cong min.cong sub in
excise {us; com; min; xs; sub; zs; pgs= true} let zs = Var.Set.empty in
>>| fun remainder -> Sh.exists (Set.union ys ws) remainder ) let+ remainder =
>>| fun remainder -> Sh.or_ remainders remainder ) excise {us; com; min; xs; sub; zs; pgs= true}
in
Sh.exists (Set.union ys ws) remainder )
in
Sh.or_ remainders remainder )
let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option = let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
fun minuend xs subtrahend -> fun minuend xs subtrahend ->

Write Preview
Loading…
Cancel
Save