-
Notifications
You must be signed in to change notification settings - Fork 16
Dynamic analysis #1
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
cemcebeci
wants to merge
16
commits into
rl-language:master
Choose a base branch
from
cemcebeci:dynamic-analysis
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from all commits
Commits
Show all changes
16 commits
Select commit
Hold shift + click to select a range
cd8f891
implemented lowering for minvalOp. To be cleaned.
cemcebeci 9cb5f6d
added support for max
cemcebeci c31c19f
recurse into CallOp's to CanOp results.
cemcebeci 94f95e0
organized the implementation to a more readable form.
cemcebeci 0cb4c44
added explanation.
cemcebeci fe26171
added the blackjack example.
cemcebeci 0eba407
fixed how we handle multiple conjunctions.
cemcebeci dd9cb27
pick arguments one by one, binding previously picked ones each time.
cemcebeci c703544
replaced ArgConstraintsOp with PickedArgOp
cemcebeci 1d7f24e
laid out the method for picking structs, not yet accounting for alrea…
cemcebeci 8cdde83
bind values of previously picked struct fields while picking new ones.
cemcebeci 81933b9
fixed struct args in wrapped subaction functions.
cemcebeci 1f0c92d
correctly use the assign operators to assign non-built-in data types.
cemcebeci ffb82ec
correctly transfer all bindings when analysing a wrapped precondition.
cemcebeci 95df97e
implement the option to not check legality of subactions.
cemcebeci e9fa060
implement the option to turn off precondition analysis.
cemcebeci File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
177 changes: 177 additions & 0 deletions
177
lib/dialect/include/rlc/dialect/DynamicArgumentAnalysis.hpp
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,177 @@ | ||
| #include <cassert> | ||
| #include <cstdint> | ||
| #include <ranges> | ||
| #include <strings.h> | ||
| #include "llvm/ADT/DenseMap.h" | ||
| #include "llvm/ADT/SmallVector.h" | ||
| #include "mlir/IR/Builders.h" | ||
| #include "mlir/IR/Location.h" | ||
| #include "mlir/IR/Operation.h" | ||
| #include "mlir/IR/Region.h" | ||
| #include "mlir/IR/Value.h" | ||
| #include "mlir/IR/ValueRange.h" | ||
| #include "mlir/Support/LLVM.h" | ||
| #include "rlc/dialect/Operations.hpp" | ||
|
|
||
|
|
||
| struct DeducedConstraints { | ||
| mlir::Value min; | ||
| mlir::Value max; | ||
| }; | ||
|
|
||
| enum TermType { | ||
| DEPENDS_ON_UNBOUND, | ||
| DEPENDS_ON_OTHER_UNKNOWNS, | ||
| KNOWN_VALUE | ||
| }; | ||
|
|
||
| /* | ||
| Given a function and a set of known (bound) arguments for the function, we try to find the | ||
| minimum and maximum values the unknown (unbound) arguments can take while satisfying the | ||
| function's precondition. | ||
|
|
||
| We first normalize the precondition to be a disjunction of conjunction of terms, where each | ||
| term is a value produced by something other than an AndOp or an OrOp. i.e. we express the | ||
| precondition in the form (t_1 AND t_2 AND ...) OR (t_3 AND t_4 AND ...). | ||
|
|
||
| Then, to find the minimum and the maximum for a given argument "arg", we emit code as follows: | ||
| We emit declarations for aggregate_min and aggregate_max, initialized to minus and plus infinity. | ||
|
|
||
| For each conjunction (t_1 AND t_2 AND ...) we classify the terms as | ||
| - conditions: terms depending only on known values | ||
| - constraints: terms depending on "arg" and no other unknown values | ||
| - others: terms depending on other unknown values. | ||
|
|
||
| We analyse the minimum and maximum values each constraint implies on "arg" in terms of known | ||
| dynamic values. Currently, this returns [-infinity, +infinity] for anything but <, >, >=, <=, == | ||
| constraints where one of the sides is "arg", and calls to CanOp results. | ||
|
|
||
| Then, we emit an if statement in the form of | ||
| if(condition_1 & condition_2....) { | ||
| current_min = -inf | ||
| if(imposed_min(constraint_1) > current_min) | ||
| current_min = imposed_min(constraint_1) | ||
| if(imposed_min(constraint_2) > current_min) | ||
| current_min = imposed_min(constraint_2) | ||
| ... | ||
| if ( uninitialized(aggregate_min) || current_min < aggregate_min) | ||
| aggregate_min = current_min | ||
| } | ||
|
|
||
| In other words, we compute | ||
| aggregate_min = max([ | ||
| min([imposed_min(term) for term in conjunction.constraints]) | ||
| for conjunction in constraint | ||
| where evaluate(conjunction.conditions) == true | ||
| ]) | ||
|
|
||
| and similarly for the maximum. | ||
| */ | ||
|
|
||
|
|
||
| /* | ||
| memberAddress is the "path" from the arg to the value we want to pick. | ||
| Example: arg = arg2, memberAddress = [2, 1] maps to MemberAccess(MemberAccess(arg,2), 1) | ||
| */ | ||
| struct UnboundValue { | ||
| mlir::BlockArgument argument; | ||
| llvm::SmallVector<uint64_t> memberAddress; | ||
|
|
||
| /* | ||
| Returns whether this unbound value corressponds to the expression. | ||
| */ | ||
| bool matches(mlir::Value expr) { | ||
| mlir::Value current = expr; | ||
| // walk the member address in reverse, test if it leads to the argument. | ||
| for(uint64_t & index : std::ranges::reverse_view(memberAddress)) { | ||
| auto definingOp = current.getDefiningOp(); | ||
| if( not llvm::detail::isPresent(definingOp)) | ||
| return false; | ||
| if(auto memberAccess = mlir::dyn_cast<mlir::rlc::MemberAccess>(definingOp)) { | ||
| if (memberAccess.getMemberIndex() != index) { | ||
| return false; | ||
| } | ||
| current = memberAccess.getValue(); | ||
| } else { | ||
| return false; | ||
| } | ||
| } | ||
| return current == argument; | ||
| } | ||
|
|
||
| /* | ||
| Returns true if this unbound value is a recursive member of the given expression. | ||
| */ | ||
| bool isMemberOf(mlir::Value expr) { | ||
| mlir::Value current = expr; | ||
| llvm::SmallVector<uint64_t> indices; | ||
|
|
||
| while(true) { | ||
| if(current == argument) { | ||
| for(size_t i = 0; i < indices.size(); i++) { | ||
| if(indices[i] != memberAddress[i]) | ||
| return false; | ||
| } | ||
| return true; | ||
| } | ||
|
|
||
| auto definingOp = current.getDefiningOp(); | ||
| if( not llvm::detail::isPresent(definingOp)) | ||
| return false; | ||
| if(auto memberAccess = mlir::dyn_cast<mlir::rlc::MemberAccess>(definingOp)) { | ||
| indices.insert(indices.begin(), memberAccess.getMemberIndex()); | ||
| current = memberAccess.getValue(); | ||
| } else return false; | ||
| } | ||
| } | ||
|
|
||
| mlir::Type getType() { | ||
| auto type = argument.getType(); | ||
| for (auto index : memberAddress) { | ||
| type = type.cast<mlir::rlc::EntityType>().getBody()[index]; | ||
| } | ||
| return type; | ||
| } | ||
| }; | ||
|
|
||
| class DynamicArgumentAnalysis | ||
| { | ||
| public: | ||
| explicit DynamicArgumentAnalysis(mlir::rlc::FunctionOp op, mlir::ValueRange boundArgs, mlir::Value argPicker, bool analysePreconditions, mlir::OpBuilder builder, mlir::Location loc); | ||
| mlir::Value pickArg(int argIndex); | ||
|
|
||
| private: | ||
| DeducedConstraints deduceIntegerUnboundValueConstraints(UnboundValue unbound); | ||
| llvm::SmallVector<llvm::SmallVector<mlir::Value>> expandToDNF(mlir::Value constraint); | ||
| TermType decideTermType(mlir::Value term, UnboundValue unbound); | ||
| mlir::Value compute(mlir::Value expression); | ||
| DeducedConstraints findImposedConstraints(mlir::Value constraint, UnboundValue unbound); | ||
| DeducedConstraints findImposedConstraints(mlir::Operation *binaryOperation, UnboundValue unbound); | ||
| DeducedConstraints findImposedConstraints(mlir::rlc::CallOp call, UnboundValue unbound); | ||
|
|
||
| mlir::Value pickIntegerUnboundValue(UnboundValue unbound); | ||
| mlir::Value pickUnboundValue(UnboundValue unbound); | ||
|
|
||
| mlir::rlc::FunctionOp function; | ||
| mlir::Region& precondition; | ||
|
|
||
| llvm::SmallVector<std::pair<UnboundValue, mlir::Value>> bindings; | ||
| /* | ||
| If the passed value matches an UnboundValue that has a binding, | ||
| return the value bound to it. | ||
| Otherwise returns nullptr. | ||
| */ | ||
| mlir::Value getBoundValue(mlir::Value expr) { | ||
| for(auto binding : bindings) { | ||
| if(binding.first.matches(expr)) | ||
| return binding.second; | ||
| } | ||
| return nullptr; | ||
| } | ||
|
|
||
| bool analysePreconditions; | ||
| mlir::Value argPicker; | ||
| mlir::OpBuilder builder; | ||
| mlir::Location loc; | ||
| llvm::SmallVector<llvm::SmallVector<mlir::Value>> conjunctions; | ||
| }; | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
i think that DNF will be something that will come up a lot, you can wrap the vectors into a class like and put this in a header of their own
to be honest i would not be even opposed to have a operation called DNFExpression and have this analysis as a pass that mutates the ir and turns every precondition into a DNF