diffblue / cbmc Goto Github PK

C Bounded Model Checker

Home Page: https://diffblue.github.io/cbmc

License: Other

Makefile 0.60% C 33.51% C++ 59.47% Java 2.03% Perl 0.07% Shell 0.29% Yacc 0.57% Lex 0.36% Batchfile 0.01% Scilab 1.08% Python 0.38% SMT 0.13% Jasmin 1.05% Emacs Lisp 0.01% Roff 0.01% Groovy 0.02% Gnuplot 0.01% CMake 0.39% JavaScript 0.03% Dockerfile 0.01%

cbmc's Introduction

CProver Documentation

About

CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio. It also supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions. Furthermore, it can check C and C++ for consistency with other languages, such as Verilog. The verification is performed by unwinding the loops in the program and passing the resulting equation to a decision procedure.

For full information see cprover.org.

For an overview of the various tools that are part of CProver and how to use them see TOOLS_OVERVIEW.md.

Versions

Get the latest release

Releases are tested and for production use.

Get the current develop version: git clone https://github.com/diffblue/cbmc.git

Develop versions are not recommended for production use.

Installing

Windows

For windows you can install cbmc binaries via the .msi's found on the releases page.

Note that we depend on the Visual C++ redistributables. You likely already have these, if not please download and run vcredist.x64.exe from Microsoft to install them prior to running cbmc.

Linux

For different linux environments, you have these choices:

Install CBMC through the distribution's repositories, with the downside that this might install an older version of cbmc, depending on what the package maintenance policy of the distribution is, or
Install CBMC through the .deb package built by each release, available on the releases page. To do that, download the .deb package and run apt install cbmc-x.y.deb with root privileges, with x.y being substituted for the version you are attempting to install.

NOTE: Because of libc/libc++ ABI compatibility and package dependency names, if you follow this path make sure you install the package appropriate for the version of operating system you are using.
Compile from source using the instructions here

macOS

For macOS there is a package available in Homebrew/core. Assuming you have homebrew installed, you can run

$ brew install cbmc

to install CBMC, or if you already have it installed via homebrew

$ brew upgrade cbmc

to get an up-to-date version.

Homebrew will always update formulas to their latest version available, so you may periodically see an upgraded version of CBMC being downloaded regardless of whether you explicitly requested that or not. If you would rather this didn't happen, you can pin the CBMC version with:

$ brew pin cbmc

If instead of the latest version, you would want to install a historic version, you can do so with a homebrew tap that we maintain. Instructions for that are available in the documentation

Report bugs

If you encounter a problem please file a bug report:

Create an issue

Contributing to the code base

Fork the repository
Clone the repository git clone [email protected]:YOURNAME/cbmc.git
Create a branch from the develop branch (default branch)
Make your changes (follow the coding guidelines)
Push your changes to your branch
Create a Pull Request targeting the develop branch

New contributors can look through the mini projects page for small, focussed feature ideas.

License

4-clause BSD license, see LICENSE file.

cbmc's People

Contributors

Stargazers

Watchers

Forkers

tautschnig pkesseli-archive lihaol agriggio peterschrammel martin-cs bkolb neuroradiology danielneville vincentjzimmer danpoe lucasccordeiro theyoucheng annatrost ngothan rjmunro thk123 royletron ssvlab sosy-lab glaubitz smowton lennonchaves vladrich nathanjphillips mgudemann nmanthey allredj cristina-david reuk owen-mc-diffblue nlightnfotis zemanlx sumanthsprabhu mariusmc92 degiorgio marek-trtik rnbguy admiral-akk cesaro dcattaruzza uwevil jeremygu eigold damianvesk appcoreopc jasigal polgreen grockious kpouliasis janmroczkowski arpit94 antlechner majakusber chrisr-diffblue markrtuttle karkhaz andreast271 duzhanyuan elaghs viktormalik alipourm tiandiyixian hannes-steffenhagen-diffblue rongqinglee thomasspriggs charliemowood melshuber jeannielynnmoulton mi-ki c0demark ibliss mbeckersys arthurfait johndumbell fuzzamos sonodtt qaphla mre zhixing-xu damonliuthu codebyzeb mmuesly codzart nchong xbauch tjj2017 ovascos yumibagge clccc bitcalc huangshiyou jgwilson42 edstenson fanhy2114 lpmi-13 nanolith freddytuxworth poornima77 jin-hui

cbmc's Issues

bug in concurrency encoding for arrays and structs

regression tests coming...

CBMC in SVComp 16

Hi,

This is not an issue but just few queries regarding cbmc in svcomp16.

Which version of cbmc was used in svcomp-16?
What are the command line options used when running cbmc in svcomp?
How can I reproduce same results?

Extend SMT backend to use string theory

start with CVC4, Z3

links with front end via #45 and #46

Problems with showing the symbol table for some class files

For some class files, --show-symbol-table fails with identifier java::java.lang.Object not found

For example for the class file of the inner class Responses$Authenticate generated from: https://github.com/v-l-a-d/java-driver/blob/2.1/driver-core/src/main/java/com/datastax/driver/core/Responses.java

the whole result is:

CBMC version 5.4 64-bit x86_64 linux
Parsing com/datastax/driver/core/Responses$Authenticate.class
Java main class: com.datastax.driver.core.Responses$Authenticate
failed to load class `com.datastax.driver.core.Message'
failed to load class `com.datastax.driver.core.Responses'
failed to load class `com.datastax.driver.core.Message$Decoder'
failed to load class `com.datastax.driver.core.Responses$Authenticate$1'
failed to load class `java.lang.StringBuilder'
failed to load class `java.lang.String'
failed to load class `com.datastax.driver.core.Message$Response'
failed to load class `com.datastax.driver.core.Message$Response$Type'
Converting

Symbols:

Symbol......: __CPROVER_malloc_object
Pretty name.: 
Module......: 
Base name...: __CPROVER_malloc_object
Mode........: C
Type........: void *
Value.......: 
Flags.......: lvalue thread_local state_var
Location....: 

Symbol......: __CPROVER_rounding_mode
Pretty name.: 
Module......: 
Base name...: __CPROVER_rounding_mode
Mode........: C
Type........: signed int
Value.......: 
Flags.......: lvalue thread_local state_var
Location....: 

identifier java::java.lang.Object not found

The C front-end should support function pointer return types in KnR

This is currently known as ansi-c/KnR3 regression test, which fails with a parser error.

Why CBMC is reporting this program as safe?

Hi,
I'm using CMBC 5.3 to check pointer safety of following program.

#include<stdio.h>
#include<stdlib.h>
int main()
{
        char *c = malloc(1);
        printf("%p\n", c);
        c = c + 20;

        printf("%p\n", c);
        printf("%d\n", *c);

        free(c - 20);
        return 0;
}

Here I'm dereferencing a pointer which is 20 unit away from legally allocated memory. Why CBMC is not reporting this program as unsafe? Am I missing something?

Cannot build CBMC

I am trying to build the current master on my mac.
The build fails because zip.h cannot be found:

$ make
## Entering big-int
/Applications/Xcode.app/Contents/Developer/usr/bin/make  -C big-int
make[1]: Nothing to be done for `first_target'.
## Entering util
/Applications/Xcode.app/Contents/Developer/usr/bin/make  -C util
make[1]: Nothing to be done for `first_target'.
## Entering langapi
/Applications/Xcode.app/Contents/Developer/usr/bin/make  -C langapi
make[1]: Nothing to be done for `first_target'.
## Entering ansi-c
/Applications/Xcode.app/Contents/Developer/usr/bin/make  -C ansi-c
make[1]: Nothing to be done for `first_target'.
## Entering linking
/Applications/Xcode.app/Contents/Developer/usr/bin/make  -C linking
make[1]: Nothing to be done for `first_target'.
## Entering cpp
/Applications/Xcode.app/Contents/Developer/usr/bin/make  -C cpp
make[1]: Nothing to be done for `first_target'.
## Entering xmllang
/Applications/Xcode.app/Contents/Developer/usr/bin/make  -C xmllang
make[1]: Nothing to be done for `first_target'.
## Entering assembler
/Applications/Xcode.app/Contents/Developer/usr/bin/make  -C assembler
make[1]: Nothing to be done for `first_target'.
## Entering java_bytecode
/Applications/Xcode.app/Contents/Developer/usr/bin/make  -C java_bytecode
clang++ -c -MMD -MP -mmacosx-version-min=10.9 -std=c++11 -stdlib=libc++ -D STL_HASH_STD -Wall -O2 -I .. -I ../../libzip/lib -DHAVE_LIBZIP -o jar_file.o jar_file.cpp
jar_file.cpp:15:10: fatal error: 'zip.h' file not found
#include <zip.h>
         ^
1 error generated.
make[1]: *** [jar_file.o] Error 1
make:

static member in class

In the following program the function f verifies div-by-zero, g correctly fails this property.

public class StaticMember
{
  static int xs;
  int x;
  public void f()
  {
    int d = 1 / (1 + xs);
  }
  public void g()
  {
    int d = 1 / (1 + x);
  }
}

When using either function as entry point, the value of the non-local variable should be considered non-deterministic.

cbmc --smt2 reports success for any property when no solver is available

cbmc --smt2 foo.c with

int main() { assert(0); }

yields

$ cbmc/cbmc --smt2 foo.c
CBMC version 5.4 64-bit x86_64 macos
Parsing foo.c
Converting
Type-checking foo
file foo.c line 1 function main: function `assert' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 30 steps
simple slicing removed 3 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to SMT2 QF_AUFBV using MathSAT
converting SSA
Running SMT2 QF_AUFBV using MathSAT
Runtime decision procedure: 0.008s

** Results:
[main.assertion.1] assertion 0: SUCCESS

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

when I don't have MathSAT anywhere near my PATH.
Best,
Michael

Refinement-based reduction of partial order constraints

patches exist, further performance improvements on the todo list...

Make --function work with non-static functions (Java)

For non-static (in the Java sense) functions, we need to create a valid this object (with 'non-deterministic or null' members) in the _start function before invoking a method.
We should refuse to use --function with an interface or abstract class methods.

Variable Type Analysis for resolving virtual methods

StackMapTable attribute is ignored in class files, leading to wrong names and types in goto program

In the current implementation, the indices of the variables in the local variable table are used without considering the StackMapTable code attribute. For larger methods this leads to wrong names and types of the variables.

For example in BasicTikaFSConsumerBuilder.java the following code

        if( tikaConfigPath == null) {
            Node tikaConfigNode = node.getAttributes().getNamedItem("tikaConfig");
            if (tikaConfigNode != null) {
                tikaConfigPath = PropsUtil.getString(tikaConfigNode.getNodeValue(), null);
            }
        }
        if (tikaConfigPath != null) {
            try (InputStream is = Files.newInputStream(Paths.get(tikaConfigPath))) {
                config = new TikaConfig(is);
            } catch (Exception e) {
                throw new RuntimeException(e);
            }
        } else {
            config = TikaConfig.getDefaultConfig();
        }

        List<FileResourceConsumer> consumers = new LinkedList<FileResourceConsumer>();
        int numConsumers = BatchProcessBuilder.getNumConsumers(runtimeAttributes);

results in the following bytecode

       167: ifnonnull     203
       170: aload_1       
       171: invokeinterface #8,  1            // InterfaceMethod org/w3c/dom/Node.getAttributes:()Lorg/w3c/dom/NamedNodeMap;
       176: ldc           #14                 // String tikaConfig
       178: invokeinterface #9,  2            // InterfaceMethod org/w3c/dom/NamedNodeMap.getNamedItem:(Ljava/lang/String;)Lorg/w3c/dom/Node;
       183: astore        10
       185: aload         10
       187: ifnull        203
       190: aload         10
       192: invokeinterface #10,  1           // InterfaceMethod org/w3c/dom/Node.getNodeValue:()Ljava/lang/String;
       197: aconst_null   
       198: invokestatic  #15                 // Method org/apache/tika/util/PropsUtil.getString:(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;
       201: astore        9
       203: aload         9
       205: ifnull        342
       208: aload         9
       210: iconst_0      
       211: anewarray     #4                  // class java/lang/String
       214: invokestatic  #16                 // Method java/nio/file/Paths.get:(Ljava/lang/String;[Ljava/lang/String;)Ljava/nio/file/Path;
       217: iconst_0      
       218: anewarray     #17                 // class java/nio/file/OpenOption
       221: invokestatic  #18                 // Method java/nio/file/Files.newInputStream:(Ljava/nio/file/Path;[Ljava/nio/file/OpenOption;)Ljava/io/InputStream;
       224: astore        10
...
       342: invokestatic  #27                 // Method org/apache/tika/config/TikaConfig.getDefaultConfig:()Lorg/apache/tika/config/TikaConfig;
       345: astore        8
       347: new           #28                 // class java/util/LinkedList
       350: dup           
       351: invokespecial #29                 // Method java/util/LinkedList."<init>":()V
       354: astore        10

with the following local variable table (irrelevant parts omitted):

      LocalVariableTable:
        Start  Length  Slot  Name   Signature
...
             185      18    10 tikaConfigNode   Lorg/w3c/dom/Node;
             260       7    12    x2   Ljava/lang/Throwable;
             309       7    14    x2   Ljava/lang/Throwable;
             226     101    10    is   Ljava/io/InputStream;
...
             356     293    10 consumers   Ljava/util/List;
...

in the goto-program, it is the variable consumers which gets assigned the values intended for tikaConfigNode

       // 410 file BasicTikaFSConsumersBuilder.java line 87
        return_tmp18 = NONDET(struct org.w3c.dom.Node *);
        // 411 file BasicTikaFSConsumersBuilder.java line 87
        consumers = (struct java.util.List *)return_tmp18;
        // 412 file BasicTikaFSConsumersBuilder.java line 88
        IF (void *)(void *)consumers == null THEN GOTO 5
        // 413 file BasicTikaFSConsumersBuilder.java line 89
        ASSERT false // block 31
        // 414 file BasicTikaFSConsumersBuilder.java line 89
        (void *)consumers . org.w3c.dom.Node.getNodeValue:()Ljava/lang/String;();

and is

        // 437 file BasicTikaFSConsumersBuilder.java line 93
        return_tmp24 = NONDET(struct java.io.InputStream *);
        // 438 file BasicTikaFSConsumersBuilder.java line 93
        consumers = (struct java.util.List *)return_tmp24;
        // 439 file BasicTikaFSConsumersBuilder.java line 93
        numConsumers = (int)null;
        // 440 file BasicTikaFSConsumersBuilder.java line 94
        new_tmp25 = MALLOC(struct org.apache.tika.config.TikaConfig, 4);
        // 441 file BasicTikaFSConsumersBuilder.java line 94
        *new_tmp25 = { .@class_identifier="java::org.apache.tika.config.TikaConfig" };
        // 442 file BasicTikaFSConsumersBuilder.java line 94
        new_tmp25 . org.apache.tika.config.TikaConfig.<init>:(Ljava/io/InputStream;)V((void *)consumers);
        // 443 file BasicTikaFSConsumersBuilder.java line 94
        ASSERT false // block 38
        // 444 file BasicTikaFSConsumersBuilder.java line 94
        config = (struct org.apache.tika.config.TikaConfig *)new_tmp25;
        // 445 file BasicTikaFSConsumersBuilder.java line 95
        IF (void *)(void *)consumers == null THEN GOTO 7
        // 446 file BasicTikaFSConsumersBuilder.java line 95
        ASSERT false // block 39
        // 447 file BasicTikaFSConsumersBuilder.java line 95
        IF (void *)(void *)numConsumers == null THEN GOTO 6
        // 448 file BasicTikaFSConsumersBuilder.java line 95
        ASSERT false // block 40
        // 449 file BasicTikaFSConsumersBuilder.java line 95
        (void *)consumers . java.io.InputStream.close:()V();

although consumers is of type List<FileResourceConsumer>, which is also the cast in the goto-program in the above example.

The reason for this is that the index of all three variables is 10 and consumers is the last using this index.

To correct this, one has to take into account the relevant StackMapTable of the code (if such a table does exists). The relevant frame for the correct usage of consumers is this:

           frame_type = 255 /* full_frame */
          offset_delta = 34
          locals = [ class org/apache/tika/batch/fs/builders/BasicTikaFSConsumersBuilder, class org/w3c/dom/Node, class java/util/Map, class java/util/concurrent/ArrayBlockingQueue, int, class java/lang/String, class java/lang/Long, class java/lang/String, class org/apache/tika/config/TikaConfig, class java/lang/String, class java/util/List, int, class org/w3c/dom/NodeList, class org/w3c/dom/Node, class org/w3c/dom/Node, class org/w3c/dom/Node, int ]
          stack = []

while the correct ones for the preceeding variables with index 10 have to be constructed with the stack frame entries before.

Error with parameters of the form `.class`

For example, when supplying a Class object in the form of String.class, CBMC fails with

function call: parameter "java::classtest1.f:(Ljava/lang/Class;Z)Z::arg1a" type mismatch: got struct
  * incomplete_class: 1
  * name: java::java.lang.String
  * tag: java.lang.String
  * base_name: java.lang.String
  * components:
    0:
      * type: string
      * name: @class_identifier
      * pretty_name: @class_identifier
  * #class: 1, expected pointer
  * #reference: 1
  0: symbol
      * identifier: java::java.lang.Class
      * #base_name: java.lang.Class

regression test:

public class classtest1
{
  public void test()
  {
    assert(f(String.class, true));
  }

  public boolean f(Class c, boolean b)
  {
    return b;
  }
}

cbmc --show-goto-functions should exit with return code 0

currently it returns 6

Advanced goto-diff

syntactic and semantic diffing of goto programs

Support for GNU GCC nested functions

(...or better not!)

I stumbled over this concession to Pascal programmers:
https://gcc.gnu.org/onlinedocs/gcc/Nested-Functions.html

Test case:
https://github.com/JoliOS/grub2/blob/master/util/grub-fstest.c#L211

Note that this feature is not used in the original grub code:
http://git.savannah.gnu.org/cgit/grub.git/tree/util/grub-fstest.c#n240

#cformat contains incorrect value after modifying constants in simplify_expr

Constants modified by simplify_expr get printed incorrectly by expr2c. Either update #cformat or remove it and use "value" in expr2c.

Error `byte_extract flatting of non-constant source size: byte_extract_little_endian`

This file returns the following error with cbmc --cover location --unwind 3 --function "com.datastax.driver.core.VersionNumber.hashCode:()I" com/datastax/driver/core/VersionNumber.class

converting SSA
byte_extract flatting of non-constant source size: byte_extract_little_endian
  * type: pointer
      0: struct
          * tag: java::array[reference]
          * components: 
            0: 
              * type: struct
                  * incomplete_class: 1
                  * name: java::java.lang.Object
                  * tag: java.lang.Object
                  * base_name: java.lang.Object
                  * components: 
                    0: 
                      * type: string
                      * name: @class_identifier
                      * pretty_name: @class_identifier
                  * #class: 1
              * name: @java.lang.Object
            1: 
              * type: signedbv
                  * width: 32
                  * #c_type: signed_int
              * name: length
            2: 
              * type: pointer
                  0: pointer
                      * #failed_symbol: java::com.datastax.driver.core.VersionNumber.hashCode:()I::this$object
                      0: empty
              * name: data
  0: symbol
      * type: empty
      * identifier: tmp_struct_init$1!0#1
      * expression: symbol
          * type: empty
          * identifier: tmp_struct_init$1
      * L0: 0
      * L2: 1
      * #SSA_symbol: 1
  1: constant
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      * value: 0000000000000000000000000000000000000000000000000000000000100100

a similar error appears for this method

object reference for static methods in Java

When checking for division by zero, the following shows different results when analyzing the static method f (passes the verification) and g (fails verification), although non-deterministic choice for the input integer should allow for a = -1 in the first case, too.

public class StaticMethod { 
  static public void f(int a, int b) {
    int c = b/(a+1);
  }
  static public void g(int a, int b) {
    int c = a/(b+1);
  }
}

The problem seems to be that the first parameter that is passed to the static method is the result of a malloc, i.e., the memory allocated for a StaticMethod object instance. Whereas, in the function it is treated as a NONDET(int).

        // 0 no location
        __CPROVER_initialize();
        // 1 no location
        tmp_struct_init$1 = MALLOC(struct StaticMethod { struct java.lang.Object @java.lang.Object; }, 4);
        // 2 no location
        tmp_struct_init$1->@java.lang.Object.@class_identifier = "StaticMethod";
        // 3 no location
        StaticMethod.g:(II)V(tmp_struct_init$1, NONDET(int));
        // 4 no location
        END_FUNCTION

StaticMethod.f() /* java::StaticMethod.f:(II)V */
        // 7 file StaticMethod.java line 4
        ASSERT !(arg0i == -1) // division by zero in arg1i / (arg0i + 1)
        // 8 file StaticMethod.java line 4
        local2i = arg1i / (arg0i + 1);
        // 9 no location
        END_FUNCTION

The C front-end should fully support typeof and real

This is currently tracked in regression test ansi-c/gcc_builtins2.

Error in loop unwinding using iterators

With the command line cbmc --cover location --unwind 3 --function iterator1.f iterator1.class, the following program unwinds the loop indefinitely:

import java.util.List;

public class iterator1
{
  public void f(List<List<String>> list)
  {
    int i = 0;
    for(List<String> l : list)
      for(String s : l)
        i++;
  }
}

leads to

Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
...

Translation of Java string operations

introduce string operator expressions,
and built-ins for Java String operations

to link up with @agriggio's work on SMT backend #44

Type mismatch when using enum in Java

There is a regression test for this in #89

Error `convert_bitwise: unexpected operand width`

The following fails with cbmc --cover location --function bitwise1.f bitwise1.class with the above error.

public class bitwise1
{
  static char c;
  void f()
  {
    int i = (c & 2);
  }
}

In boolbvt_bitwise::convert_bitwise the reported width of the char operand is 16 (from std::size_t width=boolbv_width(expr.type());) but the size of the converted operand is 32. Java uses widening numeric promotion to int in this case. Interestingly, this program does not produce the above error in the following version (1 instead of 2):

public class bitwise1
{
  static char c;
  void f()
  {
    int i = (c & 1);
  }
}

Add CBMC internal variable names to JSON goto trace output

...to be able to distinguish e.g. global/local variables.

ansi-c/Array_Declarator* regression tests: front end is too permissive

These are marked KNOWNBUG at the moment, because goto-cc accepts what gcc wouldn't:

Array_Declarator2/main.c:5:18: error: variable length array must be bound in function definition
void fooStar(int x[*])
                 ^
1 error generated.
$ gcc Array_Declarator3/main.c
Array_Declarator3/main.c:7:11: error: type qualifier used in array declarator outside of function prototype
  int bar0[restrict] = {0};
          ^
1 error generated.
$ gcc Array_Declarator4/main.c
Array_Declarator4/main.c:7:11: error: 'static' used in array declarator outside of function prototype
  int bar1[static 1U] = {1};
          ^
1 error generated.
$ gcc Array_Declarator5/main.c
Array_Declarator5/main.c:7:11: error: type qualifier used in array declarator outside of function prototype
  int bar2[restrict 2U] = {1, 2};
          ^
1 error generated.
$ gcc Array_Declarator6/main.c
Array_Declarator6/main.c:7:11: error: 'static' used in array declarator outside of function prototype
  int bar3[restrict static 3U] = {1, 2, 3};
          ^
1 error generated.
$ gcc Array_Declarator7/main.c
Array_Declarator7/main.c:7:11: error: 'static' used in array declarator outside of function prototype
  int bar4[static restrict 4U] = {1, 2, 3, 4};
          ^
1 error generated.

It may be debatable whether the C front end really needs to produce errors here, it safely ignores these extra qualifiers anyway.

Best,
Michael

Pointer encoding limits address space to 24bits for ILP32

The following fails when checking with --ilp32 (for nbytes >=2^24)

uint32_t nondet_uint32_t();

void mk_char_array() {
uint32_t nbytes = nondet_uint32_t();
char memory[nbytes];
char *start = &memory[0];
char *end = &memory[nbytes];
uint32_t diff = end - start;
__CPROVER_assert(diff == nbytes, "Check size match");
}

It's rare to allocate arrays of that size in software, and few people use ILP32, however, the restriction is an unnecessary artefact of the encoding that CBMC uses (upper 8 bits for object reference, remaining bits for offset within the object)...
The problem doesn't occur with LP64 (64-8 > 48).

Issue raised by Nathan Chong, ARM.

Type mismatch with Bool type for Java

This program

public class boolean2
{
  public void entry(boolean b)
  {
    f(b);
    assert(true);
  }

  public boolean f(boolean b)
  {
    return !b;
  }
}

fails with

function call: parameter "java::boolean2.f:(Z)Z::arg1z" type mismatch: got signedbv
  * width: 32, expected c_bool
  * width: 8

on cbmc --function "boolean2.entry" boolean2.class with cbmc version that passes boolean1 test.

Replace static_analysis by ai

extract patch from new lock analysis implementation

Error on recursive functions in Java

For recursive functions in JVM bytecode, CBMC fails with

main method ` ... ' has no body

Make goto binaries work with java

currently,
goto-cc class-file -o goto-binary
produces a goto-binary, but
cbmc goto-binary
fails with "Multi-language linking not supported", and
goto-instrument goto-binary --show-goto-functions
fils with "symbol `_start' has unknown mode 'java'"

Error `identifier __CPROVER_memory not found`

For thie file the following cbmc --unwind 3 --function "com.datastax.driver.core.querybuilder.Utils.containsBindMarker:(Ljava/lang/Object;)Z" com/datastax/driver/core/querybuilder/Utils.class returns identifier __CPROVER_memory not found

Error on switch on variable in base class

This program

public class Inheritance2
{
  int x;
  public class A extends Inheritance2
  {
    void m1(int i)
    {
      if (x == 1)
        assert(true);
      else
        assert(false);
    }
    void m2(int i)
    {
      switch(x)
        {
        case 1:
          assert(true);
          break;
        default:
          assert(false);
          break;
        }
    }

    void test1(int i)
    {
      m1(i);
    }
    void test2(int i)
    {
      m2(i);
    }
  }
}

correctly reports on cbmc --function "Inheritance2\$A.test1" Inheritance2.class

** Results:
[assertion.1] assertion at file Inheritance2.java line 11: FAILURE
[assertion.2] assertion at file Inheritance2.java line 21: SUCCESS

but fails on cbmc --function "Inheritance2\$A.test2" Inheritance2.class with

size of program expression: 57 steps
simple slicing removed 8 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
component x not found in structure

Error `equality without matching types`

For the following program

public class NullPointer5
{
  void f()
  {
    Object o = new Object();
    if(null == o)
      assert false;
    assert true;
  }
  void g()
  {
    Object o = new Object();
    if(o == null)
      assert false;
    assert true;
  }
}

the result of checking --function NullPointer5.g is ok, while --function NullPointer.f fails with the above error.

The same error is triggered with --function Inheritance3.f in

class Inheritance3
{
  class A
  {
  }
  class B extends A
  {
  }
  void f()
  {
    A a = new A();
    B b = new B();
    if(a == b)
      assert false;
    assert true;
  }
}

Bug in --dump-c when there is "continue" statement inside a loop

A continue statement in the loop disappears after the --dump-c operation. This bug in --dump-c can be re-generated as follows. The code used is from regression/cbmc/for2/main.c

int main()
{
  int i;
  int k;

  for (i=0; i<3; i++)
  {
    k=3;
    continue;
    k=4;
  }

  assert(0);
}

goto-cc main.c -o main.goto
goto-instrument main.goto --dump-c

The resulted code after '--dump-c' is shown in below.

#include <assert.h>

// assert
// file main.c line 13 function main
signed int assert(void);

// main
// file main.c line 1
signed int main()
{
  signed int i;
  signed int k;
  i = 0;
  for( ; !(i >= 3); i = i + 1)
  {
    k = 3;
    k = 4;
  }
  /* assertion 0 */
  assert((_Bool)0);
}

As we can see, the 'continue' statement disappears in the --dump-c result.

Meanwhile, the --show-goto-functions confirms that the continue statement is still within the goto program.

Add JSON_UI

produce JSON formatted output, similar to --xml-ui

Error 'The program has no entry point' on goto-binary without main(), although --function is given

when --function is given, cbmc should analyze the binary regardless of the presence of a main() function

--dump-java

create pull request for existing patch

Refinement-based slicing

patches exist, but performance is not yet convincing

Translation of Java strings to string_type

to make handling of string objects language independent

to link up with @agriggio's work on SMT backend #44

Incorrect verification failed when using pointers to pointers inside structs

Both CBMC 5.4 and the current development version (master branch) incorrectly output "VERIFICATION FAILED" when run on the following test case.

#include <assert.h>
#include <stdbool.h>
#include <stdlib.h>

struct list_entry {
    struct list_entry *next;
};

struct linked_list {
    struct list_entry *head;
    struct list_entry **tail;
};

struct linked_list_container {
    struct linked_list list;
};

int main(int argc, char* argv[])
{
    struct linked_list_container container;
    struct linked_list *list = &container.list;
    struct list_entry head;

    list->head = NULL;
    list->tail = &list->head;

    *list->tail = &head;
    list->tail = &head.next;

    assert(list->head);

    return 0;
}

I have uploaded CBMC's output for this program to this gist. It looks CBMC thinks that list->tail points to an invalid object at line 27 of test_case.c.

Bug in the inequality normalisation of the simplifier

I got the following from Madhukar. The input formula has a single satisfying assignment (0). The output formula has also 2^31-1.

Hi,

There seems to be a bug in the simplify_expr code. For the following input formula:

f.a <= 2147483646 && -((signed __CPROVER_bitvector[33])f.a) <= -1 || FALSE && FALSE || f.a <= -1 && -((signed __CPROVER_bitvector[33])f.a) <= 2147483648 || f.a <= 2147483647 && -((signed __CPROVER_bitvector[33])f.a) <= -2147483647 || FALSE && FALSE

I get an output formula (see below) which is not equisatisfiable to the input formula.

output:

!(f.a >= 0) && !(-((signed __CPROVER_bitvector[33])f.a) >= 2147483649) || !(f.a >= 2147483647) && !(-((signed __CPROVER_bitvector[33])f.a) >= 0) || !(-((signed __CPROVER_bitvector[33])f.a) >= -2147483646)

Best regards,
Madhukar

Refactor bmct into a more convenient API

bmct and incremental_bmct can be easily used interchangeably in other BMC-based tools (like cegis)
most of that has already been done in the peter-incremental-unwinding branch

For goto-binaries, --show-reachable-properties always starts from main(), even if --function is given

Error on synchronization on objects in Java

This example fails with unexpected statement: monitorenter

public class monitorenter1
{
  public boolean doIt(boolean b)
  {
    boolean a;
    synchronized(this) {
      a = !b;
    }
    return a;
  }
  public void test()
  {
    assert(doIt(false));
  }
}

the critical section is enclosed between monitorenter and monitorexit in the bytecode.

smt2_conv does not handle update of objects with variable size

run for example with --unwind 2 --z3

array theory should be used, but "failed to get width of byte_update" is thrown

array index expressions are translated correctly for arrays of variable size

#include <assert.h>

unsigned nondet_unsigned();

int main() {
  unsigned n = nondet_unsigned();
  __CPROVER_assume(n>0);
//  unsigned p[n]; // (1)
  unsigned *p = (unsigned *)malloc(sizeof(unsigned) * n); // (2)

  for (int i=0; i<n; i++) {
    p[i] = i; // correctly translated for (1), error thrown for (2)
  }
  assert(p[n-1] == n-1);

  return 0;
}

byte_update is used for p[i] although the type of p in the goto program is array of size (const * variable). Couldn't an index expression be generated if the access is obviously aligned?

Non-deterministic left hand side in assignment with Java byte code

When analyzing Java bytecode, it is possible to get assignments with a nondet_symbol on the left hand side. For the following program:

public class nondetassign1
{
  class B
  {
    boolean a;
    B f()
    {
      this.a = true;
      return this;
    }
  }
  class A extends B
  {
    A f()
    {
      this.a = true;
      return this;
    }
    void g()
    {
      boolean b = this.a;
      boolean c = this.a;
      assert(b == c);
    }
  }
}

when one removes the nondetassign1\$B.class file, one gets the following result for cbmc --function "nondetassign1\$A.f:()Lnondetassign1\$A;" nondetassign1\$A.class:

assignment to 'nondet_symbol' not handled

this does work with the temporary fix as follows:

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index c75905f..a9323aa 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -235,6 +235,8 @@ void goto_symext::symex_assign_rec(

     symex_assign_rec(state, lhs.op0(), full_lhs, new_rhs, guard, assignment_type);
   }
+  else if(lhs.id() == ID_nondet_symbol)
+    return;
   else
     throw "assignment to `"+lhs.id_string()+"' not handled";
 }

in addition, the result for cbmc --function "nondetassign1\$A.g" nondetassign1\$A.class is:

** Results:
[assertion.1] assertion at file nondetassign1.java line 23: FAILURE

** 1 of 1 failed (1 iteration)
VERIFICATION FAILED

Would it be possible to treat such a variable in the following way:

create a variable $nondet1 and assign an initial NONDET value
allow assignments to this variable just as for other variables
assign a new NONDET value to it when the control flow leaves the current function, e.g., for a function call that might modify $nondet1 as side effect

Bug in cbmc's strchr implementation?

When built with gcc, this program runs and the assertion does not fire:

#include <string.h>
#include <assert.h>
int main() {
    char arr[] = { 'a', 'a', 'a', 0};
    assert(strchr(arr, 0) == arr + sizeof(arr) - 1);
}

However, cbmc 5.4 says that VERIFICATION FAILED:

CBMC version 5.4 64-bit x86_64 linux
Parsing strend.c
Converting
Type-checking strend
Generating GOTO Program
Adding CPROVER library (x86_64)
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop main.0 iteration 1 file strend.c line 5 function main thread 0
Unwinding loop main.0 iteration 2 file strend.c line 5 function main thread 0
Unwinding loop main.0 iteration 3 file strend.c line 5 function main thread 0
size of program expression: 60 steps
simple slicing removed 3 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
264 variables, 11 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.001s
Building error trace

Counterexample:

State 18 file strend.c line 4 function main thread 0
----------------------------------------------------
  arr={ 0, 0, 0, 0 } ({ 00000000, 00000000, 00000000, 00000000 })

State 19 file strend.c line 4 function main thread 0
----------------------------------------------------
  arr={ 'a', 'a', 'a', 0 } ({ 01100001, 01100001, 01100001, 00000000 })

Violated property:
  file strend.c line 5 function main
  assertion strchr(arr, 0) == arr + sizeof(arr) - 1
  return_value_strchr$1 == (arr + (signed long int)sizeof(char [4l]) /*4ul*/ ) - (signed long int)1

VERIFICATION FAILED

I think that the implementation of strchr (and probably strrchr, though I did not test it) is defective, because it ignores this statement from the C99 standard: "The terminating null character is considered to be part of the string." (7.21.5.2 in ISO/IEC 9899:TC3 Committee Draft WG14/N1256)

Problems loading some class files

For the class file of this source, CBMC fails on loading with the following assertion violation:

Converting
cbmc: java_bytecode_typecheck_expr.cpp:114: void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt&): Assertion `has_prefix(id2string(identifier), "java::")' failed.

The problem is the identifier `::ceil`` (line 49/50).