diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 98ea94c5349d..319a435987c7 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -1010,6 +1010,9 @@ check and use loop contracts when provided \fB\-loop\-contracts\-no\-unwind\fR do not unwind transformed loops .TP +\fB\-loop\-contract\-file\fR \fIfile\fR +annotate loop contracts from the file to the goto program +.TP \fB\-\-replace\-call\-with\-contract\fR \fIfun\fR replace calls to \fIfun\fR with \fIfun\fR's contract .TP diff --git a/regression/contracts-dfcc/CMakeLists.txt b/regression/contracts-dfcc/CMakeLists.txt index b03adb344127..872fdc9f2475 100644 --- a/regression/contracts-dfcc/CMakeLists.txt +++ b/regression/contracts-dfcc/CMakeLists.txt @@ -14,12 +14,12 @@ endif() add_test_pl_tests( - "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ $ ${is_windows} true" + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ $ ${is_windows} true" ${gcc_only} ) add_test_pl_profile( "contracts-non-dfcc" - "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ $ ${is_windows} false" + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ $ ${is_windows} false" ${gcc_only} "-C;-X;dfcc-only;-s;non-dfcc" "CORE" ) diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.json b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.json new file mode 100644 index 000000000000..24ddbdb183a4 --- /dev/null +++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.json @@ -0,0 +1,15 @@ +{ + "functions": [ + { + "foo": [ + { + "loop_id": "0", + "assigns": "i", + "invariants": "0 <= i && i <= 10", + "decreases": "i", + "symbol_map": "i,foo::1::1::i" + } + ] + } + ] + } diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test_contract_file.desc b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test_contract_file.desc new file mode 100644 index 000000000000..3e254b9b0865 --- /dev/null +++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test_contract_file.desc @@ -0,0 +1,14 @@ +CORE +main.c +--loop-contract-file test.json --dfcc main --apply-loop-contracts +^\[foo.assigns.\d+\] .* Check that nondet_var is assignable: FAILURE$ +^\[foo.assigns.\d+\] .* Check that __VERIFIER_var is assignable: FAILURE$ +^\[foo.assigns.\d+\] .* Check that __CPROVER_var is assignable: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that program variables with special name prefixes +__CPROVER_, __VERIFIER, or nondet do not escape assigns clause checking. +Using loop contracts from the contract file. diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.json b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.json new file mode 100644 index 000000000000..572287066b82 --- /dev/null +++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.json @@ -0,0 +1,18 @@ +{ + "functions": [ + { + "foo": [ + { + "loop_id": "0", + "assigns": "i,nondet_var, __VERIFIER_var, __CPROVER_var", + "invariants": "0 <= i && i <= 10", + "decreases": "i", + "symbol_map": "i,foo::1::1::i; + nondet_var,foo::1::nondet_var; + __VERIFIER_var, foo::1::__VERIFIER_var; + __CPROVER_var,foo::1::__CPROVER_var" + } + ] + } + ] + } diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test_contract_file.desc b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test_contract_file.desc new file mode 100644 index 000000000000..ebe486fe5937 --- /dev/null +++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test_contract_file.desc @@ -0,0 +1,15 @@ +CORE +main.c +--loop-contract-file test.json --dfcc main --apply-loop-contracts +^\[foo.assigns.\d+\] .* Check that nondet_var is assignable: SUCCESS$ +^\[foo.assigns.\d+\] .* Check that __VERIFIER_var is assignable: SUCCESS$ +^\[foo.assigns.\d+\] .* Check that __CPROVER_var is assignable: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that when program variables names have special prefixes +__CPROVER_, __VERIFIER, or nondet, adding them to the write set makes them +assignable. +Using loop contracts from the contract file. diff --git a/regression/contracts-dfcc/history-index/test.json b/regression/contracts-dfcc/history-index/test.json new file mode 100644 index 000000000000..534c1b99c576 --- /dev/null +++ b/regression/contracts-dfcc/history-index/test.json @@ -0,0 +1,13 @@ +{ + "functions": [ + { + "main": [ + { + "loop_id": "0", + "invariants": "x[0] == __CPROVER_loop_entry(x[0])", + "symbol_map": "x,main::1::x" + } + ] + } + ] + } diff --git a/regression/contracts-dfcc/history-index/test_contract_file.desc b/regression/contracts-dfcc/history-index/test_contract_file.desc new file mode 100644 index 000000000000..3e9ccc20f766 --- /dev/null +++ b/regression/contracts-dfcc/history-index/test_contract_file.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--loop-contract-file test.json --dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^Tracking history of index expressions is not supported yet\. +-- +This test checks that `ID_index` expressions are allowed within history variables. +Using loop contracts from the contract file. diff --git a/regression/contracts-dfcc/loop_contracts_memcmp/main.c b/regression/contracts-dfcc/loop_contracts_memcmp/main.c new file mode 100644 index 000000000000..66ca01826e7b --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_memcmp/main.c @@ -0,0 +1,34 @@ +inline int memcmp(const void *s1, const void *s2, unsigned n) +{ + int res = 0; + const unsigned char *sc1 = s1, *sc2 = s2; + for(; n != 0; n--) + // clang-format off + __CPROVER_loop_invariant(n <= __CPROVER_loop_entry(n)) + __CPROVER_loop_invariant(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1))) + __CPROVER_loop_invariant(__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2))) + __CPROVER_loop_invariant(sc1 <= s1 + __CPROVER_loop_entry(n)) + __CPROVER_loop_invariant(sc2 <= s2 + __CPROVER_loop_entry(n)) + __CPROVER_loop_invariant(res == 0) + __CPROVER_loop_invariant(sc1 -(const unsigned char*)s1 == sc2 -(const unsigned char*)s2 + && sc1 -(const unsigned char*)s1== __CPROVER_loop_entry(n) - n) + // clang-format on + { + res = (*sc1++) - (*sc2++); + long d1 = sc1 - (const unsigned char *)s1; + long d2 = sc2 - (const unsigned char *)s2; + if(res != 0) + return res; + } + return res; +} + +int main() +{ + unsigned SIZE; + __CPROVER_assume(1 < SIZE && SIZE < 65536); + unsigned char *a = malloc(SIZE); + unsigned char *b = malloc(SIZE); + memcpy(b, a, SIZE); + assert(memcmp(a, b, SIZE) == 0); +} diff --git a/regression/contracts-dfcc/loop_contracts_memcmp/test.desc b/regression/contracts-dfcc/loop_contracts_memcmp/test.desc new file mode 100644 index 000000000000..9f4e5b034bc7 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_memcmp/test.desc @@ -0,0 +1,9 @@ +CORE gcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that loop contracts work correctly on memcmp. diff --git a/regression/contracts-dfcc/loop_contracts_memcmp/test.json b/regression/contracts-dfcc/loop_contracts_memcmp/test.json new file mode 100644 index 000000000000..b528b11ae360 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_memcmp/test.json @@ -0,0 +1,19 @@ +{ + "functions": [ + { + "memcmp": [ + { + "loop_id": "0", + "invariants": "(n <= __CPROVER_loop_entry(n))&&(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))&& + (__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))&& + (sc1 <= s1 + __CPROVER_loop_entry(n))&& + (sc2 <= s2 + __CPROVER_loop_entry(n))&& + (res == 0)&& + (sc1 -(const unsigned char*)s1 == sc2 -(const unsigned char*)s2 + && sc1 -(const unsigned char*)s1== __CPROVER_loop_entry(n) - n)", + "symbol_map": "n,memcmp::n; sc1,memcmp::1::sc1; sc2,memcmp::1::sc2; res,memcmp::1::res; s1, memcmp::s1; s2, memcmp::s2" + } + ] + } + ] + } diff --git a/regression/contracts-dfcc/loop_contracts_memcmp/test_contract_file.desc b/regression/contracts-dfcc/loop_contracts_memcmp/test_contract_file.desc new file mode 100644 index 000000000000..c9bdc7e62d5e --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_memcmp/test_contract_file.desc @@ -0,0 +1,10 @@ +CORE gcc-only +main.c +--loop-contract-file test.json --dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that loop contracts work correctly on memcmp. +Using loop contracts from the contract file. diff --git a/regression/contracts-dfcc/variant_multi_instruction_loop_head/test.json b/regression/contracts-dfcc/variant_multi_instruction_loop_head/test.json new file mode 100644 index 000000000000..48592a284649 --- /dev/null +++ b/regression/contracts-dfcc/variant_multi_instruction_loop_head/test.json @@ -0,0 +1,14 @@ +{ + "functions": [ + { + "main": [ + { + "loop_id": "0", + "invariants": "0 <= *y && *y <= 10", + "decreases": "10-x", + "symbol_map": "y,main::1::y;x,main::1::x" + } + ] + } + ] + } diff --git a/regression/contracts-dfcc/variant_multi_instruction_loop_head/test_contract_file.desc b/regression/contracts-dfcc/variant_multi_instruction_loop_head/test_contract_file.desc new file mode 100644 index 000000000000..c76b07ddf4a4 --- /dev/null +++ b/regression/contracts-dfcc/variant_multi_instruction_loop_head/test_contract_file.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--loop-contract-file test.json --dfcc main --apply-loop-contracts +^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] line \d+ Check that x is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test checks that decreases clause is properly initialized +when the loop head and loop invariant compilation emit several goto instructions. +Using loop contracts from the contract file. diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 1be65de97ed9..5661c1b6d91b 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -65,6 +65,7 @@ class c_typecheck_baset: virtual void typecheck()=0; virtual void typecheck_expr(exprt &expr); + virtual void typecheck_spec_assigns(exprt::operandst &targets); protected: symbol_table_baset &symbol_table; @@ -160,7 +161,6 @@ class c_typecheck_baset: /// is found in expr. virtual void check_was_freed(const exprt &expr, std::string &clause_type); - virtual void typecheck_spec_assigns(exprt::operandst &targets); virtual void typecheck_spec_frees(exprt::operandst &targets); virtual void typecheck_conditional_targets( exprt::operandst &targets, diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 5e3c42074ed7..f1facd37db3b 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -17,6 +17,7 @@ SRC = accelerate/accelerate.cpp \ branch.cpp \ call_sequences.cpp \ contracts/contracts.cpp \ + contracts/contract_wrangler.cpp \ contracts/dynamic-frames/dfcc_utils.cpp \ contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \ contracts/dynamic-frames/dfcc_contract_mode.cpp \ diff --git a/src/goto-instrument/contracts/contract_wrangler.cpp b/src/goto-instrument/contracts/contract_wrangler.cpp new file mode 100644 index 000000000000..6a04a3182a12 --- /dev/null +++ b/src/goto-instrument/contracts/contract_wrangler.cpp @@ -0,0 +1,391 @@ +/*******************************************************************\ + +Module: Parse and annotate contracts from configuration files + +Author: Qinheping Hu + +Date: June 2023 + +\*******************************************************************/ + +/// \file +/// Parse and annotate contracts + +#include "contract_wrangler.h" + +#include +#include +#include +#include +#include + +#include + +#include +#include +#include + +contract_wranglert::contract_wranglert( + goto_modelt &goto_model, + const std::string &file_name, + messaget &log) + : ns(goto_model.symbol_table), + goto_model(goto_model), + symbol_table(goto_model.symbol_table), + goto_functions(goto_model.goto_functions), + log(log) +{ + jsont configuration; + + if(parse_json(file_name, log.get_message_handler(), configuration)) + throw deserialization_exceptiont(file_name + " is not a valid JSON file"); + + configure_functions(configuration); + + // Mangle loop contract function by function. + // We match function with a regex. There should one and only one function + // with name matched by the regex. + for(const auto &function_entry : this->functions) + { + bool function_found = 0; + + for(const auto &function : goto_model.goto_functions.function_map) + { + // We find a matched function. + if(std::regex_match(function.first.c_str(), function_entry.first)) + { + if(function_found) + throw deserialization_exceptiont( + "function regex" + function_entry.second.regex_str + + " match more than one function"); + + function_found = 1; + + // Mangle all loop contracts in the function. + for(const auto &loop_entry : function_entry.second.loop_contract) + { + mangle(loop_entry, function.first); + } + } + } + + if(!function_found) + throw deserialization_exceptiont( + "function " + function_entry.second.regex_str + " match no function"); + } +} + +void contract_wranglert::add_builtin_pointer_function_symbol( + std::string function_name, + const unsigned num_of_args) +{ + // Already exist. + if(symbol_table.lookup(CPROVER_PREFIX + function_name) != nullptr) + return; + + code_typet::parameterst parameters; + for(unsigned i = 0; i < num_of_args; i++) + { + parameters.emplace_back(pointer_typet(signedbv_typet(32), 32)); + } + symbolt fun_symbol( + CPROVER_PREFIX + function_name, code_typet(parameters, empty_typet()), "c"); + symbol_table.add(fun_symbol); +} + +void contract_wranglert::substitute_symbol( + exprt &expr, + const std::map &symbol_map) +{ + for(depth_iteratort it = expr.depth_begin(); it != expr.depth_end(); it++) + { + if(it->id() != ID_symbol) + continue; + for(auto &symbol_entry : symbol_map) + { + if(it->get(ID_identifier) == symbol_entry.first) + { + exprt symbol(symbol_entry.second); + it.mutate().swap(symbol); + break; + } + } + } +} + +void contract_wranglert::mangle( + const loop_contract_clauset &loop_contract, + const irep_idt &function_id) +{ + // Loop contracts mangling consists of four steps. + // + // 1. Construct a fake function with a fake loop that contains the loop + // contracts for parsing the contracts. + // 2. Parse the fake function and extract the contracts as exprt. + // 3. Substitute symbols in the extracted exprt with the symbols in the + // symbol table of the goto model according to the symbol map provided by + // the user. + // 4. Typecheck all contract exprt. + // 5. Annotate all contract exprt to the corresponding loop. + + // Construct a fake function to parse. + // void function_id() + // { + // while(1==1) + // __CPROVER_assigns(assigns_str) // optional + // __CPROVER_loop_invariant(invariants_str) + // __CPROVER_decreases(decreases_str) // optional + // } + ::std::ostringstream pr; + pr << "void _fn() { while(1==1)"; + if(loop_contract.assigns != "") + { + pr << CPROVER_PREFIX << "assigns(" << loop_contract.assigns << ") "; + } + pr << CPROVER_PREFIX << "loop_invariant(" << loop_contract.invariants << ") "; + if(loop_contract.decreases != "") + { + pr << CPROVER_PREFIX << "decreases(" << loop_contract.decreases << ") "; + } + pr << " {}}" << ::std::endl; + + log.debug() << "Constructing fake function:\n" << pr.str() << log.eom; + + // Parse the fake function. + ::std::istringstream is(pr.str()); + ansi_c_parser.clear(); + ansi_c_parser.set_line_no(0); + ansi_c_parser.set_file(""); + ansi_c_parser.in = &is; + ansi_c_scanner_init(); + ansi_c_parser.parse(); + + // Extract the invariants from prase_tree. + exprt &inv_expr(static_cast(ansi_c_parser.parse_tree.items.front() + .declarator() + .value() + .operands()[0] + .add(ID_C_spec_loop_invariant)) + .operands()[0]); + + log.debug() << "Extracted loop invariants: " << inv_expr.pretty() << "\n" + << log.eom; + + // Extract the assigns from parse_tree. + optionalt assigns_expr; + if(loop_contract.assigns != "") + { + assigns_expr = static_cast(ansi_c_parser.parse_tree.items.front() + .declarator() + .value() + .operands()[0] + .add(ID_C_spec_assigns)) + .operands()[0]; + } + + // Extract the decreases from parse_tree. + exprt::operandst decreases_exprs; + if(loop_contract.decreases != "") + { + for(auto op : static_cast(ansi_c_parser.parse_tree.items.front() + .declarator() + .value() + .operands()[0] + .add(ID_C_spec_decreases)) + .operands()) + { + decreases_exprs.emplace_back(op); + } + } + + // Substitute symbols in the clauses with the symbols in the symbol table. + log.debug() << "Start to substitute symbols" << log.eom; + substitute_symbol(inv_expr, loop_contract.symbol_map); + if(assigns_expr.has_value()) + { + substitute_symbol(assigns_expr.value(), loop_contract.symbol_map); + } + for(exprt &decrease_expr : decreases_exprs) + { + substitute_symbol(decrease_expr, loop_contract.symbol_map); + } + + // Add builtin functions that might be used in contracts to the symbol table. + add_builtin_pointer_function_symbol("loop_entry", 1); + add_builtin_pointer_function_symbol("same_object", 2); + add_builtin_pointer_function_symbol("OBJECT_SIZE", 1); + add_builtin_pointer_function_symbol("POINTER_OBJECT", 1); + add_builtin_pointer_function_symbol("POINTER_OFFSET", 1); + + // Typecheck clauses. + ansi_c_typecheckt ansi_c_typecheck( + ansi_c_parser.parse_tree, + symbol_table, + symbol_table.lookup(function_id)->module.c_str(), + log.get_message_handler()); + + // Typecheck and annotate invariants. + { + log.debug() << "Start to typecheck invariants." << log.eom; + ansi_c_typecheck.typecheck_expr(inv_expr); + if(has_subexpr(inv_expr, ID_old)) + throw invalid_input_exceptiont(CPROVER_PREFIX + "old is not allowed in loop invariants."); + + invariant_mapt inv_map; + inv_map[loop_idt(function_id, std::stoi(loop_contract.identifier))] = + and_exprt(simplify_expr(inv_expr, ns), true_exprt()); + annotate_invariants(inv_map, goto_model); + } + + // Typecheck and annotate assigns. + log.debug() << "Start to typecheck assigns." << log.eom; + if(assigns_expr.has_value()) + { + ansi_c_typecheck.typecheck_spec_assigns(assigns_expr.value().operands()); + + invariant_mapt assigns_map; + assigns_map[loop_idt(function_id, std::stoi(loop_contract.identifier))] = + assigns_expr.value(); + annotate_assigns(assigns_map, goto_model); + } + + // Typecheck an annotate decreases. + log.debug() << "Start to typecheck decreases." << log.eom; + if(!decreases_exprs.empty()) + { + std::map> decreases_map; + decreases_map[loop_idt(function_id, std::stoi(loop_contract.identifier))] = + std::vector(); + for(exprt &decrease_expr : decreases_exprs) + { + ansi_c_typecheck.typecheck_expr(decrease_expr); + decreases_map[loop_idt(function_id, std::stoi(loop_contract.identifier))] + .emplace_back(decrease_expr); + } + annotate_decreases(decreases_map, goto_model); + } + + log.debug() << "Mangling finished." << log.eom; + // Remove added symbol. + symbol_table.remove(CPROVER_PREFIX "loop_entry"); + symbol_table.remove(CPROVER_PREFIX "same_object"); + symbol_table.remove(CPROVER_PREFIX "OBJECT_SIZE"); + symbol_table.remove(CPROVER_PREFIX "POINTER_OBJECT"); + symbol_table.remove(CPROVER_PREFIX "POINTER_OFFSET"); +} + +void contract_wranglert::configure_functions(const jsont &config) +{ + auto functions = config["functions"]; + + if(functions.is_null()) + return; + + if(!functions.is_array()) + throw deserialization_exceptiont("functions entry must be sequence"); + + for(const auto &function : to_json_array(functions)) + { + if(!function.is_object()) + throw deserialization_exceptiont("function entry must be object"); + + for(const auto &function_entry : to_json_object(function)) + { + const auto function_name = function_entry.first; + const auto &items = function_entry.second; + + if(!items.is_array()) + throw deserialization_exceptiont("loops entry must be sequence"); + + this->functions.emplace_back(function_name, functiont{}); + functiont &function_config = this->functions.back().second; + function_config.regex_str = function_name; + + for(const auto &function_item : to_json_array(items)) + { + if(!function_item.is_object()) + throw deserialization_exceptiont("loop entry must be object"); + + std::string loop_id = ""; + std::string invariants_str = ""; + std::string assigns_str = ""; + std::string decreases_str = ""; + std::map symbol_map; + + for(const auto &loop_item : to_json_object(function_item)) + { + if(!loop_item.second.is_string()) + throw deserialization_exceptiont("loop item must be string"); + + if(loop_item.first == "loop_id") + { + loop_id = loop_item.second.value; + continue; + } + + if(loop_item.first == "assigns") + { + assigns_str = loop_item.second.value; + continue; + } + + if(loop_item.first == "decreases") + { + decreases_str = loop_item.second.value; + continue; + } + + if(loop_item.first == "invariants") + { + invariants_str = loop_item.second.value; + continue; + } + + if(loop_item.first == "symbol_map") + { + std::string symbol_map_str = loop_item.second.value; + + // Remove all space in symbol_map_str + symbol_map_str.erase( + std::remove_if( + symbol_map_str.begin(), symbol_map_str.end(), isspace), + symbol_map_str.end()); + + for(const auto &symbol_map_entry : + split_string(symbol_map_str, ';')) + { + const auto symbol_map_pair = split_string(symbol_map_entry, ','); + const auto &symbol = symbol_table.lookup(symbol_map_pair.back()); + if(symbol == nullptr) + throw deserialization_exceptiont( + "symbol \"" + symbol_map_pair.front() + + "\" does not exist in the symbol table"); + symbol_map[symbol_map_pair.front()] = + symbol_table.lookup(symbol_map_pair.back())->symbol_expr(); + } + + continue; + } + + throw deserialization_exceptiont("unexpected loop item"); + } + + if(loop_id.empty()) + { + throw deserialization_exceptiont( + "loop entry must have one identifier"); + } + + if(invariants_str.empty()) + { + throw deserialization_exceptiont( + "loop entry must have one invariant string"); + } + + function_config.loop_contract.emplace_back( + loop_id, invariants_str, assigns_str, decreases_str, symbol_map); + } + } + } +} diff --git a/src/goto-instrument/contracts/contract_wrangler.h b/src/goto-instrument/contracts/contract_wrangler.h new file mode 100644 index 000000000000..88a286926123 --- /dev/null +++ b/src/goto-instrument/contracts/contract_wrangler.h @@ -0,0 +1,102 @@ +/*******************************************************************\ + +Module: Parse and annotate contracts from configuration files + +Author: Qinheping Hu + +Date: June 2023 + +\*******************************************************************/ + +/// \file +/// Parse and annotate contracts + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACT_WRANGLER_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACT_WRANGLER_H + +#include +#include +#include + +#include +#include + +#include + +#include + +struct loop_contract_clauset +{ + std::string identifier; + std::string invariants; + std::string assigns; + std::string decreases; + std::map symbol_map; + + loop_contract_clauset( + std::string _identifier, + std::string _invariants_str, + std::string _assigns_str, + std::string _decreases_str, + std::map _symbol_map) + : identifier(std::move(_identifier)), + invariants(std::move(_invariants_str)), + assigns(_assigns_str), + decreases(_decreases_str), + symbol_map(_symbol_map) + { + } +}; + +struct functiont +{ + std::vector loop_contract; + std::string regex_str; +}; + +using functionst = std::list>; + +class contract_wranglert +{ +public: + contract_wranglert( + goto_modelt &goto_model, + const std::string &file_name, + messaget &log); + + namespacet ns; + +protected: + goto_modelt &goto_model; + symbol_tablet &symbol_table; + goto_functionst &goto_functions; + + messaget &log; + + functionst functions; + + void configure_functions(const jsont &); + + /// @brief Mangle `loop_contract` in the function with `function_id` + /// @param loop_contract The contract mangle in the function. + /// @param function_id The function containing the loop we mangle to. + void mangle( + const loop_contract_clauset &loop_contract, + const irep_idt &function_id); + + /// @brief Substitute symbols in `expr` with `symbol_map. + /// @param expr Underlying expression. + /// @param symbol_map Symbol_map from symbol name to the symbol to substitute. + void substitute_symbol( + exprt &expr, + const std::map &symbol_map); + + /// @brief Add builtin function symbol with `function_name` into symbol table. + /// @param function_name Name of the function to add. + /// @param num_of_args Number of arguments of the added symbol. + void add_builtin_pointer_function_symbol( + std::string function_name, + const unsigned num_of_args); +}; + +#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACT_WRANGLER_H diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 3302dcf30745..599c811bc0b9 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -40,6 +40,10 @@ Date: February 2016 " --loop-contracts-no-unwind\n" \ " do not unwind transformed loops\n" +#define FLAG_LOOP_CONTRACT_FILE "loop-contract-file" +#define HELP_LOOP_CONTRACT_FILE \ + " --loop-contract-file parse and annotate loop contracts from files\n" + #define FLAG_REPLACE_CALL "replace-call-with-contract" #define HELP_REPLACE_CALL \ " --replace-call-with-contract [/contract]\n" \ diff --git a/src/goto-instrument/contracts/module_dependencies.txt b/src/goto-instrument/contracts/module_dependencies.txt index a797c099df6c..d97a048f0bad 100644 --- a/src/goto-instrument/contracts/module_dependencies.txt +++ b/src/goto-instrument/contracts/module_dependencies.txt @@ -3,6 +3,7 @@ ansi-c goto-instrument/contracts goto-instrument goto-programs +json langapi linking util diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index cd0899fd79b6..70802b92548f 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -738,3 +738,44 @@ void annotate_assigns( condition.add(ID_C_spec_assigns) = assigns; } } + +void annotate_assigns( + const std::map &assigns_map, + goto_modelt &goto_model) +{ + for(const auto &assigns_map_entry : assigns_map) + { + loop_idt loop_id = assigns_map_entry.first; + irep_idt function_id = loop_id.function_id; + unsigned int loop_number = loop_id.loop_number; + + // get the last instruction of the target loop + auto &function = goto_model.goto_functions.function_map[function_id]; + goto_programt::targett loop_end = get_loop_end(loop_number, function); + + exprt &condition = loop_end->condition_nonconst(); + condition.add(ID_C_spec_assigns) = assigns_map_entry.second; + } +} + +void annotate_decreases( + const std::map> &decreases_map, + goto_modelt &goto_model) +{ + for(const auto &decreases_map_entry : decreases_map) + { + loop_idt loop_id = decreases_map_entry.first; + irep_idt function_id = loop_id.function_id; + unsigned int loop_number = loop_id.loop_number; + + // get the last instruction of the target loop + auto &function = goto_model.goto_functions.function_map[function_id]; + goto_programt::targett loop_end = get_loop_end(loop_number, function); + + exprt &condition = loop_end->condition_nonconst(); + auto decreases = exprt(ID_target_list); + for(const auto &e : decreases_map_entry.second) + decreases.add_to_operands(e); + condition.add(ID_C_spec_decreases) = decreases; + } +} diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 81173aed8fc5..0d1546965ef0 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -317,4 +317,14 @@ void annotate_assigns( const std::map> &assigns_map, goto_modelt &goto_model); +void annotate_assigns( + const std::map &assigns_map, + goto_modelt &goto_model); + +/// Annotate the decreases in `decreases_map` to their corresponding +/// loops. Corresponding loops are specified by keys of `decreases_map` +void annotate_decreases( + const std::map> &decreases_map, + goto_modelt &goto_model); + #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 619b178b4ba8..9f93a03825dc 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1158,6 +1158,12 @@ void goto_instrument_parse_optionst::instrument_goto_program() goto_model.goto_functions.update(); } + if(cmdline.isset("loop-contract-file")) + { + const auto file_name = cmdline.get_value("loop-contract-file"); + contract_wranglert contract_wrangler(goto_model, file_name, log); + } + bool use_dfcc = cmdline.isset(FLAG_DFCC); if(use_dfcc) { @@ -2012,6 +2018,7 @@ void goto_instrument_parse_optionst::help() HELP_DFCC HELP_LOOP_CONTRACTS HELP_LOOP_CONTRACTS_NO_UNWIND + HELP_LOOP_CONTRACT_FILE HELP_REPLACE_CALL HELP_ENFORCE_CONTRACT HELP_ENFORCE_CONTRACT_REC diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 07c0dfd9e1c9..9cb22056f25f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -41,6 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "uninitialized.h" #include "unwindset.h" +#include "contracts/contract_wrangler.h" #include "contracts/contracts.h" #include "contracts/dynamic-frames/dfcc.h" #include "wmm/weak_memory.h" @@ -101,6 +102,7 @@ Author: Daniel Kroening, kroening@kroening.com OPT_DFCC \ "(" FLAG_LOOP_CONTRACTS ")" \ "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \ + "(" FLAG_LOOP_CONTRACT_FILE "):" \ "(" FLAG_REPLACE_CALL "):" \ "(" FLAG_ENFORCE_CONTRACT "):" \ OPT_ENFORCE_CONTRACT_REC \