Summary:
- Change representation of Concat expressions from curried binary
operator to an nary one. This enables normalizing Concat expressions
with respect to associativity.
- Generalize Exp.solve to return a map rather than a pair of exps, to
enable expressing cases where solving an equation yields multiple
equations.
- Strengthen solver with implied equalities between sums of sizes of
concatenations of byte arrays.
Reviewed By: ngorogiannis
Differential Revision: D14297865
fbshipit-source-id: b40871559
Summary: After a redeclaration of a global constant, it is not parsed as ICE(integral constant expression), which results in FN.
Reviewed By: ezgicicek
Differential Revision: D14299288
fbshipit-source-id: 394afd595
Summary:
It assigns symbolic values for global variables in the load commands. However, it does not instantiate the symbols for the global variables yet, which will be addressed in another diff.
Depends on D14208643
Reviewed By: ezgicicek
Differential Revision: D14257619
fbshipit-source-id: f9113c8a3
Summary:
the predicate to check that a decl is const was not working for VarDecl.
This diff fixes this
Reviewed By: jvillard
Differential Revision: D14106798
fbshipit-source-id: 1f6c24113
Summary:
This patch adds an embarrassingly inefficient implementation of a
decision procedure for equality in the theories of uninterpreted
functions and linear arithmetic. A Shostak-style approach, where a
single congruence closure structure is shared by all theories, is
used. This is mostly based on the corrected variant of Shostak's
algorithm from:
Harald Rueβ and Natarajan Shankar. 2001. Deconstructing Shostak. In
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer
Science (LICS '01).
Reviewed By: jvillard
Differential Revision: D14251655
fbshipit-source-id: 8a080145f
Summary:
Now with rational coefficients, dividing a polynomial by an integer
can be simplified.
Reviewed By: jvillard
Differential Revision: D14251656
fbshipit-source-id: 01094bc61
Summary:
Exp simplification must not generate fresh subexpressions in its
output that do not appear in its input, lest congruence closure gets
confused. Previously this check only considered immediate
subexpressions, which is overly restrictive.
Reviewed By: ngorogiannis
Differential Revision: D14251653
fbshipit-source-id: f8d5d9756
Summary:
Trace.report is essentially redundant with Trace.fail, and does not
behave as well wrt flushing when raising exceptions.
Reviewed By: ngorogiannis
Differential Revision: D14251657
fbshipit-source-id: 69a61c915
Summary:
Represent Add and Mul directly as associative and commutative nary
operations, rather than have Add and Mul operators and a separate AppN
nary application.
Reviewed By: ngorogiannis
Differential Revision: D14231544
fbshipit-source-id: 4fb7a06cf
Summary:
- docstrings
- mli
- split `get_control_maps`: `get_loop_head_to_source_nodes` is used both by Cost and Hoisting. If using both analyzers, it is called twice whereas it could be shared (which is done later in the stack of diffs).
Reviewed By: ezgicicek
Differential Revision: D14258372
fbshipit-source-id: 29addddb7
Summary:
Figure out where libgmp and libmpfr are auto-magically by looking at where
`ldd` (or `otool` on osx) thinks they are.
This way we don't need to hardcode as much.
Reviewed By: ngorogiannis
Differential Revision: D14208580
fbshipit-source-id: 3b2dca5b2
Summary:
:
Since traces are attached to symbols, currently it will make no difference.
Calling `subst` on `Top` or on constant is constant-time.
But I need this to record `Call` trace elements for `Top`.
Reviewed By: ezgicicek
Differential Revision: D14249265
fbshipit-source-id: d3aa4ac9e
Summary:
This diff differentiates proof obligations by allocsites. Sizes and
offsets of arrays were joined when making proof obligations.
Reviewed By: mbouaziz
Differential Revision: D14163149
fbshipit-source-id: cb6608c16
Summary:
The Eradicate backend is reporting nullable type errors, that are not always necessarily leading to null pointer exceptions.
For example, the analysis is designed to be consistent with the Java type system and report on the following code:
String foo(boolean test) {
Object object = test ? new Object() : null;
if (test) {
return object.toString(); // the analysis reports here
}
}
even though the code will not crash.
In order to make this aspect clear, this diff renames the warnings `Null Method Call` and `Null Field Access` into `Nullable Dereference`
Reviewed By: ngorogiannis
Differential Revision: D14001979
fbshipit-source-id: ff1285283
Summary:
`Utils.with_intermediate_temp_file_out` is conceptually simpler. Plus,
this removes a dependency on Unix.flock, which is not portable under
Windows.
Pull Request resolved: https://github.com/facebook/infer/pull/1066
Differential Revision: D14208138
Pulled By: jvillard
fbshipit-source-id: 7587007e5
Summary:
- Add nary expressions implemented using a form of multisets which
support any integer multiplicity
- Reimplement polynomials using new nary expressions
- Move the decomposition of exps into "base plus offset" form into
Exp, to enforce simplification invariants
- Revise expression simplification to cooperate with congruence
closure (mainly: simplification should not invent new
subexpressions)
- Reimplement congruence closure plus integer offsets to
+ cope with new representation of polynomials using nary expression forms
+ be diligent about maintaining which expressions are in the relation
+ add lots of invariant checking for the correlations between the
componnents of the congruence closure data structures
Reviewed By: jvillard
Differential Revision: D14075512
fbshipit-source-id: 2dbaf3d11
Summary:
Even pretty-printed congruence relations are verbose, and most
operations do not change much of the relation. So on return, print
only the symmetric difference between input and output relations.
Reviewed By: mbouaziz
Differential Revision: D14075513
fbshipit-source-id: b1f0ae6d0
Mehdi Bouaziz
Josh Berdine
Sungkeun Cho
Nikos Gorogiannis
Ezgi Çiçek
Dino Distefano
Jules Villard
Jeremy Dubreil
Boris Yakobowski