When the index is not constant when accessing a constant size array, we
should expand the expression into `{array[0]; array[1];...}[index]` so
that the relation with field sensitivity expressions `array[[0]]`,
`array[[1]]`, etc, is not lost.
In some cases, like the test in regression/cbmc/Global_Initialization2,
the array type is incomplete and changed in the symbol table after the
main function has been converted, leading to inconsistencies.
This means we can get nil instead of the size in
field_sensitivityt::apply, though the actual size is present in the
symbol table.
The issue is reported here: https://github.com/diffblue/cbmc/issues/5022
The use of field_sensitivity for arrays can be expensive for big arrays
so we have to set a limit on the size of constant arrays which get
processed.
The value 64 was determined by changing the size of the array in the
test regression/cbmc/variable-access-to-constant-array and reducing it
until there was no significant difference in execution time between the
versions of CBMC with and without array cell propagation.
For the chosen value the execution time was around 0.05 second in both
cases (for comparison with size 1024 the time with propagation was 0.5
sec, against 0.1 without).
This may lead to application of array-cell-sensitivity (i.e. querying the symbol
some_array[[1]] instead of some_array[some_index]), leading to higher precision.
Some tests must be amended because better constant propagation causes some test behaviour
to change as symex has better knowledge regarding the targets of pointers.
This allows applying constant propagation without upgrading non-constant symbols to L2,
which is useful for the dereferencing logic, as the value-set used to resolve pointer
aliasing is indexed by L1 names.
When printing a character, it is required to escape the ' character, but
when printing it as part of a string, it is not. Therefore, this has
been separated into two separate functions.
This is to make sure that the length of the array before the assignment
isn't unconstrained. Otherwise it could be set to be arbitrarily large
by the solver which will causes invalid traces.
This option takes a function name (usually the test harness entry point) and
inserts `assert(false)` at the end of the function body. This assertion is
*expected to fail*. If it passes then this may indicate that the test harness
has inconsistent assumptions. Note that there are other reasons why the assert
may pass (such as insufficient loop unwind depth). It is up to the user to
interpret the results.
This tests the solver directly on a set of desired formula instead of
through symex as would a regression test.
This can be easier to debug when trying to track a bug or add an new
feature, as the correspondence with the string solver code would be
easier to see.
Even if they are not equations, they may contain formulas talking about
char arrays and other expressions which require special handling by the solver.
Accept formulas that are not equations as input.
This is to make the solver more robust to different kind of formulas.
In particular, formulas of the form
`guard1 => result = some_string_builin_function(s)` should be accepted.
This make it handle the cases where the function application is not
directly the right hand side of the equation but may be deeper inside
the expression.
The add_node function was only handling expressions of the form:
`lhs = builtin_function(args)`
We make it handle more general expressions and look recursively for
functions to replace, for instance
`(lhs == a) && (builtin_function(b) == builtin_function(c))`
would be replaced by
`(lhs == a) && (string_builtin_return1 == string_builtin_return2)`.
Since the argument is a unique_ptr, it cannot be copied so having the
function take the argument by copy means that it has to be moved at the
function call, which makes clear from there that the argument is moved
and shouldn't be used afterwards.
These are derivatives of constant_exprt which give a pointer's numerical address in the usual
constant value slot, but which also have an operand giving its symbolic value (e.g. "0xabcd0004"
vs. "&some_object + 4"
Add regression tests that check that the constant propagator does not simplify
substring() invocations with only constant arguments when the indices are out of
bounds.
This implements constant propagation of ID_cprover_string_substring_func
function application expressions. These are in turn used by the various
substring operations of String and StringBuilder.
Romain Brenguier