Summary:
The explicit marker for nondeterministic states was used to speed up the
shallow implementations of Topl, which ar enow removed.
Reviewed By: jvillard
Differential Revision: D27297019
fbshipit-source-id: 0fce93817
Summary:
Before this diff, TOPL had 3 implementations:
1. a post-processing of biabduction summaries
2. a post-processing of pulse summaries
3. a deep embedding in pulse
1 and 2 additionally require instrumenting SIL to generate monitors for
the TOPL properties. 3 is faster than both 1 and 2, by a good lot, and
doesn't require instrumenting the SIL code. Thus, delete 1 and 2!
Also harmonise the CLI so that TOPL is activated by --topl, which
actives it as a checker, like other analyses.
Reviewed By: rgrig
Differential Revision: D27270178
fbshipit-source-id: e86cf972b
Summary:
When extracting summaries, ask PulseFormula to work harder to prove that
path-conditions are unsat. This reduces the number of false positives.
Reviewed By: jvillard
Differential Revision: D25270609
fbshipit-source-id: 61ef5e8ac
Summary:
Added a topl-max-disjuncts, which is analogous to pulse-max-disjuncts.
Note, however, that the maximum number of states tracked will be the
product of the two limits.
Added also topl-max-conjuncts, which drops Topl states that became too
complex.
Reviewed By: jvillard
Differential Revision: D25240386
fbshipit-source-id: 588c90390
Summary:
For a long sequence of calls nop();...;nop() the runtime was quadratic
because formals and actuals were bound via equalities. Now,
substitutions are used, when easy.
Reviewed By: jvillard
Differential Revision: D25211504
fbshipit-source-id: 696e3dcdf
Summary:
If f() calls g() and g() violates a property, there used to be two
traces (one for f() and one for g()) even if all that f() has to do with
the property is that it calls g(). Now the error is reported only in
g().
Reviewed By: jvillard
Differential Revision: D25210007
fbshipit-source-id: 68ea57e71
Summary:
A "large step" is a call, and it is "trivial" if it does not affect the
automaton state; i.e., if it is irrelevant to the property being
tracked.
Reviewed By: jvillard
Differential Revision: D25209670
fbshipit-source-id: bf3e594b3
Summary:
Makes sure that topl summaries don't repeat. Previously this happened
when two posts led to the same summary when procedure-local variables
were killed. Such repeated summaries quickly lead to exponential
explosion. (For example, the added test -- `ManyLoops.java` -- didn't
finish in any reasonable time.)
Reviewed By: jvillard
Differential Revision: D25209623
fbshipit-source-id: 04b1a3e12
Summary:
Now one can use the pattern #ArrayWrite(A,I) to match on a write at
index I in array A. This only works in the Pulse variant of Topl (not in
the one based on SIL instrumentation).
Reviewed By: jvillard
Differential Revision: D25202768
fbshipit-source-id: 479f434e3
Summary:
PulseTopl.large_step is now implemented
All active tests are migrated now to topl-in-pulse.
Reviewed By: jvillard
Differential Revision: D25179556
fbshipit-source-id: dc1136bab
Summary:
When running the deep-Pulse version of Topl, it now produces and reports
traces.
Reviewed By: jvillard
Differential Revision: D25177139
fbshipit-source-id: 6955ee0cd
Summary:
Report errors found by running Topl on top of Pulse, when using
--topl-pulse. Topl tests now run on top of Pulse.
Reviewed By: jvillard
Differential Revision: D23030771
fbshipit-source-id: 8770c2902
Summary:
The generated code used to contain Prune statements that had boolean
connectives in their conditions. After this commit, all conditions
should have no boolean connective (LNot, LOr, LAnd) at top-level; that
is, prune conditions should be atomic.
The main motivation behind this change is that (a) frontends follow this
convention, and (b) Pulse assumes this convention.
Reviewed By: jvillard
Differential Revision: D23022273
fbshipit-source-id: 1313328e4
Summary:
The old --topl-only is now --topl-biabd-only, and there's also
--topl-pulse-only. This is WIP: the latter runs pulse, but it doesn't yet
extract Topl errors from pulse summaries. (The citv part of pulse path
conditions appears to have the necessary information.)
Reviewed By: jvillard
Differential Revision: D22815250
fbshipit-source-id: a01792945
Summary:
This seems to make sense as it's a separate analysis (that depends on
biabduction). This introduces unpleasant `|| is_checker_enabled TOPL`
whenever we try to figure out if biabduction will run. I think this is a
more general problem that deserves a more general solution to express
the fact that checkers can depend on others, so that, eg,
`is_checker_enabled Purity` is true when we pass `--loop-hoisting`. Will
address in another diff.
Reviewed By: ngorogiannis
Differential Revision: D21618460
fbshipit-source-id: 8b0c9a015
Summary:
Currenlty the cost issue is printed at the first node of a function, which is usually the first
statment of the function. This may give a wrong impression that the cost of the statement is
changed.
This diff re-locate where to print issues with heuristics. Going backward from the first node
lines, it looks up a line satisfying,
1. A line should start with <fname> or should include " <fname>".
2. The <fname> found in 1 should be followed by a space, '<', '(', or end of line.
Reviewed By: jvillard
Differential Revision: D20766876
fbshipit-source-id: b4fee3180
Summary: These tests fail when seemingly unrelated changes are made to infer. In particular, it seems timeout limits have to be increased by 10x or more to make them succeed again. Disabling until we have a more stable replacement.
Reviewed By: ezgicicek
Differential Revision: D20489647
fbshipit-source-id: 9706b0807
Summary:
This is the kind of property for which the previous syntax forced one to
use spurious registers.
Reviewed By: ngorogiannis
Differential Revision: D20118863
fbshipit-source-id: b49740d33
Summary:
This syntax
- is less confusing (according to several people who are not me);
objectively, there's less magic under the hood
- gives fine control over register number (because condition/action are separated)
- lets one compare values of different arguments of the same call
(e.g., one could have a transition that is taken only if two
arguments of a method call are equal)
Reviewed By: ngorogiannis
Differential Revision: D20005403
fbshipit-source-id: fad8f3b3d
Summary:
The test shows what that TOPL can express, in addition to bugs,
efficiency properties. However, there seems to be an underlying problem
in biabdaction that prevents this particular problem from being caught.
Reviewed By: ngorogiannis
Differential Revision: D20005404
fbshipit-source-id: 466f79050
Summary:
This adds a violation of baos.topl found in github/seata/seata. However,
it is not a bug (see comment in commit).
Reviewed By: ngorogiannis
Differential Revision: D19518641
fbshipit-source-id: e219245ee
Summary:
1. One should use either a writer or a stream to send a response, but not both.
2. A response should be forwarded only if it was commited.
Both properties are extracted from API comments on classes in the servlet API.
Reviewed By: jvillard
Differential Revision: D19514568
fbshipit-source-id: 79f0257ed
Summary:
If data comes from an outer OutputStream, then this outer OutputStream
needs to be flushed before getting the byte array.
Reviewed By: jvillard
Differential Revision: D19514569
fbshipit-source-id: e3e025394
Summary:
The property SkipAfterRemove already had a test, but not for
intra-procedural violations. This adds a test for that case.
Reviewed By: ngorogiannis
Differential Revision: D19330471
fbshipit-source-id: 1dd1c3ad7
Summary: add subdirectories so that we can run each java file against its own topl properties
Reviewed By: rgrig
Differential Revision: D19347302
fbshipit-source-id: 562830774
Summary:
Old versions of sawja/javalib got the line numbers slightly wrong. The workaround was to do a regexp search in the source file for the right line.
My understanding is that this is no longer necessary. This diff removes it.
Reviewed By: jvillard
Differential Revision: D19033415
fbshipit-source-id: 2da19d66d
Summary:
This is an optimization. We ask the user to tell us which states are nondeterministic, and we
generate code that handle nondeterminism only for those states. It is common for only one state per
TOPL property to be nondeterministic. This speeds up the biabduction-analysis of the monitor by a
factor of ~10. But, using the monitor is only a little faster.
Facebook
Reviewed By: jvillard
Differential Revision: D19160286
fbshipit-source-id: 4dd39769a
Summary:
This havocs event data, so that biabduction doesn't try to
track what was the last event processed by the monitor
(which is redundant as long as the state of the monitor
is tracked).
Reviewed By: ngorogiannis
Differential Revision: D19035491
fbshipit-source-id: a1c75daae
Summary:
Don't instrument SIL when we can determine statically that
biabduction symexec would be a no-op.
Reviewed By: ngorogiannis
Differential Revision: D19116849
fbshipit-source-id: 4d25462a3
Summary:
In addition to
state1 -> state2: pattern
one can now also write
state1 -> state2: pattern if condition
where "condition" is some conjunction of comparisons (==,<,>) that
involve variables bound by "pattern", registers of the automaton, and
constants.
Reviewed By: ngorogiannis
Differential Revision: D19035496
fbshipit-source-id: 6f6e6a9be
Summary:
The synthetic methods from `topl.Property` are now nonempty: they
simulate a nondeterministic automaton.
Reviewed By: jvillard
Differential Revision: D15668471
fbshipit-source-id: 050408283
Summary:
Instrument SIL according to TOPL properties. Roughly, the
instrumentation is a set of calls into procedures that simulate a
nondeterministic automaton. For now, those procedures are NOP dummies.
Reviewed By: jvillard
Differential Revision: D15063942
fbshipit-source-id: d22c2f6fa
Summary:
TOPL properties are essentially automata, which specify a bad pattern.
This commit is just a parser for them.
Reviewed By: jvillard
Differential Revision: D14477671
fbshipit-source-id: c38a8ef37
Radu Grigore
Jules Villard
Sungkeun Cho
Nikos Gorogiannis
Josh Berdine