Summary:
The constructor of `folly::SocketAddress` conditionally deletes some
object and then makes that condition false. The destructor then does the
same. Pulse ignores conditionals so will see a double delete.
Just skip that function for now, but it should be easy for pulse to be
more correct here if it knew how to compare constant values.
Reviewed By: mbouaziz
Differential Revision: D16005395
fbshipit-source-id: 036f5091b
Summary:
[apologies for the unreviewable diff...]
Get rid of HIL expressions in pulse. This finishes the HIL -> SIL
migration. The first step made pulse start from SIL instructions but
would translate most accesses to HIL to re-use most of the existing
pulse code. This diff gets rid of the intermediate translation of SIL
expressions to HIL expressions.
Big changes:
1. `PulseOperations` mostly rewritten, driven by using `Exp.t` instead of `HilExp.AccessExpression.t` for everything.
2. Stop trying to reverse-engineer what addresses mean in terms of
access paths from program variables. Rely on the trace pointing at
the right places in the code to be enough. This is because it wasn't
that useful (and could even be misleading when wrong) but could be
prohibitively expensive in degenerate cases (eg nodes with tens of
thousands of successive array accesses...)
3. `PulseAbductiveDomain.apply_post` now returns the computed return
value instead of recording it itself.
4. Change of vocabulary: `materialize` -> `eval`, `crumb` -> `event`
5. Function calls arguments are now evaluated prior to doing anything
else, which saves everything else from having to (remember to) do
that. In particular, this changes how models look quite a bit.
Reviewed By: mbouaziz
Differential Revision: D15986373
fbshipit-source-id: 1d79935de
Summary:
Now that HIL doesn't help us anymore we need to reconstruct its mapping
"SIL logical var -> program access path". We already have everything we
need in pulse: it suffices to walk the current memory graph starting
from program variables until we find the value of the temporary we are
interested in.
This diff also builds some type machinery to make sure all accesses are
explained.
Reviewed By: mbouaziz
Differential Revision: D15824959
fbshipit-source-id: 722c81b39
Summary:
Just moving code around.
This is needed later to make some types in `PulseTrace` depend on
a new that I'll have to define in `PulseDomain`.
Also, this gives better names all around I think
Reviewed By: mbouaziz
Differential Revision: D15881281
fbshipit-source-id: e86c1472e
Summary:
Just moving code around.
This is needed later to make some types in `PulseInvalidation` depend on
a new type that I'll have to define in `PulseDomain`.
Reviewed By: mbouaziz
Differential Revision: D15824962
fbshipit-source-id: 86cba2bfb
Summary:
This is useful for the model of `exit` that returns 0 disjuncts. All
other models return 1 disjunct for now, but in the future things like
`malloc()` will need to return 2 possible states for instance.
Reviewed By: ngorogiannis
Differential Revision: D14753491
fbshipit-source-id: 3e7387d6d
Summary:
This isn't needed now that this information is recorded in
`PulseTrace.action` instead.
Reviewed By: mbouaziz
Differential Revision: D14645089
fbshipit-source-id: 9c3f38722
Summary:
For each operation on the domain, try to record what it requires of the
precondition of the function. This is akin to what happens in the
biabduction backend, hence the terminology used.
Reviewed By: jberdine
Differential Revision: D14387148
fbshipit-source-id: a61fe30c8
Summary:
Instead of emitting an ad-hoc builtin on variable declaration emit a new
metadata instruction. This allows us to remove the code matching on that
ad-hoc builtin that had to be inserted in several checkers.
Inferbo & pulse used that information meaningfully and had to undergo
some minor changes to cope with the new metada instruction.
Reviewed By: ezgicicek
Differential Revision: D14833100
fbshipit-source-id: 9b3009d22
Summary: It's all grown up now and taking quite some space in src/checkers/.
Reviewed By: skcho
Differential Revision: D14568273
fbshipit-source-id: b843c031e
Jules Villard
Josh Berdine
Peter O'Hearn