New Property: INFINITE_LOOP detector (aka pulse-infinite). No regression. #1896
Conversation
There was a problem hiding this comment.
Looks great! Lots of comments but almost all are very minor. The less minor ones are:
- can the internal workings of PulseFormula be simplified further to avoid having to record raw atoms in the middle of normalization?
- can we avoid the alarm CFG node reference inside the abstract interpreter by storing this information in the
InfiniteProgram(possibly renamed toInfiniteLoop) instead?
| @@ -253,7 +265,7 @@ struct | |||
| disjuncts are already deduplicated *) | |||
| if has_geq_disj ~leq ~than:hd into then | |||
| (* [hd] implies one of the states in [into]; skip it | |||
| ([(a=>b) => (a\/b <=> b)]) *) | |||
| ([(a=>b) => (a\/b <=> b)]) *) | |||
There was a problem hiding this comment.
can you remove this spurious change?
| @@ -314,14 +326,23 @@ struct | |||
| let max_iter = | |||
| match DConfig.widen_policy with UnderApproximateAfterNumIterations max_iter -> max_iter | |||
| in | |||
| if phys_equal prev next then prev | |||
There was a problem hiding this comment.
Can we keep this short circuiting? I think calling T.back_edge (fst prev) (fst next) before the conditional would have the same effect.
| let back_edges (prev : T.DisjDomain.t list) (next : T.DisjDomain.t list) (num_iters : int) : | ||
| T.DisjDomain.t list * int = | ||
| T.back_edge prev next num_iters | ||
| in | ||
| let fp = fst prev in | ||
| let fn = fst next in | ||
| let dbe, _ = back_edges fp fn num_iters in |
There was a problem hiding this comment.
This could all be one line I think (but maybe moved before the conditional as per comment a few lines above). Can you expand dbe? It's not clear to me what it stands for.
| let back_edges (prev : T.DisjDomain.t list) (next : T.DisjDomain.t list) (num_iters : int) : | |
| T.DisjDomain.t list * int = | |
| T.back_edge prev next num_iters | |
| in | |
| let fp = fst prev in | |
| let fn = fst next in | |
| let dbe, _ = back_edges fp fn num_iters in | |
| let dbe, _ = T.back_edge (fst prev) (fst next) num_iters in |
| if hasnew then | ||
| join_up_to_with_leq ~limit:disjunct_limit T.DisjDomain.leq ~into:dbe (fst next) | ||
| else | ||
| join_up_to_with_leq ~limit:disjunct_limit T.DisjDomain.leq ~into:(fst prev) (fst next) |
There was a problem hiding this comment.
very minor but it's less code duplication and clearer that the only difference is the ~into parameter this way
| if hasnew then | |
| join_up_to_with_leq ~limit:disjunct_limit T.DisjDomain.leq ~into:dbe (fst next) | |
| else | |
| join_up_to_with_leq ~limit:disjunct_limit T.DisjDomain.leq ~into:(fst prev) (fst next) | |
| let into = if has_new then dbe else (fst prev) in | |
| join_up_to_with_leq ~limit:disjunct_limit T.DisjDomain.leq ~into (fst next) |
| @@ -78,6 +78,8 @@ module type DisjReady = sig | |||
|
|
|||
| val pp_session_name : CFG.Node.t -> Format.formatter -> unit | |||
|
|
|||
| val back_edge : DisjDomain.t list -> DisjDomain.t list -> int -> DisjDomain.t list * int | |||
There was a problem hiding this comment.
can you add a comment to say what the returned int is? ~~Also, please name the int parameter otherwise we don't know what it is either.~~actually it looks like num_iters is never used so remove the int parameter altogether?
| val back_edge : DisjDomain.t list -> DisjDomain.t list -> int -> DisjDomain.t list * int | |
| val back_edge : DisjDomain.t list -> DisjDomain.t list -> DisjDomain.t list * int |
| (* Infinite Loop Detection: check for cases like while (x == x) | ||
| by rewriting them to while (0 == 0) first *) |
There was a problem hiding this comment.
can you add to the comment why this is needed?
|
|
||
| (* Infinite Loop Detection: check for cases like while (x == x) | ||
| by rewriting them to while (0 == 0) first *) | ||
| let opcond = match (tx, ty) with Term.Var v1, Term.Var v2 -> phys_equal v1 v2 | _, _ -> false in |
There was a problem hiding this comment.
please avoid phys_equal when possible
| let opcond = match (tx, ty) with Term.Var v1, Term.Var v2 -> phys_equal v1 v2 | _, _ -> false in | |
| let opcond = match (tx, ty) with Term.Var v1, Term.Var v2 -> Var.equal v1 v2 | _, _ -> false in |
| let swapcond = match (bop : Binop.t) with Eq -> true | _ -> false in | ||
| let swapterm = Term.of_binop Eq Term.zero Term.zero in | ||
| let atom = if opcond && swapcond then swapterm else t in | ||
| let newphi = Formula.and_termcond_binop formula.phi atom in |
There was a problem hiding this comment.
why add the atom at all if it's just 0=0?
|
|
||
|
|
||
| let prune_binop ?(depth = 0) ~negated (bop : Binop.t) x y formula = | ||
| let prune_binop ?(depth = 0) ~negated (bop : Binop.t) ?(ifk = false) x y formula = | ||
| let tx = Term.of_operand x in | ||
| let ty = Term.of_operand y in | ||
| let t = Term.of_binop bop tx ty in | ||
| (* [Option.value_exn] is justified by [force_to_atom:true] *) |
There was a problem hiding this comment.
This is now very far from the call to Option.value_exn, please move down
| | InfiniteProgram _ -> | ||
| let curnode = Metadata.get_infinite_node in | ||
| let curloc = Procdesc.Node.get_loc (curnode ()) in |
There was a problem hiding this comment.
I think you could store the current node inside InfiniteProgram at the point it is created and then read it back here instead of maintaining a ref inside AbstractInterpreter.DisjunctiveMetadata. You can get the node under analysis at any point in pulse with AnalysisState.get_node_exn.
|
@ngorogiannis has imported this pull request. If you are a Meta employee, you can view this diff on Phabricator. |
Opening up new PR for Jules to review.