Summary:
In practice this has not been observed to matter so far, since
treating `Splat N` as interpreted or uninterpreted does not matter
when `N` is a literal constant, and code seen so far only uses `Splat`
for zero initializers or memset with literal constant bytes.
Reviewed By: jvillard
Differential Revision: D24934118
fbshipit-source-id: 213e9724e
Summary:
0 and Splat 0 need to be treated the same since code relies on knowing
that 0 consists of all-0 bytes, and extracting a subsequence of a
Splat 0 yields 0. For example, initializing a struct to all-zeros and
then reading a member of pointer type out of it needs to produce the
null pointer. Therefore 0 and Splat 0 are redundant representations,
and all uses of Splat need to be updated to also handle 0.
This unfortunately leads to some near code duplication that seems to
be necessary. The issue is that 0 and Splat 0 are, from the backend's
perspective, constants in two distinct theories. Since 0 is chosen
over Splat 0 as the representation, the sequence theory solver needs
to treat 0 as if it was Splat 0, which duplicates some code handling
the general Splat cases.
Reviewed By: jvillard
Differential Revision: D24920758
fbshipit-source-id: 7c02be62b
Summary:
Global variables and function names in LLAIR are constant and so do
not need to be handled like normal assignable or shadowable
variables. This diff does this by changing the translation from LLAIR
to FOL to map globals and functions to uninterpreted constants instead
of variables.
Reviewed By: jvillard
Differential Revision: D24886571
fbshipit-source-id: efb8c9f49
Summary:
Localizing the entry of a procedure needs the globals (that the
procedure uses), but later creating a summary does not.
Reviewed By: jvillard
Differential Revision: D24886570
fbshipit-source-id: 8a7b18c58
Summary:
The computation of provable reachability through the heap currently
uses a set of variables whose values are either determined by the
desired roots or by the heap constraints. This requires globals to be
treated as variables. In preparation for distinguishing globals from
variables, this diff changes the reachability computation to use a set
of atomic terms instead of variables.
Reviewed By: jvillard
Differential Revision: D24886573
fbshipit-source-id: c0e6763b6
Summary:
No functional change, only simplifiying and making easier to
generalize.
Reviewed By: jvillard
Differential Revision: D24886572
fbshipit-source-id: e487b815d
Summary:
Distinguish expressions that name globals from registers. This leads
to clearer code, and globals are semantically distinct from general
registers. In particular, they are constant, so any machinery for
handling assignment does not need to consider them. This diff only
adds the distinction to LLAIR, it is not pushed through to FOL, which
will come later.
Reviewed By: jvillard
Differential Revision: D24846676
fbshipit-source-id: 3aca025bf
Summary:
This module represents the definition of a global constant, rather
than the global itself.
Reviewed By: jvillard
Differential Revision: D24846673
fbshipit-source-id: d47e67984
Summary:
Distinguish expressions that name functions from registers. This leads
to clearer code, and function names are semantically distinct from
general registers. In particular, they are constant, so any machinery
for handling assignment does not need to consider them. Unlike general
globals, they never have initializer expressions, and in particular
not recursive initializers. This diff only adds the distinction to
LLAIR, it is not pushed through to FOL, which will come later.
Reviewed By: jvillard
Differential Revision: D24846672
fbshipit-source-id: 2101f353f
Summary:
LLVM and Llair use a form of records, in particular for values of
constant structs and arrays. In Llair, these use standard `select` and
`update` operations a la McCarthy's theory of functional arrays, with
a compact `record` operation for constructing complete records. This
is fine and logically well-understood. The issue is that once
constructed, these values are accessed using instructions that (may)
operate over byte-ranges, rather than struct member indices. The
backend uses a theory of sequences to represent such values (the
contents of memory). So some code depends on high fidelity
interoperation between these two views.
This diff resolves this by removing the record theory from the backend
and instead encoding them using the sequence theory. The approach
taken keeps records in Llair and translates them to sequences in
Llair_to_Fol. This choice is made since the encoding into the sequence
theory involves terms that do not have types that are expressible in
terms of the source types. In particular, `(update r i e)`, is encoded
as the concatenation of the prefix of `r` up to the offset of index
`i`, followed by `e` (possibly with padding), and then the suffix of
`r` from index `i+1` on. The prefix and suffix sequences do not
necessarily have source-expressible types.
Reviewed By: jvillard
Differential Revision: D24800866
fbshipit-source-id: e7238c558
Summary:
The support for recursive references to globals from within their
initializers is enough to handle all the cases of recursive structs
that have been encountered so far. Therefore this diff removes the
complication of recursive records entirely.
Reviewed By: jvillard
Differential Revision: D24772955
fbshipit-source-id: f59f06257
Summary:
It happens so seldomly that it is not worth it to optimistically
assume that linking will make opaque types sized. In particular, it is
incongruent for `Typ.is_sized` to hold and then `Typ.size_of` to
raise.
Reviewed By: jvillard
Differential Revision: D24772956
fbshipit-source-id: 96a72a5cf
Summary:
This information is needed to mediate between index-based
operations (such as on records) and offset-based operations (such as
load/store). Since it is fragile to recompute, the approach here is to
query llvm during translation and store the result.
Reviewed By: jvillard
Differential Revision: D24772954
fbshipit-source-id: ad22c3ecf
Summary: Do not fail when resolving the realpath of a debug info path.
Reviewed By: jvillard
Differential Revision: D24746237
fbshipit-source-id: b9dc35176
Summary:
Change Arith.map to not descend through non-interpreted arithmetic
operators. For example, in `2×(x × y) + 3×z + 4`, `map ~f` will apply
`f` to the subterms `x × y` and `z`, but not `x` or `y`.
The logical notion of "subterm" that is needed by the solver does not
coincide with the representation. This is essentially due to not
"flattening" or "purifying" terms. That is, traditionally `x × y`
would not be permitted as an indeterminate of a polynomial. Instead, a
new variable would need to be introduced: `v = x × y` and then the
polynomial would be expressed as `2×v + 3×z + 4`. Taking maximal
non-interpreted subterms as the definition of "subterm" results in
subterms in the non-flattened representation that are equivalent to
those that would result from flattening the representation.
Reviewed By: jvillard
Differential Revision: D24746235
fbshipit-source-id: d8fcf46a1
Summary:
The implementation of Arithmetic relies on the partial projection from
terms to polynomials. This diff enables it to also embed polynomials
back into terms.
Reviewed By: jvillard
Differential Revision: D24746223
fbshipit-source-id: b6010e7b7
Summary:
Add a distinction between interpreted and uninterpreted arithmetic
terms, and use it in Context.classify. This enables correctly
classifying non-linear terms such as `x × y` as uninterpreted.
Reviewed By: ngorogiannis
Differential Revision: D24746228
fbshipit-source-id: 1a4b0e3bd
Summary:
It was possible for the scope of existentials to be violated. In
particular, before this diff the order of re-quantifying the
existentials and conjoining the non-eliminated equations from the
solution of solving for existentials was wrong.
Reviewed By: ngorogiannis
Differential Revision: D24746231
fbshipit-source-id: d96cc60a6
Summary:
In the process of computing `Context.solve`, fresh variables can be
generated. Not all of these end up in the final solution
substitution. Currently all of the freshly generated variables are
returned to the client, which leads to extraneous existentials. This
diff trims the returned fresh variables to only those that appear in
the final solution.
Reviewed By: ngorogiannis
Differential Revision: D24746241
fbshipit-source-id: 59a2f221b
Summary:
Since floats of any width are interpreted the same (as exact rationals
where possible and uninterpreted constants otherwise), this does not
introduce additional infidelity.
Reviewed By: da319
Differential Revision: D24746225
fbshipit-source-id: bc8e7bdb9
Summary:
Since non-integral address spaces are not currently supported anyhow,
this does not introduce additional infidelity.
Reviewed By: da319
Differential Revision: D24746234
fbshipit-source-id: 1f6887a78
Summary: Just to make the source and destination types of the conversion more clear.
Reviewed By: da319
Differential Revision: D24746239
fbshipit-source-id: 592c7d0f1
Summary:
Since Context treats only equality directly, formulas involving other
literals can normalize to false when the context is not unsat. This
diff changes Sh.star to check this case, and return the canonical
false symbolic heap.
Reviewed By: da319
Differential Revision: D24746227
fbshipit-source-id: 50a51b8a6
Summary:
When exceptions are used due to the lack of goto, use `raise_notrace`
instead of `raise` to avoid the overhead of populating the backtrace.
Reviewed By: ngorogiannis
Differential Revision: D24630525
fbshipit-source-id: c5051d9c4
Summary:
The implementation in Context, in terms of Fol.Term and Fol.Formula,
can now be used instead of Ses.Equality, implemented using
Ses.Term. The Ses modules can now be removed.
Reviewed By: jvillard
Differential Revision: D24532362
fbshipit-source-id: cee9791b7
Summary:
Adapt the solver implementation from Ses.Equality to Context, and use
the interface of Fol.Context.
Reviewed By: jvillard
Differential Revision: D24532348
fbshipit-source-id: 2c6d41669
Josh Berdine