Feature request: specify input arguments of verified programs

[vmihalko]

Hi,
We are (at RedHat) developing a tool for running dynamic analysis on RPM packages fully automatically. For this purpose, we want to use the open-source tools like Divine, Symbiotic, CBMC, Valgrind and others.
Because the "size" of the verified model is often too large, cbmc is running for too long (or forever). We would appreciate if CBMC had an option to enter specific input arguments for verified programs e.g. cbmc print.c --argv 'Hello world'. It would simplify the verification process a lot.
Do you plan to add such an option to CBMC in the near future?

[martin-cs]

Glad to hear you are finding it useful. I'm not sure I would class it as a dynamic analysis tool in the same way as Valgrind though.

You can pass arguments, sort of using two different approaches. -DMACRO=VALUE allows you to set preprocessor macros. The other option is to generate some C:

$ cat main_with_args.c
int main_with_args(void) {
  char *name="print";
  char *argument="Hello world";
  int argc = 2;
  char *argv[argc] = {name, argument};
  int return_value = main(argc, argv);
  assert(return_value == 0);
  return;
}

Then run cbmc print.c main_with_args.c --function main_with_args. You might also want to try out --depth to limit the execution. HTH.

As far I know there is no plan to add the kind of option that you describe but it shouldn't be too hard to do.

[vmihalko]

Thank you for your quick reply.

The things you have mentioned are possible if it were a one-time affair, but the whole process of automatic analysis of RPM packages is quite complex and uses several different programs and scripts. Therefore, I think that the implementation of some of the methods you mentioned is unnecessarily demanding (and opens up room for bugs).

If the implementation of such an option for cbmc isn't too hard to do, then let's do it.
Would you mind implementing it, or should I try it myself? And in case I won't be successful, I kindly ask for your help or advice.

[martin-cs]

I'll see if I can make the time to have a go. Before I do though, could you clarify what you mean by dynamic analysis? CBMC is really not the same kind of tool as valgrind and if you try to use it in the same way, your effort / result curve will likely not be very good.

[vmihalko]

This is short talk about what we are doing, and how (and why) we want to use the tools for formal verification.

If you take the time, we'd appreciate it.

[martin-cs]

Working note : goto-instrument's --model-argc-argv could be relatively easily adapted to do this.

[vmihalko]

I was trying to implement this feature by myself, but I will need some help.

So this is similar approach as you have mentioned in second comment - wrap the program with some new function...
And what we need is to somehow pass the arguments from outside to argv_string. We could modify these lines in way to pass the argv arguments.
Do I understand the problem correctly?
How would you implement it? Can you give me some instructions, what to do?

[martin-cs]

Hi @vmihalko ! Sorry I hadn't got to doing this; as you can imagine, life in a University has been quite ... chaotic this year.

Your understanding is correct. If I was doing this I would...

1. Grep the regression/ tests for something that uses --model-argc-argv and check that A. the test was run and B. it did what I thought it did.
2. Create a new folder in regression/goto-instrument/ with one .c file (normally main.c) and two .desc files. It is fine to copy and modify from regression/goto-instrument/argc-argv1/test.desc. The format is documented here :

   cbmc/regression/test.pl

   Line 310 in 29ca8a9

   test.pl expects a test.desc file in each subdirectory. The file test.desc

   . One of the .desc files should be for just a call with --model-argc-argv and verification should fail because setting the command line length is not enough. The other should use your new option --model-cmd-line or whatever and verification should pass. Just having an assert for the first letter of argv[0] is probably enough.
3. Add your new option to

   cbmc/src/goto-instrument/goto_instrument_parse_options.h

   Line 101 in 29ca8a9

   "(horn)(skip-loops):(model-argc-argv):" \

   note that the : at the end will be important because that means it takes an argument. Also add help text here

   cbmc/src/goto-instrument/goto_instrument_parse_options.cpp

   Line 1846 in 29ca8a9

   // NOLINTNEXTLINE(whitespace/line_length)

   [ If you are feeling super helpful, you could even refactor the declaration and help of model-argc-argv and your option out to https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/goto_instrument_parse_options.h using the same pattern as https://github.com/diffblue/cbmc/blob/29ca8a96db4cdcf567a8e6accd2e3ea3e26f02cd/src/goto-instrument/count_eloc.h#L24 . ]
4. Add handling for your flag here

   cbmc/src/goto-instrument/goto_instrument_parse_options.cpp

   Line 1063 in 29ca8a9
   . Copy-paste-modify the handling of --model-argc-argv is fine.
5. Add model_cmd_line( goto_modelt &, const std::string &, message_handlert & ); here

   cbmc/src/goto-instrument/model_argc_argv.h

   Line 24 in 29ca8a9
   .
6. Implement model_cmd_line in https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/model_argc_argv.cpp sharing as much code with model_argc_argv as possible. It is OK to basically rename the existing model_argc_argv give it an extra argument and then have both of the model_* functions call it.
7. Compile up your main.c test, run your new option, use --show-goto-functions and --validate-goto-model to check that it is generating what you feel is right. Run cbmc on it with --validate-ssa-equation and make sure you get the right result.
8. Run the test suite and make sure everything passes.
9. Build a series of commits. Refactoring should go in the first one, new functionality in the second and the new tests in the third one.
10. See https://github.com/diffblue/cbmc/blob/develop/README.md#contributing-to-the-code-base and https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md although most of the important stuff is checked in CI.
11. Submit a PR!

HTH.

[vmihalko]

Hi @martin-cs, thank you very much for such a detailed instructions!

I'm struggling with model-argc-argv function and I would appreciate if you could help me.

This is my first attempt to change (what I think is) the important part of model-argc-argv function :

  std::ostringstream argv_strings;
  std::ostringstream argv_strings_lengths;
  std::string sep_s, sep_sl = "";
  for (auto const& arg : args /* args type: std::list<std::string>*/) {
        argv_strings << sep_s << arg;
        argv_strings_lengths << sep_sl << arg.size();
        sep_s = " ";
        sep_sl = ",";
  }

  oss2 << "int ARGC = " << max_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] = \"" << argv_strings.str() << "\";\n"
      << "  int args_len[" << max_argc << "] = {" << argv_strings_lengths.str() <<"} ;\n"
      << "  " CPROVER_PREFIX "input(\"arg_string\", &arg_string[0]);\n"
      << "  for(int i=0; i<ARGC && i<" << max_argc << "; ++i)\n"
      << "  {\n"
      << "    unsigned len = args_len[next];\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"
      << "}";

  
  std::istringstream iss(oss2.str());

This is how my test.c program looks like:

#include <assert.h>

int main(int argc, char* argv[])
{
  if(argc>=2)
    assert(*argv[1]=='H'); //First char from argv[1]

  return 0;
}

After running:
goto-cc test.c -o test_com;goto-instrument --model-cmd-line 'AAAAA' --model-cmd-line 'BBBBB' --model-cmd-line 'CCCCC' --show-goto-functions test_com output is:

Adding 3 arguments: AAAAA BBBBB CCCCC
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

__CPROVER__start /* __CPROVER__start */
        // 10 no location
        CALL __CPROVER_initialize()
        // 11 no location
        ASSUME argc' ≥ 1
        // 12 no location
        ASSUME argc' ≤ 268435456
        // 13 no location
        OTHER code statement="input"(address_of("argc"[0]), argc')        // 14 no location
        ASSIGN argv'[argc'] := NULL
        // 15 file <built-in-library> line 5 function __CPROVER__start
        DECL __CPROVER__start::1::next : unsignedbv[32]
        // 16 file <built-in-library> line 5 function __CPROVER__start
        ASSIGN __CPROVER__start::1::next := 0
        // 17 file <built-in-library> line 6 function __CPROVER__start
        ASSUME argc' ≥ 1
        // 18 file <built-in-library> line 7 function __CPROVER__start
        ASSUME argc' ≤ 3
        // 19 file <built-in-library> line 8 function __CPROVER__start
        DECL __CPROVER__start::1::arg_string : signedbv[8][4096]
        // 20 file <built-in-library> line 8 function __CPROVER__start
        ASSIGN __CPROVER__start::1::arg_string := { 65, 65, 65, 65, 65, 32, 66, 66, 66, 66, 66, 32, 67, 67, 67, 67, 67, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, <LOT_OF_ZEROES>, 0 }
        // 21 file <built-in-library> line 9 function __CPROVER__start
        DECL __CPROVER__start::1::args_len : signedbv[32][3]
        // 22 file <built-in-library> line 9 function __CPROVER__start
        ASSIGN __CPROVER__start::1::args_len := { 5, 5, 5 }
        // 23 file <built-in-library> line 10 function __CPROVER__start
        OTHER code #source_location="" statement="input"(address_of("arg_string"[0]), address_of #source_location=""(__CPROVER__start::1::arg_string[cast(0, signedbv[64])]))        // 24 file <built-in-library> line 11 function __CPROVER__start
        DECL __CPROVER__start::1::1::i : signedbv[32]
        // 25 file <built-in-library> line 11 function __CPROVER__start
        ASSIGN __CPROVER__start::1::1::i := 0
        // 26 file <built-in-library> line 11 function __CPROVER__start
     1: IF ¬(__CPROVER__start::1::1::i < argc' ∧ __CPROVER__start::1::1::i < 3) THEN GOTO 2
        // 27 file <built-in-library> line 13 function __CPROVER__start
        DECL __CPROVER__start::1::1::1::len : unsignedbv[32]
        // 28 file <built-in-library> line 13 function __CPROVER__start
        ASSIGN __CPROVER__start::1::1::1::len := cast(__CPROVER__start::1::args_len[cast(__CPROVER__start::1::next, signedbv[64])], unsignedbv[32])
        // 29 file <built-in-library> line 14 function __CPROVER__start
        ASSUME __CPROVER__start::1::1::1::len < cast(4096, unsignedbv[32])
        // 30 file <built-in-library> line 15 function __CPROVER__start
        ASSUME __CPROVER__start::1::next + __CPROVER__start::1::1::1::len < cast(4096, unsignedbv[32])
        // 31 file <built-in-library> line 16 function __CPROVER__start
        ASSUME cast(__CPROVER__start::1::arg_string[cast(__CPROVER__start::1::next + __CPROVER__start::1::1::1::len, signedbv[64])], signedbv[32]) = 0
        // 32 file <built-in-library> line 17 function __CPROVER__start
        ASSIGN argv'[cast(__CPROVER__start::1::1::i, signedbv[64])] := address_of #source_location=""(__CPROVER__start::1::arg_string[cast(__CPROVER__start::1::next, signedbv[64])])
        // 33 file <built-in-library> line 18 function __CPROVER__start
        ASSIGN __CPROVER__start::1::next := __CPROVER__start::1::next + (__CPROVER__start::1::1::1::len + cast(1, unsignedbv[32]))
        // 34 file <built-in-library> line 19 function __CPROVER__start
        DEAD __CPROVER__start::1::1::1::len
        // 35 file <built-in-library> line 11 function __CPROVER__start
        ASSIGN __CPROVER__start::1::1::i := __CPROVER__start::1::1::i + 1
        // 36 file <built-in-library> line 11 function __CPROVER__start
        GOTO 1
        // 37 file <built-in-library> line 19 function __CPROVER__start
     2: DEAD __CPROVER__start::1::1::i
        // 38 file <built-in-library> line 19 function __CPROVER__start
        DEAD __CPROVER__start::1::args_len
        // 39 file <built-in-library> line 19 function __CPROVER__start
        DEAD __CPROVER__start::1::arg_string
        // 40 file <built-in-library> line 19 function __CPROVER__start
        DEAD __CPROVER__start::1::next
        // 41 file main.c line 3
        CALL return' := main(argc', address_of(argv'[0]))
        // 42 file main.c line 3
        OTHER code #source_location="" statement="output"(address_of("return'"[0]), return')        // 43 no location
        END_FUNCTION

^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

__CPROVER_initialize /* __CPROVER_initialize */
        // 44 no location
        SKIP
        // 45 file <built-in-additions> line 20
        ASSIGN __CPROVER_alloca_object := NULL
        // 46 file <built-in-additions> line 14
        ASSIGN __CPROVER_dead_object := NULL
        // 47 file <built-in-additions> line 13
        ASSIGN __CPROVER_deallocated := NULL
        // 48 file <built-in-additions> line 23
        ASSIGN __CPROVER_malloc_failure_mode_assert_then_assume := 2
        // 49 file <built-in-additions> line 22
        ASSIGN __CPROVER_malloc_failure_mode_return_null := 1
        // 50 file <built-in-additions> line 17
        ASSIGN __CPROVER_malloc_is_new_array := 0 ≠ 0
        // 51 file <built-in-additions> line 15
        ASSIGN __CPROVER_malloc_object := NULL
        // 52 file <built-in-additions> line 16
        ASSIGN __CPROVER_malloc_size := 0
        // 53 file <built-in-additions> line 24
        ASSIGN __CPROVER_max_malloc_size := cast(36028797018963968, unsignedbv[64])
        // 54 file <built-in-additions> line 18
        ASSIGN __CPROVER_memory_leak := NULL
        // 55 file <built-in-additions> line 8
        ASSIGN __CPROVER_next_thread_id := cast(0, unsignedbv[64])
        // 56 file <built-in-additions> line 11
        ASSIGN __CPROVER_next_thread_key := cast(0, unsignedbv[64])
        // 57 file <built-in-additions> line 38
        ASSIGN __CPROVER_pipe_count := cast(0, unsignedbv[32])
        // 58 file <built-in-additions> line 29
        ASSIGN __CPROVER_rounding_mode := 0
        // 59 file <built-in-additions> line 6
        ASSIGN __CPROVER_thread_id := cast(0, unsignedbv[64])
        // 60 file <built-in-additions> line 10
        ASSIGN __CPROVER_thread_key_dtors := array_of #source_location=""(NULL)
        // 61 file <built-in-additions> line 9
        ASSIGN __CPROVER_thread_keys := array_of #source_location=""(NULL)
        // 62 file <built-in-additions> line 7
        ASSIGN __CPROVER_threads_exited := array_of #source_location=""(false)
        // 63 no location
        END_FUNCTION

^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

main /* main */
        // 0 file main.c line 5 function main
        DECL main::1::a : signedbv[8][5]
        // 1 file main.c line 5 function main
        ASSIGN main::1::a := { 97, 104, 111, 106, 0 }
        // 2 file main.c line 6 function main
        IF ¬(main::argc ≥ 2) THEN GOTO 1
        // 3 file main.c line 7 function main
        OTHER code #source_location="" statement="expression"(cast(4, empty))        // 4 file main.c line 7 function main
        ASSERT cast(*(*(main::argv + cast(1, signedbv[64]))), signedbv[32]) = 72 // assertion *argv[1]=='H'
        // 5 no location
     1: SKIP
        // 6 file main.c line 9 function main
        RETURN 0
        // 7 file main.c line 9 function main
        DEAD main::1::a
        // 8 file main.c line 9 function main
        GOTO 2
        // 9 file main.c line 10 function main
     2: END_FUNCTION

Finally cbmc --validate-ssa-equation test_instr:

CBMC version 5.38.0 (n/a) 64-bit x86_64 linux
Reading GOTO program from file
Reading: test_instr
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00730338s
size of program expression: 79 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 0.000192961s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00375059s
Running propositional reduction
Post-processing
Runtime Post-process: 5.9584e-05s
Solving with MiniSAT 2.2.1 with simplifier
33600 variables, 795 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 8.2501e-05s
Runtime decision procedure: 0.00388338s

** Results:
main.c function main
[main.assertion.1] line 7 assertion *argv[1]=='H': SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL

1. I'm not sure, what is this line, function input doing?
2. I assume that it is more or less enough to change mentioned part of model-argc-argv function, is my assumption correct? The other code is unreadable (for me) without jumps to definitions...
3. My problem is that even from the --show-goto-functions output, I'm not able to recognize where the problem is and what am I doing wrong(?)

[martin-cs]

This looks like a really good start. I am not sure if github comments are the most efficient way of debugging this. Would it be possible to have a virtual meeting by jisti, zoom, teams or the like? If you drop me an e-mail I hope we can arrange a time.

[vmihalko]

I agree, my email is vmihalko@redhat.com.