From 116c66d8a7a55b5d2850a0f939fe9d182d4ef6f8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 9 May 2024 18:25:05 +0000 Subject: [PATCH] Move __CPROVER_uninterpreted_* conversion to C type checker We already had type checking of mathematical_function types to support lambda expressions. Special-case symbols with name `__CPROVER_uninterpreted_*` will now also produce these types. GOTO conversion will no longer give specific treatment to function calls with symbol name `__CPROVER_uninterpreted_*`. --- .../undeclared_uninterpreted.desc | 2 +- .../quantifiers-uninterpreted-function/main.c | 28 +++++++++++++++++ .../test.desc | 13 ++++++++ src/ansi-c/c_typecheck_base.cpp | 21 +++++++++++-- src/ansi-c/c_typecheck_expr.cpp | 25 +++++++++++----- .../goto-conversion/builtin_functions.cpp | 30 ------------------- 6 files changed, 79 insertions(+), 40 deletions(-) create mode 100644 regression/contracts-dfcc/quantifiers-uninterpreted-function/main.c create mode 100644 regression/contracts-dfcc/quantifiers-uninterpreted-function/test.desc diff --git a/regression/ansi-c/undeclared_function/undeclared_uninterpreted.desc b/regression/ansi-c/undeclared_function/undeclared_uninterpreted.desc index fb5a570f790..39b01b819c2 100644 --- a/regression/ansi-c/undeclared_function/undeclared_uninterpreted.desc +++ b/regression/ansi-c/undeclared_function/undeclared_uninterpreted.desc @@ -2,7 +2,7 @@ CORE uninterpreted.c missing type information required to construct call to uninterpreted function -^EXIT=70$ +^EXIT=(1|64)$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/contracts-dfcc/quantifiers-uninterpreted-function/main.c b/regression/contracts-dfcc/quantifiers-uninterpreted-function/main.c new file mode 100644 index 00000000000..26f9f9cc0cc --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-uninterpreted-function/main.c @@ -0,0 +1,28 @@ +#include + +int __CPROVER_uninterpreted_tolower(int); + +// clang-format off +void tl1(char *dst, __CPROVER_size_t len) + __CPROVER_requires(__CPROVER_is_fresh(dst, len)) + __CPROVER_assigns(__CPROVER_object_whole(dst)) + __CPROVER_ensures(__CPROVER_forall { + int i; + (0 <= i && i < len) ==> dst[i % len] == + __CPROVER_uninterpreted_tolower(__CPROVER_old(dst[i % len])) + }); +// clang-format on + +void tl1(char *dst, __CPROVER_size_t len) +{ + for(__CPROVER_size_t i = 0; i < len; i++) + { + dst[i] = tolower(dst[i]); + } +} + +int main() +{ + char st[8] = "HELLOROD"; + tl1(st, 8); +} diff --git a/regression/contracts-dfcc/quantifiers-uninterpreted-function/test.desc b/regression/contracts-dfcc/quantifiers-uninterpreted-function/test.desc new file mode 100644 index 00000000000..fc10a4a5d4c --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-uninterpreted-function/test.desc @@ -0,0 +1,13 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract tl1 +^\[tl1.postcondition.1\] line \d+ Check ensures clause of contract contract::tl1 for function tl1: FAILURE$ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +The purpose of this test is to ensure that we can use uninterpreted functions +within quantifiers. diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index f11e08f7e14..17e2d070f99 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -142,7 +142,8 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) { if( (!old_it->second.is_static_lifetime || !symbol.is_static_lifetime) && - symbol.type.id() != ID_code) + (symbol.type.id() != ID_code && + symbol.type.id() != ID_mathematical_function)) { error().source_location = symbol.location; error() << "redeclaration of '" << symbol.display_name() @@ -346,8 +347,12 @@ void c_typecheck_baset::typecheck_redefinition_non_type( } // do initializer, this may change the type - if(new_symbol.type.id() != ID_code && !new_symbol.is_macro) + if( + new_symbol.type.id() != ID_code && + new_symbol.type.id() != ID_mathematical_function && !new_symbol.is_macro) + { do_initializer(new_symbol); + } const typet &final_new = new_symbol.type; @@ -871,6 +876,18 @@ void c_typecheck_baset::typecheck_declaration( irep_idt identifier=symbol.name; declarator.set_name(identifier); + if( + symbol.type.id() == ID_code && + identifier.starts_with(CPROVER_PREFIX "uninterpreted_")) + { + const code_typet &function_call_type = to_code_type(symbol.type); + mathematical_function_typet::domaint domain; + for(const auto ¶meter : function_call_type.parameters()) + domain.push_back(parameter.type()); + symbol.type = + mathematical_function_typet{domain, function_call_type.return_type()}; + } + typecheck_symbol(symbol); // check the contract, if any diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 1ade7b9c8a6..a1cff1b05ec 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2424,6 +2424,16 @@ void c_typecheck_baset::typecheck_side_effect_function_call( } else { + if(identifier.starts_with(CPROVER_PREFIX "uninterpreted_")) + { + throw invalid_source_file_exceptiont{ + "'" + id2string(identifier) + + "' is not declared, " + "missing type information required to construct call to " + "uninterpreted function", + expr.source_location()}; + } + // This is an undeclared function that's not a builtin. // Let's just add it. // We do a bit of return-type guessing, but just a bit. @@ -2480,13 +2490,14 @@ void c_typecheck_baset::typecheck_side_effect_function_call( for(auto &p : make_range(expr.arguments()).zip(mathematical_function_type.domain())) { - if(p.first.type() != p.second) - { - error().source_location = p.first.source_location(); - error() << "expected argument of type " << to_string(p.second) - << " but got " << to_string(p.first.type()) << eom; - throw 0; - } + implicit_typecast(p.first, p.second); + } + + if(f_op.id() != ID_lambda && f_op.id() != ID_symbol) + { + throw invalid_source_file_exceptiont{ + "expected function symbol or lambda, but got " + id2string(f_op.id()), + f_op.source_location()}; } function_application_exprt function_application(f_op, expr.arguments()); diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp index dc944e3d964..6b4db0cdc82 100644 --- a/src/ansi-c/goto-conversion/builtin_functions.cpp +++ b/src/ansi-c/goto-conversion/builtin_functions.cpp @@ -17,8 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include -#include #include #include #include @@ -1089,34 +1087,6 @@ void goto_convertt::do_function_call_symbol( assignment.add_source_location() = function.source_location(); copy(assignment, ASSIGN, dest); } - else if(identifier.starts_with(CPROVER_PREFIX "uninterpreted_")) - { - // make it a side effect if there is an LHS - if(lhs.is_nil()) - return; - - if(function.type().get_bool(ID_C_incomplete)) - { - error().source_location = function.find_source_location(); - error() << "'" << identifier << "' is not declared, " - << "missing type information required to construct call to " - << "uninterpreted function" << eom; - throw 0; - } - - const code_typet &function_call_type = to_code_type(function.type()); - mathematical_function_typet::domaint domain; - for(const auto ¶meter : function_call_type.parameters()) - domain.push_back(parameter.type()); - mathematical_function_typet function_type{ - domain, function_call_type.return_type()}; - const function_application_exprt rhs( - symbol_exprt{function.get_identifier(), function_type}, arguments); - - code_assignt assignment(lhs, rhs); - assignment.add_source_location() = function.source_location(); - copy(assignment, ASSIGN, dest); - } else if(identifier == CPROVER_PREFIX "array_equal") { do_array_op(ID_array_equal, lhs, function, arguments, dest);