search

ftsrg / gazer

An LLVM-based formal verification frontend for C programs.
24 stars 5 forks source link

Target type and integer cast error on several tasks #52

Closed AdamZsofi closed 4 years ago

AdamZsofi commented 4 years ago

Describe the bug Gazer is unable to produce test harnesses on several SSH SVComp tasks. Fails on the following assert: gazer/src/LLVM/Trace/TestHarnessGenerator.cpp:32: llvm::Constant* exprToLLVMValue(gazer::ExprRef<gazer::AtomicExpr>&, llvm::LLVMContext&, llvm::Type*): Assertion targetTy->isIntegerTy() || (!expr->getType().isBvType() && !expr->getType().isIntType() && !expr->getType().isBoolType()) && "Bitvectors, integers, and booleans may only have integer as their target type!"' failed.

When using --no-optimize with the same command the run fails earlier when generating the CFA with an Invalid integer cast type!

Output from both: no-optimize-output.txt test_harness_output.txt

My only guess is that it has to do something with really big unsigned integer values, as those are frequently used in these tasks.

To Reproduce Run gazer/tools/gazer-theta/gazer-theta --inline all --search ERR --domain PRED_CART --refinement BW_BIN_ITP --initprec EMPTY --trace -test-harness=s3_clnt.blast.01.i.cil-2.c.ll sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c using this task. (Take into account, that the sv-benchmarks repo is huge, so cloning it only for this task might not be practical.)

Expected behavior Generating a test harness.

Version: Gazer master branch, Theta 2.5

Additional context I only included one example, but this happens with most of these tasks and with tasks from other sets as well.

AdamZsofi commented 4 years ago

In the no-optimize case the "Invalid integer cast type!" comes from here. The expectedType is Int, but cast.getOpcode() returns llvm::Instruction::PtrToInt. There really are some mallocs and pointers in the task. How can it be, that it seems to work without --no-optimize? Does Gazer support pointers to any extent?

sallaigy commented 4 years ago

The counterexample is quite likely a false-positive. We currently do not support dynamic memory, so malloc is currently not supported either. Pointers are supported through the bit-precise flat memory model, however it is disabled if -math-int is enabled and the havoc memory model takes its place. The -no-optimize version works fine if the chosen memory model is the flat one.

Nevertheless, the issue probably comes from the fact that while we support pointers in the verification phase, currently there is no support for them in the test harness generator.

AdamZsofi commented 4 years ago

Thanks for the heads up! Yes, I validated the generated witness with CPAChecker and it seems like a false counterexample, so I'll close this now. There is probably no bug here, only lots of opportunities for future enhancements.