Can I use CBMC (a static verification tool for C) for code-golf?

Question

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 in gcc) and / or like array-input which needs to be taken via pre-defined constants (either as global const 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

Would your submission be the program you feed to CBMC? Could you write a simple language, that uses CBMC, but makes the IO more standard? — H.PWiz, Sep 2, 2018 at 0:02
You show the output, but can you also show the program and what the input looks like? — Nathan Merrill, Sep 2, 2018 at 0:35
@NathanMerrill I have edited the program and the input in, but will probably follow H.PWiz' suggestion anyways. — SEJPM, Sep 2, 2018 at 8:04
not about the outputting, but the PPCG I/O rules don't permit the input being taken as named variables anyway — dzaima, Sep 2, 2018 at 11:06
@dzaima true, but we've made exceptions for languages before: for example, SQL can accept input from named tables (which is equivalent to named variables IMO) — Nathan Merrill, Sep 2, 2018 at 12:53

SEJPM · Accepted Answer · 2018-09-02 15:45:47Z

Because I had a few spare hours on my hands, I wrote a simple parser / compiler / whatevs that will effectively solve all the problems of this post:

The new language will take input as line-by-line from STDIN (which is allowed) and will hardcode it into a copy of the source program which then gets fed to CBMC.
The output of which gets redirected to a file, post-processed and then send to STDOUT.
The loop-unrolling parameter is still there, but set high enough to hopefully deal with most loops for which the iteration count can't be easily identified, ie you want to lower it using a command-line argument if you have nested loops.

As for whether CBMC without the above should be allowed, I'd be inclined to say "no" for now because it indeed violates the most-downvoted I/O format and exceptions apparently only get granted on a case-by-case basis which I don't want to invoke due to the above solution.

Stack Exchange Network

Can I use CBMC (a static verification tool for C) for code-golf?

1 Answer 1

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged
discussion
output
languages
.

Linked

Hot Network Questions

Can I use CBMC (a static verification tool for C) for code-golf?

1 Answer 1

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged discussionoutputlanguages.

Linked

Related

Hot Network Questions

Not the answer you're looking for? Browse other questions tagged
discussion
output
languages
.