[feat] KValue base class #161
Conversation
S1eGa
force-pushed
the
kvalue
branch
3 times, most recently
from
004b273 to
c8e6394
Compare
Codecov Report
Additional details and impacted files@@ Coverage Diff @@
## main #161 +/- ##
==========================================
+ Coverage 67.66% 67.70% +0.04%
==========================================
Files 224 226 +2
Lines 31379 31491 +112
Branches 6888 6901 +13
==========================================
+ Hits 21233 21322 +89
- Misses 7536 7542 +6
- Partials 2610 2627 +17
|
S1eGa
force-pushed
the
kvalue
branch
7 times, most recently
from
894b8b8 to
a260f75
Compare
… llvm::* structures (KInstruction, KConstant, etc.) [feat] Model unsized globals as objects of symbolic size.
|
|
||
| namespace klee { | ||
|
|
||
| struct KValue { |
There was a problem hiding this comment.
Make KValue an abstract class.
lib/Expr/SymbolicSource.cpp
Outdated
| @@ -102,8 +103,11 @@ int SymbolicSizeConstantAddressSource::internalCompare( | |||
| return size < ub.size ? -1 : 1; | |||
| } | |||
| if (allocSite != ub.allocSite) { | |||
| return allocSite->getGlobalIndex() < ub.allocSite->getGlobalIndex() ? -1 | |||
| : 1; | |||
| if (allocSite->getKind() == ub.allocSite->getKind()) { | |||
There was a problem hiding this comment.
KVlaue comparisons must be made within this class.
lib/Module/KValue.cpp
Outdated
| @@ -0,0 +1,30 @@ | |||
| #include "klee/Support/CompilerWarning.h" | |||
| #include <klee/Module/KValue.h> | |||
include/klee/Module/KModule.h
Outdated
| @@ -84,6 +89,10 @@ struct KBlock { | |||
|
|
|||
| /// Block number in function | |||
| [[nodiscard]] uintptr_t getId() const; | |||
|
|
|||
| static bool classof(const KValue *rhs) { | |||
| return rhs->getKind() == Kind::BLOCK ? classof(cast<KBlock>(rhs)) : false; | |||
There was a problem hiding this comment.
Ternary operator -> &&
include/klee/Core/Context.h
Outdated
| @@ -40,6 +40,8 @@ class Context { | |||
|
|
|||
| /// Returns width of the pointer in bits | |||
| Expr::Width getPointerWidth() const { return PointerWidth; } | |||
|
|
|||
| Expr::Width getPointerWidthInBytes() const { return PointerWidth / CHAR_BIT; } | |||
There was a problem hiding this comment.
I don't think this is a good idea. A function taking an Expr::Width parameter will not know whether the width is in bits or bytes. There should be two types, Expr::BitWidth and Expr::ByteWidth with explicit conversions to each other.
lib/Solver/BitwuzlaSolver.cpp
Outdated
| @@ -771,7 +771,7 @@ class BitwuzlaIncNativeSolver { | |||
| Bitwuzla &getOrInit(); | |||
|
|
|||
| bool isConsistent() const { | |||
| klee_warning("Empty isConsistent() check"); | |||
| // klee_warning("Empty isConsistent() check"); | |||
There was a problem hiding this comment.
I think we should attach a comment to this function that will describe what kind of check is to be expected here in the future (or remove this function altogether).
lib/Expr/SourceBuilder.cpp
Outdated
| @@ -21,7 +22,7 @@ SourceBuilder::uninitialized(unsigned version, const KInstruction *allocSite) { | |||
| } | |||
|
|
|||
| ref<SymbolicSource> SourceBuilder::symbolicSizeConstantAddress( | |||
| unsigned version, const KInstruction *allocSite, ref<Expr> size) { | |||
| unsigned version, const KValue *allocSite, ref<Expr> size) { | |||
There was a problem hiding this comment.
We need some way to restrict allocSite to those types of KValue that make sense as alloc sites. At least make a comment somewhere describing accepted derivatives or make a set of constructors accepting those derivatives only.
…s factory method for instructions and global variables. Added consistency check in bitwuzla.
No description provided.