cprover
string_constraint_generator_format.cpp File Reference

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

#include <iomanip>
#include <regex>
#include <string>
#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 is_null (const array_string_exprt &string)
 Expression which is true when the string is equal to the literal "null". More...
 
static std::pair< array_string_exprt, string_constraintstadd_axioms_for_format_specifier (symbol_generatort &fresh_symbol, const format_specifiert &fs, const std::function< exprt(const irep_idt &)> &get_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...
 
static exprt format_arg_from_string (const array_string_exprt &string, const irep_idt &id)
 Deserialize an argument for format from string. 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 445 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 595 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 std::function< exprt(const irep_idt &)> &  get_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 string representing one of: string expr, int, float, char, boolean, hashcode, date_time. The correct type will be retrieved by calling get_arg with an id depending on the format specifier.

Parameters
fresh_symbolgenerator of fresh symbols
fsa format specifier
get_arga function returning the possible value of the argument to format given their type.
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 271 of file string_constraint_generator_format.cpp.

◆ format_arg_from_string()

static exprt format_arg_from_string ( const array_string_exprt string,
const irep_idt id 
)
static

Deserialize an argument for format from string.

id should be one of: string_expr, int, char, boolean, float. The primitive values are expected to all be encoded using 4 characters.

Definition at line 394 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 196 of file string_constraint_generator_format.cpp.

◆ is_null()

static exprt is_null ( const array_string_exprt string)
static

Expression which is true when the string is equal to the literal "null".

Definition at line 245 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 220 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 568 of file string_constraint_generator_format.cpp.