From 25e6c7bc0889ea463db70bf764a5f280af88f8b3 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 4 Apr 2025 06:30:29 +0000 Subject: [PATCH 1/2] Fix quantifiers with nested statement-expressions - Added support for `ID_address_of` and 'ID_typecast` expressions to `find_base_symbol`. - Corrected the multi-path handling in `convert_statement_expression`---a path not reaching the terminal expression should be ignored. --- .../Quantifiers-statement-expression/main.c | 2 -- .../Quantifiers-statement-expression3/main.c | 11 ++++++ .../goto-conversion/goto_clean_expr.cpp | 36 +++++++++++++++---- 3 files changed, 40 insertions(+), 9 deletions(-) create mode 100644 regression/cbmc/Quantifiers-statement-expression3/main.c diff --git a/regression/cbmc/Quantifiers-statement-expression/main.c b/regression/cbmc/Quantifiers-statement-expression/main.c index 98e0233f268..3222418c54f 100644 --- a/regression/cbmc/Quantifiers-statement-expression/main.c +++ b/regression/cbmc/Quantifiers-statement-expression/main.c @@ -3,8 +3,6 @@ int main() // clang-format off // no side effects! int j = 0; - //assert(j++); - //assert(({int i = 0; while(i <3) i++; i <3;})); int a[5] = {0 , 0, 0, 0, 0}; assert(__CPROVER_forall { int i; ({ int j = i; i=i; if(i < 0 || i >4) i = 1; ( a[i] < 5); }) }); // clang-format on diff --git a/regression/cbmc/Quantifiers-statement-expression3/main.c b/regression/cbmc/Quantifiers-statement-expression3/main.c new file mode 100644 index 00000000000..8a0ae9db277 --- /dev/null +++ b/regression/cbmc/Quantifiers-statement-expression3/main.c @@ -0,0 +1,11 @@ +int main() +{ + // clang-format off + // no side effects! + int j; + int a[5] = {0 , 0, 0, 0, 0}; + assert(__CPROVER_forall { int i; ({ ( 0 <= i && i < 4) ==> ({ int k = j; if(j < 0 || j > i) k = 1; ( a[k] == 0); }); }) }); + // clang-format on + + return 0; +} diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index 4b7545d030b..ff976217d34 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -43,6 +43,14 @@ static symbol_exprt find_base_symbol(const exprt &expr) { return find_base_symbol(to_dereference_expr(expr).pointer()); } + else if(expr.id() == ID_typecast) + { + return find_base_symbol(to_typecast_expr(expr).op()); + } + else if(expr.id() == ID_address_of) + { + return find_base_symbol(to_address_of_expr(expr).op()); + } else { throw "unsupported expression type for finding base symbol"; @@ -63,6 +71,10 @@ static exprt convert_statement_expression( INVARIANT( natural_loops.loop_map.size() == 0, "quantifier must not contain loops"); + std::unordered_set declared_symbols; + // All bound variables are local. + declared_symbols.insert(qex.variables().begin(), qex.variables().end()); + // `last` is the instruction corresponding to the last expression in the // statement expression. goto_programt::const_targett last = where.instructions.end(); @@ -75,6 +87,11 @@ static exprt convert_statement_expression( { last = it; } + + if(it->is_decl()) + { + declared_symbols.insert(it->decl_symbol()); + } } DATA_INVARIANT( @@ -82,6 +99,12 @@ static exprt convert_statement_expression( "expression statements must contain a terminator expression"); auto last_expr = to_code_expression(last->get_other()).expression(); + if( + last_expr.id() == ID_typecast && + to_typecast_expr(last_expr).type().id() == ID_empty) + { + to_typecast_expr(last_expr).type() = bool_typet(); + } struct pathst { @@ -139,10 +162,6 @@ static exprt convert_statement_expression( {1, where.instructions.begin()}, {1, std::make_pair(true_exprt(), replace_mapt())}); - std::unordered_set declared_symbols; - // All bound variables are local. - declared_symbols.insert(qex.variables().begin(), qex.variables().end()); - exprt res = true_exprt(); // Visit the quantifier body along `paths`. @@ -151,9 +170,12 @@ static exprt convert_statement_expression( auto ¤t_it = paths.back_it(); auto &path_condition = paths.back_path_condition(); auto &value_map = paths.back_value_map(); - INVARIANT( - current_it != where.instructions.end(), - "Quantifier body must have a unique end expression."); + + if(current_it == where.instructions.end()) + { + paths.pop_back(); + continue; + } switch(current_it->type()) { From be065690ed2808a613771cb67e667a099a34ae45 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Sat, 5 Apr 2025 05:38:23 +0000 Subject: [PATCH 2/2] Replace conditions in quantified statement expressions --- .../cbmc/Quantifiers-statement-expression/main.c | 2 +- src/ansi-c/goto-conversion/goto_clean_expr.cpp | 13 +++++-------- 2 files changed, 6 insertions(+), 9 deletions(-) diff --git a/regression/cbmc/Quantifiers-statement-expression/main.c b/regression/cbmc/Quantifiers-statement-expression/main.c index 3222418c54f..efd5c55f9ca 100644 --- a/regression/cbmc/Quantifiers-statement-expression/main.c +++ b/regression/cbmc/Quantifiers-statement-expression/main.c @@ -4,7 +4,7 @@ int main() // no side effects! int j = 0; int a[5] = {0 , 0, 0, 0, 0}; - assert(__CPROVER_forall { int i; ({ int j = i; i=i; if(i < 0 || i >4) i = 1; ( a[i] < 5); }) }); + assert(__CPROVER_forall { int i; ({ int j = i; int cond = i < 0 || i >4; if(cond) i = 1; ( a[i] < 5); }) }); // clang-format on return 0; diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index ff976217d34..4a605141902 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -211,19 +211,16 @@ static exprt convert_statement_expression( // path_condition && cond. case goto_program_instruction_typet::GOTO: { - if(!current_it->condition().is_true()) + exprt condition = current_it->condition(); + replace_expr(value_map, condition); + if(!condition.is_true()) { auto next_it = current_it->targets.front(); exprt copy_path_condition = path_condition; - replace_mapt copy_symbol_map = value_map; - auto copy_condition = current_it->condition(); - path_condition = - and_exprt(path_condition, not_exprt(current_it->condition())); + path_condition = and_exprt(path_condition, not_exprt(condition)); current_it++; paths.push_back( - next_it, - and_exprt(copy_path_condition, copy_condition), - copy_symbol_map); + next_it, and_exprt(copy_path_condition, condition), value_map); } else {