Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
76 commits
Select commit Hold shift + click to select a range
e3b0ff9
Adding only wp-interpolant check
rasoolmaghareh Apr 2, 2021
90e57c1
Undoing partitioning in TxWeakestPreCondition::updateSubsumptionTable…
rasoolmaghareh Apr 2, 2021
2eb4e39
Removed the first return statement from -getFunctionArgument()- funct…
sanghu1790 Apr 30, 2021
52a4e0a
Modified the TxWP.cpp by removing few return statements from function…
sanghu1790 May 7, 2021
a01477d
removed the changes done in return statement of function --getCmpCond…
sanghu1790 May 13, 2021
3d455a4
added a check in --getFunctionArgument(llvm::Argument *arg)-- funtion
sanghu1790 May 19, 2021
0e971cc
Print updates
sanghu1790 May 20, 2021
150d455
Function argument mapping
sanghu1790 Jun 8, 2021
1966a0f
.settings
ArpitaDutta Jun 8, 2021
3c2d669
nano.save
ArpitaDutta Jun 8, 2021
abaa839
Release+Asserts
ArpitaDutta Jun 8, 2021
386fb51
Release+Asserts files added
ArpitaDutta Jun 8, 2021
b08780c
Mapping of function arguments by checking their correct index value
ArpitaDutta Jun 10, 2021
d485876
updated supporting files
ArpitaDutta Jun 10, 2021
1afe28c
Assigning name to the unnamed llvm instructions with --TX_named_var--
ArpitaDutta Jun 23, 2021
c2a5949
Added some print statements
ArpitaDutta Jul 23, 2021
411178a
Adding back deletion interpolation and partitioning
rasoolmaghareh Sep 6, 2021
a227cbe
Deleted the file from the Debug+Assert
ArpitaDutta Sep 7, 2021
0b3f847
Deleted print statements
ArpitaDutta Sep 7, 2021
16301a3
Merge branch 'new-wpinterpolant' of https://github.com/tracer-x/klee …
ArpitaDutta Sep 7, 2021
96760b9
add updated files
ArpitaDutta Sep 7, 2021
8018301
Deleted Release+Assert folder
ArpitaDutta Sep 7, 2021
ecb7fc3
removed files from lib/core/Debug+Asserts and lib/Solver/Debug+Asserts
ArpitaDutta Sep 7, 2021
c8e051d
removed files from lib/Baisc/Debug+Asserts and lib/Baisc/Release+Asserts
ArpitaDutta Sep 7, 2021
1b7b72c
removed files from lib/Module/Debug+Asserts and lib/Module/Release+As…
ArpitaDutta Sep 7, 2021
dd56d89
removed files from lib/Core/Release+Assert/* and lib/Expr/Debug+Asser…
ArpitaDutta Sep 7, 2021
43f59fd
removed files from lib/Expr/Release+Asserts/*
ArpitaDutta Sep 7, 2021
372ba04
Deleted unwanted files
ArpitaDutta Sep 8, 2021
8731f59
removing build files
rasoolmaghareh Sep 12, 2021
71b5619
removing other unwanted files
rasoolmaghareh Sep 12, 2021
2bf7839
TimeInfo
ArpitaDutta Sep 14, 2021
0053b55
commenting few parts
ArpitaDutta Sep 22, 2021
2f68b8f
removing unwanted files
ArpitaDutta Sep 22, 2021
ec3d8dc
returning dummy variable for SEL expression
sanghu1790 Nov 29, 2021
917ea0d
returning dummy variable from 'TxWeakestPreCondition::getConstantExpr'
ArpitaDutta Jan 21, 2022
ed4449d
checking historical values
ArpitaDutta Mar 1, 2022
b42a943
Checking historical values
ArpitaDutta Mar 1, 2022
b4ed8f7
Checking historical values
ArpitaDutta Mar 1, 2022
be20653
Removed a few comments
ArpitaDutta May 18, 2022
6ac158a
Removed a few comments
sanghu1790 May 18, 2022
34c5f8e
Removed a few comments
sanghu1790 May 18, 2022
3be8bb9
Removed few comments
ArpitaDutta May 18, 2022
9ebc8e6
Commented few statements
ArpitaDutta May 18, 2022
2e9c887
Handled null dereferencing
ArpitaDutta May 23, 2022
ff5ddc1
Fixed division by zero error for SDiv kind Expr in instantiateWPatSub…
ArpitaDutta May 26, 2022
eae6fcb
Renamed interpolant to pi
ArpitaDutta Jun 10, 2022
8c27bd2
Added a check condition in Z3Simplification to avoid division-by-zero…
ArpitaDutta Jun 15, 2022
87bd0de
removed redundant statements
ArpitaDutta Jun 16, 2022
645fe12
Fixed getCondition
ArpitaDutta Jun 21, 2022
d696169
Mapped program point to its corresponding block data
ArpitaDutta Jun 21, 2022
54a059a
supporting trunc instruction in TxWeakestPreCondition::getCondition()
ArpitaDutta Jun 27, 2022
e328dd8
Fix in Partitioning for Global Variables
ArpitaDutta Jul 20, 2022
2579aef
Fixed Global Variable Partitioning
ArpitaDutta Jul 24, 2022
6831a10
Int64 support added for FunctionArgumentSize
ArpitaDutta Aug 24, 2022
6db7823
Int64 support added for getGlobalVariabletSize
ArpitaDutta Aug 25, 2022
08deff5
Int64 support added for getGepSize
ArpitaDutta Aug 25, 2022
bb51926
Fixed empty if statement warnings
ArpitaDutta Aug 25, 2022
7cc560b
Added array and pointer type support for getCastInst
ArpitaDutta Aug 25, 2022
44ebb0c
Fix in getFunctionArgument()
ArpitaDutta Sep 9, 2022
f3446cc
Checking the historical store
ArpitaDutta Oct 11, 2022
da405c7
commented the block info and other unwanted print statements
ArpitaDutta Nov 10, 2022
b830321
Global variable fix
ArpitaDutta Nov 10, 2022
b447140
Fix in miu closure
ArpitaDutta Jan 11, 2023
ca2ecbe
Commented few print statements for better readability
ArpitaDutta Sep 8, 2021
b9ba43e
Commented few print statements for better readability
sanghu1790 Sep 8, 2021
6090339
Printing Block Info for Subsumption Table Entry
sanghu1790 Oct 13, 2021
9d0e7c6
added debugSubsumptionLevel as a function parameter
sanghu1790 Nov 10, 2021
54af174
Create Sample.c
ArpitaDutta Apr 7, 2022
db33402
Add files via upload
ArpitaDutta Apr 7, 2022
05abf21
Smoke Test file update
ArpitaDutta May 24, 2022
6db4088
Add files via upload
ArpitaDutta Jun 21, 2022
a6be554
Removing partitioning
rasoolmaghareh Feb 1, 2023
2a72637
Adding back global and deletion interpolation
rasoolmaghareh Feb 14, 2023
0da8d48
commting partitoning at WP interpolant mergingpoint
rasoolmaghareh Feb 17, 2023
1a58ce8
Fixing the WP push-up on assert(0)
rasoolmaghareh Feb 28, 2023
fb7e6de
Fixing narrowing (false interpolants) on no-abduction WP interpolant
rasoolmaghareh Mar 10, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion include/klee/Internal/Module/TxValues.h
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ class TxStoreEntry;
class TxStore;

const uint64_t symbolicBoundId = ULONG_MAX;
void setDebugSubsumptionLevelTxValue(int debugSubsumptionLevel);

class TxAllocationContext {

Expand Down Expand Up @@ -626,7 +627,8 @@ class TxStateAddress {
///
/// \param stream The stream to print the data to.
/// \param prefix Padding spaces to print before the actual data.
void print(llvm::raw_ostream &stream, const std::string &prefix) const;
void print(llvm::raw_ostream &stream, const std::string &prefix, int debug) const;
void print(llvm::raw_ostream &stream, const std::string &prefix) const;
};

/// \brief A class that represents LLVM value that can be destructively
Expand Down
2 changes: 1 addition & 1 deletion include/klee/util/TxPrintUtil.h
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ class TxPrettyExpressionBuilder {
static std::string construct(ref<Expr> e);

static std::string constructQuery(ConstraintManager &constraints,
ref<Expr> e);
ref<Expr> e, int debugSubsumptionLevel);
};

/// \brief Output function name to the output stream
Expand Down
2 changes: 1 addition & 1 deletion lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2857,7 +2857,7 @@ static inline const llvm::fltSemantics *fpWidthToSemantics(unsigned width) {
void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
Instruction *i = ki->inst;
// if this is starting a new BB then
// check for non-linear & new BB in speculation mode
// check for non-linear & new BB in speculation mode
if (INTERPOLATION_ENABLED && SpecTypeToUse != NO_SPEC &&
txTree->isSpeculationNode() &&
(i == &state.txTreeNode->getBasicBlock()->front())) {
Expand Down
15 changes: 10 additions & 5 deletions lib/Core/TxDependency.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
///
//===----------------------------------------------------------------------===//


#include "TxDependency.h"

#include "Context.h"
Expand Down Expand Up @@ -44,7 +45,6 @@
using namespace klee;

namespace klee {

bool TxDependency::isMainArgument(const llvm::Value *loc) {
const llvm::Argument *vArg = llvm::dyn_cast<llvm::Argument>(loc);

Expand Down Expand Up @@ -305,20 +305,25 @@ TxDependency::TxDependency(
std::map<const llvm::GlobalValue *, ref<ConstantExpr> > *_globalAddresses)
: parent(parent), left(0), right(0), targetData(_targetData),
globalAddresses(_globalAddresses) {


if (parent) {
pathCondition = TxPathCondition::create(parent->pathCondition);
store = TxStore::create(parent->store);
debugSubsumptionLevel = parent->debugSubsumptionLevel;
setDebugSubsumptionLevelTxValue(debugSubsumptionLevel);
debugStateLevel = parent->debugStateLevel;
} else {
pathCondition = TxPathCondition::create(0);
store = TxStore::create(0);
#ifdef ENABLE_Z3
debugSubsumptionLevel = DebugSubsumption;
debugStateLevel = DebugState;
setDebugSubsumptionLevelTxValue(debugSubsumptionLevel);
#else
debugSubsumptionLevel = 0;
debugStateLevel = 0;
setDebugSubsumptionLevelTxValue(debugSubsumptionLevel);
#endif
}
}
Expand Down Expand Up @@ -1576,21 +1581,21 @@ ref<TxStateValue> TxDependency::evalConstantExpr(

/// \brief Print the content of the object to the LLVM error stream
void TxDependency::print(llvm::raw_ostream &stream) const {
this->print(stream, 0);
this->print(stream);
}

void TxDependency::print(llvm::raw_ostream &stream,
const unsigned paddingAmount) const {
const unsigned paddingAmount, int debugSubsumptionLevel) const {
std::string tabs = makeTabs(paddingAmount);

pathCondition->print(stream, paddingAmount);
pathCondition->print(stream, paddingAmount, debugSubsumptionLevel);
stream << "\n";

store->print(stream, paddingAmount);

if (parent) {
stream << tabs << "\n--------- Parent Dependencies ----------\n";
parent->print(stream, paddingAmount);
parent->print(stream, paddingAmount, debugSubsumptionLevel);
}
}
}
7 changes: 6 additions & 1 deletion lib/Core/TxDependency.h
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
#ifndef KLEE_DEPENDENCY_H
#define KLEE_DEPENDENCY_H


#include "TxPathCondition.h"
#include "TxStore.h"

Expand Down Expand Up @@ -336,6 +337,10 @@ class TxDependency {

std::set<ref<TxStoreEntry> > &getMarkedGlobal() { return markedGlobal; }

void setMarkedGlobal(std::set<ref<TxStoreEntry> >& newMarkedGlobal) {
markedGlobal = newMarkedGlobal;
}

bool isEntryInParent(ref<TxStoreEntry> se) {
if (!parent)
return false;
Expand Down Expand Up @@ -586,7 +591,7 @@ class TxDependency {
/// \param stream The stream to print the data to.
/// \param paddingAmount The number of whitespaces to be printed before each
/// line.
void print(llvm::raw_ostream &stream, const unsigned paddingAmount) const;
void print(llvm::raw_ostream &stream, const unsigned paddingAmount, int debugSubsumptionLevel) const;
};
}

Expand Down
4 changes: 2 additions & 2 deletions lib/Core/TxPathCondition.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -197,11 +197,11 @@ ref<Expr> TxPathCondition::packInterpolant(
}

void TxPathCondition::print(llvm::raw_ostream &stream) const {
print(stream, 0);
print(stream, 0, 0);
}

void TxPathCondition::print(llvm::raw_ostream &stream,
const unsigned paddingAmount) const {
const unsigned paddingAmount, int debugSubsumptionLevel) const {
std::string tabs = makeTabs(paddingAmount);
std::string tabsNext = appendTab(tabs);

Expand Down
2 changes: 1 addition & 1 deletion lib/Core/TxPathCondition.h
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@ class TxPathCondition {
/// \param stream The stream to print the data to.
/// \param paddingAmount The number of whitespaces to be printed before each
/// line.
void print(llvm::raw_ostream &stream, const unsigned paddingAmount) const;
void print(llvm::raw_ostream &stream, const unsigned paddingAmount, int debugSubsumptionLevel) const;
};
}

Expand Down
5 changes: 3 additions & 2 deletions lib/Core/TxPrintUtil.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -533,10 +533,11 @@ std::string TxPrettyExpressionBuilder::construct(ref<Expr> e) {

std::string
TxPrettyExpressionBuilder::constructQuery(ConstraintManager &constraints,
ref<Expr> query) {
ref<Expr> query, int debugSubsumptionLevel) { // Added 'debugSubsumptionLevel' variable for PrettyPrint
std::string msg;
std::string tabs = makeTabs(1);
llvm::raw_string_ostream stream(msg);
if (debugSubsumptionLevel>3){ /*Added 'debugSubsumptionLevel' varaible here for Pretty Print*/
stream << "antecedent:\n";
for (ConstraintManager::const_iterator it = constraints.begin(),
ie = constraints.end();
Expand All @@ -545,7 +546,7 @@ TxPrettyExpressionBuilder::constructQuery(ConstraintManager &constraints,
}
stream << "consequent:\n";
stream << tabs << construct(query) << "\n";
stream.flush();
stream.flush();}
return msg;
}

Expand Down
35 changes: 32 additions & 3 deletions lib/Core/TxStore.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -301,6 +301,7 @@ TxStore::getAddressofLatestCopyLLVMValue(llvm::Value *val) {
ie = internalStore.end();
it != ie; ++it) {
ref<TxAllocationContext> temp = (*it).first;
//llvm::outs()<<"Address-01\n";
if (temp->getValue() == val) {
if (!foundValue) {
address = temp;
Expand All @@ -311,11 +312,39 @@ TxStore::getAddressofLatestCopyLLVMValue(llvm::Value *val) {
}
}
}

// Maybe NULL
return address;
}

ref<TxStoreEntry> TxStore::getAddressofLatestCopyLLVMValueFromHistoricalStore(llvm::Value *val){
ref<TxStoreEntry> address;
bool foundValue = false;
for (LowerStateStore::const_iterator
it = symbolicallyAddressedHistoricalStore.begin(),
ie = symbolicallyAddressedHistoricalStore.end();
it != ie; ++it) {
ref<TxStoreEntry> temp = (*it).second;
if (temp->getValue() == val) {
address = temp;
foundValue = true;
}
}
if(!foundValue)
{
for (LowerStateStore::const_iterator
it = concretelyAddressedHistoricalStore.begin(),
ie = concretelyAddressedHistoricalStore.end();
it != ie; ++it) {
ref<TxStoreEntry> temp = (*it).second;
if (temp->getValue() == val) {
address = temp;
foundValue = true;
}
}

}
return address;
}

inline void TxStore::concreteToInterpolant(
ref<TxVariable> variable, ref<TxStoreEntry> entry,
const std::map<ref<Expr>, ref<Expr> > &substitution,
Expand Down Expand Up @@ -795,7 +824,7 @@ bool TxStore::markPointerFlow(ref<TxStateValue> target,
}

/// \brief Print the content of the object to the LLVM error stream
void TxStore::print(llvm::raw_ostream &stream) const { this->print(stream, 0); }
void TxStore::print(llvm::raw_ostream &stream) const { this->print(stream); }

void TxStore::print(llvm::raw_ostream &stream,
const unsigned paddingAmount) const {
Expand Down
2 changes: 2 additions & 0 deletions lib/Core/TxStore.h
Original file line number Diff line number Diff line change
Expand Up @@ -272,6 +272,8 @@ class TxStore {
LowerInterpolantStore &_symbolicallyAddressedHistoricalStore) const;

ref<TxAllocationContext> getAddressofLatestCopyLLVMValue(llvm::Value *val);

ref<TxStoreEntry> getAddressofLatestCopyLLVMValueFromHistoricalStore(llvm::Value *val);

/// \brief Newly relate a location with its stored value, when the value is
/// loaded from the location
Expand Down
Loading