cprover
simplify_expr.cpp File Reference
#include "simplify_expr.h"
#include <algorithm>
#include "arith_tools.h"
#include "byte_operators.h"
#include "c_types.h"
#include "config.h"
#include "endianness_map.h"
#include "expr_util.h"
#include "fixedbv.h"
#include "invariant.h"
#include "mathematical_expr.h"
#include "namespace.h"
#include "pointer_offset_size.h"
#include "pointer_offset_sum.h"
#include "range.h"
#include "rational.h"
#include "rational_tools.h"
#include "simplify_utils.h"
#include "std_expr.h"
#include "string_constant.h"
#include "string_expr.h"
#include "symbol.h"
#include "simplify_expr_class.h"
+ Include dependency graph for simplify_expr.cpp:

Go to the source code of this file.

Functions

static simplify_exprt::resultt simplify_string_endswith (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.endsWith function when arguments are constant. More...
 
static simplify_exprt::resultt simplify_string_contains (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.contains function when arguments are constant. More...
 
static simplify_exprt::resultt simplify_string_is_empty (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.isEmpty function when arguments are constant. More...
 
static simplify_exprt::resultt simplify_string_compare_to (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.compareTo function when arguments are constant. More...
 
static simplify_exprt::resultt simplify_string_index_of (const function_application_exprt &expr, const namespacet &ns, const bool search_from_end)
 Simplify String.indexOf function when arguments are constant. More...
 
static simplify_exprt::resultt simplify_string_char_at (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.charAt function when arguments are constant. More...
 
static bool lower_case_string_expression (array_exprt &string_data)
 Take the passed-in constant string array and lower-case every character. More...
 
static simplify_exprt::resultt simplify_string_equals_ignore_case (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.equalsIgnorecase function when arguments are constant. More...
 
static simplify_exprt::resultt simplify_string_startswith (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.startsWith function when arguments are constant. More...
 
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array (const exprt &content, const namespacet &ns)
 Get char sequence from content field of a refined string expression. More...
 
bool simplify (exprt &expr, const namespacet &ns)
 
exprt simplify_expr (exprt src, const namespacet &ns)
 

Function Documentation

◆ lower_case_string_expression()

static bool lower_case_string_expression ( array_exprt string_data)
static

Take the passed-in constant string array and lower-case every character.

Definition at line 488 of file simplify_expr.cpp.

◆ simplify()

bool simplify ( exprt expr,
const namespacet ns 
)
Returns
returns true if expression unchanged; returns false if changed

Definition at line 2693 of file simplify_expr.cpp.

◆ simplify_expr()

exprt simplify_expr ( exprt  src,
const namespacet ns 
)

Definition at line 2698 of file simplify_expr.cpp.

◆ simplify_string_char_at()

static simplify_exprt::resultt simplify_string_char_at ( const function_application_exprt expr,
const namespacet ns 
)
static

Simplify String.charAt function when arguments are constant.

Parameters
exprthe expression to simplify
nsnamespace
Returns
: the modified expression or an unchanged expression

Definition at line 448 of file simplify_expr.cpp.

◆ simplify_string_compare_to()

static simplify_exprt::resultt simplify_string_compare_to ( const function_application_exprt expr,
const namespacet ns 
)
static

Simplify String.compareTo function when arguments are constant.

The behaviour is similar to the implementation in OpenJDK: http://hg.openjdk.java.net/jdk8/jdk8/jdk/file/687fd7c7986d/src/share/classes/java/lang/String.java#l1140

Parameters
exprthe expression to simplify
nsnamespace
Returns
the modified expression or an unchanged expression

Definition at line 254 of file simplify_expr.cpp.

◆ simplify_string_contains()

static simplify_exprt::resultt simplify_string_contains ( const function_application_exprt expr,
const namespacet ns 
)
static

Simplify String.contains function when arguments are constant.

Definition at line 184 of file simplify_expr.cpp.

◆ simplify_string_endswith()

static simplify_exprt::resultt simplify_string_endswith ( const function_application_exprt expr,
const namespacet ns 
)
static

Simplify String.endsWith function when arguments are constant.

Parameters
exprthe expression to simplify
nsnamespace
Returns
the modified expression or an unchanged expression

Definition at line 156 of file simplify_expr.cpp.

◆ simplify_string_equals_ignore_case()

static simplify_exprt::resultt simplify_string_equals_ignore_case ( const function_application_exprt expr,
const namespacet ns 
)
static

Simplify String.equalsIgnorecase function when arguments are constant.

Parameters
exprthe expression to simplify
nsnamespace
Returns
: the modified expression or an unchanged expression

Definition at line 516 of file simplify_expr.cpp.

◆ simplify_string_index_of()

static simplify_exprt::resultt simplify_string_index_of ( const function_application_exprt expr,
const namespacet ns,
const bool  search_from_end 
)
static

Simplify String.indexOf function when arguments are constant.

Parameters
exprthe expression to simplify
nsnamespace
search_from_endreturn the last instead of the first index
Returns
: the modified expression or an unchanged expression

Definition at line 303 of file simplify_expr.cpp.

◆ simplify_string_is_empty()

static simplify_exprt::resultt simplify_string_is_empty ( const function_application_exprt expr,
const namespacet ns 
)
static

Simplify String.isEmpty function when arguments are constant.

Parameters
exprthe expression to simplify
nsnamespace
Returns
the modified expression or an unchanged expression

Definition at line 229 of file simplify_expr.cpp.

◆ simplify_string_startswith()

static simplify_exprt::resultt simplify_string_startswith ( const function_application_exprt expr,
const namespacet ns 
)
static

Simplify String.startsWith function when arguments are constant.

Parameters
exprthe expression to simplify
nsnamespace
Returns
: the modified expression or an unchanged expression

Definition at line 561 of file simplify_expr.cpp.

◆ try_get_string_data_array()

optionalt<std::reference_wrapper<const array_exprt> > try_get_string_data_array ( const exprt content,
const namespacet ns 
)

Get char sequence from content field of a refined string expression.

If content is of the form &id[e], where id is an array-typed symbol expression (and e is any expression), return the value of the symbol id (as given by the value field of the symbol in the namespace ns); otherwise return an empty optional.

Parameters
contentcontent field of a refined string expression
nsnamespace
Returns
array expression representing the char sequence which forms the content of the refined string expression, empty optional if the content cannot be determined

Definition at line 1837 of file simplify_expr.cpp.