Puzzling strcmp behavior about cbmc HOT 12 CLOSED

The initial problem here is that this requires a model of argc/argv, else argv[1] will just be an invalid pointer (run cbmc ./minimal-strcmp.c --pointer-check to see this). It'll take the following workflow instead:

goto-cc minimal_strcmp.c
goto-instrument --model-argc-argv 2 a.out b.out
cbmc b.out

Now that invocation of cbmc will take a lot longer, bug unfortunately still yields a spurious counterexample. I am yet to further investigate, but it seems that the model that we produce with --model-argc-argv still permits strcmp to produce non-deterministic results.

I'll keep investigating.

from cbmc.

Hi @gleachkr

There are a number of things that are going on here. CBMC does indeed have internal implementations of some library functions. In this case:

Secondly, CBMC has to do some non-deterministic modelling of the environment (including argc and argv). I think the interaction of these two is producing some unexpected results because there are some inputs where it is possible that the comparison fails and some where it is possible it succeeds.

Try:

int ret = strcmp("STORE", command);
assert(ret != 0 || ret == 0);

HTH

from cbmc.

Also, could you post the full output of the tool? It would be good to understand how many unwindings of the loop it uses.

My conjecture is that if argv[1] is "STORE\0!\0" then our internal version of strcmp would produce both outcomes as possibilities. I think our current modelling of argv will allow this value to be taken.

from cbmc.

Thanks for answering so quickly! Here's the plain output. If there's a debug flag that would be helpful, please just let me know:

CBMC version 5.91.0 (n/a) 64-bit x86_64 linux
Parsing minimal-strcmp.c
Converting
Type-checking minimal-strcmp
file /nix/store/3mmvgb08qy8n6n37mnprf77fnp4rssi9-glibc-2.38-27-dev/include/bits/strings_fortified.h line 26 function bcopy: fun
ction '__builtin_dynamic_object_size' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
file /nix/store/3mmvgb08qy8n6n37mnprf77fnp4rssi9-glibc-2.38-27-dev/include/bits/strings_fortified.h line 26 function bcopy: fun
ction '__builtin_dynamic_object_size' is not declared
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Unwinding loop strcmp.0 iteration 1 file <builtin-library-strcmp> line 44 function strcmp thread 0
Unwinding loop strcmp.0 iteration 2 file <builtin-library-strcmp> line 44 function strcmp thread 0
Unwinding loop strcmp.0 iteration 3 file <builtin-library-strcmp> line 44 function strcmp thread 0
Unwinding loop strcmp.0 iteration 4 file <builtin-library-strcmp> line 44 function strcmp thread 0
Unwinding loop strcmp.0 iteration 5 file <builtin-library-strcmp> line 44 function strcmp thread 0
Unwinding loop strcmp.0 iteration 1 file <builtin-library-strcmp> line 44 function strcmp thread 0
Unwinding loop strcmp.0 iteration 2 file <builtin-library-strcmp> line 44 function strcmp thread 0
Unwinding loop strcmp.0 iteration 3 file <builtin-library-strcmp> line 44 function strcmp thread 0
Unwinding loop strcmp.0 iteration 4 file <builtin-library-strcmp> line 44 function strcmp thread 0
Unwinding loop strcmp.0 iteration 5 file <builtin-library-strcmp> line 44 function strcmp thread 0
Runtime Symex: 0.0157539s
size of program expression: 237 steps
simple slicing removed 8 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 6.0344e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00679451s
Running propositional reduction
Post-processing
Runtime Post-process: 0.00115968s
Solving with CaDiCaL 1.9.4
2885 variables, 6198 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00171876s
Runtime decision procedure: 0.00860137s

** Results:
minimal-strcmp.c function main
[main.assertion.1] line 8 assertion strcmp("STORE", command) != 0 || strcmp("STORE", command) == 0: FAILURE

** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

from cbmc.

Thanks. It looks like it is unrolling the loops correctly, so yes, my conjecture still stands and it is a buggy interaction between the two models.

@tautschnig would any of the memory predicates that you have been working on help with this?

from cbmc.

I'm not certain, but is it possible that this is related?

cbmc ./minimal-strcmp.c, where minimal-strcmp.c is:

#include <assert.h>

int mystrcmp(const char *cs, const char *ct) {
  unsigned char c1, c2;
  while (1) {
    c1 = *cs++;
    c2 = *ct++;
    if (c1 != c2)
      return c1 < c2 ? -1 : 1;
    if (!c1)
      break;
  }
  return 0;
}

int main(int argc, char **argv) {
  if (argc != 2)
    return 1;
  char *command = argv[1];
  assert(mystrcmp("STORE", command) != 0);
  return 0;
}

yields

** Results:
minimal-strcmp.c function main
[main.assertion.1] line 21 assertion mystrcmp("STORE", command) != 0: SUCCESS

I would have expected failure, since compiling the program and passing STORE as a command line argument triggers the assert. (Again, provisos about probably doing something silly here).

from cbmc.

Try:

int ret = strcmp("STORE", command);
assert(ret != 0 || ret == 0);

Also, this works as expected.

** Results:
minimal-strcmp.c function main
[main.assertion.1] line 9 assertion ret != 0 || ret == 0: SUCCESS

from cbmc.

Now that invocation of cbmc will take a lot longer, bug unfortunately still yields a spurious counterexample. I am yet to further investigate, but it seems that the model that we produce with --model-argc-argv still permits strcmp to produce non-deterministic results.

I'll keep investigating.

#8174 addresses this problem.

from cbmc.

Closing this issue as #8174 has been merged. Please feel free to re-open!

from cbmc.

Thanks for being so welcoming as I find my way around cbmc. I'm still running into some puzzling strcmp behavior, seemingly unrelated to argv, although as usual it might be me misunderstanding something. Here's the example:

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>

char* myconcat(char* s1, char* s2) {
    int l1 = strlen(s1);
    int l2 = strlen(s2);
    char *out = malloc(l1 + l2);
    int i = 0;

    for (; i < l1; i++) out[i] = s1[i];
    for (; i < l1 + l2; i++) out[i] = s2[i - l1];

    return out;
}

char* myconcat2(char* s1, char* s2) {
    int l1 = strlen(s1);
    int l2 = strlen(s2);
    char *out = malloc(l1 + l2);
    memcpy(out,s1, l1);
    memcpy(out + l1,s2, l2);
    return out;
}

int main(void) {
    char* rslt1 = myconcat("a", "b");
    char* rslt2 = myconcat2("a", "b");
    assert(strcmp(rslt1, "ab") == 0);
    assert(strcmp(rslt2, "ab") == 0);
}

Both asserts pass when running as a normal binary. Both fail under cbmc min-ex.c. Any idea what's going on?

from cbmc.

You might want to re-run this with --pointer-check enabled (which will be the default with the upcoming 6.0 release) to learn that there may be an out-of-bounds access in strcmp. The reason for this out-of-bounds access is your lack of zero termination in the concatenated strings. The following patch addresses this problem in your code:

--- 8173.c	2024-02-09 08:54:09.908916308 +0000
+++ 8173+fix.c	2024-02-09 08:53:58.272781945 +0000
@@ -12,6 +12,7 @@
     for (; i < l1; i++) out[i] = s1[i];
     for (; i < l1 + l2; i++) out[i] = s2[i - l1];

+    out[l1 + l2] = 0;
     return out;
 }

@@ -21,6 +22,7 @@
     char *out = malloc(l1 + l2 + 1);
     memcpy(out,s1, l1);
     memcpy(out + l1,s2, l2);
+    out[l1 + l2] = 0;
     return out;
 }

from cbmc.

Ah, right... thanks!

from cbmc.