Loading...

Searching...

No Matches

string_refinement.h File Reference

String support via creating string constraints and progressively instantiating the universal constraints as needed. More...

#include <util/union_find_replace.h>
#include <solvers/refinement/bv_refinement.h>
#include "string_constraint_generator.h"
#include "string_dependencies.h"
#include "string_refinement_util.h"

+ Include dependency graph for string_refinement.h:

[フレーム]

+ This graph shows which files directly or indirectly include this file:

[フレーム]

Go to the source code of this file.

Classes

class string_refinementt

struct string_refinementt::configt

struct string_refinementt::infot

string_refinementt constructor arguments More...

Macros

#define OPT_STRING_REFINEMENT

#define HELP_STRING_REFINEMENT

#define OPT_STRING_REFINEMENT_CBMC

#define HELP_STRING_REFINEMENT_CBMC

#define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()

Functions

exprt substitute_array_lists (exprt expr, std::size_t string_max_length)

union_find_replacet string_identifiers_resolution_from_equations (const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)

Symbol resolution for expressions of type string typet.

exprt substitute_array_access (exprt expr, symbol_generatort &symbol_generator, const bool left_propagate)

Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expressions, in particular:

Detailed Description

String support via creating string constraints and progressively instantiating the universal constraints as needed.

The procedure is described in the PASS paper at HVC'13: "PASS: String Solving with Parameterized Array and Interval Automaton" by Guodong Li and Indradeep Ghosh

Definition in file string_refinement.h.

Macro Definition Documentation

◆ DEFAULT_MAX_NB_REFINEMENT

#define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()

Definition at line 61 of file string_refinement.h.

◆ HELP_STRING_REFINEMENT

#define HELP_STRING_REFINEMENT

Value:

" {y--no-refine-strings} \t turn off string refinement\n" \

" {y--string-printable} \t restrict to printable strings and characters\n" \

" {y--string-non-empty} \t restrict to non-empty strings (experimental)\n" \

" {y--string-input-value} {ust} \t " \

"restrict non-null strings to a fixed value {ust}; the switch can be used " \

"multiple times to give several strings\n" \

" {y--max-nondet-string-length} {un} \t " \

"bound the length of nondet (e.g. input) strings. Default is " + \

std::to_string(MAX_CONCRETE_STRING_SIZE - 1) + \

"; note that setting the value higher than this does not work " \

"with {y--trace} or {y--validate-trace}.\n"

MAX_CONCRETE_STRING_SIZE

const std::size_t MAX_CONCRETE_STRING_SIZE

Definition magic.h:14

Definition at line 38 of file string_refinement.h.

◆ HELP_STRING_REFINEMENT_CBMC

#define HELP_STRING_REFINEMENT_CBMC

Value:

" {y--refine-strings} \t use string refinement (experimental)\n" \

" {y--string-printable} \t restrict to printable strings (experimental)\n"

Definition at line 57 of file string_refinement.h.

◆ OPT_STRING_REFINEMENT

#define OPT_STRING_REFINEMENT

Value:

"(no-refine-strings)" \

"(string-printable)" \

"(string-input-value):" \

"(string-non-empty)" \

"(max-nondet-string-length):"

Definition at line 31 of file string_refinement.h.

◆ OPT_STRING_REFINEMENT_CBMC

#define OPT_STRING_REFINEMENT_CBMC

Value:

"(refine-strings)" \

"(string-printable)"

Definition at line 53 of file string_refinement.h.

Function Documentation

◆ string_identifiers_resolution_from_equations()

union_find_replacet string_identifiers_resolution_from_equations ( const std::vector< equal_exprt > & equations,

const namespacet & ns,

messaget::mstreamt & stream

)

Symbol resolution for expressions of type string typet.

We record equality between these expressions in the output if one of the function calls depends on them.

Parameters: equations list of equations

ns namespace

stream output stream

Returns: union_find_replacet structure containing the correspondences.

Definition at line 470 of file string_refinement.cpp.

◆ substitute_array_access()

exprt substitute_array_access ( exprt expr,

symbol_generatort & symbol_generator,

const bool left_propagate

)

Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expressions, in particular:

for an array access arr[index], where: arr := {12, 24, 48} the constructed expression will be: index==0 ? 12 : index==1 ? 24 : 48
for an array access arr[index], where: arr := array_of(12) with {0:=24} with {2:=42} the constructed expression will be: index==0 ? 24 : index==2 ? 42 : 12
for an array access (g1?arr1:arr2)[x] where arr1 := {12} and arr2 := {34}, the constructed expression will be: g1 ? 12 : 34
for an access in an empty array { }[x] returns a fresh symbol, this corresponds to a non-deterministic result Note that if left_propagate is set to true, the with case will result in something like: index <= 0 ? 24 : index <= 2 ? 42 : 12
Parameters

expr an expression containing array accesses

symbol_generator a symbol generator

left_propagate should values be propagated to the left in with expressions

Returns
an expression containing no array access

Definition at line 1282 of file string_refinement.cpp.

◆ substitute_array_lists()

exprt substitute_array_lists ( exprt expr,

std::size_t string_max_length

)