Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add an abstraction for "uninitialized or" #138

Open
arthaud opened this issue Jul 11, 2019 · 0 comments
Open

Add an abstraction for "uninitialized or" #138

arthaud opened this issue Jul 11, 2019 · 0 comments
Labels
C-false-positive Category: False Positive C-feature-request Category: Feature Request L-c Language: C P-medium Priority: Medium

Comments

@arthaud
Copy link
Member

arthaud commented Jul 11, 2019

The current analysis is imprecise when merging branches where one side has uninitialized variables.

For instance:

#include <ikos/analyzer/intrinsic.h>

int main(int argc, char** argv) {
    int tab[10];

    if (argc > 2) {
        tab[0] = 2;
    }

    __ikos_print_values("tab[0]", tab[0]);

    return 0;
}

The output of the analyzer is:

test.c:10:5: __ikos_print_values("tab[0]", tab[0]):
	tab[0] is in [-2147483648, 2147483647]
	tab[0] may be uninitialized

We could add an abstraction that remembers whether a value is uninitialized or within a given range.

This should help with #136.

@arthaud arthaud added C-false-positive Category: False Positive L-c Language: C P-medium Priority: Medium C-feature-request Category: Feature Request labels Jul 11, 2019
arthaud added a commit that referenced this issue Sep 24, 2019
This patch is a big refactoring of some abstract domain interfaces.

Non exhaustive list of changes:
* Add `scalar::AbstractDomain`, a scalar abstract domain interface. It
models an abstract domain that can operate on machine integer variables,
floating point variables and pointer variables. It does not provide the
access to the underlying domains like `pointer::AbstractDomain` does,
which will allow the implementation of #137 and #138;
* Add `scalar::CompositeDomain`, the implementation of a scalar abstract
domain using a machine integer abstract domain, an uninitialized
abstract domain, a nullity domain and a points to set map. This is
based on `pointer::PointerDomain`, but using the new interface;
* Add `scalar::MachineIntDomain` that wraps a machine integer abstract
domain and safely ignores floating point variables and pointer variables;
* Add `scalar::DummyDomain` that ignores all operations safely;
* Update `memory::AbstractDomain` to inherit from `scalar::AbstractDomain`.
The memory abstract domain interface is now a wrapper on a scalar domain,
adding memory operations;
* Update `memory::DummyDomain`: it now wraps a scalar abstract domain and
safely ignores memory operations;
* Update `memory::ValueDomain` to implement the new memory abstract
domain interface;
* Add `scalar::VariableTraits`, an interface for scalar variables;
* Add `CellFactoryTraits`, an interface for memory cell factories;
* Remove `pointer::AbstractDomain`, `pointer::DummyDomain`,
`pointer::PointerDomain` and `pointer::VariableTraits`;
* Add `NumericalExecutionEngine::implicit_bitcast()` that does not propagate
uninitialized variables but allows sign conversions;
* Update `NumericalExecutionEngine::exec(ar::Load*)`: reading uninitialized
memory is an error, so the result should always be initialized;
* Update `NumericalExecutionEngine::exec(ar::Store*)`: writing an
uninitialized variable is an error;
* Update `NumericalExecutionEngine::exec(ar::InsertElement*)`: allow
uninitialized aggregate operands;
* Update `UninitializedVariableChecker`: allow uninitialized aggregate
operands in `ar::InsertElement*`;
* `UninitializedVariableChecker` (uva) now only checks for uninitialized
variable operands, and not for uninitialized memory accesses. This will be
done in the Uninitialized Memory Analysis (see #99), coming soon;
* Move tests on uninitialized memory accesses to the `uma` folder;
* Enable the uninitialized variable analysis by default.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
C-false-positive Category: False Positive C-feature-request Category: Feature Request L-c Language: C P-medium Priority: Medium
Projects
None yet
Development

No branches or pull requests

1 participant