Juspreet - New Fixpoint Graph Builder - Immutable Only by jssandh2 · Pull Request #3 · shravanrn/RefinementTypes_llvm

jssandh2 · 2017-10-29T04:05:40Z

Certain fixes in logic in the CFG logic.
Reconstruction of code for Liquid Type generation and verification for Immutable Environments.
New files :
- VariablesEnvironmentImmutable.h
- VariablesEnvironmentImmutable.cpp
- VariablesEnvLibEImmutable.cpp
NOTES :
- Compilation works. Verified.
TODO ( @jssandh2 ) :
- Verify logic for startBlock, getCommonVariables, validateFinishedAndUnfinishedBlocks, Phi Node Logic is correct
  cc : @shravanrn
UPDATES : i) Example added. We should go through the PR and verify the logic.

… folder

…ock Modification and exposed functions

….cpp

…rrors. Compilation woks.

shravanrn · 2017-11-10T23:58:56Z

+namespace liquid
+{
+
+  class PhiNodeObligation


PhiNodeObligation is a DS used to automatically infer phi nodes for mutable code - not needed here

shravanrn · 2017-11-10T23:59:34Z

+
+      std::map<std::string, std::set<std::string>> variablesValuesPerBlock;
+      std::set<std::string> finishedBlocks;
+      std::map<std::string, std::vector<PhiNodeObligation>> phiNodeObligations;


jssandh2 · 2017-11-26T00:23:31Z

@shravanrn : PhiNodeObligation removed. A git grep -e phiNodeObligations shows they aren't being used anywhere else. Good catch, because it was only being called for removing a block, which means we would've had a segfault at some point.

shravanrn · 2017-11-27T02:07:20Z

+
+    // Ensure that :
+    // 1) forall blocks in PreviousFinishedBlocks, dominate(blocks, block), forall block in PreviousUnfinishedblocks
+    for (const auto& previousUnfinishedBlock : previousFinishedBlocks)


previousUnfinishedBlock : previousFinishedBlocks is definitely wrong

shravanrn · 2017-11-27T02:10:47Z

+    bool first = true;
+
+    for (auto& previousBlock : previousBlocks)
+    {


Strictly dominates

shravanrn · 2017-11-27T02:11:17Z

+  }
+
+  ResultType VariablesEnvironmentImmutable::validateFinishedAndUnfinishedBlockStates(
+    const std::vector<std::string>& previousFinishedBlocks,


Probably remove this function

The upcoming commit may not immediately remove this function. I am first removing redundant variables, and making sure the new logic is not broken because of removals. This will come up next.

jssandh2 · 2017-11-27T02:12:02Z

+
+    bool first = true;
+
+    for (auto& previousBlock : previousBlocks)


Impose the linear order by checking ancestors - Juspreet

shravanrn · 2017-11-27T02:12:41Z

+
+    for (auto& previousBlock : previousBlocks)
+    {
+      if (first)


Before accessing variablesMappingsPerBlock[previousBlock] there should be a check to make sure variablesMappingsPerBlock[previousBlock] is actually filled in... else the order of iteration is broken

See finishedBlocks

shravanrn · 2017-11-27T02:29:56Z

+    return ResultType::Success();
+  }
+
+  ResultType VariablesEnvironmentImmutable::createPhiNodeWithoutCreatedBinders(const std::string& variable, const std::string& mappedVariableName, const FixpointType& type, const std::vector<std::string>& sourceVariableNames, const std::vector<std::string>& previousBlocks)


createPhiNodeAssumingNoFutureBinders

I reversed this, as this was wrong. We were not using createPhiNodeAssumingNoFutureBinders and were actually using createPhiNodeWithoutCreatedBinders. The functionality wasn't different, as there is a statement check for undeclared variables that we will never go into (save for the sake of for loops).

shravanrn · 2017-11-27T02:42:30Z

+
+	predecessorTransitionGuards.emplace_back("("s + predecessorEntryGuard + " && "s + transitionGuardName + ")"s);
+      }
+


Throw error if more than 2 predecessors

jssandh2 · 2017-11-27T02:42:43Z

+	if (!getPredRes.Succeeded) { return getPredRes; }
+      }
+
+      std::vector<std::string> predecessorTransitionGuards;


predecessors.size() > 2 => Not good.

shravanrn · 2017-11-27T03:11:29Z

+  }
+
+  //@TODO:: (juspreet) - The recursive call here isn't clear. Verify.
+  ResultType VariablesEnvironmentImmutable::getBlockGuard(const std::string& blockName, std::string& blockGuard)


Replace with fixpoint algorithm

shravanrn · 2017-11-27T03:13:04Z

+      }
+    }
+
+    for (const auto& blockName : blockNames)


get rid of block guards

This is on the next part of the TODO list - Replacing blockGuards with a purely Fixpoint approach.

shravanrn · 2017-11-27T03:30:53Z

+      const FunctionBlockGraph& functionBlockGraph;
+
+      std::map<std::string, FixpointType> variableTypes;
+      std::map<std::string, std::map<std::string, std::string>> variablesMappingsPerBlock;


shravanrn · 2017-11-27T03:31:08Z

+      std::map<std::string, FixpointType> variableTypes;
+      std::map<std::string, std::map<std::string, std::string>> variablesMappingsPerBlock;
+
+      std::map<std::string, std::set<std::string>> variablesValuesPerBlock;


change to vector

I've changed this to a vector, and added a RefinementUtils function to get a set from a vector. As a result, I'm wondering if this should be changed in the first place ?

shravanrn · 2017-11-27T03:32:03Z

+  }
+
+  // Get the name of the variable
+  std::string VariablesEnvironmentImmutable::GetVariableName(const std::string variableName)


shravanrn · 2017-11-27T03:38:22Z

+      std::map<std::string, std::set<std::string>> variablesValuesPerBlock;
+      std::set<std::string> finishedBlocks;
+
+      std::set<std::string> outputVariables;


shravanrn · 2017-11-27T03:38:28Z

+
+      std::set<std::string> outputVariables;
+
+      std::map<std::string, std::string> cachedBlockGuards;


shravanrn · 2017-11-27T03:38:37Z

+      ResultType endBlock(const std::string& blockName);
+
+    public:
+      Counter FreshState;


jssandh2 · 2017-12-26T00:10:57Z

i) There is one more part with changes - Part 3 that is WIP and will come as the next commit.
ii) The WIP part includes :
- a) Removal of cachedBlockGuards
- b) Introduction of Fixpoint Algorithm instead of BlockGuards
- c) Sanitization of code after Line 391

jssandh2 · 2018-02-05T01:03:53Z

There are still ~3 things to discuss (though, for the sake of practicality and incremental work, this PR can be merged as it is verified to work):

The concept of StrictlyDominates and its future.
- How will we use it when we use a Fixpoint approach for BlockGuards.
- What exactly will be its running definition when cycles are possible in the Graph.
The strategy for the introduction of the Fixpoint approach.
The necessity (or lack thereof) of __block__ + blockName as a blockBinder.

jssandh2 and others added 10 commits October 6, 2017 19:59

Create VariablesEnvironmenmtImmutable.cpp

489fca1

Addition of the VariablesEnvironmentImmutable.h file in the inlcude/…

f77217f

… folder

Begin adding cpp files

57e1fde

Dumb

da4b5e9

Some more functions. Almost done.

5dffd44

Compute common variables. 2 more commits to go.

005c468

Add some Phi-Node functions (modified). 1 more commit, till we add Bl…

0341293

…ock Modification and exposed functions

Final addition of code (first run) for VariablesEnvironmentImmutable…

26b23b9

….cpp

Add an example file - VariableEnvLibImmutable.cpp. Fix compilation e…

9e9831c

…rrors. Compilation woks.

Add example

c801712

shravanrn requested changes Nov 11, 2017

View reviewed changes

Remove PhiNodeObligation

d9dad87

shravanrn reviewed Nov 27, 2017

View reviewed changes

jssandh2 commented Nov 27, 2017

View reviewed changes

shravanrn reviewed Nov 27, 2017

View reviewed changes

jssandh2 changed the title ~~Juspreet - New Fixpoint Constraint Builder - Immutable Only~~ Juspreet - New Fixpoint Graph Builder - Immutable Only Nov 27, 2017

shravanrn reviewed Nov 27, 2017

View reviewed changes

jssandh2 commented Nov 27, 2017

View reviewed changes

shravanrn reviewed Nov 27, 2017

View reviewed changes

jssandh2 added 2 commits December 25, 2017 13:06

Changes: Part-1

614be5c

Changes: Part 2

c978840

jssandh2 and others added 6 commits December 25, 2017 16:19

Remove the old function

a7bf894

NOTE: This does not compile. The blockguard fix is en-route. Part-1.

360693f

Large Changes: Part-1

0812e28

Larg changes: Part 2

e40f0cc

Fix compiler errors + Test a.out

b8f475b

Fixpoint output checcked! Works!

95e8e3f

Assertion

5723324


		bool first = true;

		for (auto& previousBlock : previousBlocks)


		predecessorTransitionGuards.emplace_back("("s + predecessorEntryGuard + " && "s + transitionGuardName + ")"s);
		}


		std::set<std::string> outputVariables;

		std::map<std::string, std::string> cachedBlockGuards;

Conversation

jssandh2 commented Oct 29, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jssandh2 commented Nov 26, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jssandh2 Feb 5, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jssandh2 commented Dec 26, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jssandh2 commented Feb 5, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jssandh2 commented Oct 29, 2017 •

edited

Loading

jssandh2 Feb 5, 2018 •

edited

Loading

jssandh2 commented Dec 26, 2017 •

edited

Loading

jssandh2 commented Feb 5, 2018 •

edited

Loading