search

karelklic / canal

Abstract interpreter for real-world application programs
https://github.com/karelklic/canal/wiki
Other
32 stars 2 forks source link

Fix infinite loop in fixpoint calculation in seq #127

Closed xbrukner closed 11 years ago

xbrukner commented 11 years ago

Seq from coreutils compiles, but even after two minutes, fixpoint is not reached. http://www.fi.muni.cz/~xbrukner/integration/seq.c and http://www.fi.muni.cz/~xbrukner/integration/seq.s

xbrukner commented 11 years ago

Apparently, this only happens on 32 bit architecture; on 64 bits, it fails with:

/var/research/canal/canal/lib/Utils.h:152(dynCast) fatal error: std::bad_cast from N5Canal9StructureE to N5Canal7Integer9ContainerE
[bt]: (1) /var/research/canal/canal-build-31/lib/libcanal.so : Canal::Integer::Container const& Canal::dynCast<Canal::Integer::Container const&, Canal::Domain>(Canal::Domain const&)+0x8a [0x2b0d16810b29]
[bt]: (2) /var/research/canal/canal-build-31/lib/libcanal.so : Canal::Integer::Container::join(Canal::Domain const&)+0x33 [0x2b0d1680f681]
[bt]: (3) /var/research/canal/canal-build-31/lib/libcanal.so : Canal::StateMap::merge(Canal::StateMap const&)+0x14f [0x2b0d16841381]
[bt]: (4) /var/research/canal/canal-build-31/lib/libcanal.so : Canal::State::merge(Canal::State const&)+0x2b [0x2b0d1683e951]
[bt]: (5) /var/research/canal/canal-build-31/lib/libcanal.so : Canal::Interpreter::OperationsCallback::onFunctionCall(llvm::Function const&, Canal::State const&, Canal::State&, llvm::Value const&)+0x2f2 [0x2b0d16827780]
[bt]: (6) /var/research/canal/canal-build-31/lib/libcanal.so : void Canal::Operations::interpretCall<llvm::CallInst>(llvm::CallInst const&, Canal::State&)+0x3d5 [0x2b0d1682f4cd]
[bt]: (7) /var/research/canal/canal-build-31/lib/libcanal.so : Canal::Operations::call(llvm::CallInst const&, Canal::State&)+0x2b [0x2b0d1682c1df]
[bt]: (8) /var/research/canal/canal-build-31/lib/libcanal.so : Canal::Operations::interpretInstruction(llvm::Instruction const&, Canal::State&)+0x4b [0x2b0d1682798f]
[bt]: (9) /var/research/canal/canal-build-31/lib/libcanal.so : Canal::Interpreter::Iterator::interpretInstruction()+0x3e [0x2b0d16822cec]
[bt]: (10) /var/research/canal/canal-build-31/tool/canal : State::run()+0x36 [0x48fcba]
[bt]: (11) /var/research/canal/canal-build-31/tool/canal : CommandRun::run(std::vector<std::string, std::allocator<std::string> > const&)+0x86 [0x48732e]
[bt]: (12) /var/research/canal/canal-build-31/tool/canal : Commands::executeLine(std::string const&)+0x244 [0x488fe0]
[bt]: (13) /var/research/canal/canal-build-31/tool/canal : main+0x178 [0x470632]
[bt]: (14) /lib/libc.so.6 : __libc_start_main+0xfd [0x2b0d17c79c8d]
[bt]: (15) /var/research/canal/canal-build-31/tool/canal() [0x470089]
xbrukner commented 11 years ago

There is no widening for Float::Interval.