From 489fca16f148bc7870bb5ffc1ae61c0bfe0cefd9 Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Fri, 6 Oct 2017 19:59:15 -0400 Subject: [PATCH 01/20] Create VariablesEnvironmenmtImmutable.cpp --- .../LiquidFixpointBuilder/VariablesEnvironment.cpp | 4 ++-- .../VariablesEnvironmentImmutable.cpp | 11 +++++++++++ 2 files changed, 13 insertions(+), 2 deletions(-) create mode 100644 lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironment.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironment.cpp index 6b067dd7cc15e..f5d5f56d5a94c 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironment.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironment.cpp @@ -43,9 +43,9 @@ namespace liquid auto search = mapToUse.find(variable); if(search != mapToUse.end()) { mapToUse.erase(search); - } + } mapToUse.emplace(variable, type); - } + } ResultType VariablesEnvironment::createIOVariable( const std::string& variable, diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp new file mode 100644 index 0000000000000..6899b7f49f596 --- /dev/null +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -0,0 +1,11 @@ +#include "llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h" +#include "llvm/Transforms/LiquidFixpointBuilder/RefinementUtils.h" +#include +#include + +using namespace std::literals::string_literals; + +namepsace liquid +{ + // Create an Immutable Variable + ResultType VariablesEnvironment::CreateImmutableInputVariable From f77217f8620ee3d4d86646ae0ea74a83dc874b71 Mon Sep 17 00:00:00 2001 From: jssandh2 Date: Sat, 14 Oct 2017 17:28:42 -0400 Subject: [PATCH 02/20] Addition of the VariablesEnvironmentImmutable.h file in the inlcude/ folder --- .../VariablesEnvironment.h | 2 +- .../VariablesEnvironmentImmutable.h | 82 +++++++++++++++++++ 2 files changed, 83 insertions(+), 1 deletion(-) create mode 100644 include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h diff --git a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironment.h b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironment.h index da7c4234392f6..1c486b483368f 100644 --- a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironment.h +++ b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironment.h @@ -30,7 +30,7 @@ namespace liquid std::string currentBlockName = ""s; const FunctionBlockGraph& functionBlockGraph; - std::map variableTypes; + std::map variableTypes; std::map mutableVariableState; std::map> mutableVariableConstraints; std::map> variablesMappingsPerBlock; diff --git a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h new file mode 100644 index 0000000000000..588f321975875 --- /dev/null +++ b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h @@ -0,0 +1,82 @@ +#ifndef LLVM_TRANSFORMS_UTILS_LIQUID_VARIABLESENVIRONMENTIMMUTABLE_H +#define LLVM_TRANSFORMS_UTILS_LIQUID_VARIABLESENVIRONMENTIMMUTABLE_H + +#include +#include +#include +#include +#include "llvm/Transforms/LiquidFixpointBuilder/FixpointConstraintBuilder.h" +#include "llvm/Transforms/LiquidFixpointBuilder/FixpointType.h" +#include "llvm/Transforms/LiquidFixpointBuilder/FunctionBlockGraph.h" + +using namespace std::literals::string_literals; + +namespace liquid +{ + + class PhiNodeObligation + { + public: + const std::string VariableSource; + const std::string TargetFutureVariable; + + PhiNodeObligation() {} + PhiNodeObligation(const std::string variableSource, const std::string targetFutureVariable) : VariableSource(variableSource), TargetFutureVairable(targetFutureVariable) {} + }; + + class VariablesEnvironmentImmutable + { + private: + std::string currentBlockName = ""s; + const FunctionBlockGraph& functionBlockGraph; + + std::map variableTypes; + std::map> variablesMappingPerBlock; + + std::map> variablesValuesPerBlock; + std::set finishedBlocks; + std::map> phiNodeObligations; + + std::set outputVariables; + + std::map cachedBlockGuards; + + ResultType createVariable(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& constaints, const std::string& expression); + ResultType createIOVariable(const std::string& variable, const FixpointType& type, const std::vector& constraints); + ResultType validateFinishedAndUnfinishedBlockStates(const std::vector& previousFinishedBlocks, const std::vector& previousUnfinishedBlocks); + ResultType getCommonVariables(std::vector previousBlocks, std::set& commonVariables); + std::string getNextVariableName(const std::string& variable); + std::vector getBlockBinders(const std::string& blockName); + ResultType getBlockBindersForPhiNode(const std::string& previousBlock, const std::string& blockName, const std::string& mappedVariableName, std::vector& binders); + ResultType createPhiNodeWithoutCreatedBinders(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks); + ResultType createPhiNodeInternal(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks); + + ResultType getBlockGuard(const std::string& blockName, std::string& blockGuard); + ResultType addVariableToBlockAndSuccessors(const std::string& blockName, const std::string& transitionGuardName); + ResultType initializeBlockGuards(); + ResultType endBlock(const std::string& blockName); + + public: + Counter FreshState; + FixpointConstraintBuilder constraintBuilder; + + VariablesEnvironmentImmutable(const FunctionBlockGraph& _functionBlockGraph) : functionBlockGraph(_functionBlockGraph) {} + ResultType StartBlock(const std::string& blockName); + ResultType CreateImmutableInputVariable(const std::string& variable, const FixpointType &type, const std::vector& constraints); + ResultType CreateImmutableVariable(std::string variable, FixpointType type, std::vector constaints, std::string expression); + ResultType AddJumpInformation(const std::string& targetBlock); + ResultType AddBranchInformation(const std::string& booleanVariable, const bool variableValue, const std::string& targetBlock); + ResultType CreatePhiNode(const std::string& variable, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks); + + bool IsVariableDefined(std::string variableName); + std::string GetVariableName(std::string variableName); + std::string GetVariableAddress(std::string variableName); + ResultType ToStringOrFailure(std::string& output); + }; +} + +#endif + + + + From 57e1fdee683478aa5b7645b5c33c8ca6e8d4eba8 Mon Sep 17 00:00:00 2001 From: jssandh2 Date: Sun, 15 Oct 2017 22:43:05 -0400 Subject: [PATCH 03/20] Begin adding cpp files --- .../VariablesEnvironmentImmutable.cpp | 58 ++++++++++++++++++- 1 file changed, 56 insertions(+), 2 deletions(-) diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index 6899b7f49f596..b0761bc30bb72 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -7,5 +7,59 @@ using namespace std::literals::string_literals; namepsace liquid { - // Create an Immutable Variable - ResultType VariablesEnvironment::CreateImmutableInputVariable + // Check whether a variable is defined + bool VariablesEnvironmentImmutable::IsVariableDefined(std::string variableName) + { + return RefinementUtils::ContainsKey(variableTypes, variableName); + } + + // Get the name of the variable + std::string VariablesEnvironmentImmutable::GetVariableName(const std::string variableName) + { + assert(RefinementUtils::ContainsKey(variablesMappingsPerBlock, currentBlockName)); + assert(RefinementUtils::ContainsKey(variablesMappingsPerBlock[currentBlockName], variableName)); + return variablesMappingPerBlock[currentBlockName][variableName]; + } + + // Get the address of the variable + std::string VariablesEnvironmentImmutable::GetVariableAddress(std::string variableName) + { + return constraintBuilder.GetBinderAddress(variableName); + } + + // Get the binders for the block + std::vector VariablesEnvironmentImmutable::getBlockBinders(const std::string& blockName) + { + auto currBinders = variablesValuesPerBlock[blockName]; + std::vector ret(currBinders.begin(), currBinders.end()); + ret.emplace_back("__block__"s + blockName); + return ret; + } + + // Create an Immutable Input Variable + ResultType VariablesEnvironmentImmutable: :CreateImmutableInputVariable( + const std::string& variable, + const FixpointType& type, + const std::vector& constraints) + { + auto createRes = createIOVariable(variable, type, constraints); + if (!createRes.Succeeded) { return createRes; } + + // Since, this is an input variable make it accessible to every block + auto internalVarName = GetVariableName(variable); + + for (auto& blockVarMap : variablesMappingsPerBlock) + { + if (!RefinementUtils::ContainsKey(blockVarMap.second, variable)) + { + blockVarMap.second[variable] = internalVarName; + variablesValuesPerBlock[blockVarMap.first].emplace(internalVarName); + } + } + + return ResultType::Success(); + } + + + + From da4b5e91cfc6a92388d6aeee3667a9528620d761 Mon Sep 17 00:00:00 2001 From: jssandh2 Date: Sun, 15 Oct 2017 23:03:50 -0400 Subject: [PATCH 04/20] Dumb --- .../Transforms/LiquidFixpointBuilder/VariablesEnvironment.h | 2 +- .../LiquidFixpointBuilder/VariablesEnvironmentImmutable.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironment.h b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironment.h index 1c486b483368f..da7c4234392f6 100644 --- a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironment.h +++ b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironment.h @@ -30,7 +30,7 @@ namespace liquid std::string currentBlockName = ""s; const FunctionBlockGraph& functionBlockGraph; - std::map variableTypes; + std::map variableTypes; std::map mutableVariableState; std::map> mutableVariableConstraints; std::map> variablesMappingsPerBlock; diff --git a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h index 588f321975875..43783c0465e3d 100644 --- a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h +++ b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h @@ -30,7 +30,7 @@ namespace liquid std::string currentBlockName = ""s; const FunctionBlockGraph& functionBlockGraph; - std::map variableTypes; + std::map variableTypes; std::map> variablesMappingPerBlock; std::map> variablesValuesPerBlock; From 5dffd44fc8c59041659e3fc59290c7aacdde103e Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Mon, 23 Oct 2017 01:59:56 -0400 Subject: [PATCH 05/20] Some more functions. Almost done. --- .../VariablesEnvironmentImmutable.cpp | 172 +++++++++++++++++- 1 file changed, 168 insertions(+), 4 deletions(-) diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index b0761bc30bb72..8a4d942fc7e55 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -35,9 +35,42 @@ namepsace liquid ret.emplace_back("__block__"s + blockName); return ret; } - + + // Assign a Type to a pre-existing variable, or give a variable a new Type + void insertOrAssignType(std::map& mapToUse, const std::string& variable, const FixpointType& type) + { + auto search = mapToUse.find(variable); + if (search!= mapToUse.end()) { + mapToUse.erase(search); + } + mapToUse.emplace(variable, type); + } + + // Create an Input Output Variable + ResultType VariablesEnvironmentImmutable::createIOVariable(const std::string& variable, + const FixpointType& type, + const std::vector& constraints) + { + if (RefinementUtils::ContainsKey(variableTypes, variable)) { + return ResultType::Error("Variable"s + variable + " already exists."s); + } + + std::string mappedVariableName = variable; + + { + auto createBinderRes = constraintBuilder.CreateBinderWithConstraints(mappedVariableName, type, constraints); + if (!createBinderRes.Succeeded) { return createBinderRes; } + } + + insertOrAssignType(variableTypes, variable, type); + variablesMappingsPerBlock[currentBlockName][variable] = mappedVariableName; + variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); + + return ResultType::Success(); + } + // Create an Immutable Input Variable - ResultType VariablesEnvironmentImmutable: :CreateImmutableInputVariable( + ResultType VariablesEnvironmentImmutable::CreateImmutableInputVariable( const std::string& variable, const FixpointType& type, const std::vector& constraints) @@ -60,6 +93,137 @@ namepsace liquid return ResultType::Success(); } + // Create a Variable + ResultType VariablesEnvironmentImmutable::CreateVariable( + const std::string& variable, + const std::string& mappedVariableName, + const FixpointType& type, + const std::vector& constraints, + const std::string& expression) + { + auto currVariablesAndInfo = getBlockBinders(currentBlockName); + + { + auto createBinderRes = constraintBuilder.CreateBinderWithUnknownType(mappedVariableName, type, currVariablesAndInfo); + if (!createBinderRes.Succeeded) { return createBinderRes; } + } + + // If there is any constraint, add it to the constraintBuilder and resolve it + if (constraints.size() > 0) + { + std::string constraintName = "Variable_"s + mappedVariableName + "_ConstraintCheck"s; + auto addConstRes = constraintBuilder.AddConstraint(constraintName, type, constraints, expression, currVariablesAndInfo); + if (!addConstRes.Succeeded) { return addConstRes; } + } + + // Make an assignment to the variable + { + std::string constraintName = "Variable_"s + mappedVariableName + "_Assignment"s; + auto addConstRes = constraintBuilder.AddConstraintForAssignment(constaintName, mappedVariableName, expression, currVariablesAndInfo); + if (!addConstRes.Succeeded) { return addConstRes; } + } + + // Make updates to Variable Mappings and Values for State Update of the Block + insertOrAssignVarType(variableTypes, variable, type); + variablesMappingsPerBlock[currentBlockName][variable] = mappedVariableName; + variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); + + return ResultType::Success(); + } - - + // Create an Immutable Variable + ResultType VariablesEnvironmentImmutable::CreateImmutableVariable( + std::string variable, + FixpointType type, + std::vector constraints, + std::string expression) + { + if (RefinementUtils::ConstainsKey(variableTypes, variable)) + { + return ResultType::Error("Variable"s + variable + " already exists."s); + } + + return CreateVariable(variable, variable, type, constraints, expression); + } + + ResultType VariablesEnvironmentImmutable::AddJumpInformation(const std::string& targetBlock) + { + std::string transitionGuardName = "__transition__"s + currentBlockName + "__"s + targetBlock; + { + auto createBinderRes = constraintBuilder.CreateBinderWithConstraints(transitionGuardName, FixpointType::GetBoolType(), { "true"s }); + if (!createBinderRes.Succeeded) { return createBinderRes; } + } + + return ResultType::Success(); + } + + ResultType VariablesEnvironment::AddBranchinformation(const std::string& booleanVariable, const bool variableValue, const std::string& targetBlock) + { + // Verify the variable doesn't already exist + if (!RefinementUtils::ContainsKey(variableTypes, booleanVariable)) + { + return ResultType::Error("Missing variable: "s + booleanVariable); + } + + // Enforce the variable type is Boolean + if (variableTypes.at(booleanVariable) != FixpointType::GetBoolType()) + { + return ResultType::Error("Expected boolean type for variable: "s + booleanVariable); + } + + // Convert the variable into a Proposition for a Fixpoint Constraint + const std::string assignedExpr = "__value <=> "s + (variableValue ? ""s : "~"s) + booleanVariable; + const std::string transitionGuardName = "__transition__"s + currentBlockName + "__"s + targetBlock; + + { + auto createbinderRes = constraintBuilder.CreateBinderWithConstraints(transitionGuardName, FixpointType::GetBoolType(), { assignedExpr }); + if (!createdBinderRes.Succeeded) { return createBinderRes; } + } + + return ResultType::Success(); + } + + ResultType VariablesEnvironmentImmutable::validateFinishedAndUnfinishedBlockStates( + const std::vector& previousFinishedBlocks, + const std::vector& previousUnfinishedBlocks) + { + //@TODO::(juspreet) - The logic is odd. It might be the cause of problem in loops. Verify. + if (previousFinishedBlocks.size() == 0 || previousFinishedBlocks.size() > 1) { + return ResultType::Error("Blocks were not completed in the right order. Expected one Completed Block, got "s + std::to_string(previousFinishedBlocks.size())); + } + + // Ensure that : + // 1) forall blocks in PreviousFinishedBlocks, dominate(blocks, block), forall block in PreviousUnfinishedblocks + for (const auto& previousUnfinishedBlock : previousFinishedBlocks) + { + bool allDominated = true; + for (const auto& previousFinishedBlock : previousUnfinishedBlocks) + { + bool dominated; + { + auto domRes = functionBlockGraph.StrictlyDominates(previousFinishedBlock, previousUnfinishedBlock, dominate); + if (!domRes.Succeeded) { return domRes; } + } + + if (!dominated) + { + allDominated = false; + break; + } + } + + // If all blocks are not dominated, then exit with an appropriate error message + if (!allDominated) + { + return ResultType::Error("Blocks were not completed in the right order. Unexpected control flow graph. Finished: "s + + RefinementUtils::StringJoin(", "s, previousFinishedBlocks) + + " . Unfinished: "s + + RefinementUtils::StringJoin(", "s, previousUnfinishedBlocks) + ); + } + } + return ResultType::Success(); + } + + //@TODO::(juspreet) - Continue ripping and verifying. +} From 005c468daa3cf729b076b29e621557461ebc06c6 Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Fri, 27 Oct 2017 19:40:58 -0400 Subject: [PATCH 06/20] Compute common variables. 2 more commits to go. --- .../VariablesEnvironmentImmutable.cpp | 43 ++++++++++++++++++- 1 file changed, 41 insertions(+), 2 deletions(-) diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index 8a4d942fc7e55..0d945a677bc63 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -223,7 +223,46 @@ namepsace liquid } } return ResultType::Success(); - } + } + + ResultType VariablesEnvironmentImmutable::getCommonVariables(std::vector previousBlocks, std::set& commonVariables) + { + std::vector previousFinishedBlocks; + std::vector previousUnfinishedBlocks; + + for (auto& previousBlock: previousBlocks) + { + RefinementUtils::Contains(finishedBlocks, previousBlock) ? + previousFinishedBlocks.push_back(previousBlock) : + previousUnfinishedBlocks.push_back(previousBlock); + } - //@TODO::(juspreet) - Continue ripping and verifying. + // In a CFG, it is possible that previous blocks aren't _all_ processed (loops) + // However, for immutable constructs, this shouldn't happen. Raise an Error, if it does. + if (previousUnfinishedBlocks.size() > 0) + { + return ResultType::Error("There exist: "s + std::to_string(previousUnfinishedBlocks.size()) + " unfinished Block that were appended without processing. This is an error in an immutable environment."s); + } + + bool first = true; + + for (auto& previousBlock : previousBlocks) + { + if (first) + { + commonVariables = RefinementUtils::GetKeysSet(variablesMappingsPerBlock[previousBlock]); + first = false; + } + else + { + std::set currBlockVars = RefinementUtils::GetKeysSet(variablesMappingsPerBlock[previousBlock]); + commonVariables = RefinementUtils::SetIntersection(commonVariables, currBlockVars); + } + } + return ResultType::Success(); + } + + //@TODO::juspreet - Continue ripping and verifying. + + } From 03412934a6d86f8e3f4244f2ebec3d5c15fec83e Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Fri, 27 Oct 2017 23:51:05 -0400 Subject: [PATCH 07/20] Add some Phi-Node functions (modified). 1 more commit, till we add Block Modification and exposed functions --- .../VariablesEnvironmentImmutable.cpp | 76 ++++++++++++++++++- 1 file changed, 75 insertions(+), 1 deletion(-) diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index 0d945a677bc63..8824e6141a23d 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -263,6 +263,80 @@ namepsace liquid } //@TODO::juspreet - Continue ripping and verifying. - + ResultType VariablesEnvironmentImmutable::getBlockBindersForPhiNode(const std::string& previousBlock, const std::string& blockName, const std::string& mappedVariableName, std::vector& binders) + { + binders = getBlockBinders(previousBlock); + + // Add the transition Edge Type to the Environment + std::string transitionGuardName = "__transition__"s + previousBlock + "__"s + currentBlockName; + binders.emplace_back(transitionGuardName); + + std::string predecessorEntryGuard; + { + auto getPredEntryRes = getBlockGuard(previousBlock, predecessorEntryGuard); + if (!getPredEntryRes.Succeeded) { return getPredEntryRes; } + } + + std::string phiNodeTransitionGuard = predecessorEntryGuard + " && "s + transitionGuardName; + std::string phiNodeGuardName = "__phi__"s + mappedVariableName + "_"s + previousBlock; + + { + auto createBinderRes = constraintBuilder.CreateBinderWithConstraints(phiNodeGuardName, FixpointType::GetBoolType(), { phiNodeTransitionGuard }); + if (!createBinderRes.Succeeded) { return createBinderRes; } + } + + binders.emplace_back(phiNodeGuardName); + return ResultType::Success(); + } + + ResultType VariablesEnvironmentImmutable::createPhiNodewithoutCreatedBinders(const std::string& variable, vonst std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks) + { + if (sourceVariableNames.size() != previousBlocks.size()) + { + return ResultType::Error("Expected Phi-Node Variables and associated Block Size to be the sames"s); + } + + { + auto currVariablesAndInfo = getBlockBinders(currentBlockName); + auto createBinderRes = constraintBuilder.CreatebinderWithUnkownType(mappedVariableName, type, currVariablesAndInfo); + if (!createBinderRes.Succeeded) { return createBinderRes; } + } + + for (size_t i = 0, csize = previosBlocks.size(); i < csize; i++) + { + auto& previousBlock = previousBlocks[i]; + std::vector blockVariablesAndInfo; + { + auto getBinderRes = getBlockBindersForPhiNode(previousBlock, currentBlockName, mappedVariableName, blockVariablesAndInfo); + if (!getBinderRes.Succeeded) { return getBinderRes; } + } + + auto blockVariableMapping = sourceVariableNames[i]; + // Ensure that the future binder is part of the current info + if (!RefinementUtils::Contains(blockVariablesAndInfo, blockVariableMapping)) + { + blockVariablesAndInfo.push_back(blockVariableMapping); + } + + std::string constraintName = "Variable_"s + previousBlock + "_"s + currentBlockName + "_"s + mappedVariableName; + + // Create Variable Mappings for Future Binders (which are immutable) + std::string variableName = blockVariableMapping; + if (RefinementUtils::ContainsKey(variablesMappingsPerBlock[previousBlock], blockVariableMapping)) + { + variableName = variablesMappingsPerBlock[previousBlock][blockVariableMapping]; + } + + std::string assignedExpr = "__value == "s + variableName; + + auto addConstres = constraintBuilder.AddConstraintForAssignment(constraintName, mappedVariableName, assignedExpr, blockVariablesAndInfo); + if (!addConstRes.Succeeded) { return addConstRes; } + } + + variablesMappingsPerBlock[currentBlockName][variable] = mappedVariableName; + variablesValuesPerBlock[currentBlockName].emplace_back(mappedVariableName); + return ResultType::Success(); + } + } From 26b23b9c2624d60fc77f5c6cf4d50d1bdb7e7bbb Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Sat, 28 Oct 2017 22:35:27 -0400 Subject: [PATCH 08/20] Final addition of code (first run) for VariablesEnvironmentImmutable.cpp --- .../VariablesEnvironmentImmutable.cpp | 245 ++++++++++++++++++ 1 file changed, 245 insertions(+) diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index 8824e6141a23d..d40e76eff2171 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -338,5 +338,250 @@ namepsace liquid return ResultType::Success(); } + ResultType VariablesEnvironmentImmutable::createPhiNodeInternal( + const std::string& variable, + const std::string& mappedVariableName, + const FixpointType& type, + const std::vector& sourceVariableNames, + const std::vector& previousblocks) + { + if (sourceVariablesNames.size() != previousBlocks.size()) + { + return ResultType::Error("Expected phi node variables and associated block size to be the same"s); + } + + //Check if any parts of the phi node are variables that are not yet declared + for (size_t i = 0, csize = previousBlocks.size(); i < csize; i++) + { + auto& previousBlock = previousBlocks[i]; + auto blockVariableMapping = sourceVariableNames[i]; + + //variable of a phi node hasn't been created yet + if (!RefinementUtils::ContainsKey(variablesMappingsPerBlock[previousBlock], blockVariableMapping)) + { + auto futureBinderRes = constraintBuilder.CreateFutureBinder(blockVariableMapping, type); + if (!futureBinderRes.Succeeded) { return futureBinderRes; } + } + } + + return createPhiNodeWithoutCreatedBinders(variable, mappedVariableName, type, sourceVariableNames, previousBlocks); + } + + ResultType VariablesEnvironmentImmutable::CreatePhiNode(const std::string& variable, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks) + { + std::string mappedVariableName = variable; + return createPhiNodeInternal(variable, mappedVariableName, type, sourceVariableNames, previousBlocks); + } + + //@TODO:: (juspreet) - The recursive call here isn't clear. Verify. + ResultType VariablesEnvironmentImmutable::getBlockGuard(const std::string& blockName, std::string& blockGuard) + { + if (RefinementUtils::ContainsKey(cachedBlockGuards, blockName)) + { + blockGuard = cachedBlockGuards[blockName]; + return ResultType::Success(); + } + + if (blockName == functionBlockGraph.GetStartingBlockName()) + { + blockGuard = "true"; + } + else + { + std::vector predecessors; + { + auto getPredRes = functionBlockGraph.GetPreviousBlocks(blockName, predecessors); + if (!getPredRes.Succeeded) { return getPredRes; } + } + + std::vector predecessorTransitionGuards; + for (const auto& predecessor : predecessors) + { + std::string transitionGuardName = "__transition__"s + predecessor + "__"s + blockName; + + // (Bug?) The recursive call later gives unallocated strings here, until we find a predecessor that is the same as the current block. + std::string predecessorEntryGuard; + { + if (predecessor == blockName) + { + predecessorEntryGuard = transitionGuardName; + } + else + { + auto getPredEntryRes = getBlockGuard(predecessor, predecessorEntryGuard); + if (!getPredEntryRes.Succeeded) { return getPredEntryRes; } + } + } + + predecessorTransitionGuards.emplace_back("("s + predecessorEntryGuard + " && "s + transitionGuardName + ")"s); + } + + blockGuard = "("s + RefinementUtils::StringJoin(" || ", predecessorTransitionGuards) + ")"s; + } + + cachedBlockGuards[blockName] = blockGuard; + return ResultType::Success(); + } + + ResultType VariablesEnvironment::addVariableToBlockAndSuccessors(const std::string& blockName, const std::string& transitionGuardName) + { + std::vector successors; + { + auto getSuccRes = functionBlockGraph.GetAllSuccessorBlockNames(blockName, successors); + if (!getSuccRes.Succeeded) { return getSuccRes; } + }; + + for (const auto& successor : successors) + { + variablesMappingsPerBlock[successor][transitionGuardName] = transitionGuardName; + variablesValuesPerBlock[successor].emplace(transitionGuardName); + } + + return ResultType::Success(); + } + + ResultType VariablesEnvironment::initializeBlockGuards() + { + std::vector blockNames; + { + auto getBlockRes = functionBlockGraph.GetAllBlockNames(blockNames); + if (!getBlockRes.Succeeded) { return getBlockRes; } + } + + for (const auto& blockName : blockNames) + { + std::vector successors; + { + auto getSuccRes = functionBlockGraph.GetSuccessorBlocks(blockName, successors); + if (!getSuccRes.Succeeded) { return getSuccRes; } + } + + for(const auto& successor : successors) + { + std::string transitionGuardName = "__transition__"s + blockName + "__"s + successor; + { + auto createBinderRes = constraintBuilder.CreateFutureBinder(transitionGuardName, FixpointType::GetBoolType()); + if (!createBinderRes.Succeeded) { return createBinderRes; } + } + + { + auto addVarRes = addVariableToBlockAndSuccessors(successor, transitionGuardName); + if (!addVarRes.Succeeded) { return addVarRes; } + } + } + } + + for (const auto& blockName : blockNames) + { + std::string blockGuardName = "__block__"s + blockName; + std::string blockGuard; + { + auto getBlockGuardRes = getBlockGuard(blockName, blockGuard); + if (!getBlockGuardRes.Succeeded) { return getBlockGuardRes; } + } + + auto createBinderRes = constraintBuilder.CreateBinderWithConstraints(blockGuardName, FixpointType::GetBoolType(), { blockGuard }); + if (!createBinderRes.Succeeded) { return createBinderRes; } + + //Don't add block guard to the variablesMapping, as it is added in the getBinders functions + } + + return ResultType::Success(); + } + + ResultType VariablesEnvironmentImmutable::endBlock(const std::string& blockName) + { + auto& phiNodeObligationsForBlock = phiNodeObligations[blockName]; + + for (const auto& phiNodeObligation : phiNodeObligationsForBlock) + { + auto expression = "__value == "s + GetVariableName(phiNodeObligation.VariableSource); + auto currentMapping = phiNodeObligation.TargetFutureVariable; + auto createRes = CreateImmutableVariable(currentMapping, variableTypes.at(phiNodeObligation.VariableSource), {}, expression); + if (!createRes.Succeeded) { return createRes; }; + } + + phiNodeObligationsForBlock.clear(); + + finishedBlocks.emplace(blockName); + return ResultType::Success(); + } + + ResultType VariablesEnvironment::StartBlock(const std::string& blockName) + { + if (currentBlockName == ""s) + { + auto initRes = initializeBlockGuards(); + if (!initRes.Succeeded) { return initRes; } + } + else + { + auto endBlockRes = endBlock(currentBlockName); + if (!endBlockRes.Succeeded) { return endBlockRes; } + } + + currentBlockName = blockName; + + if (RefinementUtils::Contains(finishedBlocks, currentBlockName)) + { + return ResultType::Error("Block "s + currentBlockName + " has already finished"); + } + + std::vector previousBlocks; + { + auto previousBlockRes = functionBlockGraph.GetPreviousBlocks(currentBlockName, previousBlocks); + if (!previousBlockRes.Succeeded) { return previousBlockRes; } + } + + // Get variables which are present in ALL of the predecessor blocks + std::set commonVariables; + { + auto getCommonVarsRes = getCommonVariables(previousBlocks, commonVariables); + if (!getCommonVarsRes.Succeeded) { return getCommonVarsRes; } + } + + // Add to the environment any variables which are unchanged in predecessors + std::set phiNodeVariables; + for (auto& commonVariable : commonVariables) + { + bool usingIdenticalMappings = std::all_of(previousBlocks.begin(), previousBlocks.end(), [&](std::string block) { + return variablesMappingsPerBlock[block][commonVariable] == variablesMappingsPerBlock[previousBlocks[0]][commonVariable]; + }); + + if (usingIdenticalMappings) + { + variablesMappingsPerBlock[currentBlockName][commonVariable] = variablesMappingsPerBlock[previousBlocks[0]][commonVariable]; + variablesValuesPerBlock[currentBlockName].emplace(variablesMappingsPerBlock[previousBlocks[0]][commonVariable]); + } + else + { + phiNodeVariables.emplace(commonVariable); + } + } + + // Add to the environment any variables which require phi nodes + for (auto& phiNodeVariable : phiNodeVariables) + { + std::string mappedVariableName = getNextVariableName(phiNodeVariable); + auto blockSpecificVarNames = RefinementUtils::SelectString(previousBlocks, [&](const std::string& blockName) { + return variablesMappingsPerBlock.at(blockName).at(phiNodeVariable); + }); + + auto createPhiRes = createPhiNodeWithoutCreatedBinders(phiNodeVariable, mappedVariableName, variableTypes.at(phiNodeVariable), blockSpecificVarNames, previousBlocks); + if (!createPhiRes.Succeeded) { return createPhiRes; } + + variablesMappingsPerBlock[currentBlockName][phiNodeVariable] = mappedVariableName; + variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); + } + + return ResultType::Success(); + } + ResultType VariablesEnvironment::ToStringOrFailure(std::string& output) + { + auto endBlockRes = endBlock(currentBlockName); + if (!endBlockRes.Succeeded) { return endBlockRes; } + + return constraintBuilder.ToStringOrFailure(output); + } } From 9e9831c9b439e8efe64363718bfaada56e1c5ece Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Sat, 28 Oct 2017 23:58:52 -0400 Subject: [PATCH 09/20] Add an example file - VariableEnvLibImmutable.cpp. Fix compilation errors. Compilation woks. --- .../VariablesEnvironmentImmutable.h | 4 +- .../VariablesEnvironmentImmutable.cpp | 50 ++++++++++--------- .../VariableEnvLibImmutable.cpp | 43 ++++++++++++++++ 3 files changed, 71 insertions(+), 26 deletions(-) create mode 100644 tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp diff --git a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h index 43783c0465e3d..df3ec8365148c 100644 --- a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h +++ b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h @@ -21,7 +21,7 @@ namespace liquid const std::string TargetFutureVariable; PhiNodeObligation() {} - PhiNodeObligation(const std::string variableSource, const std::string targetFutureVariable) : VariableSource(variableSource), TargetFutureVairable(targetFutureVariable) {} + PhiNodeObligation(const std::string variableSource, const std::string targetFutureVariable) : VariableSource(variableSource), TargetFutureVariable(targetFutureVariable) {} }; class VariablesEnvironmentImmutable @@ -31,7 +31,7 @@ namespace liquid const FunctionBlockGraph& functionBlockGraph; std::map variableTypes; - std::map> variablesMappingPerBlock; + std::map> variablesMappingsPerBlock; std::map> variablesValuesPerBlock; std::set finishedBlocks; diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index d40e76eff2171..21c48d22cddd4 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -2,10 +2,11 @@ #include "llvm/Transforms/LiquidFixpointBuilder/RefinementUtils.h" #include #include +#include using namespace std::literals::string_literals; -namepsace liquid +namespace liquid { // Check whether a variable is defined bool VariablesEnvironmentImmutable::IsVariableDefined(std::string variableName) @@ -18,7 +19,7 @@ namepsace liquid { assert(RefinementUtils::ContainsKey(variablesMappingsPerBlock, currentBlockName)); assert(RefinementUtils::ContainsKey(variablesMappingsPerBlock[currentBlockName], variableName)); - return variablesMappingPerBlock[currentBlockName][variableName]; + return variablesMappingsPerBlock[currentBlockName][variableName]; } // Get the address of the variable @@ -37,7 +38,7 @@ namepsace liquid } // Assign a Type to a pre-existing variable, or give a variable a new Type - void insertOrAssignType(std::map& mapToUse, const std::string& variable, const FixpointType& type) + void insertOrAssignVarType(std::map& mapToUse, const std::string& variable, const FixpointType& type) { auto search = mapToUse.find(variable); if (search!= mapToUse.end()) { @@ -62,7 +63,7 @@ namepsace liquid if (!createBinderRes.Succeeded) { return createBinderRes; } } - insertOrAssignType(variableTypes, variable, type); + insertOrAssignVarType(variableTypes, variable, type); variablesMappingsPerBlock[currentBlockName][variable] = mappedVariableName; variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); @@ -94,7 +95,7 @@ namepsace liquid } // Create a Variable - ResultType VariablesEnvironmentImmutable::CreateVariable( + ResultType VariablesEnvironmentImmutable::createVariable( const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, @@ -119,7 +120,7 @@ namepsace liquid // Make an assignment to the variable { std::string constraintName = "Variable_"s + mappedVariableName + "_Assignment"s; - auto addConstRes = constraintBuilder.AddConstraintForAssignment(constaintName, mappedVariableName, expression, currVariablesAndInfo); + auto addConstRes = constraintBuilder.AddConstraintForAssignment(constraintName, mappedVariableName, expression, currVariablesAndInfo); if (!addConstRes.Succeeded) { return addConstRes; } } @@ -138,12 +139,12 @@ namepsace liquid std::vector constraints, std::string expression) { - if (RefinementUtils::ConstainsKey(variableTypes, variable)) + if (RefinementUtils::ContainsKey(variableTypes, variable)) { return ResultType::Error("Variable"s + variable + " already exists."s); } - return CreateVariable(variable, variable, type, constraints, expression); + return createVariable(variable, variable, type, constraints, expression); } ResultType VariablesEnvironmentImmutable::AddJumpInformation(const std::string& targetBlock) @@ -157,7 +158,7 @@ namepsace liquid return ResultType::Success(); } - ResultType VariablesEnvironment::AddBranchinformation(const std::string& booleanVariable, const bool variableValue, const std::string& targetBlock) + ResultType VariablesEnvironmentImmutable::AddBranchInformation(const std::string& booleanVariable, const bool variableValue, const std::string& targetBlock) { // Verify the variable doesn't already exist if (!RefinementUtils::ContainsKey(variableTypes, booleanVariable)) @@ -176,8 +177,8 @@ namepsace liquid const std::string transitionGuardName = "__transition__"s + currentBlockName + "__"s + targetBlock; { - auto createbinderRes = constraintBuilder.CreateBinderWithConstraints(transitionGuardName, FixpointType::GetBoolType(), { assignedExpr }); - if (!createdBinderRes.Succeeded) { return createBinderRes; } + auto createdBinderRes = constraintBuilder.CreateBinderWithConstraints(transitionGuardName, FixpointType::GetBoolType(), { assignedExpr }); + if (!createdBinderRes.Succeeded) { return createdBinderRes; } } return ResultType::Success(); @@ -201,7 +202,7 @@ namepsace liquid { bool dominated; { - auto domRes = functionBlockGraph.StrictlyDominates(previousFinishedBlock, previousUnfinishedBlock, dominate); + auto domRes = functionBlockGraph.StrictlyDominates(previousFinishedBlock, previousUnfinishedBlock, dominated); if (!domRes.Succeeded) { return domRes; } } @@ -289,7 +290,7 @@ namepsace liquid return ResultType::Success(); } - ResultType VariablesEnvironmentImmutable::createPhiNodewithoutCreatedBinders(const std::string& variable, vonst std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks) + ResultType VariablesEnvironmentImmutable::createPhiNodeWithoutCreatedBinders(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks) { if (sourceVariableNames.size() != previousBlocks.size()) { @@ -298,11 +299,11 @@ namepsace liquid { auto currVariablesAndInfo = getBlockBinders(currentBlockName); - auto createBinderRes = constraintBuilder.CreatebinderWithUnkownType(mappedVariableName, type, currVariablesAndInfo); + auto createBinderRes = constraintBuilder.CreateBinderWithUnknownType(mappedVariableName, type, currVariablesAndInfo); if (!createBinderRes.Succeeded) { return createBinderRes; } } - for (size_t i = 0, csize = previosBlocks.size(); i < csize; i++) + for (size_t i = 0, csize = previousBlocks.size(); i < csize; i++) { auto& previousBlock = previousBlocks[i]; std::vector blockVariablesAndInfo; @@ -329,12 +330,12 @@ namepsace liquid std::string assignedExpr = "__value == "s + variableName; - auto addConstres = constraintBuilder.AddConstraintForAssignment(constraintName, mappedVariableName, assignedExpr, blockVariablesAndInfo); + auto addConstRes = constraintBuilder.AddConstraintForAssignment(constraintName, mappedVariableName, assignedExpr, blockVariablesAndInfo); if (!addConstRes.Succeeded) { return addConstRes; } } variablesMappingsPerBlock[currentBlockName][variable] = mappedVariableName; - variablesValuesPerBlock[currentBlockName].emplace_back(mappedVariableName); + variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); return ResultType::Success(); } @@ -343,9 +344,9 @@ namepsace liquid const std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, - const std::vector& previousblocks) + const std::vector& previousBlocks) { - if (sourceVariablesNames.size() != previousBlocks.size()) + if (sourceVariableNames.size() != previousBlocks.size()) { return ResultType::Error("Expected phi node variables and associated block size to be the same"s); } @@ -423,7 +424,7 @@ namepsace liquid return ResultType::Success(); } - ResultType VariablesEnvironment::addVariableToBlockAndSuccessors(const std::string& blockName, const std::string& transitionGuardName) + ResultType VariablesEnvironmentImmutable::addVariableToBlockAndSuccessors(const std::string& blockName, const std::string& transitionGuardName) { std::vector successors; { @@ -440,7 +441,7 @@ namepsace liquid return ResultType::Success(); } - ResultType VariablesEnvironment::initializeBlockGuards() + ResultType VariablesEnvironmentImmutable::initializeBlockGuards() { std::vector blockNames; { @@ -507,7 +508,7 @@ namepsace liquid return ResultType::Success(); } - ResultType VariablesEnvironment::StartBlock(const std::string& blockName) + ResultType VariablesEnvironmentImmutable::StartBlock(const std::string& blockName) { if (currentBlockName == ""s) { @@ -562,7 +563,8 @@ namepsace liquid // Add to the environment any variables which require phi nodes for (auto& phiNodeVariable : phiNodeVariables) { - std::string mappedVariableName = getNextVariableName(phiNodeVariable); + // Initialize the counter for the PhiNodevariable to be 0. Immutability => No increment. + std::string mappedVariableName = phiNodeVariable + "__"s + std::to_string(0); auto blockSpecificVarNames = RefinementUtils::SelectString(previousBlocks, [&](const std::string& blockName) { return variablesMappingsPerBlock.at(blockName).at(phiNodeVariable); }); @@ -577,7 +579,7 @@ namepsace liquid return ResultType::Success(); } - ResultType VariablesEnvironment::ToStringOrFailure(std::string& output) + ResultType VariablesEnvironmentImmutable::ToStringOrFailure(std::string& output) { auto endBlockRes = endBlock(currentBlockName); if (!endBlockRes.Succeeded) { return endBlockRes; } diff --git a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp new file mode 100644 index 0000000000000..d182ae49463fb --- /dev/null +++ b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp @@ -0,0 +1,43 @@ +#include +#include + +#include "llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h" +using namespace liquid; + +std::string format(VariablesEnvironmentImmutable& env, std::string expression) +{ + std::regex r("\\{\\{(.+?)\\}\\}"); + std::smatch m; + + while (std::regex_search(expression, m, r)) { + std::string varname = m[1]; + std::string replacement = env.GetVariableName(varname); + expression = m.prefix().str() + replacement + m.suffix().str(); + } + + return expression; +} + +// int ifImmutableExample(); +// int ifThenElseExample(); +// int forLoopExample(); + +int main() +{ + int a; + std::cout << "Enter a number" << std::endl; + std::cout << "1 for (immutable) example with if" << std::endl; + std::cout << "Choice: "; + std::cin >> a; + + if(a == 1) + { + // return ifImmutableExample(); + return 0; + } + else + { + std::cout << "Example not available" << std::endl; + return -1; + } +} From c80171238e08b31d6b718b3781c8fe3c4ccef6bb Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Sun, 29 Oct 2017 21:59:22 -0400 Subject: [PATCH 10/20] Add example --- .../VariableEnvLib_IfImmutableExample.cpp | 90 +++++++++++++++++++ 1 file changed, 90 insertions(+) create mode 100644 tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp diff --git a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp new file mode 100644 index 0000000000000..8826beac263e5 --- /dev/null +++ b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp @@ -0,0 +1,90 @@ +#include "llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h" +#include "llvm/Transforms/LiquidFixpointBuilder/FunctionBlockGraph.h" +#include "llvm/Transforms/LiquidFixpointBuilder/ResultType.h" +#include +#include + +using namespace liquid; +using namespace std::literals::string_literals; + +class LLVMFunctionBlockGraph_IfImmutable: public FunctionBlockGraph +{ +public: + std::string GetStartingBlockName() const + { + return "entry"s; + } + + ResultType GetSuccessorBlocks(const std::string& blockName, std::vector& successorBlocks) const + { + if (blockName == "entry") + { + successorBlocks.emplace_back("if.then"); + successorBlocks.emplace_back("if.end"); + } + else if (blockName == "if.then") + { + successorBlocks.emplace_back("if.end"); + } + else if (blockName == "if.end") + { + } + else + { + return ResultType::Error("NA"); + } + + return ResultType::Success(); + } + + ResultType SttrictlyDominates(const std::string& firstBlockName, const std::string& secondBlockName, bool& result) const + { + result = (firstBlockName == "entry" && secondBlockName != "entry"); + return ResultType::Success(); + } +}; + +std::string format(VariablesEnvironmentImmutable& env, std::string expression); + +#define E(exp) \ +{\ + ResultType a = exp; \ + if (!a.Succeeded) { str = a.ErrorMsg; goto errh; } \ +} + +int ifImmutableExample() +{ + LLVMFunctionBlockGraph_IfImmutable llvmFunctionBlockGraph; + VariablesEnvironment env(llvmFunctionBlockGraph); + + std::string str; + + E(env.StartBlock("entry"s)); + + E(env.CreateImmutableInputVariable("a"s, FixpointType::GetIntType(), { "__value == 4"s })); + + E(env.CreateImmutableVariable("b"s, FixpointType::GetIntType(), {}, format(env, " __value == 5"s))); + + E(env.CreateImmutableVariable("c"s, FixpointType::GetIntType(), {}, format(env, " __value == 6"s))); + + E(env.CreateImmutableVariable("cmp"s, FixpointType::GetBoolType(), {}, format(env, " __value <=> {{a}} == 4"s))); + + E(env.AddBranchInformation("cmp"s, true, "if.then")); + E(env.AddBranchinformation("cmp"s, false, "if.end")); + + E(env.StartBlock("if.then"s)); + E(env.CreateImmutableVariable("d"s, FixpointType::GetIntType(), {}, format(env, "__value == {{b}}"s))); + E(env.AddJumpInformation("if.end"s)); + + E(env.StartBlock("if.end"s)); + E(env.CreatePhiNode("e"s, FixpointType::GetIntType(), { "c"s, "d"s }, { "entry"s, "if.then"s })); + + E(env.ToStringOrFailure(str)); + + std::cout << "Succeeded:" << std::endl << str; + return 0; + +errh: + std::cout << "Failed:" << std::endl << str; + return -1; +} From d9dad8725886d63c1abe94f9fa580c967c700397 Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Sat, 25 Nov 2017 19:21:51 -0500 Subject: [PATCH 11/20] Remove PhiNodeObligation --- .../VariablesEnvironmentImmutable.h | 12 ------------ .../VariablesEnvironmentImmutable.cpp | 12 ------------ 2 files changed, 24 deletions(-) diff --git a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h index df3ec8365148c..292af33107624 100644 --- a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h +++ b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h @@ -13,17 +13,6 @@ using namespace std::literals::string_literals; namespace liquid { - - class PhiNodeObligation - { - public: - const std::string VariableSource; - const std::string TargetFutureVariable; - - PhiNodeObligation() {} - PhiNodeObligation(const std::string variableSource, const std::string targetFutureVariable) : VariableSource(variableSource), TargetFutureVariable(targetFutureVariable) {} - }; - class VariablesEnvironmentImmutable { private: @@ -35,7 +24,6 @@ namespace liquid std::map> variablesValuesPerBlock; std::set finishedBlocks; - std::map> phiNodeObligations; std::set outputVariables; diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index 21c48d22cddd4..0de3b2b52bee7 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -492,18 +492,6 @@ namespace liquid ResultType VariablesEnvironmentImmutable::endBlock(const std::string& blockName) { - auto& phiNodeObligationsForBlock = phiNodeObligations[blockName]; - - for (const auto& phiNodeObligation : phiNodeObligationsForBlock) - { - auto expression = "__value == "s + GetVariableName(phiNodeObligation.VariableSource); - auto currentMapping = phiNodeObligation.TargetFutureVariable; - auto createRes = CreateImmutableVariable(currentMapping, variableTypes.at(phiNodeObligation.VariableSource), {}, expression); - if (!createRes.Succeeded) { return createRes; }; - } - - phiNodeObligationsForBlock.clear(); - finishedBlocks.emplace(blockName); return ResultType::Success(); } From 614be5c061c93ee3ff6477854c708b4d9f8b36f0 Mon Sep 17 00:00:00 2001 From: jssandh2 Date: Mon, 25 Dec 2017 13:06:56 -0800 Subject: [PATCH 12/20] Changes: Part-1 --- .../VariablesEnvironmentImmutable.h | 4 -- .../VariablesEnvironmentImmutable.cpp | 42 +++++-------------- 2 files changed, 11 insertions(+), 35 deletions(-) diff --git a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h index 292af33107624..a64a7a3d934f8 100644 --- a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h +++ b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h @@ -20,13 +20,10 @@ namespace liquid const FunctionBlockGraph& functionBlockGraph; std::map variableTypes; - std::map> variablesMappingsPerBlock; std::map> variablesValuesPerBlock; std::set finishedBlocks; - std::set outputVariables; - std::map cachedBlockGuards; ResultType createVariable(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& constaints, const std::string& expression); @@ -57,7 +54,6 @@ namespace liquid ResultType CreatePhiNode(const std::string& variable, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks); bool IsVariableDefined(std::string variableName); - std::string GetVariableName(std::string variableName); std::string GetVariableAddress(std::string variableName); ResultType ToStringOrFailure(std::string& output); }; diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index 0de3b2b52bee7..59e6512f44f35 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -13,14 +13,6 @@ namespace liquid { return RefinementUtils::ContainsKey(variableTypes, variableName); } - - // Get the name of the variable - std::string VariablesEnvironmentImmutable::GetVariableName(const std::string variableName) - { - assert(RefinementUtils::ContainsKey(variablesMappingsPerBlock, currentBlockName)); - assert(RefinementUtils::ContainsKey(variablesMappingsPerBlock[currentBlockName], variableName)); - return variablesMappingsPerBlock[currentBlockName][variableName]; - } // Get the address of the variable std::string VariablesEnvironmentImmutable::GetVariableAddress(std::string variableName) @@ -56,6 +48,7 @@ namespace liquid return ResultType::Error("Variable"s + variable + " already exists."s); } + // @TODO::(Juspreet) - Is this really necessary ? `variable` is already a const reference. std::string mappedVariableName = variable; { @@ -64,7 +57,7 @@ namespace liquid } insertOrAssignVarType(variableTypes, variable, type); - variablesMappingsPerBlock[currentBlockName][variable] = mappedVariableName; + // @TODO::(Juspreet) - Is the Environment of bindings in a block ordered ? If so, is it FIFO/LIFO ? variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); return ResultType::Success(); @@ -76,20 +69,8 @@ namespace liquid const FixpointType& type, const std::vector& constraints) { - auto createRes = createIOVariable(variable, type, constraints); - if (!createRes.Succeeded) { return createRes; } - - // Since, this is an input variable make it accessible to every block - auto internalVarName = GetVariableName(variable); - - for (auto& blockVarMap : variablesMappingsPerBlock) - { - if (!RefinementUtils::ContainsKey(blockVarMap.second, variable)) - { - blockVarMap.second[variable] = internalVarName; - variablesValuesPerBlock[blockVarMap.first].emplace(internalVarName); - } - } + auto createRes = createIOVariable(variable, type, constraints); + if (!createRes.Succeeded) { return createRes; } return ResultType::Success(); } @@ -119,14 +100,13 @@ namespace liquid // Make an assignment to the variable { - std::string constraintName = "Variable_"s + mappedVariableName + "_Assignment"s; - auto addConstRes = constraintBuilder.AddConstraintForAssignment(constraintName, mappedVariableName, expression, currVariablesAndInfo); + std::string assignmentConstraintName = "Variable_"s + mappedVariableName + "_Assignment"s; + auto addConstRes = constraintBuilder.AddConstraintForAssignment(assignmentConstraintName, mappedVariableName, expression, currVariablesAndInfo); if (!addConstRes.Succeeded) { return addConstRes; } } // Make updates to Variable Mappings and Values for State Update of the Block insertOrAssignVarType(variableTypes, variable, type); - variablesMappingsPerBlock[currentBlockName][variable] = mappedVariableName; variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); return ResultType::Success(); @@ -160,19 +140,19 @@ namespace liquid ResultType VariablesEnvironmentImmutable::AddBranchInformation(const std::string& booleanVariable, const bool variableValue, const std::string& targetBlock) { - // Verify the variable doesn't already exist + // Verify the variable doesn't already exist. if (!RefinementUtils::ContainsKey(variableTypes, booleanVariable)) { return ResultType::Error("Missing variable: "s + booleanVariable); } - // Enforce the variable type is Boolean + // Enforce the variable type is Boolean. if (variableTypes.at(booleanVariable) != FixpointType::GetBoolType()) { return ResultType::Error("Expected boolean type for variable: "s + booleanVariable); } - // Convert the variable into a Proposition for a Fixpoint Constraint + // Convert the variable into a Proposition for a Fixpoint Constraint. const std::string assignedExpr = "__value <=> "s + (variableValue ? ""s : "~"s) + booleanVariable; const std::string transitionGuardName = "__transition__"s + currentBlockName + "__"s + targetBlock; @@ -195,10 +175,10 @@ namespace liquid // Ensure that : // 1) forall blocks in PreviousFinishedBlocks, dominate(blocks, block), forall block in PreviousUnfinishedblocks - for (const auto& previousUnfinishedBlock : previousFinishedBlocks) + for (const auto& previousfinishedBlock : previousFinishedBlocks) { bool allDominated = true; - for (const auto& previousFinishedBlock : previousUnfinishedBlocks) + for (const auto& previousUnfinishedBlock : previousUnfinishedBlocks) { bool dominated; { From c9788403f70fa6d5c29705889237f518f5fd096a Mon Sep 17 00:00:00 2001 From: jssandh2 Date: Mon, 25 Dec 2017 16:07:58 -0800 Subject: [PATCH 13/20] Changes: Part 2 --- .../LiquidFixpointBuilder/RefinementUtils.h | 9 ++- .../VariablesEnvironmentImmutable.h | 2 +- .../VariablesEnvironmentImmutable.cpp | 81 +++++++++++++------ 3 files changed, 66 insertions(+), 26 deletions(-) diff --git a/include/llvm/Transforms/LiquidFixpointBuilder/RefinementUtils.h b/include/llvm/Transforms/LiquidFixpointBuilder/RefinementUtils.h index cd26fb88a59c0..3a7caea0d51ce 100644 --- a/include/llvm/Transforms/LiquidFixpointBuilder/RefinementUtils.h +++ b/include/llvm/Transforms/LiquidFixpointBuilder/RefinementUtils.h @@ -130,7 +130,14 @@ namespace liquid { std::transform(m.begin(), m.end(), std::back_inserter(ret), [](const typename std::map::value_type& val) { return val.second; }); return ret; } + + template + static inline std::set GetValuesSet(const std::vector& v) + { + std::set s(v.begin(), v.end()); + return s; + } }; } -#endif \ No newline at end of file +#endif diff --git a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h index a64a7a3d934f8..440e69917d0a4 100644 --- a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h +++ b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h @@ -21,7 +21,7 @@ namespace liquid std::map variableTypes; - std::map> variablesValuesPerBlock; + std::map> variablesValuesPerBlock; std::set finishedBlocks; std::map cachedBlockGuards; diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index 59e6512f44f35..d69b364784111 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -164,17 +164,17 @@ namespace liquid return ResultType::Success(); } + // @TODO::(Juspreet) - The function is not used anywhere in the immutable construct (yet). Verify if it can be ripped off. ResultType VariablesEnvironmentImmutable::validateFinishedAndUnfinishedBlockStates( const std::vector& previousFinishedBlocks, const std::vector& previousUnfinishedBlocks) { - //@TODO::(juspreet) - The logic is odd. It might be the cause of problem in loops. Verify. if (previousFinishedBlocks.size() == 0 || previousFinishedBlocks.size() > 1) { return ResultType::Error("Blocks were not completed in the right order. Expected one Completed Block, got "s + std::to_string(previousFinishedBlocks.size())); } // Ensure that : - // 1) forall blocks in PreviousFinishedBlocks, dominate(blocks, block), forall block in PreviousUnfinishedblocks + // 1) forall blocks in PreviousFinishedBlocks, dominate(blocks, block), forall block in PreviousUnfinishedblocks. for (const auto& previousfinishedBlock : previousFinishedBlocks) { bool allDominated = true; @@ -193,7 +193,7 @@ namespace liquid } } - // If all blocks are not dominated, then exit with an appropriate error message + // If all blocks are not dominated, then exit with an appropriate error message. if (!allDominated) { return ResultType::Error("Blocks were not completed in the right order. Unexpected control flow graph. Finished: "s @@ -211,6 +211,7 @@ namespace liquid std::vector previousFinishedBlocks; std::vector previousUnfinishedBlocks; + // Iterate through previousBlocks, and build the finished and unfinished blocks. for (auto& previousBlock: previousBlocks) { RefinementUtils::Contains(finishedBlocks, previousBlock) ? @@ -218,32 +219,69 @@ namespace liquid previousUnfinishedBlocks.push_back(previousBlock); } - // In a CFG, it is possible that previous blocks aren't _all_ processed (loops) + // In a CFG, it is possible that previous blocks aren't _all_ processed (loops). // However, for immutable constructs, this shouldn't happen. Raise an Error, if it does. + + // @TODO::(Juspreet) - If there are supposed to be 0 previousUnfinishedBlocks, then what are we to check the Linear Order with respect to ? + // Currently - The linear order is checked to verify all finishedBlocks have been finished to respect the Partial Order. if (previousUnfinishedBlocks.size() > 0) { - return ResultType::Error("There exist: "s + std::to_string(previousUnfinishedBlocks.size()) + " unfinished Block that were appended without processing. This is an error in an immutable environment."s); + return ResultType::Error("There exist: "s + std::to_string(previousUnfinishedBlocks.size()) + " unfinished Block/s that were appended without processing. This is an error in an immutable environment."s); } bool first = true; - for (auto& previousBlock : previousBlocks) + for (int i = 0; i < previousFinishedBlocks.size(); i++) { + auto& currFinishedBlock = previousFinishedBlocks[i]; + + // Verify that the block and its values are present in the known blocks. + if (!RefinementUtils::Contains(variableValuesPerBlock, currFinishedBlock)) { + return ResultType::Error("The Block: "s + std::to_string(currFinishedBlock) + " violates the processing order."s); + } + if (first) { - commonVariables = RefinementUtils::GetKeysSet(variablesMappingsPerBlock[previousBlock]); + std::set commonVariables = RefinementUtils::GetValuesSet(variableValuesPerBlock[currFinishedBlock]); first = false; - } - else - { - std::set currBlockVars = RefinementUtils::GetKeysSet(variablesMappingsPerBlock[previousBlock]); + } else { + std::set currBlockVars = RefinementUtils::GetValuesSet(variablesValuesPerBlock[currFinishedBlock]); + + // @TODO::(Juspreet) - This can be optimized from O(n^{2}) -> O(n(lg(n)) by defining an overloaded operator on `StrictlyDominates`, sorting, and asserting list equality. + for (int j = 0; j < i - 1; j++) + { + auto& previousFinishedBlock = previousFinishedBlocks[j]; + + bool dominated; + { + auto domRes = functionBlockGraph.StrictlyDominates(previousFinishedBlock, currFinishedBlock, dominated); + if (!domRes.Succeeded) { return domRes; } + } + + if (!dominated) { + allDominated = false; + break; + } + + } + + // If all blocks are not dominated, then exit with an appropriate error message. + if (!allDominated) + { + return ResultType::Error("Blocks were not completed in the right order. Unexpected control flow graph. Finished: "s + + RefinementUtils::StringJoin(", "s, previousFinishedBlocks) + + " . Unfinished: "s + + RefinementUtils::StringJoin(", "s, previousUnfinishedBlocks) + ); + } + commonVariables = RefinementUtils::SetIntersection(commonVariables, currBlockVars); } } + return ResultType::Success(); } - //@TODO::juspreet - Continue ripping and verifying. ResultType VariablesEnvironmentImmutable::getBlockBindersForPhiNode(const std::string& previousBlock, const std::string& blockName, const std::string& mappedVariableName, std::vector& binders) { binders = getBlockBinders(previousBlock); @@ -270,7 +308,7 @@ namespace liquid return ResultType::Success(); } - ResultType VariablesEnvironmentImmutable::createPhiNodeWithoutCreatedBinders(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks) + ResultType VariablesEnvironmentImmutable::createPhiNodeAssumingNoFutureBinders(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks) { if (sourceVariableNames.size() != previousBlocks.size()) { @@ -293,7 +331,7 @@ namespace liquid } auto blockVariableMapping = sourceVariableNames[i]; - // Ensure that the future binder is part of the current info + // Ensure that the future binder is part of the current info. if (!RefinementUtils::Contains(blockVariablesAndInfo, blockVariableMapping)) { blockVariablesAndInfo.push_back(blockVariableMapping); @@ -301,12 +339,8 @@ namespace liquid std::string constraintName = "Variable_"s + previousBlock + "_"s + currentBlockName + "_"s + mappedVariableName; - // Create Variable Mappings for Future Binders (which are immutable) + // Create Variable Mappings for Future Binders (which are immutable). std::string variableName = blockVariableMapping; - if (RefinementUtils::ContainsKey(variablesMappingsPerBlock[previousBlock], blockVariableMapping)) - { - variableName = variablesMappingsPerBlock[previousBlock][blockVariableMapping]; - } std::string assignedExpr = "__value == "s + variableName; @@ -314,7 +348,6 @@ namespace liquid if (!addConstRes.Succeeded) { return addConstRes; } } - variablesMappingsPerBlock[currentBlockName][variable] = mappedVariableName; variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); return ResultType::Success(); } @@ -331,14 +364,14 @@ namespace liquid return ResultType::Error("Expected phi node variables and associated block size to be the same"s); } - //Check if any parts of the phi node are variables that are not yet declared + // Check if any parts of the phi node are variables that are not yet declared. for (size_t i = 0, csize = previousBlocks.size(); i < csize; i++) { auto& previousBlock = previousBlocks[i]; auto blockVariableMapping = sourceVariableNames[i]; - //variable of a phi node hasn't been created yet - if (!RefinementUtils::ContainsKey(variablesMappingsPerBlock[previousBlock], blockVariableMapping)) + // Variable of a phi node hasn't been created yet. + if (!RefinementUtils::ContainsKey(variablesValuesPerBlock[previousBlock], blockVariableMapping)) { auto futureBinderRes = constraintBuilder.CreateFutureBinder(blockVariableMapping, type); if (!futureBinderRes.Succeeded) { return futureBinderRes; } @@ -354,7 +387,7 @@ namespace liquid return createPhiNodeInternal(variable, mappedVariableName, type, sourceVariableNames, previousBlocks); } - //@TODO:: (juspreet) - The recursive call here isn't clear. Verify. + //@TODO::(Juspreet) - Replace with Fixpoint Algorithm. To come in Part-3. ResultType VariablesEnvironmentImmutable::getBlockGuard(const std::string& blockName, std::string& blockGuard) { if (RefinementUtils::ContainsKey(cachedBlockGuards, blockName)) From a7bf894e62c4d93c37982045e9dea92cac1ed78f Mon Sep 17 00:00:00 2001 From: jssandh2 Date: Mon, 25 Dec 2017 16:19:32 -0800 Subject: [PATCH 14/20] Remove the old function --- .../VariablesEnvironmentImmutable.cpp | 68 ------------------- 1 file changed, 68 deletions(-) diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index d69b364784111..9337c2b892793 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -137,74 +137,6 @@ namespace liquid return ResultType::Success(); } - - ResultType VariablesEnvironmentImmutable::AddBranchInformation(const std::string& booleanVariable, const bool variableValue, const std::string& targetBlock) - { - // Verify the variable doesn't already exist. - if (!RefinementUtils::ContainsKey(variableTypes, booleanVariable)) - { - return ResultType::Error("Missing variable: "s + booleanVariable); - } - - // Enforce the variable type is Boolean. - if (variableTypes.at(booleanVariable) != FixpointType::GetBoolType()) - { - return ResultType::Error("Expected boolean type for variable: "s + booleanVariable); - } - - // Convert the variable into a Proposition for a Fixpoint Constraint. - const std::string assignedExpr = "__value <=> "s + (variableValue ? ""s : "~"s) + booleanVariable; - const std::string transitionGuardName = "__transition__"s + currentBlockName + "__"s + targetBlock; - - { - auto createdBinderRes = constraintBuilder.CreateBinderWithConstraints(transitionGuardName, FixpointType::GetBoolType(), { assignedExpr }); - if (!createdBinderRes.Succeeded) { return createdBinderRes; } - } - - return ResultType::Success(); - } - - // @TODO::(Juspreet) - The function is not used anywhere in the immutable construct (yet). Verify if it can be ripped off. - ResultType VariablesEnvironmentImmutable::validateFinishedAndUnfinishedBlockStates( - const std::vector& previousFinishedBlocks, - const std::vector& previousUnfinishedBlocks) - { - if (previousFinishedBlocks.size() == 0 || previousFinishedBlocks.size() > 1) { - return ResultType::Error("Blocks were not completed in the right order. Expected one Completed Block, got "s + std::to_string(previousFinishedBlocks.size())); - } - - // Ensure that : - // 1) forall blocks in PreviousFinishedBlocks, dominate(blocks, block), forall block in PreviousUnfinishedblocks. - for (const auto& previousfinishedBlock : previousFinishedBlocks) - { - bool allDominated = true; - for (const auto& previousUnfinishedBlock : previousUnfinishedBlocks) - { - bool dominated; - { - auto domRes = functionBlockGraph.StrictlyDominates(previousFinishedBlock, previousUnfinishedBlock, dominated); - if (!domRes.Succeeded) { return domRes; } - } - - if (!dominated) - { - allDominated = false; - break; - } - } - - // If all blocks are not dominated, then exit with an appropriate error message. - if (!allDominated) - { - return ResultType::Error("Blocks were not completed in the right order. Unexpected control flow graph. Finished: "s - + RefinementUtils::StringJoin(", "s, previousFinishedBlocks) - + " . Unfinished: "s - + RefinementUtils::StringJoin(", "s, previousUnfinishedBlocks) - ); - } - } - return ResultType::Success(); - } ResultType VariablesEnvironmentImmutable::getCommonVariables(std::vector previousBlocks, std::set& commonVariables) { From 360693f03013ea7b320d73bc5658f72e02a6fd6b Mon Sep 17 00:00:00 2001 From: Jus Date: Thu, 25 Jan 2018 18:02:44 -0500 Subject: [PATCH 15/20] NOTE: This does not compile. The blockguard fix is en-route. Part-1. --- .../VariablesEnvironmentImmutable.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index 9337c2b892793..a46ed0f839f7d 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -379,7 +379,6 @@ namespace liquid for (const auto& successor : successors) { - variablesMappingsPerBlock[successor][transitionGuardName] = transitionGuardName; variablesValuesPerBlock[successor].emplace(transitionGuardName); } @@ -475,10 +474,17 @@ namespace liquid } // Add to the environment any variables which are unchanged in predecessors + // This block of code is hazy at best --> We may need to revisit it during for-loops. However, for now: + // *NO* variable that is assigned to can be changed. This is enforced in immutability (with the exception of for-loops). std::set phiNodeVariables; for (auto& commonVariable : commonVariables) { - bool usingIdenticalMappings = std::all_of(previousBlocks.begin(), previousBlocks.end(), [&](std::string block) { + bool usingIdenticalMappings = true; + + for (auto& currPreviousBlock: previousBlocks) + { + std::set currPreviousBlockValueSet = RefinementUtils::GetValuesSet(variablesValuesPerBlock[ + std::all_of(previousBlocks.begin(), previousBlocks.end(), [&](std::string block) { return variablesMappingsPerBlock[block][commonVariable] == variablesMappingsPerBlock[previousBlocks[0]][commonVariable]; }); From 0812e28dcffcb929445eae8953a25632a27a4d1e Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Thu, 25 Jan 2018 23:07:02 -0500 Subject: [PATCH 16/20] Large Changes: Part-1 --- .../VariablesEnvironmentImmutable.cpp | 45 ++++++++++++++++--- .../VariableEnvLib_IfImmutableExample.cpp | 4 +- 2 files changed, 41 insertions(+), 8 deletions(-) diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index a46ed0f839f7d..22a3ed3e8ba3f 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -137,6 +137,32 @@ namespace liquid return ResultType::Success(); } + + ResultType VariablesEnvironmentImmutable::AddBranchInformation(const std::string& booleanVariable, const bool variableValue, const std::string& targetBlock) + { + // Verify the variable doesn't already exist. + if (!RefinementUtils::ContainsKey(variableTypes, booleanVariable)) + { + return ResultType::Error("Missing variable: "s + booleanVariable); + } + + // Enforce the variable type is Boolean. + if (variableTypes.at(booleanVariable) != FixpointType::GetBoolType()) + { + return ResultType::Error("Expected boolean type for variable: "s + booleanVariable); + } + + // Convert the variable into a Proposition for a Fixpoint Constraint. + const std::string assignedExpr = "__value <=> "s + (variableValue ? ""s : "~"s) + booleanVariable; + const std::string transitionGuardName = "__transition__"s + currentBlockName + "__"s + targetBlock; + + { + auto createdBinderRes = constraintBuilder.CreateBinderWithConstraints(transitionGuardName, FixpointType::GetBoolType(), { assignedExpr }); + if (!createdBinderRes.Succeeded) { return createdBinderRes; } + } + + return ResultType::Success(); + } ResultType VariablesEnvironmentImmutable::getCommonVariables(std::vector previousBlocks, std::set& commonVariables) { @@ -481,17 +507,24 @@ namespace liquid { bool usingIdenticalMappings = true; + // Extract the variable values in the most current previous block as a set. + std::set recentPreviousBlockValueSet = RefinementUtils::GetValuesSet(variablesValuesPerBlock[previousBlocks[0]]); + for (auto& currPreviousBlock: previousBlocks) { - std::set currPreviousBlockValueSet = RefinementUtils::GetValuesSet(variablesValuesPerBlock[ - std::all_of(previousBlocks.begin(), previousBlocks.end(), [&](std::string block) { - return variablesMappingsPerBlock[block][commonVariable] == variablesMappingsPerBlock[previousBlocks[0]][commonVariable]; - }); + // Extract the variable value in the current previous block. + std::set currPreviousBlockValueSet = RefinementUtils::GetValuesSet(variablesValuesPerBlock[currPreviousBlock]); + + // Compare equality and conjunct with the condition. + // Questions: + // i) What to do if the value is in one block and the subsequent one ? + // ii) Is this ever possible, and if not, does this mean an error ? + usingIdenticalMappings = usingIdenticalMappings && (currPreviousBlockValueSet[commonVariable] == recentPreviousBlockValueSet[commonVariable]) + } if (usingIdenticalMappings) { - variablesMappingsPerBlock[currentBlockName][commonVariable] = variablesMappingsPerBlock[previousBlocks[0]][commonVariable]; - variablesValuesPerBlock[currentBlockName].emplace(variablesMappingsPerBlock[previousBlocks[0]][commonVariable]); + variablesValuesPerBlock[currentBlockName].emplace(recentPreviousBlockValueSet[commonVariable]); } else { diff --git a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp index 8826beac263e5..e9b664b44cbf3 100644 --- a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp +++ b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp @@ -37,7 +37,7 @@ class LLVMFunctionBlockGraph_IfImmutable: public FunctionBlockGraph return ResultType::Success(); } - ResultType SttrictlyDominates(const std::string& firstBlockName, const std::string& secondBlockName, bool& result) const + ResultType StrictlyDominates(const std::string& firstBlockName, const std::string& secondBlockName, bool& result) const { result = (firstBlockName == "entry" && secondBlockName != "entry"); return ResultType::Success(); @@ -55,7 +55,7 @@ std::string format(VariablesEnvironmentImmutable& env, std::string expression); int ifImmutableExample() { LLVMFunctionBlockGraph_IfImmutable llvmFunctionBlockGraph; - VariablesEnvironment env(llvmFunctionBlockGraph); + VariablesEnvironmentImmutable env(llvmFunctionBlockGraph); std::string str; From e40f0cca91016ef83e28c3f0c5a2ab0938fee37d Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Sun, 4 Feb 2018 18:25:33 -0500 Subject: [PATCH 17/20] Larg changes: Part 2 --- .../VariablesEnvironmentImmutable.h | 1 - .../VariablesEnvironmentImmutable.cpp | 111 +++++++++--------- 2 files changed, 56 insertions(+), 56 deletions(-) diff --git a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h index 440e69917d0a4..ee57545fb3ab7 100644 --- a/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h +++ b/include/llvm/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.h @@ -42,7 +42,6 @@ namespace liquid ResultType endBlock(const std::string& blockName); public: - Counter FreshState; FixpointConstraintBuilder constraintBuilder; VariablesEnvironmentImmutable(const FunctionBlockGraph& _functionBlockGraph) : functionBlockGraph(_functionBlockGraph) {} diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index 22a3ed3e8ba3f..0379573264c90 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -179,37 +179,35 @@ namespace liquid // In a CFG, it is possible that previous blocks aren't _all_ processed (loops). // However, for immutable constructs, this shouldn't happen. Raise an Error, if it does. - - // @TODO::(Juspreet) - If there are supposed to be 0 previousUnfinishedBlocks, then what are we to check the Linear Order with respect to ? - // Currently - The linear order is checked to verify all finishedBlocks have been finished to respect the Partial Order. if (previousUnfinishedBlocks.size() > 0) { return ResultType::Error("There exist: "s + std::to_string(previousUnfinishedBlocks.size()) + " unfinished Block/s that were appended without processing. This is an error in an immutable environment."s); } bool first = true; + bool allDominated = true; for (int i = 0; i < previousFinishedBlocks.size(); i++) { auto& currFinishedBlock = previousFinishedBlocks[i]; // Verify that the block and its values are present in the known blocks. - if (!RefinementUtils::Contains(variableValuesPerBlock, currFinishedBlock)) { + if (!RefinementUtils::Contains(variablesValuesPerBlock, currFinishedBlock)) { return ResultType::Error("The Block: "s + std::to_string(currFinishedBlock) + " violates the processing order."s); } if (first) { - std::set commonVariables = RefinementUtils::GetValuesSet(variableValuesPerBlock[currFinishedBlock]); + commonVariables = RefinementUtils::GetValuesSet(variablesValuesPerBlock[currFinishedBlock]); first = false; } else { std::set currBlockVars = RefinementUtils::GetValuesSet(variablesValuesPerBlock[currFinishedBlock]); - // @TODO::(Juspreet) - This can be optimized from O(n^{2}) -> O(n(lg(n)) by defining an overloaded operator on `StrictlyDominates`, sorting, and asserting list equality. - for (int j = 0; j < i - 1; j++) + // @TODO::(Juspreet) - This is wrong. This will not work with 'for' loops. Fix as soon as a strategy for Fixpoint is developed. + for (int j = 0; j < i; j++) { auto& previousFinishedBlock = previousFinishedBlocks[j]; - + bool dominated; { auto domRes = functionBlockGraph.StrictlyDominates(previousFinishedBlock, currFinishedBlock, dominated); @@ -266,46 +264,48 @@ namespace liquid return ResultType::Success(); } - ResultType VariablesEnvironmentImmutable::createPhiNodeAssumingNoFutureBinders(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks) + ResultType VariablesEnvironment::createPhiNodeWithoutCreatedBinders(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks) { if (sourceVariableNames.size() != previousBlocks.size()) - { - return ResultType::Error("Expected Phi-Node Variables and associated Block Size to be the sames"s); - } - + { + return ResultType::Error("Expected phi node variables and associated block size to be the same"s); + } + { auto currVariablesAndInfo = getBlockBinders(currentBlockName); auto createBinderRes = constraintBuilder.CreateBinderWithUnknownType(mappedVariableName, type, currVariablesAndInfo); if (!createBinderRes.Succeeded) { return createBinderRes; } } - + for (size_t i = 0, csize = previousBlocks.size(); i < csize; i++) - { - auto& previousBlock = previousBlocks[i]; - std::vector blockVariablesAndInfo; { - auto getBinderRes = getBlockBindersForPhiNode(previousBlock, currentBlockName, mappedVariableName, blockVariablesAndInfo); - if (!getBinderRes.Succeeded) { return getBinderRes; } - } + auto& previousBlock = previousBlocks[i]; + std::vector blockVariablesAndInfo; + { + auto getBindersRes = getBlockBindersForPhiNode(previousBlock, currentBlockName, mappedVariableName, blockVariablesAndInfo); + if (!getBindersRes.Succeeded) { return getBindersRes; } + } + + auto blockVariableMapping = sourceVariableNames[i]; + //ensure that the future binder is part of the info + if (!RefinementUtils::Contains(blockVariablesAndInfo, blockVariableMapping)) + { + blockVariablesAndInfo.push_back(blockVariableMapping); + } + + std::string constraintName = "Variable_"s + previousBlock + "_"s + currentBlockName + "_"s + mappedVariableName; + + //hack - for variables that aren't created yet aka future binders, there will be no mapping, so we will just use the name as is + //we are relying on the fact, that the first variable mapping is the same as the variable name and that future binders are immutable + // NOTE: (Juspreet) - In immutable environments, the "mapping" is static. As such, the name will _always_ be used as is. + std::string variableName = blockVariableMapping; - auto blockVariableMapping = sourceVariableNames[i]; - // Ensure that the future binder is part of the current info. - if (!RefinementUtils::Contains(blockVariablesAndInfo, blockVariableMapping)) - { - blockVariablesAndInfo.push_back(blockVariableMapping); + std::string assignedExpr = "__value == "s + variableName; + + auto addConstRes = constraintBuilder.AddConstraintForAssignment(constraintName, mappedVariableName, assignedExpr, blockVariablesAndInfo); + if (!addConstRes.Succeeded) { return addConstRes; } } - - std::string constraintName = "Variable_"s + previousBlock + "_"s + currentBlockName + "_"s + mappedVariableName; - - // Create Variable Mappings for Future Binders (which are immutable). - std::string variableName = blockVariableMapping; - - std::string assignedExpr = "__value == "s + variableName; - - auto addConstRes = constraintBuilder.AddConstraintForAssignment(constraintName, mappedVariableName, assignedExpr, blockVariablesAndInfo); - if (!addConstRes.Succeeded) { return addConstRes; } - } - + variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); return ResultType::Success(); } @@ -512,41 +512,42 @@ namespace liquid for (auto& currPreviousBlock: previousBlocks) { - // Extract the variable value in the current previous block. + // Extract the variable values in the current previous block. std::set currPreviousBlockValueSet = RefinementUtils::GetValuesSet(variablesValuesPerBlock[currPreviousBlock]); // Compare equality and conjunct with the condition. // Questions: - // i) What to do if the value is in one block and the subsequent one ? - // ii) Is this ever possible, and if not, does this mean an error ? - usingIdenticalMappings = usingIdenticalMappings && (currPreviousBlockValueSet[commonVariable] == recentPreviousBlockValueSet[commonVariable]) + // i) It seems this check is useless. This can only be false if a variable is deleted. That seems impossible in the immutable case. + usingIdenticalMappings = usingIdenticalMappings && (currPreviousBlockValueSet[commonVariable] == recentPreviousBlockValueSet[commonVariable]); } if (usingIdenticalMappings) { - variablesValuesPerBlock[currentBlockName].emplace(recentPreviousBlockValueSet[commonVariable]); + // Append the common variable from the predecessors to the current block. + // (NOTE): This will (again), break when we are handling for-loops (with the current way variablesValuesPerBlock is used). + variablesValuesPerBlock[currentBlockName].emplace(commonVariable); } else { - phiNodeVariables.emplace(commonVariable); + return ResultType::Error("phiNodeVariables was not empty while verifying immutability of Common Variables. The variable: " + commonVariable + " was found mutated!"; } } - + // Add to the environment any variables which require phi nodes - for (auto& phiNodeVariable : phiNodeVariables) - { + // Juspreet: For now, this code is commented, as it should not be required. + //for (auto& phiNodeVariable : phiNodeVariables) + //{ // Initialize the counter for the PhiNodevariable to be 0. Immutability => No increment. - std::string mappedVariableName = phiNodeVariable + "__"s + std::to_string(0); - auto blockSpecificVarNames = RefinementUtils::SelectString(previousBlocks, [&](const std::string& blockName) { - return variablesMappingsPerBlock.at(blockName).at(phiNodeVariable); - }); + //std::string mappedVariableName = phiNodeVariable + "__"s + std::to_string(0); + //auto blockSpecificVarNames = RefinementUtils::SelectString(previousBlocks, [&](const std::string& blockName) { + // return variablesMappingsPerBlock.at(blockName).at(phiNodeVariable); + //}); - auto createPhiRes = createPhiNodeWithoutCreatedBinders(phiNodeVariable, mappedVariableName, variableTypes.at(phiNodeVariable), blockSpecificVarNames, previousBlocks); - if (!createPhiRes.Succeeded) { return createPhiRes; } + //auto createPhiRes = createPhiNodeWithoutCreatedBinders(phiNodeVariable, mappedVariableName, variableTypes.at(phiNodeVariable), blockSpecificVarNames, previousBlocks); + //if (!createPhiRes.Succeeded) { return createPhiRes; } - variablesMappingsPerBlock[currentBlockName][phiNodeVariable] = mappedVariableName; - variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); - } + //variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); + //} return ResultType::Success(); } From b8f475b7c8460acdd21a3d65ebbe1adead916c93 Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Sun, 4 Feb 2018 19:41:33 -0500 Subject: [PATCH 18/20] Fix compiler errors + Test a.out --- .../VariablesEnvironmentImmutable.cpp | 32 +++++++++++-------- .../VariableEnvLibImmutable.cpp | 2 +- .../VariableEnvLib_IfImmutableExample.cpp | 2 +- 3 files changed, 21 insertions(+), 15 deletions(-) diff --git a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp index 0379573264c90..4c219acac86ff 100644 --- a/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp +++ b/lib/Transforms/LiquidFixpointBuilder/VariablesEnvironmentImmutable.cpp @@ -58,7 +58,7 @@ namespace liquid insertOrAssignVarType(variableTypes, variable, type); // @TODO::(Juspreet) - Is the Environment of bindings in a block ordered ? If so, is it FIFO/LIFO ? - variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); + variablesValuesPerBlock[currentBlockName].emplace_back(mappedVariableName); return ResultType::Success(); } @@ -107,7 +107,7 @@ namespace liquid // Make updates to Variable Mappings and Values for State Update of the Block insertOrAssignVarType(variableTypes, variable, type); - variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); + variablesValuesPerBlock[currentBlockName].emplace_back(mappedVariableName); return ResultType::Success(); } @@ -192,8 +192,8 @@ namespace liquid auto& currFinishedBlock = previousFinishedBlocks[i]; // Verify that the block and its values are present in the known blocks. - if (!RefinementUtils::Contains(variablesValuesPerBlock, currFinishedBlock)) { - return ResultType::Error("The Block: "s + std::to_string(currFinishedBlock) + " violates the processing order."s); + if (!RefinementUtils::ContainsKey(variablesValuesPerBlock, currFinishedBlock)) { + return ResultType::Error("The Block: "s + currFinishedBlock + " violates the processing order."s); } if (first) @@ -264,7 +264,7 @@ namespace liquid return ResultType::Success(); } - ResultType VariablesEnvironment::createPhiNodeWithoutCreatedBinders(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks) + ResultType VariablesEnvironmentImmutable::createPhiNodeWithoutCreatedBinders(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector& sourceVariableNames, const std::vector& previousBlocks) { if (sourceVariableNames.size() != previousBlocks.size()) { @@ -306,7 +306,7 @@ namespace liquid if (!addConstRes.Succeeded) { return addConstRes; } } - variablesValuesPerBlock[currentBlockName].emplace(mappedVariableName); + variablesValuesPerBlock[currentBlockName].emplace_back(mappedVariableName); return ResultType::Success(); } @@ -329,7 +329,11 @@ namespace liquid auto blockVariableMapping = sourceVariableNames[i]; // Variable of a phi node hasn't been created yet. - if (!RefinementUtils::ContainsKey(variablesValuesPerBlock[previousBlock], blockVariableMapping)) + std::map variableMap; + + for (auto const &currVar: variablesValuesPerBlock[previousBlock]) { variableMap[currVar] = 1; } + + if (!RefinementUtils::ContainsKey(variableMap, blockVariableMapping)) { auto futureBinderRes = constraintBuilder.CreateFutureBinder(blockVariableMapping, type); if (!futureBinderRes.Succeeded) { return futureBinderRes; } @@ -405,7 +409,7 @@ namespace liquid for (const auto& successor : successors) { - variablesValuesPerBlock[successor].emplace(transitionGuardName); + variablesValuesPerBlock[successor].emplace_back(transitionGuardName); } return ResultType::Success(); @@ -508,28 +512,30 @@ namespace liquid bool usingIdenticalMappings = true; // Extract the variable values in the most current previous block as a set. - std::set recentPreviousBlockValueSet = RefinementUtils::GetValuesSet(variablesValuesPerBlock[previousBlocks[0]]); + std::set recentPreviousBlockValueSet = RefinementUtils::GetValuesSet(variablesValuesPerBlock[previousBlocks[0]]); for (auto& currPreviousBlock: previousBlocks) { // Extract the variable values in the current previous block. - std::set currPreviousBlockValueSet = RefinementUtils::GetValuesSet(variablesValuesPerBlock[currPreviousBlock]); + std::set currPreviousBlockValueSet = RefinementUtils::GetValuesSet(variablesValuesPerBlock[currPreviousBlock]); // Compare equality and conjunct with the condition. // Questions: // i) It seems this check is useless. This can only be false if a variable is deleted. That seems impossible in the immutable case. - usingIdenticalMappings = usingIdenticalMappings && (currPreviousBlockValueSet[commonVariable] == recentPreviousBlockValueSet[commonVariable]); + bool inCurrPreviousBlock = (currPreviousBlockValueSet.find(commonVariable) != currPreviousBlockValueSet.end()) ; + bool inRecentPreviousBlock = (recentPreviousBlockValueSet.find(commonVariable) != recentPreviousBlockValueSet.end()); + usingIdenticalMappings = usingIdenticalMappings && inCurrPreviousBlock && inRecentPreviousBlock; } if (usingIdenticalMappings) { // Append the common variable from the predecessors to the current block. // (NOTE): This will (again), break when we are handling for-loops (with the current way variablesValuesPerBlock is used). - variablesValuesPerBlock[currentBlockName].emplace(commonVariable); + variablesValuesPerBlock[currentBlockName].emplace_back(commonVariable); } else { - return ResultType::Error("phiNodeVariables was not empty while verifying immutability of Common Variables. The variable: " + commonVariable + " was found mutated!"; + return ResultType::Error("phiNodeVariables was not empty while verifying immutability of Common Variables. The variable: " + commonVariable + " was found mutated!"); } } diff --git a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp index d182ae49463fb..ad4b6dfae2625 100644 --- a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp +++ b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp @@ -11,7 +11,7 @@ std::string format(VariablesEnvironmentImmutable& env, std::string expression) while (std::regex_search(expression, m, r)) { std::string varname = m[1]; - std::string replacement = env.GetVariableName(varname); + std::string replacement = varname; // Immutability means the varname is unchanged. expression = m.prefix().str() + replacement + m.suffix().str(); } diff --git a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp index e9b664b44cbf3..2a99f32616619 100644 --- a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp +++ b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp @@ -70,7 +70,7 @@ int ifImmutableExample() E(env.CreateImmutableVariable("cmp"s, FixpointType::GetBoolType(), {}, format(env, " __value <=> {{a}} == 4"s))); E(env.AddBranchInformation("cmp"s, true, "if.then")); - E(env.AddBranchinformation("cmp"s, false, "if.end")); + E(env.AddBranchInformation("cmp"s, false, "if.end")); E(env.StartBlock("if.then"s)); E(env.CreateImmutableVariable("d"s, FixpointType::GetIntType(), {}, format(env, "__value == {{b}}"s))); From 95e8e3feb8544d4892335c1cf74ee74344d040d7 Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Sun, 4 Feb 2018 19:50:52 -0500 Subject: [PATCH 19/20] Fixpoint output checcked! Works! --- .../VariableEnvLibImmutable.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp index ad4b6dfae2625..e34924c2bfdcb 100644 --- a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp +++ b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLibImmutable.cpp @@ -18,7 +18,7 @@ std::string format(VariablesEnvironmentImmutable& env, std::string expression) return expression; } -// int ifImmutableExample(); +int ifImmutableExample(); // int ifThenElseExample(); // int forLoopExample(); @@ -32,8 +32,7 @@ int main() if(a == 1) { - // return ifImmutableExample(); - return 0; + return ifImmutableExample(); } else { From 572332498279ac6e58d8c7110c8ffdc9fa148076 Mon Sep 17 00:00:00 2001 From: Juspreet S Sandhu Date: Sun, 4 Feb 2018 21:55:37 -0500 Subject: [PATCH 20/20] Assertion --- .../VariableEnvLib_IfImmutableExample.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp index 2a99f32616619..745cec37d68ec 100644 --- a/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp +++ b/tools/liquidTypes-varibleEnvLib-example/VariableEnvLib_IfImmutableExample.cpp @@ -78,6 +78,7 @@ int ifImmutableExample() E(env.StartBlock("if.end"s)); E(env.CreatePhiNode("e"s, FixpointType::GetIntType(), { "c"s, "d"s }, { "entry"s, "if.then"s })); + E(env.CreateImmutableVariable("ret"s, FixpointType::GetIntType(), {"__value == 5"}, format(env, "__value == {{e}}"))); E(env.ToStringOrFailure(str));