nondet Namespace Reference

Functions
int	_nondet_size (int max_size)
int	_nondet_dict_size (int max_size)
int	_nondet_str_key_bound (int max_size)
int	_nondet_bool_key_bound (int max_size)
list	_nondet_list_int (int max_size)
list	_nondet_list_float (int max_size)
list	_nondet_list_bool (int max_size)
list	_nondet_list_str (int max_size)
dict	_nondet_dict_int_int (int max_size)
dict	_nondet_dict_int_float (int max_size)
dict	_nondet_dict_int_bool (int max_size)
dict	_nondet_dict_int_str (int max_size)
dict	_nondet_dict_str_int (int max_size)
dict	_nondet_dict_str_float (int max_size)
dict	_nondet_dict_str_bool (int max_size)
dict	_nondet_dict_str_str (int max_size)
dict	_nondet_dict_bool_int (int max_size)
dict	_nondet_dict_bool_float (int max_size)
dict	_nondet_dict_bool_bool (int max_size)
dict	_nondet_dict_bool_str (int max_size)
list	nondet_list (int max_size=_DEFAULT_NONDET_SIZE, Any elem_type=None)
dict	nondet_dict (int max_size=_DEFAULT_NONDET_SIZE, Any key_type=None, Any value_type=None)

Variables
int	_DEFAULT_NONDET_SIZE = 8
int	_MAX_NONDET_STR_KEYS = 8
int	_MAX_NONDET_BOOL_KEYS = 2

Detailed Description

Operational model for ESBMC's non-deterministic Python collection generators.

Every builder here is *monomorphic*: it constructs one element type only, and
calls the scalar generator (``nondet_int()`` and friends) afresh for each
element, so distinct indices hold independent symbolic values.

Monomorphism is a requirement, not a style choice.  A single builder that
dispatches on a type tag --

    if kind == 0: result.append(nondet_int())
    else:         result.append(nondet_float())

-- is silently mistyped by the frontend: every element degrades to the first
branch's type, so a float list cannot hold 0.5 and properties over it are
proved vacuously.  One function per element type avoids the dispatch entirely.

The preprocessor rewrites ``nondet_list``/``nondet_dict`` to the matching
builder below (``_parse_nondet_collection_call`` in
``preprocessor/loop_mixin.py``), so a call in *any* expression position -- an
annotated assignment, a return, a call argument -- gets fresh elements.  A
module that defines its own ``nondet_list``/``nondet_dict`` is left alone; an
*imported* one is still intercepted, which is what SV-COMP harnesses expect.
The public ``nondet_list``/``nondet_dict`` at the end of this file exist so the
name resolves for ``from esbmc import nondet_list``; direct calls are rewritten
before they reach those bodies.

Dictionary keys are concrete and sequential rather than symbolic: symbolic keys
turn every ``contains``/``find_index`` check into a linear scan of symbolic
comparisons, which is quadratic in the solver, while concrete keys make each
check trivially decidable and leave the values fully non-deterministic.  An
int-keyed dict is inserted in a loop and so honours any requested bound; a
str-keyed one is capped at ``_MAX_NONDET_STR_KEYS`` by the key table, and a
bool-keyed one at two, since that is how many bool keys exist.  Both clamp the
assumed size to their cap -- otherwise a size above it would be assumed
reachable but never populated.

See esbmc/esbmc#7575 for the element-reuse defect this file's shape addresses.

USAGE:
    # Lists:
    x = nondet_list()                                     # int list, size [0, 8]
    x = nondet_list(5)                                    # int list, size [0, 5]
    x = nondet_list(elem_type=nondet_float())             # float list, size [0, 8]
    x = nondet_list(max_size=10, elem_type=nondet_bool()) # bool list, size [0, 10]

    # Dictionaries:
    d = nondet_dict()                                     # int->int dict, size [0, 8]
    d = nondet_dict(5)                                    # int->int dict, size [0, 5]
    d = nondet_dict(key_type=nondet_str(), value_type=nondet_float())
    d = nondet_dict(max_size=10, key_type=nondet_int(), value_type=nondet_bool())

    An int-keyed dict honours any `max_size`; a str-keyed one is capped at 8
    entries and a bool-keyed one at 2 (see `_MAX_NONDET_STR_KEYS`).

Function Documentation

_nondet_bool_key_bound()

int nondet._nondet_bool_key_bound ( int max_size )

protected

Clamp a requested size to the two keys a bool admits.

_nondet_dict_bool_bool()

dict nondet._nondet_dict_bool_bool ( int max_size )

protected

Return a dict of size [0, max_size] mapping bool keys to independent bool values.

_nondet_dict_bool_float()

dict nondet._nondet_dict_bool_float ( int max_size )

protected

Return a dict of size [0, max_size] mapping bool keys to independent float values.

_nondet_dict_bool_int()

dict nondet._nondet_dict_bool_int ( int max_size )

protected

Return a dict of size [0, max_size] mapping bool keys to independent int values.

_nondet_dict_bool_str()

dict nondet._nondet_dict_bool_str ( int max_size )

protected

Return a dict of size [0, max_size] mapping bool keys to independent str values.

_nondet_dict_int_bool()

dict nondet._nondet_dict_int_bool ( int max_size )

protected

Return a dict of size [0, max_size] mapping int keys to independent bool values.

_nondet_dict_int_float()

dict nondet._nondet_dict_int_float ( int max_size )

protected

Return a dict of size [0, max_size] mapping int keys to independent float values.

_nondet_dict_int_int()

dict nondet._nondet_dict_int_int ( int max_size )

protected

Return a dict of size [0, max_size] mapping int keys to independent int values.

_nondet_dict_int_str()

dict nondet._nondet_dict_int_str ( int max_size )

protected

Return a dict of size [0, max_size] mapping int keys to independent str values.

_nondet_dict_size()

int nondet._nondet_dict_size ( int max_size )

protected

Generate a non-deterministic dict size in range [0, max_size].

Args:
    max_size: Maximum entry count (inclusive).

Returns
-------
int
    A non-deterministic integer in [0, max_size].

_nondet_dict_str_bool()

dict nondet._nondet_dict_str_bool ( int max_size )

protected

Return a dict of size [0, max_size] mapping str keys to independent bool values.

_nondet_dict_str_float()

dict nondet._nondet_dict_str_float ( int max_size )

protected

Return a dict of size [0, max_size] mapping str keys to independent float values.

_nondet_dict_str_int()

dict nondet._nondet_dict_str_int ( int max_size )

protected

Return a dict of size [0, max_size] mapping str keys to independent int values.

_nondet_dict_str_str()

dict nondet._nondet_dict_str_str ( int max_size )

protected

Return a dict of size [0, max_size] mapping str keys to independent str values.

_nondet_list_bool()

list nondet._nondet_list_bool ( int max_size )

protected

Return a list of size [0, max_size] whose elements are independent bools.

_nondet_list_float()

list nondet._nondet_list_float ( int max_size )

protected

Return a list of size [0, max_size] whose elements are independent floats.

_nondet_list_int()

list nondet._nondet_list_int ( int max_size )

protected

Return a list of size [0, max_size] whose elements are independent ints.

_nondet_list_str()

list nondet._nondet_list_str ( int max_size )

protected

Return a list of size [0, max_size] whose elements are independent strs.

_nondet_size()

int nondet._nondet_size ( int max_size )

protected

Generate a non-deterministic size in range [0, max_size].

Args:
    max_size: Maximum size (inclusive).

Returns
-------
int
    A non-deterministic integer in [0, max_size].

_nondet_str_key_bound()

int nondet._nondet_str_key_bound ( int max_size )

protected

Clamp a requested size to the number of str keys this model can build.

nondet_dict()

dict nondet.nondet_dict	(	int	max_size = _DEFAULT_NONDET_SIZE,
		Any	key_type = None,
		Any	value_type = None )

Return a non-deterministic dictionary.

Kept so the name resolves (see `nondet_list`); direct calls never reach the
body. Keys and values are independent ints.

nondet_list()

list nondet.nondet_list	(	int	max_size = _DEFAULT_NONDET_SIZE,
		Any	elem_type = None )

Return a non-deterministic list.

Kept so the name resolves -- ``from esbmc import nondet_list`` binds to this
definition rather than to esbmc.py's empty stub. Direct calls never reach
the body: the preprocessor rewrites them to the builder for their element
type. Elements are independent ints.

Variable Documentation

_DEFAULT_NONDET_SIZE

int nondet._DEFAULT_NONDET_SIZE = 8

protected

_MAX_NONDET_BOOL_KEYS

int nondet._MAX_NONDET_BOOL_KEYS = 2

protected

_MAX_NONDET_STR_KEYS

int nondet._MAX_NONDET_STR_KEYS = 8

protected