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

[john borland]

One issue that I run into from time to time is a negative number going into a square root.   The output of the square root of a negative number is typically a NaN.   I was of thinking of trying to add a check to the bug hunting analysis.   After taking a quick look at bughuntingchecks.cpp I thought I should check and see ifanyone thought the check was good idea or any advice for adding adding acheck to the bug hunting analysis would be greatly appreciated.

Thanks

[Daniel Marjamäki]

Sounds good to me! I assume you mean when using sqrt standard function.

There is configuration already in std.cfg that says that a negative input value is invalid.

There is bug hunting checking that check function calls based on configuration.. but it only handles integers right now it seems. Look in the function checkFunctionCall() below the comment // Check invalid function argument values...

Feel free to look into this.

[john borland]

Looking at std.cfg is the line <valid>0.0:</valid> the line that says the input value can't be negative.

  <!-- double sqrt(double x); -->
  <function name="sqrt,std::sqrt">
    <use-retval/>
    <pure/>
    <returnValue type="double"/>
    <noreturn>false</noreturn>
    <leak-ignore/>
    <arg nr="1" direction="in">
      <not-uninit/>
      <valid>0.0:</valid>
    </arg>
  </function>

[Daniel Marjamäki]

yes.

[john borland]

I was looking to use the cppcheck_low(x) and cppcheck_high(x) to test the bug hunting analysis on sqrt() function from the command line. I know I don't have the cppcheck_low setup right. Just using the example from the manual wouldn't compile and it didn't saying anything about it in the --bug-hunting

typedef __cppcheck_high__(100) unsigned int percent_t;percent_t x;
x = 110; 

Example code

/* sqrt example */
#include <stdio.h>      /* printf */
#include <stdlib.h>     /* atof */
#include <math.h>       /* sqrt */

int main(int argc, char* argv[])
{

  typedef __cppcheck_high__(100) unsigned int percent_t;
  percent_t x;
  x=110;

main.cpp: In function ‘int main(int, char**)’:
main.cpp:9:28: error: ISO C++ forbids declaration of ‘cppcheck_high’ with no type [-fpermissive]
typedef cppcheck_high(100) unsigned int percent_t;

How do I tell it about the types?

[Daniel Marjamäki]

I am confused. That example from the manual does not work well when I check it with cppcheck. I expected to get a warning from Cppcheck but I don't get it.

With this code:

void foo() {
    __cppcheck_high__(100) unsigned int x;
    x = 110;
}

I get this error:

1.c:6:9: error: There is assignment, cannot determine that value is lower or equal with 100 [bughuntingAssign]

When I use the typedef :

typedef __cppcheck_high__(100) unsigned int percent_t;

void foo() {
    percent_t x;
    x = 110;
}

I get no error. Not sure what I do wrong. I have the feeling this did work when I wrote the manual. If it does not work then I feel that it's a bug that should be fixed!

[Daniel Marjamäki]

Ah thanks. The manual should be clarified. There are a few solutions.. they can for instance be defined out during compilation. If you for instance have this somewhere then gcc should be happy:

#ifdef __GNUC__
#define __cppcheck_low__(X) 
#define __cppcheck_high__(X) 
#endif

I am not certain that everybody wants to put these specific cppcheck annotations __cppcheck_low__ and __cppcheck_high__ in their code. Maybe it's more interesting to define various user macros that expands into __cppcheck_low__ and __cppcheck_high__ i.e.:

#ifdef __cppcheck__
#define ValueRange(x,y) __cppcheck_low__(x) __cppcheck_high__(y)
#define ValueRangeLow(x) __cppcheck_low__(x)
#define ValueRangeHigh(x) __cppcheck_high__(x)
#else
#define ValueRange(x,y)
#define ValueRangeLow(x)
#define ValueRangeHigh(x)
#endif

With that code you just need to manually ensure that __cppcheck__ is defined during cppcheck analysis.

[john borland]

Yeah I can see most people wouldn't want to put tool specific macros in their code. At this point I'm just taking baby steps to figure out how it all works. It compiles now but I don't see comping about it in the bug hunting check. The only thing the bug hunting finds is

Checking main.cpp ...
main.cpp:17:23: error: Cannot determine that 'argv[1]' is initialized [bughuntingUninit]
  double a = atof(argv[1]);
                      ^
main.cpp:18:23: error: Cannot determine that 'argv[2]' is initialized [bughuntingUninit]
  double b = atof(argv[2]);
                      ^
nofile:0:0: information: Cppcheck cannot find all the include files (use --check-config for details) [missingIncludeSystem]

[john borland]

I was wondering if maybe there was an issue with the way I built cppcheck. Below is my cmake output. This is the first time I'm looking into using the bugging hunting option.

-- The C compiler identification is GNU 9.3.1
-- The CXX compiler identification is GNU 9.3.1
-- Check for working C compiler: /opt/rh/devtoolset-9/root/usr/bin/cc
-- Check for working C compiler: /opt/rh/devtoolset-9/root/usr/bin/cc - works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- Check for working CXX compiler: /opt/rh/devtoolset-9/root/usr/bin/c++
-- Check for working CXX compiler: /opt/rh/devtoolset-9/root/usr/bin/c++ - works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Found PythonInterp: /usr/bin/python (found version "2.7.5")
-- ------------------ General configuration for Cppcheck 2.2 -----------------
--
-- CMake Generator =       Unix Makefiles
-- Compiler =              GNU
-- Compiler Version =      9.3.1
-- Build type =            Release
-- CMAKE_INSTALL_PREFIX =  /usr/local
-- CMAKE_DISABLE_PRECOMPILE_HEADERS = On
-- C++ flags (General) =
-- C++ flags (Release) =   -O2 -DNDEBUG
-- C++ flags (RelWithDebInfo) = -O2 -g -DNDEBUG
-- C++ flags (Debug) =     -g
-- Found Define: FILESDIR="/users/jborland/opt/SL7/CppCheck/cppcheck_v2.2_blt_9.3.1/usr/local/share/Cppcheck/"
--
-- ---------------------------------------------------------
-- ANALYZE_MEMORY =        OFF
-- ANALYZE_ADDRESS =       OFF
-- ANALYZE_THREAD =        OFF
-- ANALYZE_UNDEFINED =     OFF
-- ANALYZE_DATAFLOW =      OFF
-- WARNINGS_ARE_ERRORS =   OFF
--
-- USE_MATCHCOMPILER =     ON
-- USE_MATCHCOMPILER_OPT = ON
--
-- BUILD_SHARED_LIBS =     OFF
-- BUILD_TESTS =           OFF
-- ENABLE_CHECK_INTERNAL = OFF
-- ENABLE_OSS_FUZZ =       ON
--
-- BUILD_GUI =             OFF
-- WITH_QCHART =           OFF
--
-- HAVE_RULES =            OFF
--
-- USE_Z3 =                OFF
--
-- CLANG_TIDY=CLANG_TIDY-NOTFOUND
-- Configuring done
-- Generating done
-- Build files have been written to: /users/jborland/opt/SL7/CppCheck/cppcheck-2.2/build

[john borland]

I'm thinking my problem is when I build it
-- USE_Z3 = OFF
Sine Z3 is used in the bug hunting analysis?

[Daniel Marjamäki]

Yes.. USE_Z3 should be ON.

I would not use matchcompiler during development. I have the feeling that will complicate the debugging.

[john borland]

I was able to get it to build with z3 now. It now detects the range violations on integers. I guess I was wondering where would be the best place to look to get it to try and look into range violations on floats?

Below is the example I am toying with .

/* sqrt example */
#include <stdio.h>      /* printf */
#include <stdlib.h>     /* atof */
#include <math.h>       /* sqrt */
#include <float.h>      /* DBL_MIN */

#ifdef __GNUC__
#define __cppcheck_low__(X)
#define __cppcheck_high__(X)
#endif

#define ValueRange(x,y) __cppcheck_low__(x) __cppcheck_high__(y)
#define ValueRangeLow(x) __cppcheck_low__(x)
#define ValueRangeHigh(x) __cppcheck_high__(x)

int main(int argc, char* argv[])
{

  ValueRangeHigh(100) unsigned int x;
  x=110;
  ValueRangeHigh(100) double doubleHighTest;
  doubleHighTest = 1100.1;

  double input = atof(argv[1]);
  double fixed = 1000.4501;

  printf ("input:%f\n", input);
  double number01, number02, result;

  result = sqrt(fixed);
  printf ("fixed sqrt(%f) = %f\n", fixed, result );

  result = sqrt(input);
  printf ("raw sqrt(%f) = %f\n", input, result );

  if( input > DBL_MIN)
  {
     result = sqrt(input);
     printf ("if protected sqrt(%f) = %f\n", input, result );
  }

  if( !(signbit(input)) )
  {
     result = sqrt(input);
     printf ("if signbit protected sqrt(%f) = %f\n", input, result );
  }

  result = sqrt(fabs(input));
  printf ("abs protected sqrt(%f) = %f\n", fabs(input), result );

  number01 = 16.0001 - input;
  result = sqrt(number01);
  printf ("sub of input sqrt(%f) = %f\n", number01, result );

  return 0;
}

[Daniel Marjamäki]

If you want to check sqrt I think this is a good start:

void foo(float f) {
    if (f > 0.0)
          sqrt(f);
    sqrt(f); // <- WARNING
}

We have code that will check integer values here:
https://github.com/danmar/cppcheck/blob/2a05bc565d/lib/bughuntingchecks.cpp#L576

We need to tweak that code so it works for floats also.

[Daniel Marjamäki]

It seems the problem right now for my example code is that we get false positives.

sqrt.c:3:16: error: There is function call, cannot determine that 1st argument value is valid. Bad value: less than 0.0 [bughuntingInvalidArgValue]
          sqrt(f);
               ^
sqrt.c:4:10: error: There is function call, cannot determine that 1st argument value is valid. Bad value: less than 0.0 [bughuntingInvalidArgValue]
    sqrt(f); // <- WARNING
         ^

In this code I do not want that "err" is set to true for the first function call: https://github.com/danmar/cppcheck/blob/2a05bc565d/lib/bughuntingchecks.cpp#L592

If you want to investigate why "err" will be true for the first function call feel free to do it.

[john borland]

Yeah I think starting with the false positives with the sqrt function where the best place to start.

[john borland]

I'm using cppcheck-2.3 and z3-4.8.9
It looks like z3: ast is not an expression is coming out of the catch statement in exprengine.cpp:1350

1342     try {
1343         z3::expr e = exprData.addFloat(name);
1344         for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
1345             solver.add(exprData.getConstraintExpr(constraint));
1346         exprData.addAssertions(solver);
1347         solver.add(e < value);  <<<GOES IN HERE
1348         return solver.check() == z3::sat;
1349     } catch (const z3::exception &exception) {
1350         std::cerr << "z3: " << exception << std::endl <<<OUT HERE
1351         return true;  // Safe option is to return true
1352     }

(gdb) print* constraint
$3 = (std::__shared_ptr_access<ExprEngine::Value, (__gnu_cxx::_Lock_policy)2, false, false>::element_type &) @0x1156c90: {_vptr.Value = 0xefc068 <vtable for ExprEngine::BinOpResult+16>, name = "($5)>(0.0)", type = ExprEngine::BinOpResult}

It looks like because it can't solve for what "$5" is it is throwing an exception out of the solver.add call. Any ideas?

[Georgiy Komarov]

Could you provide a minimal example that demonstrates this problem?

[john borland]

/* sqrt example */
#include <stdio.h>      /* printf */
#include <stdlib.h>     /* atof */
#include <math.h>       /* sqrt */

int main(int argc, char* argv[])
{
  double input = atof(argv[1]);
  double result;

  if( input > 0.00 )
  {
     result = sqrt(input);
     printf ("if > 0.0 sqrt(%f) = %f\n", input, result );
  }

  return 0;
}

[Daniel Marjamäki]

A more trivial code example is:

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

please use latest cppcheck-head it's hard to read the code when your code differs to what I see.

we have fixed a number of problems also .. so it would be unfortunate if you have some problem that we already fixed.

The code in ExprEngine::FloatRange::isLessThan is:

    z3::expr e = exprData.addFloat(name);
    exprData.addConstraints(solver, data);
    exprData.addAssertions(solver);
    solver.add(e < value);
    std::cout << solver << std::endl; // <- Please add this
    return solver.check() == z3::sat;

I can see that some exception is thrown but I can't personally see what exception it is.. :-(

I am not sure how to interpret the z3: ast is not an expression expression that you get.

The std::cout prints this output for me:

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

I believe the first line declares a z3 symbol with the name |0.0| .. I am not sure why we do that right here.

Not sure.. but maybe the proper output should say this instead:

(declare-fun $1 () Real)
(assert (> $1 0.0))
(assert (< $1 0.0))

[Daniel Marjamäki]

You can test the z3 expressions on the command line.

Put this in a file 1.z3:

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

Then run this command:

$z3 1.z3

It will say unsat.

I have the feeling an assertion is missing in the std::cout output that ensures that |0.0| is equal to 0.0.

[Georgiy Komarov]

It seems that I get stuck with something very similar in PR2956. I'm trying to add "null" values for string and float literals. This is necessary to handle them inside the condition statements. Something like this:

void foo() {
   const char *foo = "test\0";
   if (foo) {}
   if (0.0) {}
}

But now I get strange results in my tests for generated z3 expressions.

For example, the following snippet (test ifAlwaysFalse3) does not generate z3 expression at all:

int foo() {
  int a = 42;
  if (0.0) {
    a = 0;
  }
  return a == 0;
}

But it seems that it works correct for me, because it gives the following debug output:

2:13: 0:memory:{a=42}
3:3: 0: Split. Then:0 Else:1
5:3: 1:memory:{a=42} constraints:{(0.0)==(0.0)}
ok  int a ; a = 42 ;
ok  if ( 0.0 ) {
ok  a = 0 ;
ok  }
ok  return a == 0 ;

[Daniel Marjamäki]

But it seems that it works correct for me, because it gives the following debug output:

hmm strange. maybe there is something bad with the unit test framework.

For information.. I am guessing that the constraint can be tweaked in that debug output, I'd guess this is false too: if (0.7).

[Daniel Marjamäki]

For example, the following snippet (test ifAlwaysFalse3) does not generate z3 expression at all:

what is your test code for that? The second operand for expr(code,binop) should be a binary operator token (in cppcheck ast, not z3 expression).

[Georgiy Komarov]

It is currently marked here as TODO_ASSERT_EQUALS:

int foo() {
  int a = 42;
  if (0.0) {
    a = 0;
  }
  return a == 0;
}

According to debug output, there is no binary operator token in cppcheck AST:

##AST
[ifAlwaysFalse.cpp:2]
= 'signed int'
|-a 'signed int'
`-42 'signed int'

[ifAlwaysFalse.cpp:3]
(
|-if
`-0.0 'double'

[ifAlwaysFalse.cpp:4]
= 'signed int'
|-a 'signed int'
`-0 'signed int'

[ifAlwaysFalse.cpp:6]
return 'signed int'
`-== 'bool'
  |-a 'signed int'
  `-0 'signed int'

[john borland]

I added the cout, but my code doesn't get to it. So I added a cout before the solver.add line which shows up in my output.

I'm currently pointing at

commit 0b980537906ede57b632d138017b265698123a1a
Author: Daniel Marjamäki <daniel.marjamaki@gmail.com>
Date:   Thu Dec 17 15:29:15 2020 +0100

    Fixed Cppcheck warning; Redundant assignment

I changed the code to look like this

    try {
        z3::expr e = exprData.addFloat(name);
        exprData.addConstraints(solver, data);
        exprData.addAssertions(solver);
        std::cout << "Before solver.add" << std::endl;
        solver.add(e < value);
        std::cout << solver << std::endl;
        return solver.check() == z3::sat;
    } catch (const z3::exception &exception) {
        std::cerr << "z3: " << exception << std::endl;
        return true;  // Safe option is to return true
    } catch (const ExprData::BailoutValueException &) {
        return true;  // Safe option is to return true
    } catch (const ExprEngineException &) {
        return true;  // Safe option is to return true
    }
#else
    // The value may or may not be in range
    return false;
#endif
}

This is what my output looks like

$ ./cppcheck --bug-hunting littlest.cpp
Checking littlest.cpp ...
Before solver.add
z3: ast is not an expression
littlest.cpp:3:16: error: There is function call, cannot determine that 1st argument value is valid. Bad value: less than 0.0 [bughuntingInvalidArgValue]
          sqrt(f);
               ^

littlest.cpp Looks like this

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

I'm using z3 version 4.8.9 If I actually recompile my version of z3 with debug on it segfaults on the solve.add call.

Below is part of the stack trace

Checking littlest.cpp ...
Before solver.add

Program received signal SIGSEGV, Segmentation fault.
0x00007ffff63c1530 in ast::hash (this=0x0) at /BuildTest/z3/src/ast/ast.h:501
501         unsigned hash() const { return m_hash; }
Missing separate debuginfos, use: debuginfo-install glibc-2.17-317.el7.x86_64 libgcc-4.8.5-44.el7.x86_64 libstdc++-4.8.5-44.el7.x86_64
(gdb) where
#0  0x00007ffff63c1530 in ast::hash (this=0x0) at /BuildTest/z3/src/ast/ast.h:501
#1  0x00007ffff63f8098 in obj_ptr_hash<ast>::operator() (this=0x14530b8, a=0x0) at /BuildTest/z3/src/util/hash.h:168
#2  0x00007ffff63f3c6e in chashtable<ast*, obj_ptr_hash<ast>, ast_eq_proc>::get_hash (this=0x14530b8, d=@0x7fffffff7d10: 0x0)
    at /BuildTest/z3/src/util/chashtable.h:77
#3  0x00007ffff63eeffe in chashtable<ast*, obj_ptr_hash<ast>, ast_eq_proc>::contains (this=0x14530b8, d=@0x7fffffff7d10: 0x0)
    at /BuildTest/z3/src/util/chashtable.h:423
#4  0x00007ffff642134e in ast_manager::contains (this=0x1452dc8, a=0x0) at /BuildTest/z3/src/ast/ast.h:1669
#5  0x00007ffff76f6988 in api::context::save_ast_trail (this=0x13d6288, n=0x0) at /BuildTest/z3/src/api/api_context.cpp:222
#6  0x00007ffff76f68b1 in api::context::mk_numeral_core (this=0x13d6288, n=..., s=0x1170368) at /BuildTest/z3/src/api/api_context.cpp:202
#7  0x00007ffff7714fb6 in Z3_mk_int (c=0x13d6288, value=0, ty=0x1170368) at /BuildTest/z3/src/api/api_numeral.cpp:102
#8  0x0000000000bec591 in z3::context::num_val (this=0x7fffffff7f30, n=0, s=...) at /BuildTest/opt/usr/local/include/z3++.h:3216
#9  0x0000000000beb76b in z3::operator< (a=..., b=0) at /BuildTest/opt/usr/local/include/z3++.h:1662
#10 0x0000000000bd7290 in ExprEngine::FloatRange::isLessThan (this=0x1165030, dataBase=0x7fffffffa2c0, value=0)
    at /BuildTest/cppcheck/lib/exprengine.cpp:1449
#11 0x0000000000a30426 in checkFunctionCall (tok=0x1162a80, value=..., dataBase=0x7fffffffa2c0) at /BuildTest/cppcheck/lib/bughuntingchecks.cpp:592

The ASSERT it is tripping on is in /BuildTest/z3/src/api/api_context.cpp:222

~~~

void context::save_ast_trail(ast * n) {
    SASSERT(m().contains(n));
    if (m_user_ref_count) {
        // Corner case bug: n may be in m_last_result, and this is the only reference to n.
        // When, we execute reset() it is deleted
        // To avoid this bug, I bump the reference counter before resetting m_last_result
        ast_ref node(n, m());
        m_last_result.reset();
        m_last_result.push_back(std::move(node));
    }
    else {
        m_ast_trail.push_back(n);
    }
}

~~~
What version of z3 are you using?