error: unsupported llvm instruction fneg

[ingoahrns]

Hi,

I have got a strange behaviour of the ikos analyzer with the following C++ class of a simple vector.
I get the error:

> ikos vector.cpp 
[*] Compiling vector.cpp
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
ikos-analyzer: /tmp/ikos-5o9i8j4_/vector.pp.bc: error: unsupported llvm instruction fneg [2]
ikos: error: a run-time error occurred

However, if I change the line

vector.m_vector[i] = -m_vector[i];      // This doesn't !

into

vector.m_vector[i] = 0.-m_vector[i];  // This works

everything works fine. I also got similar behaviours with other expressions using the binary "-" operator when self-defined classes are involved...

any help would be really appreciated.

Here comes an extract of my sample program vector.cpp

KR

Ingo

#define VEC_MAX_DIM 10

namespace linmath 
{
    typedef float        TLMFloat;
    typedef unsigned int TLMUInt;
    
    class CVector 
    {
    public:
        CVector(TLMUInt dimension=1,TLMFloat value=0.) noexcept;
        CVector operator- () const;

    protected:
        // Vector dimension
        TLMUInt m_dimension;
        // Storage to store the vector elements
        TLMFloat m_vector[VEC_MAX_DIM];
    };
    
CVector::CVector(TLMUInt dimension,TLMFloat value) noexcept
{
    m_dimension = dimension;
    for (TLMUInt i=0;i<dimension;i++)
    {
        m_vector[i] = value;
    }    
}

CVector CVector::operator-() const
{
    CVector vector(m_dimension);
    for (TLMUInt i=0;i<m_dimension;i++)
    {
//        vector.m_vector[i] = 0.-m_vector[i];  // This works
        vector.m_vector[i] = -m_vector[i];      // This doesn't !
    }    
    return vector;
}

}; 

int main(int argc,char **argv=0)
{
    return 0;
}

[phoon0416]

i think the following patch can solve this issue, but i have no idea about whether it is the best way to solve it

diff --git a/frontend/llvm/src/import/function.cpp b/frontend/llvm/src/import/function.cpp
index a09ffb8..9c3d7f4 100644
--- a/frontend/llvm/src/import/function.cpp
+++ b/frontend/llvm/src/import/function.cpp
@@ -375,6 +375,13 @@ void FunctionImporter::translate_instruction(
   } else if (llvm::isa< llvm::SwitchInst >(inst)) {
     // The preprocessor should use the -lowerswitch pass
     throw ImportError("llvm switch instructions are not supported");
+  } else if (inst->getOpcode() == llvm::Instruction::FNeg) {
+       auto* binary_inst = llvm::BinaryOperator::Create(llvm::BinaryOperator::FSub,
+                       llvm::ConstantFP::getNegativeZero(inst->getOperand(0)->getType()),
+                       inst->getOperand(0));
+       inst->replaceAllUsesWith(binary_inst);
+       binary_inst->setDebugLoc(inst->getDebugLoc());
+       this->translate_binary_operator(bb_translation, binary_inst);
   } else {
     std::ostringstream buf;
     buf << "unsupported llvm instruction: " << inst->getOpcodeName() << " [1]";
@@ -2019,6 +2026,10 @@ FunctionImporter::TypeHint FunctionImporter::infer_type_hint_use(
     return {}; // no hint
   } else if (llvm::isa< llvm::ResumeInst >(user)) {
     return {}; // no hint
+  } else if (llvm::isa< llvm::Instruction >(user) 
+                 && llvm::cast< llvm::Instruction >(user)->getOpcode() == 
+                 llvm::Instruction::FNeg) {
+    return {}; // no hint
   } else if (llvm::isa< llvm::SelectInst >(user)) {
     // The preprocessor should use the -lower-select pass
     throw ImportError("llvm select instructions are not supported");

[ivanperez-keera]

I can replicate this in the catch2 tests including in the debian/ubuntu package.

[PhilipBotha]

From the LLVM Language reference manual

The value produced is a copy of the operand with its sign bit flipped. The value is otherwise completely identical; in particular, if the input is a NaN, then the quiet/signaling bit and payload are perfectly preserved.

Using compiler explorer to test:
Using (-0.0) - NaN does not flip the bit. Same with -1.0 * NaN. -NaN does flip the bit.

FNeg just seems to toggle the sign bit in the floating point while preserving the rest of the bits. Not sure if it is important to conserve that behaviour. Would probably be ideal.

[PavloVlastos]

I tried to implement this patch previously and found this error: "ikos: error: exited with signal SIGIOT". I'm on RHEL 8.9, I ran ikos-scan on a small project written in C called svs-sim. Here's the output:

[red@localhost svs-sim]$ make clean 
rm -rf obj bin *.o
[red@localhost svs-sim]$ ikos-scan make
ikos-scan-cc -std=c11 -O2 -Wall -I./modules -I./modules/common -I./modules/interface -I./modules/lin_alg -I./modules/model -I./modules/controller -I./modules/plan -c -o obj/main.o main.c
main.c:33:12: warning: unused variable 'n_bytes' [-Wunused-variable]
    size_t n_bytes = 0;
           ^
main.c:294:13: warning: unused function 'getFileSize' [-Wunused-function]
static long getFileSize(const char *filename)
            ^
2 warnings generated.
main.c:33:12: warning: unused variable 'n_bytes' [-Wunused-variable]
    size_t n_bytes = 0;
           ^
main.c:294:13: warning: unused function 'getFileSize' [-Wunused-function]
static long getFileSize(const char *filename)
            ^
2 warnings generated.
ikos-scan-cc -std=c11 -O2 -Wall -I./modules -I./modules/common -I./modules/interface -I./modules/lin_alg -I./modules/model -I./modules/controller -I./modules/plan -c -o obj/modules/controller/controller.o modules/controller/controller.c
ikos-scan-cc -std=c11 -O2 -Wall -I./modules -I./modules/common -I./modules/interface -I./modules/lin_alg -I./modules/model -I./modules/controller -I./modules/plan -c -o obj/modules/model/model.o modules/model/model.c
ikos-scan-cc -std=c11 -O2 -Wall -I./modules -I./modules/common -I./modules/interface -I./modules/lin_alg -I./modules/model -I./modules/controller -I./modules/plan -c -o obj/modules/interface/interface.o modules/interface/interface.c
ikos-scan-cc -std=c11 -O2 -Wall -I./modules -I./modules/common -I./modules/interface -I./modules/lin_alg -I./modules/model -I./modules/controller -I./modules/plan -c -o obj/modules/lin_alg/lin_alg.o modules/lin_alg/lin_alg.c
ikos-scan-cc -std=c11 -O2 -Wall -I./modules -I./modules/common -I./modules/interface -I./modules/lin_alg -I./modules/model -I./modules/controller -I./modules/plan -c -o obj/modules/common/common.o modules/common/common.c
ikos-scan-cc -std=c11 -O2 -Wall -I./modules -I./modules/common -I./modules/interface -I./modules/lin_alg -I./modules/model -I./modules/controller -I./modules/plan -L/opt/rh/gcc-toolset-10/root/usr/lib/gcc/x86_64-redhat-linux/10 -lm -o bin/svs-sim obj/main.o obj/modules/controller/controller.o obj/modules/model/model.o obj/modules/interface/interface.o obj/modules/lin_alg/lin_alg.o obj/modules/common/common.o
Analyze bin/svs-sim? [Y/n] Y
[*] Running ikos bin/svs-sim.bc -o bin/svs-sim.db
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'
While deleting: float %angle_rudder.1
Use still stuck around after Def is destroyed:  <badref> = fsub float -0.000000e+00, %angle_rudder.1, !dbg !DILocation(line: 100, column: 12, scope: <0x21fef90>)
ikos-analyzer: /home/red/llvm-project/llvm/lib/IR/Value.cpp:100: llvm::Value::~Value(): Assertion `materialized_use_empty() && "Uses remain when a value is destroyed!"' failed.
PLEASE submit a bug report to https://github.com/llvm/llvm-project/issues/ and include the crash backtrace.
Stack dump:
0.      Program arguments: /home/red/ikos/install/bin/ikos-analyzer -a=fca,dfa,sio,dbz,shc,dbg,uva,pcmp,prover,boa,dca,sound,nullity -d=interval -entry-points=main -globals-init=skip-big-arrays -proc=inter -j=1 -widening-strategy=widen -widening-delay=1 -widening-period=1 -narrowing-strategy=narrow -allow-dbg-mismatch -display-checks=no -display-inv=no -log=info -progress=auto /tmp/ikos-bgj64vl3/svs-sim.pp.bc -o bin/svs-sim.db
 #0 0x0000000000a3be0f PrintStackTraceSignalHandler(void*) Signals.cpp:0:0
 #1 0x0000000000a3959e SignalHandler(int) Signals.cpp:0:0
 #2 0x00007f44cfc63d20 __restore_rt (/lib64/libpthread.so.0+0x12d20)
 #3 0x00007f44cef9a52f raise (/lib64/libc.so.6+0x4e52f)
 #4 0x00007f44cef6de65 abort (/lib64/libc.so.6+0x21e65)
 #5 0x00007f44cef6dd39 _nl_load_domain.cold.0 (/lib64/libc.so.6+0x21d39)
 #6 0x00007f44cef92e86 (/lib64/libc.so.6+0x46e86)
 #7 0x00000000008a3980 llvm::Value::~Value() (/home/red/ikos/install/bin/ikos-analyzer+0x8a3980)
 #8 0x00000000008a39f2 llvm::Value::deleteValue() (/home/red/ikos/install/bin/ikos-analyzer+0x8a39f2)
 #9 0x00000000007b8474 llvm::BasicBlock::~BasicBlock() (/home/red/ikos/install/bin/ikos-analyzer+0x7b8474)
#10 0x00000000007b9d01 llvm::BasicBlock::eraseFromParent() (/home/red/ikos/install/bin/ikos-analyzer+0x7b9d01)
#11 0x00000000008075e6 llvm::Function::dropAllReferences() (/home/red/ikos/install/bin/ikos-analyzer+0x8075e6)
#12 0x000000000087ee8b llvm::Module::dropAllReferences() (/home/red/ikos/install/bin/ikos-analyzer+0x87ee8b)
#13 0x000000000087f088 llvm::Module::~Module() (/home/red/ikos/install/bin/ikos-analyzer+0x87f088)
#14 0x000000000042f727 main (/home/red/ikos/install/bin/ikos-analyzer+0x42f727)
#15 0x00007f44cef867e5 __libc_start_main (/lib64/libc.so.6+0x3a7e5)
#16 0x00000000004340ae _start (/home/red/ikos/install/bin/ikos-analyzer+0x4340ae)
ikos: error: exited with signal SIGIOT

[PavloVlastos]

Quick update to this, I was able to partially isolate the issue, I made two small c programs, one uses math.h and one does not. I have identical makefiles for both c programs. When I call ikos-scan on the makefile associated with the c program that uses math.h and subsequent functions like "tanf()" ikos-scan outputs the ikos SIGIOT error above. I'm assuming this is likely a linking issue in the makefile, or something like that, but still not sure. At least, I can confirm that the patch mentioned earlier does in fact work, assuming proper linkage in the makefile. Still running some tests however.

[PavloVlastos]

It looks like this patch does not address all edge cases. It will get rid of the fneg error, but can cause issues with llvm later on. I had a similar issue in which a - sign placed in front of a variable would result in the llvm error I posted above. Replacing - with (-1.0)* fixed that issue.

I was incorrect about my makefile being at fault. My apologies.

[ivanperez-keera]

Thanks for checking all of this!!!

[ivanperez-keera]

Unfortunately, there's no equivalent for integers that we can base this patch on, since the LLVM BC produced when an integer is negated is just subtracting from zero. For floats, however, LLVM does use a dedicated instruction fneg.

When llvm compiles this to object code, is just does an xorl with 2147483648 (which is, it bits, 1 << 31).

As for modeling the behavior in ikos, I wonder if we'll need to introduce a new function that each abstract domain implements, since the actual meaning will depend on the type of the element, the abstract value, and the abstract domain (somewhere in core/include/ikos/core/domain/).

[ivanperez-keera]

@arthaud This issue has come up a few times, so I would not mind getting rid of it for the next release of IKOS. Let me know if you have any thoughts or initial pointers.

[PhilipBotha]

When llvm compiles this to object code, is just does an xorl with 2147483648 (which is, it bits, 1 << 31).

As for modeling the behavior in ikos, I wonder if we'll need to introduce a new function that each abstract domain implements, since the actual meaning will depend on the type of the element, the abstract value, and the abstract domain (somewhere in core/include/ikos/core/domain/).

The xor operation flips the sign bit of the IEEE-754 floating point number (MSB). Note that a double would be with 1U << 63. That is what the LLVM manual says fneg does.

1. Best solution would be to model the sign-flipping behaviour. Most likely with a new function.
2. Just use (-1.0)* as a temporary until the proper behaviour can be implemented. Probably the best interim solution.
3. Ignore the fneg LLVM instruction like what was done previously for all floating point operations.

For options 2 and 3, I'd recommend putting a warning message so that it isn't forgotten that the implementation is less than ideal. At present, I can't quite use iKos due to the fneg error and even just having option 3 would be beneficial.

Alas, I'm not smart enough to implement option 1 myself. Might be able to implement 2 & 3.

[ivanperez-keera]

Hi @PhilipBotha

Just use (-1.0)* as a temporary until the proper behaviour can be implemented. Probably the best interim solution.

In which cases is (-1.0)* different from changing the sign bit? I can only think of cases where the input is a form of Inf, a form of NaN or a form of zero. Are any of the current abstract domains able to capture Inf or NaN (positive or negative), or -0.0?

Alas, I'm not smart enough to implement option 1 myself. Might be able to implement 2 & 3.

I'd love it if you could contribute the solution we opt for :)

[PhilipBotha]

Greetings! @ivanperez-keera

In which cases is (-1.0)* different from changing the sign bit? I can only think of cases where the input is a form of Inf, a form of NaN or a form of zero.

I think (-1.0)* would only differ from fneg for the case of a NaN.

Are any of the current abstract domains able to capture Inf or NaN (positive or negative), or -0.0?

There is some work on Inf and NaNs, but more in the sense of detecting their occurrence. I think the (-1.0)* operation would suffice for this use case. Only in cases where the semantics of the sign bit with respect to -NaNs would this be insufficient. Since (-1.0)*NaN is still a NaN and preserves all the bits, I don't see it as much of an issue. I think it would be sufficient to be able to detect the possibility of a Nan or Inf (like detecting overflow and divide by zero for integers ) and (-1.0*) does not negatively impact that from what I can surmise.

I'd love it if you could contribute the solution we opt for :)

Ha! So would I. Though don't hold your breath. This stuff is a bit (i.e. a lot) above my usual work.

[ivanperez-keera]

A first approximation could be similar to this, except that instead of $0 - x$, we translate it to $-1.0 * x$:

#197 (comment)

What is missing if we de-sugar it that way?

[PhilipBotha]

Yes, that is what I was thinking of using as well. Should be a good starting point.

[ivanperez-keera]

Ok. Well, if you want to send a draft/preliminary PR, we can help and see what else would need to change.

No pressure, and no rush, just let me know if there's something you want me to take a look at. It doesn't have to be perfect or even compile to start having a discussion on a PR :)

[PhilipBotha]

Good day all. Created a draft PR. Location and running of test cases needs work.