I was thinking about adding a square root check to the bug hunting analysis

[Daniel Marjamäki]

That is very interesting.. I use debian buster => z3-4.4.1

I could try to upgrade and see if I can reproduce your problems.. however I think you are debugging a somewhat different issue. I guess our code might not work well with latest z3 and we should fix that..

but then there is something missing in the z3 expressions also I believe that is different. I can look at that detail.

I wonder if you can run the expressions manually on the command line. I wonder if you can reproduce some exception on the command line.. then maybe you can try out some alternative fixed expressions more easily? Maybe something in the syntax needs to be changed.

[john borland]

I am able to run expressions on the command line. I ran the example bellow

(declare-fun |0.0| () Real)
(declare-fun $1 () Real)
(assert (= 0.0 |0.0|))
(assert (> $1 |0.0|))
(assert (< $1 0.0))
(check-sat)

It dose return unsat

$ ./z3 ./1.z3
unsat

This is my first time using z3. As of right now I can defiantly run any examples you all give me... I need to go spend a night or two reading about z3 syntax just to make sure I understand a few things. Just looking at it looks like it's in polish notation. But I just need to work through some examples.

[Daniel Marjamäki]

I can locally fix so it works for me. In the function z3::expr getExpr(ExprEngine::ValuePtr v) I do this:

old code:

        if (auto floatRange = std::dynamic_pointer_cast<ExprEngine::FloatRange>(v)) {
            auto it = valueExpr.find(v->name);
            if (it != valueExpr.end())
                return it->second;
            return addFloat(v->name);
        }

new code:

        if (auto floatRange = std::dynamic_pointer_cast<ExprEngine::FloatRange>(v)) {
            if (std::isdigit(floatRange->name[0]))
                return context.real_val(floatRange->name.c_str());

            auto it = valueExpr.find(v->name);
            if (it != valueExpr.end())
                return it->second;
            return addFloat(v->name);
        }

Now the false positive is gone for me. Note I use the old Z3.. this might not compile at all for you.. it would be interesting to know what happens for you..

[john borland]

I made the update.

$ ./cppcheck --bug-hunting ./littlest.cpp
Checking littlest.cpp ...
cppcheck: /BuildTest/opt/usr/local/include/z3++.h:1679: z3::expr z3::operator>(const z3::expr&, const z3::expr&): Assertion `false' failed.
Aborted (core dumped)

For me to see if the false positive goes away I will need to recompile the released version of z3. But looking at gdb that is coming from

~~~
z3::expr getExpr(const ExprEngine::BinOpResult *b) {
....
if (b->binop == ">")
return op1 > op2; <<< HERE

~~~

So it looks like I'm not even getting to ExprEngine::FloatRange::isLessThan any more.

[Daniel Marjamäki]

I pushed my fix.. so I wonder if you could get latest cppcheck and try it out.

So it looks like I'm not even getting to ExprEngine::FloatRange::isLessThan any more.

That is very confusing.

[Daniel Marjamäki]

I have installed ubuntu 20.10 with z3 4.8.8 on a VM.. I will experiment a bit with that..

[john borland]

Sure it will take me a little time before I'm back in front of my computer, but are there any other test you would like me to run while I'm set up?

[Daniel Marjamäki]

If you are more interested in the ValueRange then look in checkAssignment :
https://github.com/danmar/cppcheck/blob/2a05bc565d/lib/bughuntingchecks.cpp#L632

Feel free to fix that code to handle floats better.

[Daniel Marjamäki]

Sure it will take me a little time before I'm back in front of my computer, but are there any other test you would like me to run while I'm set up?

This is very tricky. I do not understand why we get the "z3: ast is not an expression" output! But I can also reproduce it when running ubuntu 20.10.

[Georgiy Komarov]

The easiest way to debug this is to print the generated expression using std::cout << solver; here.

The following code:

void foo(float f)
{
  if (f < 0.0)
    sqrt(f);
}

Gives me:

(declare-fun $1 () (_ FloatingPoint 11 53))
(assert (= (ite (fp.lt $1 (_ +zero 11 53)) 1 0) 0))

This is a correct z3 expression. It can be solved through z3 CLI utility. But for some reasons it gives me z3: ast is not an expression in C++ code. This is interesting, probably another bug in z3 API?

[Daniel Marjamäki]

I have been trying to debug the exception "ast is not an expression"....

For information; here is a minimal code (b2.c):

void foo(double input) {
  if( !signbit(input) )
  {
     sqrt(input);
  }
}

Cppcheck output for me (in ubuntu 20.10):

$ cppcheck --bug-hunting b2.c
Checking b2.c ...
(declare-fun $2 () Int)
(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))
(assert (= (ite (= $2 0) 1 0) 0))

z3: ast is not an expression

Here is the exception!!

The z3 expressions is a debug output I added in the BinaryResult::isEqual method.

This is an stripped down C++ code that should use the Z3 library in a very similar way as Cppcheck did:

#include <z3++.h>
#include <iostream>

z3::context context;

z3::expr notValue(z3::expr e) {
    return e == 0;
}

z3::expr int_expr(z3::expr e) {
    if (e.is_bool())
        return z3::ite(e, context.int_val(1), context.int_val(0));
    return e;
}

int main() {

    z3::solver solver(context);
    z3::expr e = context.int_const("$2");
    solver.add(e >= int(-2147483648) && e <= int(2147483647));
    solver.add(int_expr(notValue(e)) == 0);

    std::cout << solver << std::endl;

    try {
        std::cout << (solver.check() == z3::sat) << std::endl;
    } catch (const z3::exception &exception) {
        std::cout << "z3:" << exception << std::endl;
    }

    return 0;
}

When I compile and run that stripped down code I get no exception..

$ g++ -o test1 test1.cpp -lz3 && ./test1
(declare-fun $2 () Int)
(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))
(assert (= (ite (= $2 0) 1 0) 0))

1

The Z3 output is identical as far as I can tell.. so why doesn't it work in Cppcheck. Any wild guesses?

[john borland]

I'm still unable to get to my linux computer to test. Below is the rough version of a bash script I used on centos 7 to build cppcheck and z3. I know I have the devtoolset-9 installed.

git clone https://github.com/danmar/cppcheck.git  && cd cppcheck && git tag -l | tail -n 1 | xargs -n 1 -P 1 -I{} git checkout tags/{} -b {}                                                                                                                                                                                                                                                                                                                                                                               
   #Compare versions                                                                                                                                                                                                                                                            
   tagVer=`git rev-parse --abbrev-ref HEAD | awk -F / '{print $2;}'`                                                                                                                                                                                                           
   sysVer=`cppcheck --version | awk '{print $2;}'`                                                                                                                                                                                                                             

   #Build Cppcheck                                                                                                                                                                                                                                                             
   if (( $( echo "$tagVer > $sysVer" | bc -l ) )); then                                                                                                                                                                                                                        
       echo "We should build"                                                                                                                                                                                                                                                  
       source /opt/rh/devtoolset-9/enable                                                                                                                                                                                                                                      
       cd ../                                                                                                                                                                                                                                                                  
       git clone https://github.com/Z3Prover/z3.git                                                                                                                                                                                                                            
       cd z3                                                                                                                                                                                                                                                                   
       git checkout -b z3-4.8.9 tags/z3-4.8.9                                                                                                                                                                                                                                  
       #./configure --prefix=/BuildTest/opt/                                                                                                                                                                                                                    
       #cd ./build                                                                                                                                                                                                                                                             
       mkdir ./Build && cd ./Build                                                                                                                                                                                                                                             
       cmake3 -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release ../   >& cmake.out.out                                                                                                                                                                                            
       make -j 8                                                                                                                                                                                                                                                               
       make DESTDIR=../../opt install                                                                                                                                                                                                                                          
       export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/BuildTest/z3/Build/                                                                                                                                                                                             
       export PATH=$PATH:/BuildTest/opt/usr/local/lib64/cmake/z3/                                                                                                                                                                                               

       cd ../../                                                                                                                                                                                                                                                               
       cd ./cppcheck                                                                                                                                                                                                                                                           
       mkdir ./Build                                                                                                                                                                                                                                                           
       cd ./Build                                                                                                                                                                                                                                                              
       cmake3 -G "Unix Makefiles" -DUSE_Z3=YES -DUSE_MATCHCOMPILER=ON -DCMAKE_BUILD_TYPE=Release ../  >& cmake.out.out                                                                                                                                                         
       make -j 8                                                                                                                                                                                                                                                               
       make DESTDIR=../../opt install                                                                                                                                                                                                                                          
   fi

Does cppcheck get the exception with z3-4.4.1? When I get a chance it's not to hard for me to build other tagged versions of z3. I can always gdb into z3 and try and back solve from the exception.

[Georgiy Komarov]

Not sure about 4.4.1, but I get this exception with upstream z3 built from sources (commit *
28a6da4532c952a7077d233421aa498f5ca2ff59). The backtrace leads to check_error* call inside get_sort function for the result expression. I haven't looked deeper yet, but it seems, that something goes wrong in C part of z3 sources.

[Daniel Marjamäki]

I have figured out that Z3 does not like when float and int is mixed.

I don't know if a z3::expr that is int can be promoted to float. There is a "z3::to_real" but no "z3::to_fpa" as far as I see.

We need to tweak ExprData and that part somehow. But we also need to update inputs. If you write this code:

ValueRangeHigh(100) double doubleHighTest;

Then Cppcheck must convert that to a float somewhere! Right now the Cppcheck attribute is an int so it will not handle an upper limit 123.45 well..

[john borland]

One thing I was thinking might be useful is units. ValueUnit("miles per hour") It would allow for the possiblity of add maybe a limits file. So you can uses the speed of light or speed of sound for miles per hour. For temperatures you could use the melting point of tungsten. I could see this being useful for bug hunting in a use case where someone says my program should have no speeds faster than the speed of sound. It would make better constraints than max size of a double.

[Daniel Marjamäki]

I have also thought about defining units somehow. It sounds cool.

[john borland]

https://github.com/Unidata/UDUNITS-2

[Daniel Marjamäki]

what I have thought about is to detect mistakes.

for instance conversion mistakes:

    int milliseconds = 100; // [ms]
    int nanoseconds = milliseconds * 1000; // [ns]

or if we detect some arithmetic with incompatible units: expression1 [milliseconds] + expression2 [nanoseconds] we can warn about that too.

How the units for variables and constants should be defined.. I don't know.

[Daniel Marjamäki]

I think this addon will check for such mistakes: https://github.com/unl-nimbus-lab/phriky-units
it sounds very promising but I haven't looked at it closely.

[john borland]

That looks very interesting.

[john borland]

It is interesting the python and C API seem to have those type of functions.