Summary:
This is a simple CFG transformation that compresses jumps to jumps
into jumps to the final destination. LLVM's simplifycfg pass seemingly
should have eliminated these, but does not.
Reviewed By: jvillard
Differential Revision: D25196728
fbshipit-source-id: 3288dbd8d
Summary:
Currently the symbolic execution options, obtained from the command
line flags and preanalysis, are passed to the Control entry points as
a record, and then passed around within Control as needed. This diff
simplifies the code in Control by replacing the record mechanism with
an additional functor parameter containing the options. The main
benefit is that the bound option no longer needs to be part of the
analysis state.
This change does make the code in Sledge_cli slightly more
complicated, as it now performs a functor application using a
first-class module computed from the command line flags.
Reviewed By: jvillard
Differential Revision: D25196735
fbshipit-source-id: 80e5d5d62
Summary:
Revise the control-flow exploration scheduling algorithm to fix
several issues. The main difference is to change the priority queue to
keep the control edges on the frontier of exploration in sync with the
states that are waiting to be propagated. This fixes several sorts of
issue where the decision of which control and state joins to perform
was unexpected / wrong. Part of keeping the frontier edges and waiting
states in sync is that the waiting states are associated not only with
a destination block, but the stack of that block. This fixes several
issues.
Combined, these changes lead to the algorithm only attempting joins
for which the pointwise max join on depth maps is correct (with the
caveat of no mathematical proof yet).
Reviewed By: jvillard
Differential Revision: D25196733
fbshipit-source-id: db007fe1f
Summary:
The first-order solver sometimes needs to generate fresh variables to
express the solution of equations. It needs to ensure that these
generated variables do not clash. Before this diff, there was a
confusion where new variables were fresh with respect to only the
current set of "universal" variables. This is wrong, and this diff
adds the full set of variables instead.
Reviewed By: jvillard
Differential Revision: D25196732
fbshipit-source-id: afc56834a
Summary:
It can happen that the actual return variable, which is the name of
the variable in the caller's scope that receives the returned value,
clashes with the formals of the callee. The scope of the return
formula was wrong in this case, as the actual return was outscoped via
existential quantification with the rest of the formals after the
return values was passed.
Reviewed By: jvillard
Differential Revision: D25196727
fbshipit-source-id: 94cf25418
Summary:
A context with valid but extraneous equations was being kept. The
extra equations are valid, but might violate vocabulary invariants.
Reviewed By: jvillard
Differential Revision: D25196734
fbshipit-source-id: a8001a075
Summary:
Currently there is a symbolic execution option to ignore exceptional
control flow. This hack does not fit well, and it is unclear how much
backend functionality should take it into consideration. This diff
removes this option and replaces it with an option during model
compilation. This has the advantage of clarifying and simplifying the
backend, with the disadvantage of no longer supporting switching
between exceptions and no-exceptions modes at analysis time. Since the
possibility of ignoring exceptional control flow is due to it not being
ready yet, this is a good trade to make.
Reviewed By: jvillard
Differential Revision: D25146148
fbshipit-source-id: 1f1299ee1
Summary:
Use the equality class information in the symbolic state to resolve
callees of indirect calls.
Reviewed By: jvillard
Differential Revision: D25146160
fbshipit-source-id: a1c39bbe1
Summary:
The callee function of a Call can often be resolved
statically. Currently this is resolution is only done dynamically
during symbolic execution by checking if the callee expression is a
function name and looking up the function in the program. This is
wasted and redundant work. Also, the static resolution code is
duplicated in all the domains.
This diff resolves this by resolving known callees statically at
translation time. This involves:
- add an ICall terminator that is the same as Call is currently
- change Call to use a func callee instead of Exp.t
- make callee field mutable since recursive calls can create cycles
- change the Llair.Term.call constructor to return a thunk to perform
the backpatching once the callee has been translated
- modify the Frontend
+ to determine whether to emit Call or ICall depending on whether
the callee in LLVM is already a Function
+ to record the LLVM function -- backpatch thunk pairs encountered during translation
+ record the mapping of LLVM to LLAIR functions during translation
+ to enumerate the calls to backpatch after all functions have been
translated, and find the LLAIR function corresponding to each LLVM
function and backpatch the call to use it as the callee
+ to handle direct calls to undefined functions, when backpatching
translate such function declarations into undefined functions
Reviewed By: jvillard
Differential Revision: D25146152
fbshipit-source-id: 47d2ca1ff
Summary:
Current code partially tries to handle Invoke, but incorrectly, and
these names are only needed for Call. So this diff revises this to be
slightly simpler and less confusing.
Reviewed By: jvillard
Differential Revision: D25146157
fbshipit-source-id: ead4f6f31
Summary: Rework the intrinsic name detection to detect e.g. llvm.memset.*
Reviewed By: jvillard
Differential Revision: D25146150
fbshipit-source-id: 85ebcfb7a
Summary:
Rename the existing exec_intrinsic that works for calls to intrinsic
functions to exec_intrinsic_func to make room for an exec_intrinsic
that works on intrinsic instructions.
Reviewed By: jvillard
Differential Revision: D25146166
fbshipit-source-id: 80ae3aac9
Summary:
The translation of instruction intrinsics that are `Invoke`d is almost
the same as those that are `Call`ed. The same Llair instruction is
produced, but it is wired into the CFG differently. This diff uses the
translation of instruction intrinsics used for `Call`s for `Invoke`s
as well.
Reviewed By: jvillard
Differential Revision: D25146159
fbshipit-source-id: 85a93d915
Summary:
The code that computes the number of actuals is largely duplicated
between the Call and Invoke cases. But some issues have been fixed in
each that ought to be applied to the other. This factors out and
unifies this computation.
Reviewed By: jvillard
Differential Revision: D25146149
fbshipit-source-id: 78552327a
Summary:
Move the translation of Calls to intrinsics that map to instructions
into a separat function.
No functional change.
Reviewed By: jvillard
Differential Revision: D25146169
fbshipit-source-id: 79c640344
Summary:
Currently intrinsics are treated as functions, with Call instructions
to possibly-undefined functions with known names. This diff adds an
Intrinsic instruction form to express these more directly and:
- avoid the overhead of intrinsics needing to end blocks
- avoid the overhead of the function call machiery
- avoid the complexity of doing the string name lookup to find their
specs, repeatedly
This diff only adds the backend support, the added Intrinsic
instructions are not yet generated by the frontend.
Reviewed By: jvillard
Differential Revision: D25146155
fbshipit-source-id: f24024183
Summary:
Previously, when LLAIR was in SSA form, blocks took parameters just
like functions, and it was sometimes necessary to partially apply a
block to some of the parameters. For example, blocks to which function
calls return would need to accept the return value as an argument, and
sometimes immediately jump to another block passing the rest of the
arguments as well. These "trampoline" blocks were partial applications
of the eventual block to all but the final, return value,
argument.
This partial application mechanism meant that function parameters and
arguments were represented as a stack, with the first argument at the
bottom, that is, in reverse order.
Now that LLAIR is free of SSA, this confusion is no longer needed, and
this diff changes the representation of function formal parameters and
actual arguments to be in the natural order. This also brings Call
instructions in line with Intrinsic instructions, which will make
changing the handling of intrinsics from Calls to Intrinsic less
error-prone.
Reviewed By: jvillard
Differential Revision: D25146163
fbshipit-source-id: d3ed07a45
Summary:
Overwritten variables in move instructions are not impossible. Since
Domain_itv does not handle them, the check should be a `todo` rather
than an `assert false`.
Reviewed By: jvillard
Differential Revision: D25146168
fbshipit-source-id: 13d8587c7
Summary:
It was possible for the scope of a local to be incorrectly restored
when entering it for the first time in a caller after is was shadowed
by a callee. This could happen because scope management in the
analysis relies on renaming variables to adjust the vocabulary of
symbolic states. This was usually done, but optimizations of renaming
with a substitution whose domain is disjoint from the vocabulary of a
formula inadvertantly violated this vocabulary-adjustment
assumption. (Yes, this is too easy to get wrong.)
Reviewed By: jvillard
Differential Revision: D25146162
fbshipit-source-id: 30f2d657f
Summary: In Java, public class name should be the same to file name.
Reviewed By: ezgicicek
Differential Revision: D25245194
fbshipit-source-id: 49fd16748
Summary:
This diff adds a new issue type for reporting modifications to immutable fields (when `report-immutable-modifications` is enabled).
The underlying analysis depends on impurity analysis which itself is based on post-processing of pulse's summaries.
Reviewed By: skcho
Differential Revision: D25216637
fbshipit-source-id: 42e843793
Summary:
Previously, impurity analysis only collected one access for a single modification but not all other modifying accesses. This diff
- changes the impurity domain to collect all modifying accesses
- tracks and prints all the accesses seen to reach the modification, improving readability&debugging
Recording all accesses are needed in the next diff to determine if a method modifies any immutable fields. To determine that, we need to know all modifications, not just a single one.
Reviewed By: skcho
Differential Revision: D25186516
fbshipit-source-id: 43ceb3cd8
Summary: The main point here is to ignore owned interfaces when considering whether to warn about non-thread-safe calls.
Reviewed By: ezgicicek
Differential Revision: D25187775
fbshipit-source-id: c2a7ce89c
Summary: There are no users of this, and it stands in the way of refactoring.
Reviewed By: ezgicicek
Differential Revision: D25241940
fbshipit-source-id: 5e653341a
Summary: To look for captured variable address escape we should only check the validity of the addresses captured by reference. Checking the validity of the address captured by value can cause nullptr dereference false positives.
Reviewed By: jvillard
Differential Revision: D25219347
fbshipit-source-id: faf6f2b00
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
Josh Berdine
Sungkeun Cho
Daiva Naudziuniene
Ezgi Çiçek
Nikos Gorogiannis
Radu Grigore