Skip to content

Commit

Permalink
update readme
Browse files Browse the repository at this point in the history
  • Loading branch information
@PhilippGrulich
PhilippGrulich committed Jun 19, 2024
1 parent 008fcaa commit 984d6a4
Show file tree
Hide file tree
Showing 6 changed files with 103 additions and 88 deletions.
114 changes: 51 additions & 63 deletions nautilus/include/nautilus/val.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,49 +86,67 @@ tracing::value_ref getState(T&& value) {

} // namespace details

// val substitution for all arithmetic value type, integer, float, bool
template <is_arithmetic ValueType>
class val<ValueType> {
template <typename ValueType>
class base_val {
public:
using raw_type = ValueType;
using basic_type = ValueType;

#ifdef ENABLE_TRACING
const tracing::value_ref state;
inline val() : state(tracing::traceConstant(0)) {};
inline val(ValueType value) : state(tracing::traceConstant(value)), value(value) {};
base_val() : state(tracing::traceConstant(0)) {};
base_val(ValueType value) : state(tracing::traceConstant(value)), value(value) {};
// copy constructor
inline val(const val<ValueType>& other) : state(tracing::traceCopy(other.state)), value(other.value) {};
base_val(const val<ValueType>& other) : state(tracing::traceCopy(other.state)), value(other.value) {};
// move constructor
inline val(const val<ValueType>&& other) noexcept : state(other.state), value(other.value) {};
inline val(tracing::value_ref& tc) : state(tc), value() {};
base_val(const val<ValueType>&& other) noexcept
: state(other.state),
value(other.value) {
// std::cout << "move con" << state.toString() << " = " << other.state.toString() << std::endl;
};
base_val(tracing::value_ref& tc) : state(tc), value() {};
#else
val() {};
val(ValueType value) : value(value) {};
base_val() {};
base_val(ValueType value) : value(value) {};
// copy constructor
val(const val<ValueType>& other) : value(other.value) {};
base_val(const val<ValueType>& other) : value(other.value) {};
// move constructor
val(const val<ValueType>&& other) : value(other.value) {};
base_val(const val<ValueType>&& other) : value(other.value) {};
#endif

~val() {
virtual ~base_val() {
}

protected:
friend ValueType details::getRawValue<ValueType>(val<ValueType>& left);
ValueType value;
};

// val substitution for all arithmetic value type, integer, float, bool
template <is_arithmetic ValueType>
class val<ValueType> : public base_val<ValueType> {
public:

using base_val<ValueType>::base_val;

// copy constructor
val(const val<ValueType>& other) : base_val<ValueType>(other) {}
// move constructor
val(const val<ValueType>&& other) : base_val<ValueType>(std::move(other)) {}

val<ValueType>& operator=(const val<ValueType>&& other) {
#ifdef ENABLE_TRACING
if (tracing::inTracer()) {

// tracing::getVarRefMap()[state.ref]--;
// if (tracing::getVarRefMap()[state.ref] == 0) {
// tracing::traceValueDestruction(state);
// std::cout << "destructor " << state << " - " << tag << std::endl;
// }
tracing::traceAssignment(this->state, other.state, tracing::to_type<ValueType>());
}
#endif
}
this->value = other.value;
return *this;
};

val<ValueType>& operator=(const val<ValueType>& other) {
#ifdef ENABLE_TRACING
if (tracing::inTracer()) {
tracing::traceAssignment(state, other.state, tracing::to_type<ValueType>());
tracing::traceAssignment(this->state, other.state, tracing::to_type<ValueType>());
}
#endif
this->value = other.value;
Expand All @@ -141,11 +159,11 @@ class val<ValueType> {
// cast
if SHOULD_TRACE () {
#ifdef ENABLE_TRACING
auto resultRef = tracing::traceCast(state, tracing::to_type<OtherType>());
auto resultRef = tracing::traceCast(this->state, tracing::to_type<OtherType>());
return val<OtherType>(resultRef);
#endif
}
return val<OtherType>(value);
return val<OtherType>(this->value);
}

const val<ValueType>& operator++() {
Expand Down Expand Up @@ -186,9 +204,6 @@ class val<ValueType> {
}

private:
friend ValueType details::getRawValue<ValueType>(val<ValueType>& left);
ValueType value;

template <is_arithmetic LHS, is_arithmetic RHS>
friend COMMON_RETURN_TYPE mul(val<LHS>& left, val<RHS>& right);

Expand Down Expand Up @@ -245,41 +260,15 @@ class val<ValueType> {
};

template <>
class val<bool> {
class val<bool> : public base_val<bool> {
public:
using raw_type = bool;
using basic_type = bool;

#ifdef ENABLE_TRACING

tracing::value_ref state;
val() : state(tracing::traceConstant(0)), value(false) {};
val(bool value) : state(tracing::traceConstant(value)), value(value) {};
using base_val<bool>::base_val;
// copy constructor
val(const val<bool>& other) : state(tracing::traceCopy(other.state)), value(other.value) {};
val(const val<bool>& other) : base_val<bool>(other) {};
// move constructor
val(const val<bool>&& other) noexcept : state(other.state), value(other.value) {};
val(tracing::value_ref& tc) : state(tc) {};

#else
val() {};
val(bool value) : value(value) {};
// copy constructor
val(const val<bool>& other) : value(other.value) {};
// move constructor
val(const val<bool>&& other) : value(other.value) {};
#endif

~val() {
if SHOULD_TRACE () {

// tracing::getVarRefMap()[state.ref]--;
// if (tracing::getVarRefMap()[state.ref] == 0) {
// tracing::traceValueDestruction(state);
// std::cout << "destructor " << state << " - " << tag << std::endl;
// }
}
}
val(const val<bool>&& other) noexcept : base_val<bool>(std::move(other)) {};

val<bool>& operator=(const val<bool>& other) {

Expand All @@ -302,8 +291,6 @@ class val<bool> {
}
return value;
}

bool value;
};

template <class T>
Expand Down Expand Up @@ -389,7 +376,8 @@ namespace details {
auto&& lValue = cast_value<LHS, commonType>(std::forward<LHS>(left)); \
auto&& rValue = cast_value<RHS, commonType>(std::forward<RHS>(right)); \
if SHOULD_TRACE () { \
auto tc = tracing::traceBinaryOp<tracing::OP_TRACE, commonType>(details::getState(lValue), details::getState(rValue)); \
auto tc = tracing::traceBinaryOp<tracing::OP_TRACE, commonType>(details::getState(lValue), \
details::getState(rValue)); \
return RES_TYPE(tc); \
} \
return RES_TYPE(getRawValue(lValue) OP getRawValue(rValue)); \
Expand Down Expand Up @@ -567,7 +555,7 @@ val<bool> inline lOr(val<bool>& left, val<bool>& right) {
return val<bool> {tc};
}
#endif
return left.value || right.value;
return getRawValue(left) || getRawValue(right);
}

val<bool> inline lAnd(val<bool>& left, val<bool>& right) {
Expand All @@ -577,7 +565,7 @@ val<bool> inline lAnd(val<bool>& left, val<bool>& right) {
return val<bool> {tc};
}
#endif
return left.value && right.value;
return getRawValue(left) && getRawValue(right);
}

val<bool> inline lNot(val<bool>& arg) {
Expand All @@ -587,7 +575,7 @@ val<bool> inline lNot(val<bool>& arg) {
return val<bool> {tc};
}
#endif
return !arg.value;
return !getRawValue(arg);
}
} // namespace details

Expand Down
13 changes: 9 additions & 4 deletions nautilus/src/nautilus/tracing/ExecutionTrace.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,14 +11,14 @@ ExecutionTrace::ExecutionTrace() : currentBlockIndex(0), currentOperationIndex(0
createBlock();
};

bool ExecutionTrace::checkTag(Snapshot& snapshot) {
bool ExecutionTrace::checkTag(Snapshot& snapshot, std::vector<InputVariant>& inputs) {
// check if operation is in global map -> we have a repeating operation -> this is a control-flow merge
// std::cout << "\n checkTag \n" << std::endl;
// std::cout << *this << std::endl;
auto globalTabIter = globalTagMap.find(snapshot);
if (globalTabIter != globalTagMap.end()) {
auto& ref = globalTabIter->second;
processControlFlowMerge(ref);
processControlFlowMerge(ref, inputs);
return false;
}

Expand All @@ -27,7 +27,7 @@ bool ExecutionTrace::checkTag(Snapshot& snapshot) {
// TODO #3500 Fix handling of repeated operations
auto& ref = localTagIter->second;
// add loop iteration to tag
processControlFlowMerge(ref);
processControlFlowMerge(ref, inputs);
return false;
}
return true;
Expand Down Expand Up @@ -145,7 +145,8 @@ uint16_t ExecutionTrace::createBlock() {
return blocks.size() - 1;
}

Block& ExecutionTrace::processControlFlowMerge(operation_identifier oi) {
Block& ExecutionTrace::processControlFlowMerge(operation_identifier oi,
[[maybe_unused]] std::vector<InputVariant>& inputs) {
if (oi.blockIndex == currentBlockIndex) {
throw RuntimeException("Invalid trace. This is maybe caused by a constant loop.");
}
Expand All @@ -158,6 +159,10 @@ Block& ExecutionTrace::processControlFlowMerge(operation_identifier oi) {
auto mergedBlockId = createBlock();
// perform a control flow merge and merge the current block with operations in some other block.
auto& referenceBlock = blocks[oi.blockIndex];
auto& referenceOp = referenceBlock.operations[oi.operationIndex];
if (referenceOp.input.size() == inputs.size()) {
//for (referenceOp == )
}
auto& currentBlock = blocks[currentBlockIndex];

auto& mergeBlock = getBlock(mergedBlockId);
Expand Down
4 changes: 2 additions & 2 deletions nautilus/src/nautilus/tracing/ExecutionTrace.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ class ExecutionTrace {

void addReturn(Snapshot&, Type type, value_ref ref);

bool checkTag(Snapshot& snapshot);
bool checkTag(Snapshot& snapshot, std::vector<InputVariant>& inputs);

void resetExecution();

Expand Down Expand Up @@ -106,7 +106,7 @@ class ExecutionTrace {
* @param operationIndex
* @return Block&
*/
Block& processControlFlowMerge(operation_identifier oi);
Block& processControlFlowMerge(operation_identifier oi, std::vector<InputVariant>& inputs);

/**
* @brief Returns the return reference
Expand Down
50 changes: 31 additions & 19 deletions nautilus/src/nautilus/tracing/TraceContext.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,8 @@ value_ref TraceContext::traceLoad(value_ref src, Type resultType) {
auto input = InputVariant(src);
auto op = Op::LOAD;
auto tag = recordSnapshot();
if (executionTrace->checkTag(tag)) {
auto inputs = std::vector<InputVariant> {input};
if (executionTrace->checkTag(tag, inputs)) {
auto resultRef = executionTrace->addOperationWithResult(tag, op, resultType, std::vector<InputVariant> {input});
return resultRef;
}
Expand All @@ -72,7 +73,8 @@ void TraceContext::traceStore(value_ref target, value_ref src, Type valueType) {
}
auto op = Op::STORE;
auto tag = recordSnapshot();
if (executionTrace->checkTag(tag)) {
auto inputs = std::vector<InputVariant> {src};
if (executionTrace->checkTag(tag, inputs)) {
executionTrace->addOperation(tag, op, valueType, target, src);
return;
}
Expand Down Expand Up @@ -120,7 +122,9 @@ value_ref TraceContext::traceCopy(nautilus::tracing::value_ref ref) {
return currentOperation.resultRef;
}
auto tag = recordSnapshot();
if (executionTrace->checkTag(tag)) {

auto inputs = std::vector<InputVariant> {ref};
if (executionTrace->checkTag(tag, inputs)) {
auto resultRef = executionTrace->getNextValueRef();
executionTrace->addAssignmentOperation(tag, {resultRef, ref.type}, ref, ref.type);
return {resultRef, ref.type};
Expand All @@ -139,7 +143,8 @@ value_ref TraceContext::traceCall(const std::string& functionName, void* fptn, T
}

auto tag = recordSnapshot();
if (executionTrace->checkTag(tag)) {
auto inputs = std::vector<InputVariant> {};
if (executionTrace->checkTag(tag, inputs)) {
auto functionArguments = InputVariant(FunctionCall {
.functionName = functionName,
.ptr = fptn,
Expand All @@ -162,16 +167,19 @@ void TraceContext::traceAssignment(value_ref targetRef, value_ref sourceRef, Typ
return;
}
auto tag = recordSnapshot();
/*

auto found = executionTrace->globalTagMap.find(tag);
if (found != executionTrace->globalTagMap.end()) {
auto currentOp = executionTrace->getBlock(found->second.blockIndex).operations[found->second.operationIndex];
if(std::get<value_ref>(currentOp.input[0]) != sourceRef){
executionTrace->addAssignmentOperation(tag, targetRef, sourceRef, resultType);
auto currentOp = executionTrace->getBlock(found->second.blockIndex).operations[found->second.operationIndex];
if(std::get<value_ref>(currentOp.input[0]) != sourceRef){
executionTrace->getCurrentBlock().operations.emplace_back(tag, ASSIGN, resultType, targetRef, std::vector<InputVariant> {sourceRef});
return;
};
}*/
if (executionTrace->checkTag(tag)) {
//executionTrace->addAssignmentOperation(tag, targetRef, sourceRef, resultType);
//return;
};
}
auto inputs = std::vector<InputVariant> {sourceRef};
if (executionTrace->checkTag(tag, inputs)) {
executionTrace->addAssignmentOperation(tag, targetRef, sourceRef, resultType);
return;
}
Expand All @@ -191,8 +199,10 @@ value_ref TraceContext::traceCast(value_ref state, Type resultType) {
// we are in a know operation if the operation at the current block[currentOperationCounter] is equal to the
// received operation.
auto tag = recordSnapshot();
if (executionTrace->checkTag(tag)) {
auto leftIV = InputVariant(state);
auto leftIV = InputVariant(state);
auto inputs = std::vector<InputVariant> {leftIV};
if (executionTrace->checkTag(tag, inputs)) {

auto op = Op::CAST;
auto resultRef =
executionTrace->addOperationWithResult(tag, op, resultType, std::vector<InputVariant> {leftIV});
Expand Down Expand Up @@ -225,11 +235,12 @@ value_ref TraceContext::traceBinaryOperation(Op op, Type resultType, value_ref&
}

auto tag = recordSnapshot();
if (executionTrace->checkTag(tag)) {
auto leftIV = InputVariant(leftRef);
auto rightIV = InputVariant(rightRef);
auto resultRef =
executionTrace->addOperationWithResult(tag, op, resultType, std::vector<InputVariant> {leftIV, rightIV});

auto leftIV = InputVariant(leftRef);
auto rightIV = InputVariant(rightRef);
auto inputs = std::vector<InputVariant> {leftIV, rightIV};
if (executionTrace->checkTag(tag, inputs)) {
auto resultRef = executionTrace->addOperationWithResult(tag, op, resultType, std::move(inputs));
return resultRef;
}
throw TraceTerminationException();
Expand All @@ -244,7 +255,8 @@ bool TraceContext::traceCmp(value_ref targetRef) {
} else {
// record
auto tag = recordSnapshot();
if (executionTrace->checkTag(tag)) {
auto inputs = std::vector<InputVariant> {};
if (executionTrace->checkTag(tag, inputs)) {
executionTrace->addCmpOperation(tag, targetRef);
result = symbolicExecutionContext->record(tag);
} else {
Expand Down
8 changes: 8 additions & 0 deletions nautilus/test/execution-tests/ExpressionFunctions.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,14 @@ val<int32_t> assignment5(val<int32_t> x) {
return x;
}

val<int32_t> assignmentSwap(val<int32_t> x) {
auto t = x;
x = 42;
x = t + x;
return x;
}


val<int8_t> int8AddExpression(val<int8_t> x) {
val<int8_t> y = (int8_t) 2;
return y + x;
Expand Down
Loading

0 comments on commit 984d6a4

Please sign in to comment.