Summary:
Previously, only names containing '$' were considered synthetic. We need
to extend the logic and look for "_UL_" in the name as well.
Also I deduped 4 different impls of "is_synthetic/generated/autogen".
Reviewed By: ngorogiannis
Differential Revision: D25899232
fbshipit-source-id: 9463eca6b
Summary:
When used by the first-order solver, solve_extract may generate fresh
variables to express the solution substitutions, but when used by
quantifier elimination via solve_for_vars, fresh variables should not
be generated. This diff makes the difference between these use cases
simpler and clearer by replacing the obscure filter predicate argument
that is passed eventually to compose1 with a boolean indicating
whether fresh variables may be generated.
Reviewed By: jvillard
Differential Revision: D25756562
fbshipit-source-id: 53a35b71c
Summary:
Context.solve_for_vars returns a solution substitution consisting of
oriented equalities that are implied by the given context. It is
logically valid to express these equations using terms that are
normalized with respect to the solution substitution itself. This diff
normalizes uninterpreted terms with the solution substitution when
extending it. This preserves the logical strength of the solutions,
and strengthens other purely syntactic operations on the substitution,
such as Context.Subst.is_valid_eq.
Reviewed By: jvillard
Differential Revision: D25756582
fbshipit-source-id: cd997c46b
Summary:
- Fix clamping of percentage change of memory quantities
- Improve sorting of coverage changes relative to unchanged error
results
- Filter out results for invalid LLVM code
- Fix printing multiple status values
- Fix passing args to sledge, different subcommands need different
args
- Fix cleaning commands
- Add an unknown error status to the report if sledge exits without
producing a status in the report
- Internalize globals for tests, as otherwise C++ tests are unreadable
due to the runtime system models
Reviewed By: jvillard
Differential Revision: D25756567
fbshipit-source-id: 3b4c003f4
Summary:
The ~20% hit in compilation time is dominated by the time saved
running the tests. This also makes the memory allocation numbers more
robust to inconsequential changes. Note that `make check` is still
fast.
Note that normally dune passes `-g` to ocamlopt itself, but not if the
build profile includes an `ocamlopt_flags` entry. So add it explicitly
to ensure that compilation includes debug symbols.
(Also remove `-error-style short` that was missed in 9c4f263.)
Reviewed By: jvillard
Differential Revision: D25756570
fbshipit-source-id: 94d18bac2
Summary:
When a stem has an occurrence of an existential, say x, and x is
substituted out by different witnesses, say a and b, in two disjuncts,
then the connection to other occurrences of a and b are lost.
This diff fixes this problem by propagating the solved variables that
survive normalization down to subformulas, and not removing those
variables from subformulas.
Reviewed By: jvillard
Differential Revision: D25756583
fbshipit-source-id: dabda743f
Summary:
Trade a bit more code for lowering complexity from linear to
logarithmic.
Reviewed By: jvillard
Differential Revision: D25756569
fbshipit-source-id: 83ad575fe
Summary:
Composing two substitutions does not need to require that their
domains are disjoint.
Leave disjointness check for composing a single mapping just to check
expected usage.
Reviewed By: jvillard
Differential Revision: D25756557
fbshipit-source-id: 04e92b864
Summary:
The overall operation of the quantifier elimination algorithm in
Sh.simplify is to first descend through the disjunctive structure of a
symbolic heap formula, process the leaves, and then proceed back up
the formula. At each point on the way back up, the first-order solver
is used to compute a solution substitution representing witnesses of
existential variables. This substitution is then used to normalize the
entire subformula at that point. Note that this results in
substituting and normalizing each subformula a number of times
proportional to its depth in the disjunctive structure.
This diff removes this redundancy and substitutes through each
subformula once. This is done by changing from an overall bottom-up to
top-down algorithm, and involves composing solution substitutions
rather than substituting multiple times. This change also heavily
relies on the strengthened Context.apply_and_elim operation, where the
bottom-up many-substitutions approach relies on the internal details
of repeated substitutions.
Reviewed By: jvillard
Differential Revision: D25756549
fbshipit-source-id: ca7cd814a
Summary:
The current implementation of quantifier elimination in Sh.simplify is
tightly coupled with the details of what the Context operations
support. In particular, successfully eliminating variables with
Context.elim effectively relies on being given a context that has been
transformed by Context.apply_subst. These operations are sound
independently, but achieving the desired result is delicate.
To simplify this situation, this diff refactors the tightly coupled
usage into a Context.apply_and_elim operation that hides the details
of the interaction inside the Context module. This enables an accurate
specification of apply_and_elim to be given much more simply than can
be done for the separate operations. This also simplifies the
implementation of Sh.simplify.
Reviewed By: jvillard
Differential Revision: D25756577
fbshipit-source-id: b344b3da6
Summary:
The implementation of quantifier elimination in Sh.simplify currently
relies on a subtle implementation detail of Context.apply_subst to
remove some identity mappings. Now that Context.elim has been
strengthened and generalized, it can be used to to give a much clearer
implementation, that is also more robust to representation changes in
Context.
Reviewed By: jvillard
Differential Revision: D25756554
fbshipit-source-id: 6be0de2f3
Summary:
The current implementation of Context.elim crudely removes oriented
equations from terms involving the given variables. This is easy to
use in a way that violates the representation invariants of Context,
as well as destroys completeness. This diff resolves this by making
Context.elim remove the desired variables by rearranging the existing
equality classes, in particular promoting a new representative term
when the existing representative is to be removed. Also, since this
basic approach is incomplete for interpreted terms, they are detected
and not removed. As a result, the interface changes to return the set
of variables that have been removed.
Reviewed By: jvillard
Differential Revision: D25756573
fbshipit-source-id: 0eead9281
Summary:
Context.fold_uses_of should enumerate the transitive subterms of a
term rather than only the immediate subterms.
Reviewed By: jvillard
Differential Revision: D25756553
fbshipit-source-id: a3911d9f5
Summary:
Previously Sh had a representation invariant which ensured that
existentials of a subformula did not shadow universals of its
superformulas. The current implementation of Sh.freshen_nested_xs
mistakenly still assumes this invariant, but it no longer holds. This
diff fixes freshen_nested_xs to freshen nested existentials with
respect to not only ancestor universals in addition to existentials.
Reviewed By: jvillard
Differential Revision: D25756551
fbshipit-source-id: 54c48b067
Summary:
Sh.simplify propagates first-order constraints over the formula's
propositional structure, and can reveal inconsistency. It is therefore
sometimes beneficial to check consistency after simplifying rather
than before.
Reviewed By: jvillard
Differential Revision: D25756585
fbshipit-source-id: 2a205c965
Summary:
Simplifying a symbolic heap can reveal inconsistencies, either of
individual disjuncts or (therefore) of toplevel formulas. This is due
to the first-order contexts being propagated from a formula to its
descendents, and for the intersection of the contexts of disjunctions
being propagated to their parent. The later stages of eliminating
redundant quantifiers, etc. do not reveal further
inconsistencies. Therefore this diff moves the inconsistency detection
earlier, to just after the contexts are strengthened. This is clearer,
and also a minor optimization.
Reviewed By: jvillard
Differential Revision: D25756564
fbshipit-source-id: d3acf875b
Summary:
Sh operations usually detect inconsistency where needed. But some
operations such as Context.inter must treat the unsat case
specially. This diff increases robustness by not relying on Sh to
detect inconsistency in order to get the correct context or pure
constraints, or to use the fast-paths through Context or Formula
operations.
Reviewed By: jvillard
Differential Revision: D25756550
fbshipit-source-id: 091439ff6
Summary:
Sh.is_false checks if the pure constraints are inconsistent with the
first-order consequences of the spatial constraints. This involves
some, though not very expensive, logical reasoning. But is it not
checking only testing for the representation of Sh.false_, which one
might expect from its name. This renaming also makes room for the
operation that does test for the representation of Sh.false_.
Reviewed By: jvillard
Differential Revision: D25756580
fbshipit-source-id: 30510f45a
Summary:
Context.apply_subst erroneously resets everything in the
representation of a context except the solution substitution when
applying a substitution.
Reviewed By: jvillard
Differential Revision: D25756548
fbshipit-source-id: 949a34ced
Summary:
When accessing a field or array offset of a pure variable (`Exp.Var`) that does not resolve to an access expression, `HilExp.of_sil` will create an extraneous dereference that causes `HilExp.get_typ` to fail. This pull request wraps variables that are the bases of Lfield or Lindex expressions with AddressOf before they're dereferenced (this is already done for Lvar inside `AccessExpression.of_pvar`) and adds a couple of unit tests that make sure it behaves as expected.
**More details on the bug:**
Given the following code:
```
if (!event_obj->dict)
```
and SIL:
```
n$6=_fun_gdb::ref_ptr<event_object,gdbpy_ref_policy<event_object>>::operator->(&event_obj:gdb::ref_ptr<event_object,gdbpy_ref_policy<event_object>>&) [line 38, column 8];
n$7=*n$6.dict:_object* [line 38, column 8];
PRUNE(!n$7, true); [line 38, column 8];
```
`operator->` has return type `event_object*`, but `n$6.dict` only has access to the type of the struct, `event_object`. `of_sil` [calls](9f98368e49/infer/src/absint/HilExp.ml (L567)) `access_expr_of_lhs_exp` with that type, which [calls](9f98368e49/infer/src/absint/HilExp.ml (L498)) `access_exprs_of_exp` (note that `add_deref` is always true). The Lfield case will then [recurse](9f98368e49/infer/src/absint/HilExp.ml (L469)) to process the Exp.Var, and `AccessExpression.of_id` will return an `AccessPath.base` that is then [dereferenced](9f98368e49/infer/src/absint/HilExp.ml (L440)). When resolving types, `get_typ` will find a non-pointer type wrapped by a `Dereference` and return [None](9f98368e49/infer/src/absint/HilExp.ml (L286)). To fix this, we match what [of_pvar](9f98368e49/infer/src/absint/HilExp.ml (L295)) does and wrap the base in an AddressOf, which is removed by the dereference.
Pull Request resolved: https://github.com/facebook/infer/pull/1372
Reviewed By: ngorogiannis
Differential Revision: D25803049
Pulled By: jvillard
fbshipit-source-id: ceadc8cad
Summary:
Pulse support for C languages ('clang') can now be considered
mature.
Reviewed By: ezgicicek, da319, jvillard
Differential Revision: D25803707
fbshipit-source-id: 5a48eb940
Summary:
When the body of the loop doesn't created a node then they don't get
wired correctly to the rest of the loop and end up dangling. Force node
creation to fix that.
Fixes https://github.com/facebook/infer/issues/1373
Reviewed By: ezgicicek
Differential Revision: D25804185
fbshipit-source-id: 85108bdd9
Summary:
We need to make sure a node is created to avoid instructions appearing
in the wrong order in the final CFG.
Reviewed By: da319
Differential Revision: D25784405
fbshipit-source-id: 3ef27d712
Artem Pianykh
Josh Berdine
Loc Le
Daiva Naudziuniene
Kevin Higgs
Luka Rahne
Gabriela Cunha Sampaio
Jules Villard