cprover
string_constraint_generator_format.cpp File Reference

Generates string constraints for the Java format function. More...

#include <iomanip>
#include <string>
#include <regex>
#include <vector>
#include <util/std_expr.h>
#include <util/unicode.h>
#include "string_builtin_function.h"
#include "string_constraint_generator.h"
+ Include dependency graph for string_constraint_generator_format.cpp:

Go to the source code of this file.

Classes

class  format_specifiert
 
class  format_textt
 
class  format_elementt
 

Functions

static format_specifiert format_specifier_of_match (std::smatch &m)
 Helper function for parsing format strings. More...
 
static std::vector< format_elementtparse_format_string (std::string s)
 Parse the given string into format specifiers and text. More...
 
static exprt get_component_in_struct (const struct_exprt &expr, irep_idt component_name)
 Helper for add_axioms_for_format_specifier. More...
 
static std::pair< array_string_exprt, string_constraintstadd_axioms_for_format_specifier (symbol_generatort &fresh_symbol, const format_specifiert &fs, const struct_exprt &arg, const typet &index_type, const typet &char_type, array_poolt &array_pool, const messaget &message, const namespacet &ns)
 Parse s and add axioms ensuring the output corresponds to the output of String.format. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_format (symbol_generatort &fresh_symbol, const array_string_exprt &res, const std::string &s, const exprt::operandst &args, array_poolt &array_pool, const messaget &message, const namespacet &ns)
 Parse s and add axioms ensuring the output corresponds to the output of String.format. More...
 
std::string utf16_constant_array_to_java (const array_exprt &arr, std::size_t length)
 Construct a string from a constant array. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_format (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const messaget &message, const namespacet &ns)
 Formatted string using a format string and list of arguments. More...
 

Detailed Description

Generates string constraints for the Java format function.

Definition in file string_constraint_generator_format.cpp.

Function Documentation

◆ add_axioms_for_format() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_format ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const std::string &  s,
const exprt::operandst args,
array_poolt array_pool,
const messaget message,
const namespacet ns 
)

Parse s and add axioms ensuring the output corresponds to the output of String.format.

Parameters
fresh_symbolgenerator of fresh symbols
resstring expression for the result of the format function
sa format string
argsa vector of arguments
array_poolpool of arrays representing strings
messagemessage handler for warnings
nsnamespace
Returns
code, 0 on success

Definition at line 381 of file string_constraint_generator_format.cpp.

◆ add_axioms_for_format() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_format ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const messaget message,
const namespacet ns 
)

Formatted string using a format string and list of arguments.

Add axioms to specify the Java String.format function.

Parameters
fresh_symbolgenerator of fresh symbols
fa function application
array_poolpool of arrays representing strings
messagemessage handler for warnings
nsnamespace
Returns
A string expression representing the return value of the String.format function on the given arguments, assuming the first argument in the function application is a constant. Otherwise the first argument is returned.

Definition at line 510 of file string_constraint_generator_format.cpp.

◆ add_axioms_for_format_specifier()

static std::pair<array_string_exprt, string_constraintst> add_axioms_for_format_specifier ( symbol_generatort fresh_symbol,
const format_specifiert fs,
const struct_exprt arg,
const typet index_type,
const typet char_type,
array_poolt array_pool,
const messaget message,
const namespacet ns 
)
static

Parse s and add axioms ensuring the output corresponds to the output of String.format.

Assumes the argument is a structured expression which contains the fields: string expr, int, float, char, boolean, hashcode, date_time. The correct component will be fetched depending on the format specifier.

Parameters
fresh_symbolgenerator of fresh symbols
fsa format specifier
arga struct containing the possible value of the argument to format
index_typetype for indexes in strings
char_typetype of characters
array_poolpool of arrays representing strings
messagemessage handler for warnings
nsnamespace
Returns
String expression representing the output of String.format.

Definition at line 260 of file string_constraint_generator_format.cpp.

◆ format_specifier_of_match()

static format_specifiert format_specifier_of_match ( std::smatch &  m)
static

Helper function for parsing format strings.

This follows the implementation in openJDK of the java.util.Formatter class: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f96a0f/src/share/classes/java/util/Formatter.java#l2660

Parameters
ma match in a regular expression
Returns
Format specifier represented by the matched string. The groups in the match should represent: index, flag, width, precision, date and conversion type.

Definition at line 185 of file string_constraint_generator_format.cpp.

◆ get_component_in_struct()

static exprt get_component_in_struct ( const struct_exprt expr,
irep_idt  component_name 
)
static

Helper for add_axioms_for_format_specifier.

Parameters
expra structured expression
component_namename of the desired component
Returns
Expression in the component of expr named component_name.

Definition at line 237 of file string_constraint_generator_format.cpp.

◆ parse_format_string()

static std::vector<format_elementt> parse_format_string ( std::string  s)
static

Parse the given string into format specifiers and text.

This follows the implementation in openJDK of the java.util.Formatter class: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f96a0f/src/share/classes/java/util/Formatter.java#l2513

Parameters
sa string
Returns
A vector of format_elementt.

Definition at line 209 of file string_constraint_generator_format.cpp.

◆ utf16_constant_array_to_java()

std::string utf16_constant_array_to_java ( const array_exprt arr,
std::size_t  length 
)

Construct a string from a constant array.

Parameters
arran array expression containing only constants
lengthan unsigned value representing the length of the array
Returns
String of length length represented by the array assuming each field in arr represents a character.

Definition at line 483 of file string_constraint_generator_format.cpp.