From 2e30ddd41c6ad923421512eb0f5424f70b79c5d0 Mon Sep 17 00:00:00 2001
From: Vincent Mihalkovic <vmihalko@redhat.com>
Date: Sat, 22 Jan 2022 12:43:12 +0100
Subject: [PATCH 1/3] goto_instrt_parse_options, util/cmdline: refactor
src/goto-instrument/goto_instrument_parse_options: add
--add-cmd-line-arg option, refactor code around.
src/util/cmdline: refactor, do not interpret every "--{string}" as
option for CBMC.
---
.../goto_instrument_parse_options.cpp | 34 +++++++++++++++++--
.../goto_instrument_parse_options.h | 4 ++-
src/util/cmdline.cpp | 2 +-
3 files changed, 35 insertions(+), 5 deletions(-)
diff --git src/goto-instrument/goto_instrument_parse_options.cpp src/goto-instrument/goto_instrument_parse_options.cpp
index 0d337897c..cb46908b1 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -92,7 +93,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "interrupt.h"
#include "k_induction.h"
#include "mmio.h"
-#include "model_argc_argv.h"
#include "nondet_static.h"
#include "nondet_volatile.h"
#include "points_to.h"
@@ -105,6 +104,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <fstream> // IWYU pragma: keep
#include <iostream>
#include <memory>
+#include <sstream>
#include "accelerate/accelerate.h"
@@ -1054,10 +1054,38 @@ void goto_instrument_parse_optionst::instrument_goto_program()
{
unsigned max_argc=
safe_string2unsigned(cmdline.get_value("model-argc-argv"));
+ std::list<std::string> argv;
+ argv.resize(max_argc);
log.status() << "Adding up to " << max_argc << " command line arguments"
<< messaget::eom;
- if(model_argc_argv(goto_model, max_argc, ui_message_handler))
+
+ if(model_argc_argv(
+ goto_model, argv, true /*model_argv*/, ui_message_handler))
+ throw 0;
+ }
+
+ if(cmdline.isset("add-cmd-line-arg"))
+ {
+ const std::list<std::string> &argv = cmdline.get_values("add-cmd-line-arg");
+ unsigned argc = 0;
+
+ std::stringstream ss;
+ ss << "[";
+ std::string sep = "";
+ for(auto const &arg : argv)
+ {
+ ss << sep << "\"" << arg << "\"";
+ argc++;
+ sep = ", ";
+ }
+ ss << "]";
+
+ log.status() << "Adding " << argc << " arguments: " << ss.str()
+ << messaget::eom;
+
+ if(model_argc_argv(
+ goto_model, argv, false /*model_argv*/, ui_message_handler))
throw 0;
}
@@ -1862,7 +1859,7 @@ void goto_instrument_parse_optionst::help()
HELP_REMOVE_CALLS_NO_BODY
" {y--add-library} \t add models of C library functions\n"
HELP_CONFIG_LIBRARY
- " {y--model-argc-argv} {un} \t model up to {un} command line arguments\n"
+ HELP_ARGC_ARGV
" {y--remove-function-body} {uf} remove the implementation of function {uf}"
" (may be repeated)\n"
HELP_REPLACE_CALLS
diff --git src/goto-instrument/goto_instrument_parse_options.h src/goto-instrument/goto_instrument_parse_options.h
index eed0e9e3d..6aabb43d1 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -39,6 +39,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include "dump_c.h"
#include "generate_function_bodies.h"
#include "insert_final_assert_false.h"
+#include "model_argc_argv.h"
#include "nondet_volatile.h"
#include "reachability_slicer.h"
#include "replace_calls.h"
@@ -96,7 +97,8 @@ Author: Daniel Kroening, kroening@kroening.com
"(interpreter)(show-reaching-definitions)" \
"(list-symbols)(list-undefined-functions)" \
"(z3)(add-library)(show-dependence-graph)" \
- "(horn)(skip-loops):(model-argc-argv):" \
+ "(horn)(skip-loops):" \
+ OPT_ARGC_ARGV \
OPT_DFCC \
"(" FLAG_LOOP_CONTRACTS ")" \
"(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
diff --git src/util/cmdline.cpp src/util/cmdline.cpp
index 84530430a..ce7e049a5 100644
--- a/src/util/cmdline.cpp
+++ b/src/util/cmdline.cpp
@@ -305,7 +305,7 @@ bool cmdlinet::parse_arguments(int argc, const char **argv)
i++;
if(i == argc)
return true;
- if(argv[i][0] == '-' && argv[i][1] != 0)
+ if(options[*optnr].optstring != "add-cmd-line-arg" && argv[i][0] == '-' && argv[i][1] != 0)
return true;
options[*optnr].values.push_back(argv[i]);
}
--
2.31.1
From 8071c8d281bb76435c05d50b81055a6c295b0c45 Mon Sep 17 00:00:00 2001
From: Vincent Mihalkovic <vmihalko@redhat.com>
Date: Thu, 18 Nov 2021 20:30:56 +0100
Subject: [PATCH 2/3] goto-instrument/model_argc_argv: add new option:
--add-cmd-line-arg
---
src/goto-instrument/model_argc_argv.cpp | 123 +++++++++++++++++++-----
src/goto-instrument/model_argc_argv.h | 13 ++-
2 files changed, 113 insertions(+), 23 deletions(-)
diff --git src/goto-instrument/model_argc_argv.cpp src/goto-instrument/model_argc_argv.cpp
index ca3c5d1e2..378301f1e 100644
--- a/src/goto-instrument/model_argc_argv.cpp
+++ b/src/goto-instrument/model_argc_argv.cpp
@@ -30,15 +30,51 @@ Date: April 2016
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
-/// Set up argv with up to max_argc pointers into an array of 4096 bytes.
+// Escape selected character in specified string with backslashes.
+//
+// \param input_string: string where character will be escaped.
+// \param find_substring: character to escape, e.g. \"
+// \param replace_substring: string, e.g. \\\"
+std::string escape_char(
+ std::string input_string,
+ std::string find_substring,
+ std::string replace_substring){
+ size_t index = 0;
+ while (true) {
+ /* Locate the substring to replace. */
+ index = input_string.find(find_substring, index);
+
+ if (index == std::string::npos) break;
+
+ /* Make the replacement. */
+ input_string.replace(index,
+ replace_substring.size(),
+ replace_substring);
+
+ /* Advance index forward so the next iteration
+ * doesn't pick it up as well. */
+ index += replace_substring.size();
+ }
+ return input_string;
+}
+
+/// Set up argv to user-specified values (when model_argv is FALSE) or
+/// (when model_argv is TRUE) set up argv with up to max_argc pointers
+/// into a char array of 4096 bytes.
+///
/// \param goto_model: Contains the input program's symbol table and
/// intermediate representation
-/// \param max_argc: User-specified maximum number of arguments to be modelled
+/// \param argv_args: User-specified cmd-line arguments (ARGV),
+/// when model_argv is TRUE then size of argv_args represents
+/// the maximum number of arguments to be modelled
+/// \param model_argv: If set to TRUE then modelling argv with up to
+/// max_argc pointers
/// \param message_handler: message logging
/// \return True, if and only if modelling succeeded
bool model_argc_argv(
goto_modelt &goto_model,
- unsigned max_argc,
+ const std::list<std::string> &argv_args,
+ bool model_argv,
message_handlert &message_handler)
{
messaget message(message_handler);
@@ -83,25 +119,52 @@ bool model_argc_argv(
// guaranteed by POSIX (_POSIX_ARG_MAX):
// http://pubs.opengroup.org/onlinepubs/009695399/basedefs/limits.h.html
std::ostringstream oss;
- oss << "int ARGC;\n"
- << "char *ARGV[1];\n"
- << "void " << goto_model.goto_functions.entry_point() << "()\n"
- << "{\n"
- << " unsigned next=0u;\n"
- << " " CPROVER_PREFIX "assume(ARGC>=1);\n"
- << " " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n"
- << " char arg_string[4096];\n"
- << " " CPROVER_PREFIX "input(\"arg_string\", &arg_string[0]);\n"
- << " for(int i=0; i<ARGC && i<" << max_argc << "; ++i)\n"
- << " {\n"
- << " unsigned len;\n"
- << " " CPROVER_PREFIX "assume(len<4096);\n"
- << " " CPROVER_PREFIX "assume(next+len<4096);\n"
- << " " CPROVER_PREFIX "assume(arg_string[next+len]==0);\n"
- << " ARGV[i]=&(arg_string[next]);\n"
- << " next+=len+1;\n"
- << " }\n"
- << "}";
+ unsigned max_argc = argv_args.size();
+ unsigned argc = argv_args.size();
+
+ if(model_argv)
+ {
+ oss << "int ARGC;\n"
+ << "char *ARGV[1];\n"
+ << "void " << goto_model.goto_functions.entry_point() << "()\n"
+ << "{\n"
+ << " unsigned next=0u;\n"
+ << " " CPROVER_PREFIX "assume(ARGC>=1);\n"
+ << " " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n"
+ << " char arg_string[4096];\n"
+ << " " CPROVER_PREFIX "input(\"arg_string\", &arg_string[0]);\n"
+ << " for(int i=0; i<ARGC && i<" << max_argc << "; ++i)\n"
+ << " {\n"
+ << " unsigned len;\n"
+ << " " CPROVER_PREFIX "assume(len<4096);\n"
+ << " " CPROVER_PREFIX "assume(next+len<4096);\n"
+ << " " CPROVER_PREFIX "assume(arg_string[next+len]==0);\n"
+ << " ARGV[i]=&(arg_string[next]);\n"
+ << " next+=len+1;\n"
+ << " }\n"
+ << "}";
+ }
+ else
+ { // model_argv = false, set each argv[i] explicitly
+ oss << "int ARGC = " << argc << ";\n"
+ << "char *ARGV[" << argc << "];\n"
+ << "void " << goto_model.goto_functions.entry_point() << "()\n"
+ << "{\n"
+ << "int ARGC = " << argc << ";\n";
+ int i = 0;
+ for(auto &arg : argv_args)
+ {
+ oss << "ARGV[" << i << "]=\"" << escape_char(
+ escape_char(
+ escape_char(arg, "\\","\\\\"),
+ "\'","\\\'"),
+ "\"","\\\"")
+ << "\";\n";
+ i++;
+ }
+ oss << "}";
+ }
+
std::istringstream iss(oss.str());
ansi_c_languaget ansi_c_language;
@@ -169,6 +232,22 @@ bool model_argc_argv(
main_call!=end;
++main_call)
{
+ //Turn into skip instr. the INPUT(argc ...) instruction
+ if (main_call->is_other() &&
+ main_call->get_other().get_statement() == ID_input &&
+ "argc\'" == id2string(to_symbol_expr(
+ main_call->get_other().op1()).get_identifier())) {
+ main_call->turn_into_skip();
+ }
+
+ //Turn into skip instr. the ASSUME(argc ...) instruction
+ if(main_call->is_assume() &&
+ "argc\'" == id2string(to_symbol_expr(
+ main_call->condition().operands()[0]).get_identifier())){
+
+ main_call->turn_into_skip();
+ }
+
if(main_call->is_function_call())
{
const exprt &func = main_call->call_function();
diff --git src/goto-instrument/model_argc_argv.h src/goto-instrument/model_argc_argv.h
index 9328f22b4..9b39de969 100644
--- a/src/goto-instrument/model_argc_argv.h
+++ b/src/goto-instrument/model_argc_argv.h
@@ -14,12 +14,23 @@ Date: April 2016
#ifndef CPROVER_GOTO_INSTRUMENT_MODEL_ARGC_ARGV_H
#define CPROVER_GOTO_INSTRUMENT_MODEL_ARGC_ARGV_H
+#include <list>
+#include <string>
+
class goto_modelt;
class message_handlert;
bool model_argc_argv(
goto_modelt &,
- unsigned max_argc,
+ const std::list<std::string> &argv_args,
+ bool model_argv,
message_handlert &);
+#define OPT_ARGC_ARGV "(model-argc-argv):(add-cmd-line-arg):"
+
+#define HELP_ARGC_ARGV \
+ " --model-argc-argv <n> model up to <n> command line arguments\n" \
+ " --add-cmd-line-arg <arg> add command line argument (may be " \
+ "repeated)\n"
+
#endif // CPROVER_GOTO_INSTRUMENT_MODEL_ARGC_ARGV_H
--
2.31.1