So with the recent maze challenge I had the idea to implement a solution using CBMC (home / source), which is a tool that statically verifies C code and can produce counter-examples for property failures. I intend to feed it programs that, with the below input methods, generate the output a challenge demands. However I have encountered some obstacles and would like to ask whether these are obstacles of the disqualifying kind.
In particular I'd like to have confirmation that the below three properties don't disqualify CBMC:
- Scalar input needs to be taken as macro-argument
-DN=3
flag (like ingcc
) and / or like array-input which needs to be taken via pre-defined constants (either as globalconst int x[]={}
or as#define X {A,B,C}
that are#include
'd, note that the include avoids hard-coding into the source-file. - The output is quite noisy and includes intermediate program state information and other otherwise useful but here hindering output in addition to what is printed with standard formatting. This extra information (usually a couple of thousand lines) can easily be filtered out using a small external program, post-processing (stripping) the output.
- The correctness, ie whether the tool finds a valid solution, sometimes depends on a CLI parameter to the tool, ie usually for larger / more complex inputs this parameter needs to be upped (in particular this is the parameter that bounds the maximal amount of loop-unrolls the tool will do).
Example triple (input, program, output) for this challenge.
Example Input:
content of data.h
:
const int obsX[] = {1};
const int obsY[] = {1};
const int obsLen = sizeof(obsX)/sizeof(int);
paired with the following command-line call:
cbmc simple-lab.c -DN=3 -DPY=1 -DTY=1 --trace --beautify --unwind 10
Example Program:
#include <stdio.h>
#include <assert.h>
#include "data.h"
int main() {
int curX=0, curY=PY;
while(1)
{
char direction;
int newX=curX, newY=curY;
if(direction==0)
newY--; // north
else if(direction==1)
newX++; // east
else if(direction==2)
newY++; // south
else
newX--; // west
if(newX < 0 || newX >= N || newY >= N || newY < 0)
continue;
int abandon=0;
for(int i=0;i<obsLen;i++)
abandon |= newX == obsX[i] && newY == obsY[i];
if(abandon)
continue;
else
{curX=newX;curY=newY;}
printf("%d,%d\n",curX,curY);
assert(!(curX == N-1 && curY == TY));
}
return 0;
}
Example (full) tool-output (as you can see there's a pair of integers with a newline sticking out every couple of states which signify the intended output generated by the printf):
CBMC version 5.6 64-bit x86_64 linux
Parsing simple-lab.c
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Converting
Type-checking simple-lab
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop main.0 iteration 1 (10 max) file simple-lab.c line 33 function main thread 0
Unwinding loop main.1 iteration 1 (10 max) file simple-lab.c line 15 function main thread 0
Unwinding loop main.0 iteration 1 (10 max) file simple-lab.c line 33 function main thread 0
Unwinding loop main.1 iteration 2 (10 max) file simple-lab.c line 15 function main thread 0
Unwinding loop main.0 iteration 1 (10 max) file simple-lab.c line 33 function main thread 0
Unwinding loop main.1 iteration 3 (10 max) file simple-lab.c line 15 function main thread 0
Unwinding loop main.0 iteration 1 (10 max) file simple-lab.c line 33 function main thread 0
Unwinding loop main.1 iteration 4 (10 max) file simple-lab.c line 15 function main thread 0
Unwinding loop main.0 iteration 1 (10 max) file simple-lab.c line 33 function main thread 0
Unwinding loop main.1 iteration 5 (10 max) file simple-lab.c line 15 function main thread 0
Unwinding loop main.0 iteration 1 (10 max) file simple-lab.c line 33 function main thread 0
Unwinding loop main.1 iteration 6 (10 max) file simple-lab.c line 15 function main thread 0
Unwinding loop main.0 iteration 1 (10 max) file simple-lab.c line 33 function main thread 0
Unwinding loop main.1 iteration 7 (10 max) file simple-lab.c line 15 function main thread 0
Unwinding loop main.0 iteration 1 (10 max) file simple-lab.c line 33 function main thread 0
Unwinding loop main.1 iteration 8 (10 max) file simple-lab.c line 15 function main thread 0
Unwinding loop main.0 iteration 1 (10 max) file simple-lab.c line 33 function main thread 0
Unwinding loop main.1 iteration 9 (10 max) file simple-lab.c line 15 function main thread 0
Unwinding loop main.0 iteration 1 (10 max) file simple-lab.c line 33 function main thread 0
Not unwinding loop main.1 iteration 10 (10 max) file simple-lab.c line 15 function main thread 0
size of program expression: 792 steps
simple slicing removed 23 assignments
Generated 10 VCC(s), 10 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 without simplifier
12727 variables, 35264 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.029s
** Results:
[main.assertion.1] assertion !(curX == N-1 && curY == TY): FAILURE
Trace for main.assertion.1:
State 21 file simple-lab.c line 14 function main thread 0
----------------------------------------------------
curX=0 (00000000000000000000000000000000)
State 22 file simple-lab.c line 14 function main thread 0
----------------------------------------------------
curX=0 (00000000000000000000000000000000)
State 23 file simple-lab.c line 14 function main thread 0
----------------------------------------------------
curY=0 (00000000000000000000000000000000)
State 24 file simple-lab.c line 14 function main thread 0
----------------------------------------------------
curY=1 (00000000000000000000000000000001)
State 26 file simple-lab.c line 17 function main thread 0
----------------------------------------------------
direction=2 (00000010)
State 27 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 28 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 29 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=0 (00000000000000000000000000000000)
State 30 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=1 (00000000000000000000000000000001)
State 34 file simple-lab.c line 25 function main thread 0
----------------------------------------------------
newY=2 (00000000000000000000000000000010)
State 37 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 38 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 39 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 40 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 45 file simple-lab.c line 34 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 46 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=1 (00000000000000000000000000000001)
State 50 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curX=0 (00000000000000000000000000000000)
State 51 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curY=2 (00000000000000000000000000000010)
0,2
State 57 file simple-lab.c line 17 function main thread 0
----------------------------------------------------
direction=1 (00000001)
State 58 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 59 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 60 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=0 (00000000000000000000000000000000)
State 61 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=2 (00000000000000000000000000000010)
State 64 file simple-lab.c line 23 function main thread 0
----------------------------------------------------
newX=1 (00000000000000000000000000000001)
State 67 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 68 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 69 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 70 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 76 file simple-lab.c line 34 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 77 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=1 (00000000000000000000000000000001)
State 81 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curX=1 (00000000000000000000000000000001)
State 82 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curY=2 (00000000000000000000000000000010)
1,2
State 88 file simple-lab.c line 17 function main thread 0
----------------------------------------------------
direction=0 (00000000)
State 89 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 90 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=1 (00000000000000000000000000000001)
State 91 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=0 (00000000000000000000000000000000)
State 92 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=2 (00000000000000000000000000000010)
State 94 file simple-lab.c line 21 function main thread 0
----------------------------------------------------
newY=1 (00000000000000000000000000000001)
State 97 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 98 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 99 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 100 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 106 file simple-lab.c line 34 function main thread 0
----------------------------------------------------
abandon=1 (00000000000000000000000000000001)
State 107 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=1 (00000000000000000000000000000001)
State 114 file simple-lab.c line 17 function main thread 0
----------------------------------------------------
direction=2 (00000010)
State 115 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 116 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=1 (00000000000000000000000000000001)
State 117 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=0 (00000000000000000000000000000000)
State 118 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=2 (00000000000000000000000000000010)
State 122 file simple-lab.c line 25 function main thread 0
----------------------------------------------------
newY=3 (00000000000000000000000000000011)
State 128 file simple-lab.c line 17 function main thread 0
----------------------------------------------------
direction=6 (00000110)
State 129 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 130 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=1 (00000000000000000000000000000001)
State 131 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=0 (00000000000000000000000000000000)
State 132 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=2 (00000000000000000000000000000010)
State 136 file simple-lab.c line 27 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 138 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 139 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 140 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 141 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 146 file simple-lab.c line 34 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 147 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=1 (00000000000000000000000000000001)
State 151 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curX=0 (00000000000000000000000000000000)
State 152 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curY=2 (00000000000000000000000000000010)
0,2
State 158 file simple-lab.c line 17 function main thread 0
----------------------------------------------------
direction=1 (00000001)
State 159 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 160 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 161 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=0 (00000000000000000000000000000000)
State 162 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=2 (00000000000000000000000000000010)
State 165 file simple-lab.c line 23 function main thread 0
----------------------------------------------------
newX=1 (00000000000000000000000000000001)
State 168 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 169 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 170 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 171 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 177 file simple-lab.c line 34 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 178 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=1 (00000000000000000000000000000001)
State 182 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curX=1 (00000000000000000000000000000001)
State 183 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curY=2 (00000000000000000000000000000010)
1,2
State 189 file simple-lab.c line 17 function main thread 0
----------------------------------------------------
direction=1 (00000001)
State 190 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 191 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=1 (00000000000000000000000000000001)
State 192 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=0 (00000000000000000000000000000000)
State 193 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=2 (00000000000000000000000000000010)
State 196 file simple-lab.c line 23 function main thread 0
----------------------------------------------------
newX=2 (00000000000000000000000000000010)
State 199 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 200 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 201 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 202 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 207 file simple-lab.c line 34 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 208 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=1 (00000000000000000000000000000001)
State 212 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curX=2 (00000000000000000000000000000010)
State 213 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curY=2 (00000000000000000000000000000010)
2,2
State 219 file simple-lab.c line 17 function main thread 0
----------------------------------------------------
direction=0 (00000000)
State 220 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=0 (00000000000000000000000000000000)
State 221 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newX=2 (00000000000000000000000000000010)
State 222 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=0 (00000000000000000000000000000000)
State 223 file simple-lab.c line 18 function main thread 0
----------------------------------------------------
newY=2 (00000000000000000000000000000010)
State 225 file simple-lab.c line 21 function main thread 0
----------------------------------------------------
newY=1 (00000000000000000000000000000001)
State 228 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 229 file simple-lab.c line 32 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 230 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 231 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=0 (00000000000000000000000000000000)
State 236 file simple-lab.c line 34 function main thread 0
----------------------------------------------------
abandon=0 (00000000000000000000000000000000)
State 237 file simple-lab.c line 33 function main thread 0
----------------------------------------------------
i=1 (00000000000000000000000000000001)
State 241 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curX=2 (00000000000000000000000000000010)
State 242 file simple-lab.c line 39 function main thread 0
----------------------------------------------------
curY=1 (00000000000000000000000000000001)
2,1
Violated property:
file simple-lab.c line 43 function main
assertion !(curX == N-1 && curY == TY)
!(curX == 3 - 1 && curY == 1)
** 1 of 1 failed (1 iteration)
VERIFICATION FAILED