Merge pull request #7445 from remi-delmas-3000/map-contract-name

CONTRACTS: add function-contract mapping to the CLI

Author: remi-delmas-3000

regression/contracts-dfcc/function-contract-mapping/main.c

@@ -0,0 +1,40 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool my_contract(char *arr, size_t size, char *out)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(arr, size))
+__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out)))
+__CPROVER_assigns((size > 0) : arr[0], *out)
+__CPROVER_ensures(
+    (size > 0) ==> __CPROVER_return_value &&
+                   (arr[0] == 0) &&
+                   (*out == __CPROVER_old(arr[0])))
+__CPROVER_ensures(
+    (size == 0) ==> !__CPROVER_return_value)
+  // clang-format on
+  ;
+
+bool bar(char *arr, size_t size, char *out)
+{
+  if(size > 0)
+  {
+    *out = arr[0];
+    arr[0] = 0;
+    return true;
+  }
+  return false;
+}
+
+bool foo(char *arr, size_t size, char *out)
+{
+  return bar(arr, size, out);
+}
+
+void main()
+{
+  char *arr;
+  size_t size;
+  char *out;
+  foo(arr, size, out);
+}

regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-contract.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/ _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^Invalid function-contract mapping$
+^Reason: couldn't find contract name after '/' in 'foo/'$
+^EXIT=(10|6)$
+^SIGNAL=0$
+--
+--
+Checks that when the contract name is missing an error is triggered.

regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-function.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract /my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^Invalid function-contract mapping$
+^Reason: couldn't find function name before '/' in '/my_contract'$
+^EXIT=(10|6)$
+^SIGNAL=0$
+--
+--
+Checks that when the function name is missing an error is triggered.

regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-too-many.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/bar/my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^Invalid function-contract mapping$
+^Reason: couldn't parse 'foo/bar/my_contract'$
+^EXIT=(10|6)$
+^SIGNAL=0$
+--
+--
+Checks that when the function name is missing an error is triggered.

regression/contracts-dfcc/function-contract-mapping/test-enforce-pass.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test demonstrates the ability to specify a function_name/contract_name
+mapping for contract checking.

regression/contracts-dfcc/function-contract-mapping/test-enforce-replace-pass.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/my_contract --replace-call-with-contract bar/my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test demonstrates the ability to check specify a function_name/contract_name
+mapping for contract checking and contract replacement.
+
+The same contract `my_contract` is used for both `foo` and `bar` functions in
+checking and replacement mode, respectively.

regression/contracts-dfcc/function-contract-mapping/test-enforce-warning-not-found.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/my_contractt _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^Contract 'my_contractt' not found, deriving empty pure contract 'contract::my_contractt' from function 'foo'$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that we get a warning that a default contract is derived from the
+signature of the function being checked when specifying a non-existing contract.

src/goto-instrument/contracts/contracts.h

@@ -29,19 +29,22 @@ Date: February 2016
 #include <string>
 #include <unordered_set>
 
+// clang-format off
 #define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
 #define HELP_LOOP_CONTRACTS                                                    \
   " --apply-loop-contracts\n"                                                  \
   "                              check and use loop contracts when provided\n"
 
 #define FLAG_REPLACE_CALL "replace-call-with-contract"
 #define HELP_REPLACE_CALL                                                      \
-  " --replace-call-with-contract <fun>\n"                                      \
-  "                              replace calls to fun with fun's contract\n"
+  " --replace-call-with-contract <function>[/contract]\n"                      \
+  "                              replace calls to function with contract\n"
 
 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
 #define HELP_ENFORCE_CONTRACT                                                  \
-  " --enforce-contract <fun>     wrap fun with an assertion of its contract\n"
+  " --enforce-contract <function>[/contract]"                                  \
+  "                              wrap function with an assertion of contract\n"
+// clang-format on
 
 class local_may_aliast;
 

src/goto-instrument/contracts/doc/user/contracts-cli.md

@@ -5,24 +5,27 @@
 The program transformation takes the following parameters:
 
 ```
-goto-instrument [--apply-loop-contracts] [--enforce-contract f] (--replace-call-with-contract g)* in.gb out.gb
+goto-instrument [--apply-loop-contracts] [--enforce-contract <function>] (--replace-call-with-contract <function>)* in.gb out.gb
 ```
 
 Where:
 - `--apply-loop-contracts` is optional and specifies to apply loop contracts globally;
-- `--enforce-contract f` is optional and specifies that `f` must be checked against its contract.
-- `--replace-call-with-contract g` is optional and specifies that all calls to `g` must be replaced with its contract;
+- `--enforce-contract <function>` is optional and specifies that `function` must be checked against its contract.
+- `--replace-call-with-contract <function>` is optional and specifies that all calls to `function` must be replaced with its contract;
 
 ## Applying the function contracts transformation (with the dynamic frames method)
 
 The program transformation takes the following parameters:
 
 ```
-goto-instrument --dfcc harness [--enforce-contract f] (--replace-call-with-contract g)* [--apply-loop-contracts] in.gb out.gb
+goto-instrument --dfcc harness [--enforce-contract <function>[/<contract>]] (--replace-call-with-contract <function>[/<contract>])* in.gb out.gb
 ```
 
 Where:
 - `--dfcc harness` specifies the proof harness (i.e. the entry point of the analysis);
-- `--enforce-contract f` is optional and specifies that `f` must be checked against its contract.
-- `--replace-call-with-contract g` is optional and specifies that all calls to `g` must be replaced with its contract;
+- `--enforce-contract <function>[/<contract>]` is optional and specifies that `function` must be checked against `contract`.
+  When `contract` is not specfied, the contract is assumed to be carried by the `function` itself.
+- `--replace-call-with-contract <function>[/<contract>]` is optional and specifies that all calls to `function` must be replaced with `contract`.
+  When `contract` is not specfied, the contract is assumed to be carried by the `function` itself.
+
 

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -22,6 +22,7 @@ Author: Remi Delmas, [email protected]
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
+#include <util/string_utils.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_functions.h>
@@ -47,6 +48,72 @@ Author: Remi Delmas, [email protected]
 
 #include "dfcc_lift_memory_predicates.h"
 
+invalid_function_contract_pair_exceptiont::
+  invalid_function_contract_pair_exceptiont(
+    std::string reason,
+    std::string correct_format)
+  : cprover_exception_baset(std::move(reason)),
+    correct_format(std::move(correct_format))
+{
+}
+
+std::string invalid_function_contract_pair_exceptiont::what() const
+{
+  std::string res;
+
+  res += "Invalid function-contract mapping";
+  res += "\nReason: " + reason;
+
+  if(!correct_format.empty())
+  {
+    res += "\nFormat: " + correct_format;
+  }
+
+  return res;
+}
+
+#include <iostream>
+
+static std::pair<irep_idt, irep_idt>
+parse_function_contract_pair(const irep_idt &cli_flag)
+{
+  auto const correct_format_message =
+    "the format for function and contract pairs is "
+    "`<function_name>[/<contract_name>]`";
+
+  std::string cli_flag_str = id2string(cli_flag);
+
+  auto split = split_string(cli_flag_str, '/', true, false);
+
+  if(split.size() == 1)
+  {
+    return std::make_pair(cli_flag, cli_flag);
+  }
+  else if(split.size() == 2)
+  {
+    auto function_name = split[0];
+    if(function_name.size() == 0)
+    {
+      throw invalid_function_contract_pair_exceptiont{
+        "couldn't find function name before '/' in '" + cli_flag_str + "'",
+        correct_format_message};
+    }
+    auto contract_name = split[1];
+    if(contract_name.size() == 0)
+    {
+      throw invalid_function_contract_pair_exceptiont{
+        "couldn't find contract name after '/' in '" + cli_flag_str + "'",
+        correct_format_message};
+    }
+    return std::make_pair(function_name, contract_name);
+  }
+  else
+  {
+    throw invalid_function_contract_pair_exceptiont{
+      "couldn't parse '" + cli_flag_str + "'", correct_format_message};
+  }
+}
+
 void dfcc(
   const optionst &options,
   goto_modelt &goto_model,
@@ -59,17 +126,15 @@ void dfcc(
   message_handlert &message_handler)
 {
   std::map<irep_idt, irep_idt> to_replace_map;
-  for(const auto &function_id : to_replace)
-    to_replace_map.insert({function_id, function_id});
+  for(const auto &cli_flag : to_replace)
+    to_replace_map.insert(parse_function_contract_pair(cli_flag));
 
   dfcc(
     options,
     goto_model,
     harness_id,
-    to_check.has_value()
-      ? optionalt<std::pair<irep_idt, irep_idt>>(
-          std::pair<irep_idt, irep_idt>(to_check.value(), to_check.value()))
-      : optionalt<std::pair<irep_idt, irep_idt>>{},
+    to_check.has_value() ? parse_function_contract_pair(to_check.value())
+                         : optionalt<std::pair<irep_idt, irep_idt>>{},
     allow_recursive_calls,
     to_replace_map,
     apply_loop_contracts,
@@ -164,7 +229,7 @@ void dfcct::check_transform_goto_model_preconditions()
         "' either not found or has no body");
 
     // triggers signature compatibility checking
-    contract_handler.get_pure_contract_symbol(pair.second);
+    contract_handler.get_pure_contract_symbol(pair.second, pair.first);
 
     PRECONDITION_WITH_DIAGNOSTICS(
       pair.first != harness_id,
@@ -196,7 +261,7 @@ void dfcct::check_transform_goto_model_preconditions()
       "Function to replace '" + id2string(pair.first) + "' not found");
 
     // triggers signature compatibility checking
-    contract_handler.get_pure_contract_symbol(pair.second);
+    contract_handler.get_pure_contract_symbol(pair.second, pair.first);
 
     PRECONDITION_WITH_DIAGNOSTICS(
       pair.first != harness_id,

src/goto-instrument/contracts/dynamic-frames/dfcc.h

@@ -29,6 +29,7 @@ Author: Remi Delmas, [email protected]
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_H
 
+#include <util/exception_utils.h>
 #include <util/irep.h>
 #include <util/message.h>
 
@@ -56,19 +57,32 @@ class optionst;
 
 // clang-format off
 #define HELP_DFCC                                                              \
-  "--dfcc             activate dynamic frame condition checking for function\n"\
-  "                   contracts using given function as entry point"
-// clang-format on
+  "--dfcc <harness>   activate dynamic frame condition checking for function\n"\
+  "                   contracts using the given harness as entry point"
 
-// clang-format off
 #define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec"
 #define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):"
 #define HELP_ENFORCE_CONTRACT_REC                                              \
-  " --enforce-contract-rec <fun>  wrap fun with an assertion of its contract\n"\
+  " --enforce-contract-rec <function>[/<contract>]"                            \
+  "                               wrap fun with an assertion of the contract\n"\
   "                               and assume recursive calls to fun satisfy \n"\
   "                               the contract"
 // clang-format on
 
+/// Exception thrown for bad function/contract specification pairs passed on
+/// the CLI.
+class invalid_function_contract_pair_exceptiont : public cprover_exception_baset
+{
+public:
+  explicit invalid_function_contract_pair_exceptiont(
+    std::string reason,
+    std::string correct_format = "");
+
+  std::string what() const override;
+
+  std::string correct_format;
+};
+
 /// \ingroup dfcc-module
 /// \brief Applies function contracts transformation to GOTO model,
 /// using the dynamic frame condition checking approach.