Summary:
The backend does not generally interpret conditional expressions
specially. Therefore it is logically stronger to hoist them over other
boolean exps, for example normalizing
`e = (c ? t : f)` to `(c ? e = t : e =f)`
This enables the treatment of top-level conditional expressions in
terms of disjunction, conjunction and negation.
Reviewed By: mbouaziz
Differential Revision: D14495815
fbshipit-source-id: 4f2e8053f
Summary:
Eq and Dq expressions are interpreted by Equality and Exp, rather than
being considered uninterpreted functions. Classifying them as
interpreted results in stronger Equality normalization.
Reviewed By: mbouaziz
Differential Revision: D14495817
fbshipit-source-id: 44bb376c0
Summary:
The dnf implementation dates to before nested existentials were
added. Updating it was overlooked, and it is just wrong.
Reviewed By: ngorogiannis
Differential Revision: D14481988
fbshipit-source-id: 9bba570f0
Summary:
Also minor change to make strlen implementation syntactically closer
to spec.
Reviewed By: ngorogiannis
Differential Revision: D14403647
fbshipit-source-id: 48c771329
Summary:
Some functions are translated directly to an expression, rather than a
function call. The llvm instructions for calling functions that may
and may not raise exceptions differ (Invoke and Call, resp.). This
diff adds support for the Invoke case.
Reviewed By: jvillard
Differential Revision: D14385596
fbshipit-source-id: 24458d960
Summary:
These tell llvm that contents of memory will not change during
execution of some code, which the analyzer does not need.
Reviewed By: jvillard
Differential Revision: D14385597
fbshipit-source-id: 0ef566a6f
Summary:
The backend has an implicit assumption that the entry block's locals
are all the function locals, not just those that happen to appear in
the entry block.
An alternative would be to collect the inverse renaming substitutions
produced by symbolic execution of jumps, which rename variables to
avoid clashes with the destination block's locals. These inverse
substitutions could be applied upon function return, in inverse
order. The complication with this approach is that it would be
necessary to distinguish between a destination local that clashes
because it has the same name as a local of some function higher in the
call stack versus a clash due to being a previous incarnation of the
same local due to a control-flow cycle. Accumulating unrenamings for
the latter case is expensive and pointless, as well as incongrous with
true interprocedural extensions.
So it seems preferable to exploit the asymmetry between the entry
block and others a bit more.
Reviewed By: jvillard
Differential Revision: D14354530
fbshipit-source-id: 815cdb224
Summary: An initial set of basic sanity checks for frame inference.
Reviewed By: mbouaziz
Differential Revision: D14323549
fbshipit-source-id: d7cd4235f
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:
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:
- 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:
This is significant for operations involving the NULL pointer, which
is an integer of pointer type.
Reviewed By: mbouaziz
Differential Revision: D14075516
fbshipit-source-id: b727cb4c8
Summary:
Comparison operations always return Typ.bool, and Add/Mul/Integer exps
are typed. Use these types to check that arguments are type correct up
to Typ.castable.
Reviewed By: mbouaziz
Differential Revision: D12854504
fbshipit-source-id: fff1426d5
Summary:
Require Exp clients to provide the type of the result of arithmetic
operations.
Reviewed By: mbouaziz
Differential Revision: D12854511
fbshipit-source-id: cc91a39ca
Summary:
Previously only the arguments of binary operations on integers were
clamped to the given bitwidth, but the results could overflow. This
was incorrect.
Also, use a clamped version of equality to simplify equality
expressions. This was previously overlooked.
Reviewed By: mbouaziz
Differential Revision: D12854502
fbshipit-source-id: 8786b4217
Josh Berdine