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
| 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
| [[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
| /// 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
|
|
||
| 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
|
|
||
| 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.
4 participants
No description provided.