From 61610386ef5399b915748f9fde57e905c848964a Mon Sep 17 00:00:00 2001
From: Sandro Grebant <sandro.grebant@univ-lille.fr>
Date: Fri, 24 Mar 2023 10:18:04 +0100
Subject: [PATCH] input conditionals calculation
---
AUTHORS | 3 +-
Makefile | 29 ++-
include/BranchConditionner.h | 173 +++++++++++++++
include/LoopAnalyzer.h | 82 +++++++
include/PPLDomain.h | 21 +-
include/PPLManager.h | 5 -
include/PolyAnalysis.h | 1 +
include/PolyWrap.h | 1 +
poly_BranchConditionner.cpp | 127 +++++++++++
poly_LoopAnalyzer.cpp | 329 ++++++++++++++++++++++++++++
poly_PPLDomain.cpp | 411 ++++++++++++++++++++++++++++-------
poly_PolyAnalysis.cpp | 143 +++++++++++-
poly_PolyWrap.cpp | 5 +
13 files changed, 1212 insertions(+), 118 deletions(-)
create mode 100644 include/BranchConditionner.h
create mode 100644 include/LoopAnalyzer.h
create mode 100644 poly_BranchConditionner.cpp
create mode 100644 poly_LoopAnalyzer.cpp
diff --git a/AUTHORS b/AUTHORS
index 4fea413..b5fb89e 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -1,3 +1,2 @@
Clement Ballabriga <Clement.Ballabriga@univ-lille.fr>
-Julien Forget <Julien.Forget@univ-lille.fr>
-Jordy Ruiz <jordyruiz@gmail.com>
+Sandro Grebant <sandro.grebant@univ-lille.fr>
diff --git a/Makefile b/Makefile
index 32c86a9..64ba3d5 100644
--- a/Makefile
+++ b/Makefile
@@ -1,15 +1,20 @@
-CXXFLAGS=`otawa/bin/otawa-config otawa/oslice --cflags`
-LIBS=`otawa/bin/otawa-config otawa/oslice --libs`
+CXXFLAGS=`otawa-config otawa/oslice --cflags`
+LIBS=`otawa-config otawa/oslice --libs`
LIBS+=-lppl
CC=gcc
CXX=g++
-CXXFLAGS+=-fPIC -Wall -DUSE_CLANG_COMPLETER -std=c++14 -O3 -march=native
+CXXFLAGS+= -g -fPIC -Wall -DUSE_CLANG_COMPLETER -std=c++14 -O3 -march=native
#CXXFLAGS+=-fPIC -Wall -DUSE_CLANG_COMPLETER -std=c++14 -O0 -g
-all: poly.so
+default: poly.so install test_poly
+
+all: clean poly.so install test_poly
+
+test_poly:
+ cd tests;$(MAKE)
dbg: CXXFLAGS += -DELM_LOG
dbg: poly.so
@@ -17,17 +22,23 @@ dbg: poly.so
debug: CXXFLAGS += -DPOLY_DEBUG
debug: poly.so
-poly.so: poly_PolyAnalysis.o poly_PlugHook.o poly_PPLDomain.o poly_PPLManager.o poly_PolyWrap.o
- $(CC) -shared -o poly.so poly_PolyAnalysis.o poly_PlugHook.o poly_PPLDomain.o poly_PPLManager.o poly_PolyWrap.o $(LIBS)
-
+poly.so: poly_PolyAnalysis.o poly_PlugHook.o poly_PPLDomain.o poly_PPLManager.o poly_PolyWrap.o poly_BranchConditionner.o poly_LoopAnalyzer.o
+ $(CC) -shared -o poly.so poly_PolyAnalysis.o poly_PlugHook.o poly_PPLDomain.o poly_PPLManager.o poly_PolyWrap.o poly_BranchConditionner.o poly_LoopAnalyzer.o $(LIBS)
+
+poly_BranchConditionner.o: poly_BranchConditionner.cpp include/BranchConditionner.h include/PPLDomain.h include/PolyWrap.h include/PolyAnalysis.h
+ $(CXX) $(CXXFLAGS) -c poly_BranchConditionner.cpp -o poly_BranchConditionner.o
+
+poly_LoopAnalyzer.o: poly_BranchConditionner.cpp include/BranchConditionner.h include/PPLDomain.h include/PolyWrap.h include/PolyAnalysis.h
+ $(CXX) $(CXXFLAGS) -c poly_LoopAnalyzer.cpp -o poly_LoopAnalyzer.o
+
-poly_PolyAnalysis.o: poly_PolyAnalysis.cpp include/PolyAnalysis.h include/PPLDomain.h include/PolyWrap.h include/PPLManager.h include/PolyCommon.h include/MyHTable.h include/OrderedDriver.h
+poly_PolyAnalysis.o: poly_PolyAnalysis.cpp include/PolyAnalysis.h include/PPLDomain.h include/PolyWrap.h include/PPLManager.h include/PolyCommon.h include/MyHTable.h include/OrderedDriver.h include/BranchConditionner.h
$(CXX) $(CXXFLAGS) -c poly_PolyAnalysis.cpp -o poly_PolyAnalysis.o
poly_PPLManager.o: poly_PPLManager.cpp include/PolyAnalysis.h include/PPLDomain.h include/PolyWrap.h include/PPLManager.h include/PolyCommon.h include/MyHTable.h include/OrderedDriver.h
$(CXX) $(CXXFLAGS) -c poly_PPLManager.cpp -o poly_PPLManager.o
-poly_PPLDomain.o: poly_PPLDomain.cpp include/PolyAnalysis.h include/PPLDomain.h include/PolyWrap.h include/PPLManager.h include/PolyCommon.h include/MyHTable.h include/OrderedDriver.h
+poly_PPLDomain.o: poly_PPLDomain.cpp include/PolyAnalysis.h include/PPLDomain.h include/PolyWrap.h include/PPLManager.h include/PolyCommon.h include/MyHTable.h include/OrderedDriver.h include/BranchConditionner.h
$(CXX) $(CXXFLAGS) -c poly_PPLDomain.cpp -o poly_PPLDomain.o
poly_PlugHook.o: poly_PlugHook.cpp
diff --git a/include/BranchConditionner.h b/include/BranchConditionner.h
new file mode 100644
index 0000000..63d1a79
--- /dev/null
+++ b/include/BranchConditionner.h
@@ -0,0 +1,173 @@
+#ifndef BC
+#define BC 1
+
+#include <otawa/otawa.h>
+#include "PolyWrap.h"
+#include "PPLDomain.h"
+
+#define CONSTRAINTS_FILE "constraints.csv" // the file containing parametric conditionals
+#define MAX_LOOP 1000000 // macro used to have a better loop management for parametric conditionals
+
+namespace otawa {
+namespace poly {
+using namespace otawa;
+ /**
+ * Map the function arguments using register number (0 <= r <= 3)
+ * > 3 means that the value is in the stack (i.g. a function with more than 4 arguments)
+ * This identifier should be used on the function's CFG entry node
+ */
+ extern Identifier<std::map<int,WVar>> FUNCTION_ARGS;
+
+ /**
+ * Remember which variables are used in functions (useful for polyhedron projections)
+ * It maps a variable to the id of its special identifier
+ * This identifier marks a function argument variable as used
+ * It should be used on the function's CFG entry node
+ */
+ extern Identifier<std::map<int,WVar>> USED_ARGS;
+
+ /**
+ * Stores the root CFG on any CFG
+ */
+ extern Identifier<CFG*> ROOT_CFG;
+
+ /**
+ * Identifies single function calls in loops
+ * std::map<LOOP_HEADER_ID,std::map<FUNCTION_NAME,INSTANCE>>
+ */
+ extern Identifier<std::map<int,std::map<string,int>>> CURRENT_INSTANCES;
+
+ /**
+ * Tells if a loop has exited
+ */
+ extern Identifier<bool> LOOP_RESET;
+
+ /**
+ * Each loop header knows his parent loop
+ */
+ extern Identifier<int> PREVIOUS_LOOP;
+
+ /**
+ * Arm function arguments detector
+ * Enables to manage functino arguments and to track function arguments usage
+ */
+ class ArmArgumentsDetector{
+ public:
+ /**
+ * mark function parameters at the begining of the analysis
+ * @param s the initial state of the analysis
+ */
+ void initFunctionParameters(PPLDomain* s, Block* cfgEntry);
+ /**
+ * Check if a variable is a marked as used program argument
+ * It should be used in order to choose the variable needed to make a polyhedron projection
+ * @param cfgEntry the entry point of the CFG
+ * @param v the variable to check
+ * @return the id of the parameter if exists, -1 otherwise
+ */
+ int getParamId(Block* cfgEntry, WVar v);
+ };
+
+ /**
+ * Simple object class to represent the exported conditional statement
+ */
+ class Conditional{
+ private:
+ Block* b;
+ bool taken;
+ std::string conditions;
+ public:
+ /**
+ * Constructor
+ * @param b the basic block corresponding to the condition
+ * @param taken tell if the condition is taken or not
+ * @param conditions the conditions as a string
+ */
+ Conditional(Block* b, bool taken, std::string conditions);
+ /**
+ * block accessor
+ * @return the basic block of the condition
+ */
+ Block* getBlock();
+ /**
+ * taken accessor
+ * @return if the conditional is taken or not
+ */
+ bool isTaken();
+ /**
+ * conditions accessor
+ * @return the conditions as a string
+ */
+ std::string getConditions();
+ };
+
+ /**
+ * Abstract representation of an ordered element to export
+ */
+ class OrderedConditional{
+ private:
+ int loopId; //< identifies the order of the custom loopIds
+ Conditional conditional; //< if loopId == -1 then conditional != null
+ public:
+ OrderedConditional(int loopId, Conditional conditional); //< constructor for outer loop elements
+ OrderedConditional(int loopId); //< constructor for inner loops element
+ int getLoopId(); //< accessor
+ Conditional getConditional(); //< accessor
+ };
+
+ /**
+ * Keep an order for conditional inside/outside loops
+ */
+ class OrderedElements{
+ private:
+ std::map<int,OrderedConditional> order;
+ public:
+ OrderedElements();
+ void addElement(OrderedConditional conditional);
+ std::map<int,OrderedConditional> getOrder();
+ };
+
+ /**
+ * Remember global order form constraints
+ * it should be attached on root cfg
+ */
+ extern Identifier<OrderedElements> EXPORT_ORDER;
+
+ /**
+ * Store only the last condition when in a loop context
+ */
+ extern Identifier<std::map<int,std::map<bool,Conditional>>> LOOP_CONDITIONALS;
+ /**
+ * Store the current loop context
+ */
+ extern Identifier<int> CURRENT_LOOP;
+ /**
+ * A simple class to export constraints
+ */
+ class ConstraintExporter{
+ public:
+ /**
+ * Export constraints into a file
+ * @param branchingBlock the block inside which the branching instruction is
+ * @param taken if the condition is in the taken branch or the other
+ * @param conditions the conditionnal boolean expression
+ */
+ void exportToFile(Conditional c);
+ /**
+ * Allows to remove the file containing data, this is needed at the begining of an analysis
+ * @return true if the file was deleted, false otherwise
+ */
+ void resetFile();
+ /**
+ * Manage particular case of loops
+ * @param order non loop conditionals + order
+ * @param loopConstraints loop conditionals
+ */
+ //void exportLoopConstraints(std::map<int, std::map<bool,Conditional>> toExport);
+ void exportOrderedConstraints(OrderedElements order, std::map<int, std::map<bool,Conditional>> loopConstraints);
+ };
+
+}
+}
+
+#endif // !BC
diff --git a/include/LoopAnalyzer.h b/include/LoopAnalyzer.h
new file mode 100644
index 0000000..a538b7f
--- /dev/null
+++ b/include/LoopAnalyzer.h
@@ -0,0 +1,82 @@
+#ifndef LA
+#define LA 1
+
+#include <fstream>
+#include <otawa/otawa.h>
+#include "PolyWrap.h"
+#include "PPLDomain.h"
+
+#define LOOP_BOUNDS_FILE "loop_bounds.csv" // the file containing loop bounds
+//#define LINBOUND // exports linear bounds when needed
+//#define INTER_PROCEDURAL // required by LINBOUND
+
+namespace otawa{
+namespace poly{
+
+ using namespace otawa;
+
+ /**
+ * A state analysis to detect induction variables
+ */
+ class LoopAnalyzer{
+ public:
+ /**
+ * Try to compute a linear loop bound from a projected polyhedron
+ * @param b the header of the loop
+ * @param proj the result of the projection
+ */
+ void computeLinearBound(Block* b, std::vector<WCons> cs, MyHTable<int, int> mapping);
+ };
+
+ /**
+ * Represent a loop bound, which can be either static or linear
+ */
+ class LoopBound{
+ private:
+ bool linear; //< gives the kind of bound
+ int staticBound; //< static bound if exists
+ std::string linearBound; //< linear bound f exists
+ public:
+ /**
+ * Constructor
+ * @param linear true = linear, false = static
+ * @param staticBound the static bound if exists
+ * @param linearBouns the linear bound if exists
+ */
+ LoopBound(bool linear, int staticBound, std::string linearBound);
+ /**
+ * Exports the constraint into the giver file
+ * @param o the output file stream
+ * @param lid the loop id corresponding to that bound
+ */
+ void exportToFile(std::ofstream *o, int lid);
+ };
+
+ /**
+ * A simple class to export all the loop bounds at once
+ */
+ class LoopBoundsExporter{
+ public:
+ /**
+ * Exports all, the loop bounds into a file
+ * @param bounds the loop bounds to export
+ */
+ void exportToFile(std::map<int,LoopBound> bounds);
+ };
+
+ /**
+ * Identifier to store loop bounds
+ * Attached to root cfg entry
+ */
+ extern Identifier<std::map<int,LoopBound>> LOOP_BOUNDS;
+
+ /**
+ * Identifier to store the constraints detected at each loop iteration
+ * Attached to the loop header block
+ */
+ extern Identifier<std::vector<WCons>> CONSTRAINTS;
+
+}
+}
+
+#endif
diff --git a/include/PPLDomain.h b/include/PPLDomain.h
index 5bb3b90..39ccfdc 100644
--- a/include/PPLDomain.h
+++ b/include/PPLDomain.h
@@ -15,7 +15,8 @@
// #include "Clp.h"
#include "PolyCommon.h"
#include "PolyWrap.h"
-
+#include "BranchConditionner.h"
+#include "LoopAnalyzer.h"
namespace otawa {
namespace poly {
@@ -96,7 +97,6 @@ class Ident {
void print(io::Output &out) const;
-
inline bool operator==(const Ident &i) const { return (_id == i._id) && (_type == i._type); }
inline bool operator!=(const Ident &i) const { return (_id != i._id) || (_type != i._type); }
@@ -416,10 +416,6 @@ private:
// };
public:
-
-
- void showTab(const Ident&);
-
/* Basic operations (constructor, destructor, copy, comparison) */
/**
@@ -668,6 +664,12 @@ private:
* bounded.
*/
bound_t getLoopBound(int loopId) const;
+
+ /**
+ * Tries to find a parametric loop bound
+ * @param b the loop header
+ */
+ void computeParamBound(Block* b) const;
inline bound_t getBound(int loopId) const {
if (bounds.length() <= loopId)
@@ -737,7 +739,7 @@ private:
* @return The updated state.
*/
- PPLDomain onBranch(bool taken) const;
+ PPLDomain onBranch(bool taken, Block* b) const;
/**
* Process join and widening
@@ -770,8 +772,8 @@ private:
* unreachable/unbounded)
* @return The updated state.
*/
- PPLDomain onLoopExit(int loop, int bound) const;
- PPLDomain onLoopExitLinear(int loop, const PPLDomain &bound) const;
+ PPLDomain onLoopExit(int loop, int bound, Block* b) const;
+ PPLDomain onLoopExitLinear(int loop, const PPLDomain &bound, Block* b) const;
/* Operations that modify the state in-place */
@@ -1153,7 +1155,6 @@ private:
bool mayIntersect(const WVar &b1, const int s1, const WVar &n1, const WVar &b2, const int s2, const WVar &n2) const;
bool mustSupseteq(const WVar &b1, const int s1, const WVar &n1, const WVar &b2, const int s2, const WLinExpr &n2) const;
-
private:
/* Private helper functions. Subject to changes, and should not be used directly. */
diff --git a/include/PPLManager.h b/include/PPLManager.h
index d182222..759137e 100644
--- a/include/PPLManager.h
+++ b/include/PPLManager.h
@@ -43,15 +43,10 @@ class PPLManager {
inline bool equals(const t &v1, const t &v2) { return v1.equals(v2); }
inline void enableSummary() { _init.enableSummary(); }
-
- void setName(elm::String str) {
- cfg_name = str;
- }
private:
t _init;
t _bot;
t _top;
- elm::String cfg_name;
};
} // namespace poly
diff --git a/include/PolyAnalysis.h b/include/PolyAnalysis.h
index 4f2bb3b..b35f4b3 100644
--- a/include/PolyAnalysis.h
+++ b/include/PolyAnalysis.h
@@ -14,6 +14,7 @@
#include <ppl.hh>
#include "PPLManager.h"
+#include "BranchConditionner.h"
namespace otawa {
namespace poly {
diff --git a/include/PolyWrap.h b/include/PolyWrap.h
index d2eaf6d..9c1304f 100644
--- a/include/PolyWrap.h
+++ b/include/PolyWrap.h
@@ -20,6 +20,7 @@ class WCons;
class WLinExpr;
class WPoly;
+void parse(const coef_t& coef, char* buf);
output_t& operator<< (output_t& stream, const coef_t&);
output_t& operator<< (output_t& stream, const WLinExpr&);
output_t& operator<< (output_t& stream, const WCons&);
diff --git a/poly_BranchConditionner.cpp b/poly_BranchConditionner.cpp
new file mode 100644
index 0000000..a234cf5
--- /dev/null
+++ b/poly_BranchConditionner.cpp
@@ -0,0 +1,127 @@
+#include <fstream>
+#include<cstdio>
+
+#include "include/BranchConditionner.h"
+
+namespace otawa{
+ namespace poly{
+
+ void ArmArgumentsDetector::initFunctionParameters(PPLDomain* s, Block* cfgEntry){
+ if(cfgEntry->cfg() != ROOT_CFG(cfgEntry->cfg()))
+ return;
+ std::map<int,WVar> used = USED_ARGS(cfgEntry);
+ // track function arguments stored in registers
+ for(int reg=0; reg<=3; reg++){
+ WVar r = s->varNew(Ident(reg, Ident::ID_REG), NO_STEP, false, false); //< create register variable
+ WVar sr = s->varNew(Ident(-reg-1, Ident::ID_SPECIAL), NO_STEP, false, false); //< create argument variable
+ s->doNewConstraint(sr == r); //< mapping initial register value with argument variable
+ used.emplace(reg,sr); //< add the function arguments to the set of needed variables for projection
+ }
+ USED_ARGS(cfgEntry) = used;
+ }
+
+ int ArmArgumentsDetector::getParamId(Block* cfgEntry, WVar v){
+ std::map<int,WVar> map = USED_ARGS(cfgEntry);
+ for(auto i = map.begin(); i != map.end(); i++){
+ WVar cmp = (*i).second;
+ if(v.guid() == cmp.guid() && v.id() == cmp.id())
+ return (*i).first;
+ }
+ return -1;
+ }
+
+ Conditional::Conditional(Block* b, bool taken, std::string conditions){
+ this->b = b;
+ this->taken = taken;
+ this->conditions = conditions;
+ }
+
+ Block* Conditional::getBlock(){
+ return b;
+ }
+
+ bool Conditional::isTaken(){
+ return taken;
+ }
+
+ std::string Conditional::getConditions(){
+ return conditions;
+ }
+
+ OrderedConditional::OrderedConditional(int loopId, Conditional conditional) : conditional(conditional) {
+ this->loopId = loopId;
+ this->conditional = conditional;
+ }
+
+ OrderedConditional::OrderedConditional(int loopId) : conditional(nullptr,false,"") {
+ this->loopId = loopId;
+ }
+
+ int OrderedConditional::getLoopId(){
+ return loopId;
+ }
+
+ Conditional OrderedConditional::getConditional(){
+ return conditional;
+ }
+
+ OrderedElements::OrderedElements(){
+ order = std::map<int,OrderedConditional>();
+ }
+
+ void OrderedElements::addElement(OrderedConditional conditional){
+ order.emplace(order.size(), conditional);
+ }
+
+ std::map<int,OrderedConditional> OrderedElements::getOrder(){
+ return order;
+ }
+
+ void ConstraintExporter::exportToFile(Conditional c){
+ std::ofstream o;
+ o.open(CONSTRAINTS_FILE, std::ofstream::app);
+ o << c.getBlock()->toBasic()->control()->address() << ";";
+ if(c.isTaken())
+ o << "true;";
+ else
+ o << "false;";
+ o << c.getConditions() << endl;
+ o.close();
+ }
+
+ void ConstraintExporter::resetFile(){
+ std::ofstream o;
+ o.open(CONSTRAINTS_FILE, std::ofstream::trunc);
+ o << std::string("Branching Instruction Address;taken;conditions") <<endl;
+ o.close();
+ }
+
+ void ConstraintExporter::exportOrderedConstraints(OrderedElements order, std::map<int, std::map<bool,Conditional>> loopConstraints){
+ std::map<int,OrderedConditional> oc = order.getOrder();
+ for(int i = 0; i < oc.size(); i++){
+ OrderedConditional wrapper = oc.at(i);
+ // manage non loop elements
+ if(wrapper.getLoopId() == -1){
+ exportToFile(wrapper.getConditional());
+ }
+ // manage loop elements
+ else{
+ std::map<bool,Conditional> branching = loopConstraints.at(wrapper.getLoopId());
+ for(auto i = branching.begin(); i != branching.end(); i++){
+ exportToFile((*i).second);
+ }
+ }
+ }
+ }
+
+ Identifier<std::map<int,WVar>> FUNCTION_ARGS("otawa::poly::FUNCTION_ARGS", std::map<int,WVar>());
+ Identifier<std::map<int,WVar>> USED_ARGS("otawa::poly::USED_ARGS", std::map<int,WVar>());
+ Identifier<CFG*> ROOT_CFG("otawa::poly::ROOT_CFG", nullptr);
+ Identifier<std::map<int,std::map<string,int>>> CURRENT_INSTANCES("otawa::poly::CURRENT_INSTANCES",std::map<int,std::map<string,int>>());
+ Identifier<bool> LOOP_RESET("otawa::poly::LOOP_RESET", false);
+ Identifier<std::map<int,std::map<bool,Conditional>>> LOOP_CONDITIONALS("otawa::poly::LOOP_CONDITIONALS", std::map<int,std::map<bool,Conditional>>());
+ Identifier<int> CURRENT_LOOP("otawa::poly::CURRENT_LOOP", -1);
+ Identifier<int> PREVIOUS_LOOP("otawa::poly::PREVIOUS_LOOP", -1);
+ Identifier<OrderedElements> EXPORT_ORDER("otawa::poly::EXPORT_ORDER", OrderedElements());
+} // namespace poly
+} // namespace otawa
diff --git a/poly_LoopAnalyzer.cpp b/poly_LoopAnalyzer.cpp
new file mode 100644
index 0000000..98755f4
--- /dev/null
+++ b/poly_LoopAnalyzer.cpp
@@ -0,0 +1,329 @@
+#include "include/LoopAnalyzer.h"
+
+namespace otawa{
+namespace poly{
+
+ LoopBound::LoopBound(bool linear, int staticBound, std::string linearBound){
+ this->linear = linear;
+ this->staticBound = staticBound;
+ this->linearBound = linearBound;
+ }
+
+ void LoopBound::exportToFile(std::ofstream *o, int lid){
+ *o << lid;
+ if(linear)
+ *o << ";true;" << linearBound;
+ else
+ *o << ";false;" << staticBound;
+ *o << endl;
+ }
+
+ void LoopBoundsExporter::exportToFile(std::map<int,LoopBound> bounds){
+ // prepare the file
+ std::ofstream o;
+ o.open(LOOP_BOUNDS_FILE, std::ofstream::trunc);
+ o << std::string("Loop id;isLinear;bound") << endl;
+ // exports all the loop bunds
+ for(auto i = bounds.begin(); i != bounds.end(); i++){
+ int lid = (*i).first;
+ LoopBound lb = (*i).second;
+ lb.exportToFile(&o, lid);
+ }
+ // closing stream
+ o.close();
+ }
+
+ void LoopAnalyzer::computeLinearBound(Block* b, std::vector<WCons> cs, MyHTable<int, int> mapping){
+
+ // drop constraints that do not contain any parameter (e.g. lower bound)
+ std::vector<WCons> kept;
+ for(auto c = cs.begin(); c != cs.end(); c++){
+ WCons constraint = *c;
+ // cout << "CONSTRAINT: " << constraint << endl;
+ bool hasBound = false;
+ bool hasPA = false;
+ for(WLinExpr::TermIterator i(constraint.getLE()); i; i++){
+ WVar v = *i;
+ // v0 = loop bound variable
+ if(v.guid() == 0)
+ hasBound = true;
+ // vx = entry parameters
+ if(v.guid() != 0)
+ hasPA = true;
+ // push only if the two are present
+ if(hasBound && hasPA){
+ kept.push_back(constraint);
+ break;
+ }
+ }
+
+ }
+
+ // cout << "Number of constraints: " << kept.size() << endl;
+
+ // extract remaining constraints as a loop bound
+ if(kept.size() == 1){
+
+ // single loop bound
+ auto c = kept.begin();
+ WCons cons = *c;
+
+ // keep coefcicient of the loop bound (division when induction > 1)
+ char bufSign[64];
+
+ // coef1 * v1 + ... + coefn * vn + constant
+ int first = 1;
+ std::string loopBound;
+
+ // pretty printing in a string
+ for(WLinExpr::TermIterator i(cons.getLE()); i; i++){
+ WVar v = *i;
+ coef_t coef = cons.coefficient(v);
+
+ // manage induction and remove loop bound variable from constraint
+ if(v.guid() == 0){
+ gmp_snprintf(bufSign, sizeof(bufSign), "%Zd", &PPL::raw_value(-coef)); // the bound is negative in the right side of the constraint
+ continue;
+ }
+
+ // export the loop as an expression
+ // sign
+ std::string signStr = "";
+ if(!first && coef > 0)
+ signStr = " + ";
+ else if(coef == -1)
+ signStr = " - ";
+
+ // coef
+ std::string coefStr = "";
+ if(coef != 1 && coef != -1){
+ char buf[64];
+ gmp_snprintf(buf, sizeof(buf), "%Zd", &PPL::raw_value(coef));
+ coefStr = std::string(buf);
+ }
+
+ // variable mapping
+ int paramId = -(mapping[v.guid()] + 1); // get the parameter id from the mapping
+ std::string variableStr = "b:" + std::to_string(paramId);
+
+ if(first)
+ first = 0;
+
+ // building constraint term
+ loopBound = coef != 1 && coef != -1 ? loopBound + signStr + coefStr + " * " + variableStr : loopBound + signStr + variableStr;
+ }
+ // final bound
+ coef_t constant = cons.inhomogeneous_term();
+ if(constant != 0){
+ char cstBuf[64];
+ gmp_snprintf(cstBuf, sizeof(cstBuf), "%Zd", &PPL::raw_value(constant));
+ std::string constantStr(cstBuf);
+ loopBound = constant > 0 ? loopBound + " + " + constantStr : loopBound + constantStr; // - is in the constant
+ }
+
+ int induction = atoi(bufSign);
+
+ // checks
+ // check 1 : induction == 0 means that the loop is infinite (or that the coefficient is not an integer value)
+ if(induction == 0)
+ return;
+ // check 2 : induction != 1 means that we must do a division to find the real loop bound
+ if(induction != 1)
+ loopBound = "(" + loopBound + ")/" + std::string(bufSign);
+
+ // save the bound
+ LoopBound lb(true, 0, loopBound);
+ std::map<int,LoopBound> lbs = LOOP_BOUNDS(ROOT_CFG(b->cfg())->entry());
+ if(lbs.find(b->id()) != lbs.end())
+ lbs.erase(b->id());
+ lbs.emplace(b->id(), lb);
+ LOOP_BOUNDS(ROOT_CFG(b->cfg())->entry()) = lbs;
+
+ }
+ else{
+ if(kept.size() != 0)
+ cout << "[WARN] Loop have more than a single bound, case not supported yet !" << endl;
+ }
+
+ // OLD CODE
+ // std::vector<WCons> cs_bef = CONSTRAINTS(b);
+
+ // std::map<int,LoopBound> lbs = LOOP_BOUNDS(ROOT_CFG(b->cfg())->entry());
+ // // clear old data if exist
+ // if(lbs.find(b->id()) != lbs.end())
+ // lbs.erase(b->id());
+
+ // // filtering needed to remove weird constraints which are not the maximum loop bound
+ // std::vector<WCons> cs;
+ // int addedIterations = 0;
+ // std::map<int,coef_t> maximums;
+ // // find the maximum value for each constraint
+ // for(auto i = cs_bef.begin(); i != cs_bef.end(); i++){
+ // WCons c = *i;
+ // for(WLinExpr::TermIterator i(c.getLE()); i; i++){
+ // WVar v = *i;
+ // coef_t coef = c.coefficient(v);
+ // if(maximums.find(v.guid()) == maximums.end()){
+ // maximums.emplace(v.guid(),coef);
+ // }
+ // else{
+ // if(maximums.at(v.guid()) > coef){
+ // maximums.erase(v.guid());
+ // maximums.emplace(v.guid(), coef);
+ // }
+ // }
+ // }
+ // }
+ // // remove constraints not representing the maximum value
+ // for(auto i = cs_bef.begin(); i != cs_bef.end(); i++){
+ // bool add = true;
+ // WCons c = *i;
+ // for(WLinExpr::TermIterator i(c.getLE()); i; i++){
+ // WVar v = *i;
+ // coef_t coef = c.coefficient(v);
+ // //cout << "var :" << v.guid() << ", coef: " << coef << ", should be = to " << maximums.at(v.guid()) << endl;
+ // if(coef > maximums.at(v.guid())){
+ // add = false;
+ // break;
+ // }
+ // }
+ // if(add){
+ // cs.push_back(c);
+ // //cout << "added " << c << endl;
+ // } else {
+ // if(i == cs_bef.begin() || cs.size() == 0){
+ // // sometimes the first loop bound is not correctly extracted since polyhedra will simplify the constraint...
+ // // thus we need to correct the iteration number
+ // addedIterations++;
+ // }
+ // }
+ // }
+
+ // // use remaining constraints to compute loop induction
+ // WCons previous;
+ // WCons current;
+ // coef_t current_diff = 0;
+ // bool error = cs.size() > 0 ? false : true;
+ // for(auto i = cs.begin(); i != cs.end(); i++){
+ // current = *i;
+
+
+ // //cout << "ANALYZING " << current << endl;
+
+ // // detect variace between two constraints
+ // if(!(i == cs.begin())){
+ // coef_t const_current = current.inhomogeneous_term();
+ // coef_t const_previous = previous.inhomogeneous_term();
+ // coef_t diff = const_current - const_previous;
+ // //cout << "DIFF = " << diff << ", OLD DIFF = " << current_diff << endl;
+ // if(current_diff != 0 && current_diff != diff){
+ // error = true; //< This means that we do not have a constant induction
+ // cout << "WARN: There is a difference between loop iterations ? diff = " << diff << ", current diff = " << current_diff << endl;
+ // }
+ // else{
+ // cout << "INFO: Found a regular induction:" << diff << ", " << current_diff << endl;
+ // error = false;
+ // }
+ // current_diff = diff;
+ // }
+ // previous = current;
+ // }
+ // if(error || current_diff == 0 || cs.size() < 2){
+ // // Unable to compute loop induction
+ // if(error && cs.size() >= 2)
+ // cout << "WARN: Could not compute a constant loop induction" << endl;
+ // else if(cs.size() < 2)
+ // cout << "INFO: Could not compute a loop induction (too few iterations)" << endl;
+ // else if(current_diff == 0)
+ // cout << "WARN: Loop induction 0 detected, possibly an infinite loop" << endl;
+
+ // }
+ // else{
+ // // Found a loop induction and thus exports the parametric loop bound
+ //
+ // //cout << "COMPUTED DIFFERENCE = " << current_diff << endl;
+ // WCons c = *(cs.begin()); // use the first loop exit constraint to compute the bound
+
+ // // coef_1 * v_1 + ... + coef_n * v_n + constant
+ // // retrieve constant
+ // coef_t constant = c.inhomogeneous_term();
+ // //cout << "constant: " << constant << endl;
+
+ // // format constraint as a string, which is easier to export in a file
+ // // we need to reverse the constraint since we are in the loop exit case
+ // std::string cString = /*"0 " + op*/"";
+ // std::string opmult = " * ";
+ // std::string opadd = " + ";
+ // std::string opminus = " - ";
+ // char buf[128];
+ // int index=0;
+ // for(WLinExpr::TermIterator i(c.getLE()); i; i++){
+ // WVar v = *i;
+ // coef_t coef = c.coefficient(v);
+ //
+ // // manage operator
+ // std::string opv = index == 0 ? "" : " + ";
+ // opv = -coef > 0 ? opv : " - ";
+
+ // // manage coef != 1 && != 1
+ // if(coef > 1 || coef < -1){
+ // coef > 0 ? parse(coef, buf) : parse(-coef, buf);
+ // std::string cs(buf);
+ // opv = opv + cs + opmult;
+ // }
+
+ // // manage variable name
+ // std::string var = std::to_string(v.guid());
+ // opv = opv + "b:" + var;
+ // cString = cString + opv;
+
+ // ++index;
+ // }
+
+ // // manage constant value
+ // // correction of part of bug 1 : - when += >2, even if bugued for now
+ // /*cout << "CURRENT_DIFF = " << current_diff << endl;
+
+ // constant = current_diff > 0 ? constant - current_diff : constant;
+ // constant = current_diff < 0 ? constant + current_diff : constant;*/
+ //
+ // // manage constant sign
+ // std::string opconst = -constant > 0 ? opadd : opminus;
+
+ // // correction of the loop bound
+ // if(addedIterations != 0){
+ // constant = current_diff > 0 ? constant - (current_diff*addedIterations) : constant;
+ // constant = current_diff < 0 ? constant + (current_diff*addedIterations) : constant;
+ // }
+
+ // constant = -constant > 0 ? -constant : constant;
+
+ // parse(constant, buf);
+ // std::string cst(buf);
+ // if(cst != "0")
+ // cString = cString + opconst + cst;
+
+ // // support for more than i+=1 (i+=x), involves a division operator in the resulting expression
+ // if(current_diff > 1 || current_diff < -1){
+ // cout << "WARN: Unsupported loop bound (induction > 1 || induction < -1)" << endl;
+ // return; // FIXME it does not work in all cases and produces bugs
+ // std::cout << "cString before: " << cString << endl;
+ // ASSERT(current_diff > 0); // cannot be < 0 since it is a loop bound ?
+ // parse(current_diff, buf);
+ // cString = "(" + cString + ")/" + buf;
+ // }
+
+ // std::cout << "COMPUTED LOOP BOUND(" << b->id() << ") = " << cString << endl;
+ // // save the loop bound
+ // LoopBound lb(true, 0, cString);
+ // lbs.emplace(b->id(), lb);
+ // }
+ // LOOP_BOUNDS(ROOT_CFG(b->cfg())->entry()) = lbs;
+ }
+
+ Identifier<std::map<int,LoopBound>> LOOP_BOUNDS("otawa::poly::LOOP_BOUNDS", std::map<int,LoopBound>());
+ Identifier<std::vector<PPLDomain>> LOOP_STATES("otawa::poly::LOOP_STATES", std::vector<PPLDomain>());
+ Identifier<std::vector<WCons>> CONSTRAINTS("ortawa::poly::CONSTRAINTS", std::vector<WCons>());
+
+}
+}
diff --git a/poly_PPLDomain.cpp b/poly_PPLDomain.cpp
index 9f00f3e..abf98a4 100644
--- a/poly_PPLDomain.cpp
+++ b/poly_PPLDomain.cpp
@@ -215,8 +215,8 @@ void PPLDomain::print(io::Output &out) const {
#ifdef INTER_PROCEDURAL
cout << "Summary info: " << endl;
cout << "- Inputs: ";
- for (MyHTable<Ident, guid_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
- const Pair<Ident, guid_t> &p = *it;
+ for (MyHTable<Ident, idval_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
+ const Pair<Ident, idval_t> &p = *it;
if ((p.fst.getType() == Ident::ID_MEM_VAL_INPUT) || (p.fst.getType() == Ident::ID_REG_INPUT))
cout << p.fst << ", ";
}
@@ -410,7 +410,7 @@ void PPLDomain::displayLocVars(io::Output &out) const {
//out << i << endl;
WPoly poly_copy = poly;
WVar v(num_axis);
- poly_copy.add_constraint(v == ssp - i);
+ poly_copy.add_constraint(v == ssp - i - LOC_VAR_SIZE(_props));
out << " [SSP - " << hex(i) << "] ∈ ";
bool found = false;
for (MyHTable<Ident, idval_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
@@ -732,11 +732,11 @@ PPLDomain PPLDomain::getLinearExpr(const Ident &id) {
MyHTable<int, int> inputs;
int axis = 1;
PPLDomain dom(*this); /* make a working copy to do the projections */
- inputs[getVar(id).id()] = 0;
- for (MyHTable<Ident, guid_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
+ inputs[getVar(id, nullptr).id()] = 0;
+ for (MyHTable<Ident, idval_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
if (((*it).fst.getType() == Ident::ID_REG_INPUT) ||
((*it).fst.getType() == Ident::ID_MEM_VAL_INPUT)) {
- inputs[(*it).snd] = axis;
+ inputs[(*it).snd.g] = axis;
axis++;
}
}
@@ -785,6 +785,43 @@ void PPLDomain::doAvExpand(WVar &splus, WVar &sminus, WVar &vplus, WVar &vminus)
}
+void PPLDomain::computeParamBound(Block* header) const {
+ int loopId = header->id();
+ int axis = 1;
+ if (isBottom()) {
+ // cout << "L'etat de la loop " << loopId << " est bottom\n\n";
+ return;
+ }
+ MyHTable<int, int> inputs;
+ MyHTable<int, int> paramMapping;
+ Ident id(loopId, Ident::ID_LOOP);
+
+ inputs[getVar(id, nullptr).id()] = 0;
+
+ for (MyHTable<Ident, idval_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
+ if (((*it).fst.getType() == Ident::ID_SPECIAL) && (*it).fst.getId() < 0) {
+ inputs[(*it).snd.g] = axis;
+ paramMapping[axis] = (*it).fst.getId();
+ axis++;
+ }
+ }
+ PPLDomain dom(*this);
+ // cout << "Etat avant projection: \n\n" << dom << "\n\n";
+ dom.doMap(MapWithHash(inputs));
+ // cout << "Etat projeté: \n\n" << dom << "\n\n";
+
+ // copy poly constraints
+ std::vector<WCons> csts;
+ for (WPoly::ConsIterator it(dom.poly); it; it++) {
+ const WCons &c = *it;
+ csts.push_back(c);
+ }
+ // extract the loop bound
+ LoopAnalyzer la;
+ la.computeLinearBound(header, csts, paramMapping);
+
+ return;
+}
// getLoopBound: a appeler a l'INTERIEUR de la boucle pour avoir une maximisation de la variable d'induction
bound_t PPLDomain::getLoopBound(int loopId) const {
@@ -800,21 +837,21 @@ bound_t PPLDomain::getLoopBound(int loopId) const {
return bound_t::UNBOUNDED;
}
-PPLDomain PPLDomain::onLoopExitLinear(int loop, const PPLDomain &bound) const {
+PPLDomain PPLDomain::onLoopExitLinear(int loop, const PPLDomain &bound, Block* b) const {
PPLManager::t s_out = *this;
#ifdef LINBOUND
- cout << "before onLoopExitLinear: " << s_out << endl;
+ //cout << "before onLoopExitLinear: " << s_out << endl;
cout << "bound: " << bound << endl;
Ident id(loop, Ident::ID_LOOP);
ASSERT(s_out.hasIdent(id)); /* You are supposed to be already inside the loop when you call onLoopExit() */
- WVar v = s_out.getVar(id);
+ WVar v = s_out.getVar(id, nullptr);
MyHTable<int,int> map;
Vector<int> mapped;
- for (MyHTable<Ident, guid_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
+ for (MyHTable<Ident, idval_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
if (((*it).fst.getType() == Ident::ID_REG_INPUT) || ((*it).fst.getType() == Ident::ID_MEM_VAL_INPUT) || ((*it).fst == id)) {
if (hasIdent((*it).fst)) {
- const WVar &v2 = getVar((*it).fst);
- map[(*it).snd] = v2.id();
+ const WVar &v2 = getVar((*it).fst, nullptr);
+ map[(*it).snd.g] = v2.id();
mapped.add(v2.id());
}
}
@@ -830,14 +867,57 @@ PPLDomain PPLDomain::onLoopExitLinear(int loop, const PPLDomain &bound) const {
s_out.poly.intersection_assign(copy.poly);
- s_out.varKill(v);
- cout << "after onLoopExitLinear: " << s_out << endl;
+ s_out.varKill(v, NO_STEP);
+ //cout << "after onLoopExitLinear: " << s_out << endl;
+
+ // addon to support linear loop bounds related to entry parameters
+ /*if(!(*this).isBottom()){
+ MyHTable<int, int> inputs; // prepare projection map
+ PPLDomain dom(*this); // copying the domain
+
+ //cout << "BEFORE PROJECTION:" << endl << dom << endl;
+
+ // retrieve function parameters
+ Block* entry = ROOT_CFG(b->cfg())->entry();
+ std::map<int,WVar> used = USED_ARGS(entry);
+
+ int usedSize = 0;
+ if(used.size() > 0){
+ for (MyHTable<Ident, idval_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
+ int tmp = 0;
+ WVar v = dom.getVar((*it).fst, &tmp);
+ ArmArgumentsDetector detector;
+ int reg_id = detector.getParamId(entry, v);
+ if(dom.hasIdent((*it).fst) && reg_id != -1){
+ inputs[(*it).snd.g] = reg_id;
+ //cout << "v" << (*it).snd.g << " = v" << reg_id << endl;
+ usedSize++;
+ }
+ }
+ //cout << "INPUT SIZE: " << inputs.count() << endl;
+
+ dom.doMap(MapWithHash(inputs));
+ //cout << "AFTER PROJECTION:" << endl << dom << endl;
+
+ // handle constraintq
+ std::vector<WCons> csts = CONSTRAINTS(b);
+ for (WPoly::ConsIterator it(dom.poly); it; it++) {
+ const WCons &c = *it;
+ csts.push_back(c);
+ }
+ CONSTRAINTS(b) = csts;
+ LoopAnalyzer la;
+ la.computeLinearBound(b);
+ }
+ }*/
+ // end of addon
+
#endif
return s_out;
}
-PPLDomain PPLDomain::onLoopExit(int loop, int bound) const {
+PPLDomain PPLDomain::onLoopExit(int loop, int bound, Block* b) const {
PPLManager::t s_out = *this;
Ident id(loop, Ident::ID_LOOP);
ASSERT(s_out.hasIdent(id)); /* You are supposed to be already inside the loop when you call onLoopExit() */
@@ -847,6 +927,49 @@ PPLDomain PPLDomain::onLoopExit(int loop, int bound) const {
s_out.poly.add_constraint(v <= bound);
}
s_out.varKill(v, NO_STEP);
+
+ // addon to support linear loop bounds related to entry parameters
+ /*if(!(*this).isBottom()){
+ MyHTable<int, int> inputs; // prepare projection map
+ PPLDomain dom(*this); // copying the domain
+
+ //cout << "BEFORE PROJECTION:" << endl << dom << endl;
+
+ // retrieve function parameters
+ Block* entry = ROOT_CFG(b->cfg())->entry();
+ std::map<int,WVar> used = USED_ARGS(entry);
+
+ int usedSize = 0;
+ if(used.size() > 0){
+ for (MyHTable<Ident, idval_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
+ int tmp = 0;
+ WVar v = dom.getVar((*it).fst, &tmp);
+ ArmArgumentsDetector detector;
+ int reg_id = detector.getParamId(entry, v);
+ if(dom.hasIdent((*it).fst) && reg_id != -1){
+ inputs[(*it).snd.g] = reg_id;
+ //cout << "v" << (*it).snd.g << " = v" << reg_id << endl;
+ usedSize++;
+ }
+ }
+ //cout << "INPUT SIZE: " << inputs.count() << endl;
+
+ dom.doMap(MapWithHash(inputs));
+ //cout << "AFTER PROJECTION:" << endl << dom << endl;
+
+ // handle constraintq
+ std::vector<WCons> csts = CONSTRAINTS(b);
+ for (WPoly::ConsIterator it(dom.poly); it; it++) {
+ const WCons &c = *it;
+ csts.push_back(c);
+ }
+ CONSTRAINTS(b) = csts;
+ LoopAnalyzer la;
+ la.computeLinearBound(b);
+ }
+ }*/
+ // end of addon
+
if (s_out.poly.is_empty()) {
#ifdef POLY_DEBUG
cout << "State is Bottom after onLoopExit (will not propagate states to exit-edges)" << endl;
@@ -875,7 +998,7 @@ PPLDomain PPLDomain::onLoopEntry(int loop) const {
return s_out;
}
-PPLDomain PPLDomain::onBranch(bool taken) const {
+PPLDomain PPLDomain::onBranch(bool taken, Block* b) const {
if (isBottom()) {
return PPLDomain();
}
@@ -887,19 +1010,22 @@ PPLDomain PPLDomain::onBranch(bool taken) const {
cout << "Filtering, compare_reg is: " << compare_reg << ", compare_op is: " << compare_op << ", taken=" << taken << endl;
#endif
-
+ // cout << "======================================================= " << b->id() << " " << taken << endl;
+ // cout << "state before OP:" << endl << res << endl;
switch (this_op) {
case sem::NE: {
WPoly poly2 = res.poly;
res.poly.add_constraint(res.getVar(compare_reg, nullptr) <= -1);
poly2.add_constraint(res.getVar(compare_reg, nullptr) >= 1);
res.poly.poly_hull_assign(poly2);
+ // cout << "NE" << endl;
break;
PDBG("NE!" << endl)
}
case sem::EQ:
PDBG("EQ!" << endl)
res.poly.add_constraint(res.getVar(compare_reg, nullptr) == 0);
+ // cout << "EQ" << endl;
break;
case sem::GE:
case sem::UGE:
@@ -924,6 +1050,175 @@ PPLDomain PPLDomain::onBranch(bool taken) const {
default:
break;
};
+
+ //projection of res to get conditions
+ if (!res.isBottom()) {
+ MyHTable<int, int> inputs;
+ PPLDomain dom(res); /* make a working copy to do the projections */
+ // cout << "State after OP:" << endl << dom << endl;
+ //std::map<int,WVar> used = USED_ARGS(b->cfg()->entry());
+ Block* entry = ROOT_CFG(b->cfg())->entry();
+ std::map<int,WVar> used = USED_ARGS(entry);
+ //cout << "SIZE OF USED: " << used.size() << endl;
+ if(used.size() != 0){
+ //inputs[res.getVar(compare_reg).id()] = 0;
+ for (MyHTable<Ident, idval_t, HashIdent>::PairIterator it = idmap.getPairIter(); it; it++) {
+ int tmp = 0;
+ WVar v = dom.getVar((*it).fst, &tmp);
+ ArmArgumentsDetector detector;
+ int reg_id = detector.getParamId(entry, v);
+ if(dom.hasIdent((*it).fst) && reg_id != -1){
+ inputs[(*it).snd.g] = reg_id;
+ //cout << "v" << (*it).snd.g << " = v" << reg_id << endl;
+ }
+ }
+ //cout << "INPUT SIZE: " << inputs.count() << endl;
+ dom.doMap(MapWithHash(inputs));
+
+ // handle constraints
+ std::string constraints = "";
+ for (WPoly::ConsIterator it(dom.poly); it; it++) {
+ const WCons &c = *it;
+
+ //cout << "ref: " << c << endl;
+
+ // c = 0 <OP> coef_1 * v_1 + ... + coef_n * v_n + constant
+ // retrieve constant
+ coef_t constant = c.inhomogeneous_term();
+ //cout << "constant: " << constant << endl;
+
+ // retrieve function parameters
+ std::map<guid_t, coef_t> vs; ///< first = parameter register, second = coef
+ int i = 0;
+ for(WPoly::VarIterator vi(dom.poly); vi; vi++){
+ WVar v = *vi;
+ if(c.has_var(v)){
+ coef_t coef = c.coefficient(v);
+ //cout << b->cfg()->name() << "[" << v.guid() << "] * " << coef << endl;
+ vs.emplace(v.guid(), coef);
+ }
+ }
+
+ // retrieve OP
+ std::string op;
+ switch (c.getType())
+ {
+ case CONS_EQ:
+ op = "=";
+ break;
+ case CONS_GE:
+ op = "≤";
+ break;
+ default:
+ cout << "[ERROR] Unrecognized constraint type while searching for branch conditions" << endl;
+ abort();
+ break;
+ }
+
+ // format constraint as a string, which is easier to export in a file
+ std::string cString = "0 " + op;
+ std::string opmult = " * ";
+ std::string opadd = " + ";
+ std::string opminus = " - ";
+ char buf[128];
+ for(auto i = vs.begin(); i != vs.end(); i++){
+ if((*i).second > 0){
+ std::string opv = " ";
+ if(i != vs.begin()){
+ opv = opadd;
+ }
+ if((*i).second != 1){
+ parse((*i).second, buf);
+ std::string coef(buf);
+ opv = opv + coef;
+ opv = opv + opmult;
+ }
+ cString = cString + opv;
+ }
+ else{
+ std::string opv = opminus;
+ if((*i).second != -1){
+ parse(-((*i).second), buf);
+ std::string coef(buf);
+ opv = opv + coef;
+ opv = opv + opmult;
+ }
+ cString = cString + opv;
+ }
+ std::string var2 = std::to_string((*i).first);
+ std::string var = "b:" + var2;
+ cString = cString + var;
+ }
+ if(constant != 0){
+ std::string opconst = "";
+ if(constant > 0){
+ opconst = opadd;
+ parse(constant, buf);
+ }
+ else{
+ opconst = opminus;
+ parse(-constant, buf);
+ }
+ std::string cst(buf);
+ cString = cString + opconst;
+ cString = cString + cst;
+ }
+ std::string concat = "";
+ if(constraints.length() != 0)
+ concat = " & ";
+ cString = concat + cString;
+ constraints = constraints + cString;
+ }
+
+ if(constraints != ""){
+ //std::cout << "constraints found for " << b->toBasic()->control()->address() << ": " << constraints << endl;
+ // export constraints
+ // only if we are not in a loop
+ Conditional c(b, taken, constraints);
+ int current_loop = CURRENT_LOOP(ROOT_CFG(b->cfg()));
+ if(current_loop == -1){
+ //ConstraintExporter exp;
+ //exp.exportToFile(c);
+ // we now export constraints later in order
+ OrderedElements orderingManager = EXPORT_ORDER(ROOT_CFG(b->cfg()));
+ OrderedConditional oc(current_loop, c);
+ orderingManager.addElement(oc);
+ EXPORT_ORDER(ROOT_CFG(b->cfg())) = orderingManager;
+ }
+ // otherwise store it to keep only the last conditional and export it later on
+ else{
+ std::map<int, std::map<bool,Conditional>> loopConditionalMap = LOOP_CONDITIONALS(ROOT_CFG(b->cfg()));
+ // try to get current map if exists
+ std::map<bool,Conditional> conditional;
+ bool exists = true;
+ if(loopConditionalMap.find(current_loop) != loopConditionalMap.end()){
+ conditional = loopConditionalMap.at(current_loop);
+ }
+ else{
+ conditional = std::map<bool,Conditional>();
+ exists = false;
+ // it does not exist yet so we can push it in ordered export
+ OrderedElements orderingManager = EXPORT_ORDER(ROOT_CFG(b->cfg()));
+ OrderedConditional oc(current_loop);
+ orderingManager.addElement(oc);
+ EXPORT_ORDER(ROOT_CFG(b->cfg())) = orderingManager;
+ }
+ // replace the conditional with current conditional
+ conditional.erase(taken);
+ conditional.emplace(taken, c);
+ loopConditionalMap.erase(current_loop);
+ loopConditionalMap.emplace(current_loop, conditional);
+ LOOP_CONDITIONALS(ROOT_CFG(b->cfg())) = loopConditionalMap;
+ }
+ }
+ else{
+ //cout << "no constraints found for " << b->toBasic()->control()->address() << endl;
+ //cout << "STATE WITH NO CONSTRAINT RELATED TO MARKED PROGRAM PARAMETERS" << endl << "DOM (projected poly):" << endl << dom << endl << "RES (original poly):" << endl << res << endl;
+ }
+ }
+ }
+
+
//res.victims.add(res.getVar(res.compare_reg).guid());
res.varKill(res.compare_reg);
res.compare_reg = Ident();
@@ -1581,6 +1876,7 @@ PPLDomain PPLDomain::onSemInst(const BasicBlock *bb, const sem::inst &si, int in
bool isArray = _isArrayStore(bb, storeAddr);
+ // cout << "arraystore: " << isArray << endl;
sem::reg_t src = si.d();
Ident idStoreValue(src, Ident::ID_REG);
@@ -1721,12 +2017,12 @@ PPLDomain PPLDomain::onSemInst(const BasicBlock *bb, const sem::inst &si, int in
Ident idAddrNew(s_out.mem_ref - 1, Ident::ID_MEM_ADDR);
int step;
WVar newAddr = s_out.getVar(idAddrNew, &step);
-
- cout << "Create var with arraystore, attempt to find existing array" << endl;
+ // cout << "Create var with arraystore, attempt to find existing array" << endl;
+ cout << "\n";
for (MyHTable<Ident, idval_t, HashIdent>::PairIterator it = s_out.idmap.getPairIter(); it; it++) {
if ((*it).fst.getType() == Ident::ID_MEM_ADDR) {
if ((*it).fst == idAddrNew) break;
- cout << "Checking if tab " << (*it).fst << " is the start of " << idAddrNew << " \n";
+ // cout << "Checking if tab " << (*it).fst << " is the start of " << idAddrNew << " \n";
WVar tabAddr = s_out.getVar((*it).fst, &step);
Ident idCountAddr((*it).fst.getId(), Ident::ID_MEM_COUNT);
WVar count = s_out.getVar(idCountAddr, nullptr);
@@ -1744,27 +2040,25 @@ PPLDomain PPLDomain::onSemInst(const BasicBlock *bb, const sem::inst &si, int in
int tmp = num.get_si() / den.get_si();
if (tmp > 0) {
step = tmp;
- cout << "Guessed step: " << step << endl;
+ // cout << "Guessed step: " << step << endl;
}
}
}
if (step != STEP_BOT && s_out.shouldFold(tabAddr, step, count, newAddr)) {
fold = true;
- cout << "yes (keep existing step: " << step << ") " << endl;
+ // cout << "yes (keep existing step: " << step << ") " << endl;
} else {
- cout << "no." << endl;
+ // cout << "no." << endl;
}
Ident idValPlus((*it).fst.getId(), Ident::ID_MEM_VAL_PLUS);
// cout << step << " " << fold << " " << s_out.hasIdent(idValPlus) << "\n";
if (fold && s_out.hasIdent(idValPlus)) {
+ cout << "actually folding with: " << step << endl;
- cout << "Folding store " << idAddrNew << " into existing array " << (*it).fst << endl;
-
- s_out.showTab((*it).fst);
-
+ // cout << "Folding store " << idAddrNew << " into existing array " << (*it).fst << endl;
Ident idValMinus((*it).fst.getId(), Ident::ID_MEM_VAL_MINUS);
Ident idValNew(idAddrNew.getId(), Ident::ID_MEM_VAL);
Ident idCountNew(idAddrNew.getId(), Ident::ID_MEM_COUNT);
@@ -1925,11 +2219,11 @@ PPLDomain PPLDomain::onSemInst(const BasicBlock *bb, const sem::inst &si, int in
const WVar &v = s_out.memSingleCreate(loadAddr, loadReg, false);
if (s_out._summary != nullptr) {
// Unknown LOAD value. If we are summarizing, create an input.
- Ident idInputAddr = s_out.getIdent(v);
+ Ident idInputAddr = s_out.getIdent(v, NULL);
Ident idInputVal = Ident(idInputAddr.getId(), Ident::ID_MEM_VAL_INPUT);
Ident idCurrentVal = Ident(idInputAddr.getId(), Ident::ID_MEM_VAL);
- WVar currentVal = s_out.getVar(idCurrentVal);
- WVar inputVal = s_out.varNew(idInputVal); // c'est une variable qu'on lit donc pas de damaged
+ WVar currentVal = s_out.getVar(idCurrentVal, NULL);
+ WVar inputVal = s_out.varNew(idInputVal, NULL, false, false); // c'est une variable qu'on lit donc pas de damaged
PDBG("Summarizing: creating new input memory: " << " what= " << idInputVal << " where=" << idInputAddr << endl)
// s_out._summary->_inputs.add(idInputVal);
s_out.doNewConstraint(currentVal == inputVal);
@@ -2275,7 +2569,8 @@ void PPLDomain::listMemoryVariables() {
num_loop++;
}
}
- cout << (num_av + num_sing + num_tab) << " var mem, dont " << num_av << " avatars (x4), " << num_tab << " tab (x3), et " << num_sing << " acces singuliers (x3), " << num_reg << " regs, " << num_loop << " boucles, et " << num_spe << "spe" << "(tot: " << total << ")\n";
+ // DEBUG
+ //cout << (num_av + num_sing + num_tab) << " var mem, dont " << num_av << " avatars (x4), " << num_tab << " tab (x3), et " << num_sing << " acces singuliers (x3), " << num_reg << " regs, " << num_loop << " boucles, et " << num_spe << "spe" << "(tot: " << total << ")\n";
if ((num_av*4 + (num_sing + num_tab)*3 + num_reg + num_loop + num_spe) != total) {
print(cout);
@@ -2407,7 +2702,7 @@ WVar PPLDomain::getVarOrNew(const Ident &ident, bool create_input) {
ASSERT(ident.getType() == Ident::ID_REG);
Ident idInput(ident.getId(), Ident::ID_REG_INPUT);
// _summary->_inputs.add(idInput);
- WVar input = varNew(idInput);
+ WVar input = varNew(idInput, NULL, false, false);
doNewConstraint(input == v);
PDBG("Summarizing: creating new input register " << input << endl)
}
@@ -2977,7 +3272,7 @@ void PPLDomain::_doMatchGlobals(PPLDomain &l1, PPLDomain &r1,
uint32_t staticVal;
dfa::INITIAL_STATE(_ws)->get(staticAddr, staticVal); // get static constant value from OTAWA
PDBG("Static adress: " << hex(staticAddr) << " value: " << hex(staticVal) << endl)
- cout << "Static adress: " << hex(staticAddr) << " value: " << hex(staticVal) << endl;
+ DBG("Static adress: " << hex(staticAddr) << " value: " << hex(staticVal) << endl)
Ident leftIdAddr = l1.getIdent(v, STEP_BOT); /* TODO get initial values for arrays */
Ident leftIdVal = Ident(leftIdAddr.getId(), Ident::ID_MEM_VAL);
@@ -3122,10 +3417,8 @@ void PPLDomain::_doUnify(PPLDomain &l1 /* back */, PPLDomain &r1 /* header */, P
invLeftCSMap.put((*it).snd, (*it).fst);
}
- /*
_doMatchGlobals(l1, r1, leftCSMap, invRightCSMap);
_doMatchGlobals(r1, l1, rightCSMap, invLeftCSMap);
- */
/* Detect variable in left (i.e. backstate) subjected to avatar creation */
if (avcreate) {
for (MyHTable<guid_t, LEVect >::PairIterator it(leftCSMap); it; it++) {
@@ -3142,7 +3435,7 @@ void PPLDomain::_doUnify(PPLDomain &l1 /* back */, PPLDomain &r1 /* header */, P
guid_t newBase = 42, newCount = 42;
guid_t newValPlus = 42, newValMinus = 42;
- /* cout << "Creating avatar for backstate base variable: " << (*it).fst << endl; */
+ // cout << "Creating avatar for backstate base variable: " << (*it).fst << endl;
bool created = PPLDomain::_avcreate_helper(r1, l1, rightVars, idBase, WVar((*it).fst), step, newBase, newCount, newValPlus, newValMinus);
if (!created) {
@@ -3754,10 +4047,8 @@ bool PPLDomain::_isArrayStore(const BasicBlock *bb, const WVar &storeAddr) const
} else if (v.guid() > 0) {
has_bound = true;
}
- if (has_store && has_bound) {
- cout << "found cons: " << c << endl;
+ if (has_store && has_bound)
return true;
- }
}
}
return false;
@@ -3911,48 +4202,6 @@ void PPLDomain::enableSummary() {
doNewConstraint(spInput == getVar(Ident(13, Ident::ID_REG)));
*/
}
-
-extern elm::String cfgname;
-
-void PPLDomain::showTab(const Ident &ident) {
- Ident id_ssp(Ident::ID_START_SP, Ident::ID_SPECIAL);
- int step;
- WVar ssp = getVar(id_ssp, nullptr);
- WVar store = getVar(ident, &step);
-
- WPoly temp = poly;
- temp.filter_lambda([store, ssp](guid_t guid) {
- return guid == store.guid() || guid == ssp.guid();
- });
- for (WPoly::ConsIterator it(temp); it; it++) {
- const WCons &c = (*it);
- bool has_store = false;
- bool has_ssp = false;
- bool has_other = false;
- if (!c.is_equality()) continue;
- for (WCons::TermIterator it2(c); it2; it2++) {
- const WVar &v = (*it2);
- if (v.guid() == ssp.guid()) {
- has_ssp = true;
- } else if (v.guid() == store.guid()) {
- has_store = true;
- } else {
- has_other = true;
- }
- if (has_store && has_ssp && !has_other && c.coefficient(ssp) == -c.coefficient(store)) {
- int cst = -c.inhomogeneous_term().get_si();
- int coef = -c.coefficient(store).get_si();
- cout << "ARRAY: type=local func=" << cfgname << " addr=START_SP-" << hex(cst/coef) << endl;
- }
- if (has_store && !has_ssp && !has_other) {
- int cst = -c.inhomogeneous_term().get_si();
- int coef = c.coefficient(store).get_si();
-
- cout << "ARRAY: type=global addr=" << hex(cst/coef) << endl;
- }
- }
- }
-}
p::feature POLY_ANALYSIS_FEATURE("otawa::poly::POLY_ANALYSIS_FEATURE", new Maker<PolyAnalysis>());
Identifier<int> LOC_VAR_SIZE("otawa::poly::LOC_VAR_SIZE", 4);
diff --git a/poly_PolyAnalysis.cpp b/poly_PolyAnalysis.cpp
index c6d5a34..b9d84b1 100644
--- a/poly_PolyAnalysis.cpp
+++ b/poly_PolyAnalysis.cpp
@@ -18,11 +18,13 @@
#include "include/PPLDomain.h"
#include "include/PPLManager.h"
#include "include/PolyAnalysis.h"
+
+#include "include/LoopAnalyzer.h"
+
namespace otawa {
namespace poly {
using namespace otawa;
using namespace util;
-elm::String cfgname;
p::declare PolyAnalysis::reg = p::init("otawa::poly::PolyAnalysis", Version(1, 0, 0))
.require(COLLECTED_CFG_FEATURE)
@@ -44,6 +46,17 @@ void PolyAnalysis::configure(const PropList &props) {
PolyAnalysis::state_t PolyAnalysis::processHeader(ai::CFGGraph &graph, MyHTable<int,PPLDomain> &lb,
BasicBlock *header, PPLManager& man, ai::EdgeStore<PPLManager, ai::CFGGraph>& store, MyHTable<int, HeaderState> &headerState) {
+
+ // manage loop context
+ if(CURRENT_LOOP(ROOT_CFG(header->cfg())) != header->id()){
+ PREVIOUS_LOOP(header) = CURRENT_LOOP(ROOT_CFG(header->cfg()));
+ CURRENT_LOOP(ROOT_CFG(header->cfg())) = header->id();
+ }
+ // reset function instances for each iteration to insert in the same place the conditionals
+ std::map<int,std::map<string,int>> resetMap = CURRENT_INSTANCES(ROOT_CFG(header->cfg()));
+ resetMap.erase(header->id());
+ CURRENT_INSTANCES(ROOT_CFG(header->cfg())) = resetMap;
+
state_t entryState = man.bot();
state_t backState = man.bot();
@@ -92,14 +105,17 @@ DBG("Widening, entryState = " << entryState)
bound_t bound = backState.getLoopBound(header->id());
backState.setBound(header->id(), bound);
#endif
+/* cout << "\n\n\nBackState pour calcul de bornes de boucles parametrique: \n" << backState << "\n\n\n"; */
- PDBG("ITERATION: bound=" << int(bound) << endl)
+ backState.computeParamBound(header);
+
+ /*PDBG("ITERATION: bound=" << int(bound) << endl)
if(bound == -1)
DBG("ITERATION: bound=" << color::IRed << "UNREACHABLE")
else if(bound == -2)
DBG("ITERATION: bound=" << color::IRed << "UNBOUNDED")
else
- DBG("ITERATION: bound=" << color::IRed << int(bound))
+ DBG("ITERATION: bound=" << color::IRed << int(bound))*/
#ifndef LINBOUND
@@ -112,7 +128,7 @@ DBG("Widening, entryState = " << entryState)
lb[header->id()] = PPLDomain();
#ifdef LINBOUND
- const PPLDomain &oldBound = lb[header->id()];
+ PPLDomain &oldBound = lb[header->id()];
lb[header->id()] = oldBound.onMerge(linearBound, false);
#endif
@@ -173,6 +189,25 @@ void PolyAnalysis::processBB(PPLManager *man, ai::CFGGraph &graph, MyHTable<int,
*/
state_t s = man->bot();
+ if(LOOP_RESET(*ana)){
+ Block* h = nullptr;
+ auto iter = (*ana)->ins();
+ for(int i=0;i<(*ana)->countIns();i++){
+ if(ROOT_CFG((*ana)->cfg()) != nullptr && (*iter)->source()->id() == CURRENT_LOOP(ROOT_CFG((*ana)->cfg()))){
+ h = (*iter)->source();
+ break;
+ }
+ iter++;
+ }
+ if(h != nullptr){
+ CURRENT_LOOP(ROOT_CFG((*ana)->cfg())) = PREVIOUS_LOOP(h);
+ }
+ else{
+ cout << "ERROR : h is null" << endl;
+ //exit(1);
+ }
+ }
+
DBG("Processing " << color::On_Blu << "BB " << ((BasicBlock*)*ana)->index() << (LOOP_HEADER(*ana) ? " (loop header)" : "") << color::RCol)
/* Special processing for loop headers, to handle loop bounds and widening */
if (LOOP_HEADER(*ana)) {
@@ -184,6 +219,12 @@ void PolyAnalysis::processBB(PPLManager *man, ai::CFGGraph &graph, MyHTable<int,
s = ana.input();
}
+ /* doing this avoid bottom state */
+ if(((BasicBlock*)*ana)->index() == 1){
+ ArmArgumentsDetector detector;
+ detector.initFunctionParameters(&s, ((BasicBlock*)*ana)->cfg()->entry());
+ }
+
if (s.isBottom()) {
#ifdef POLY_DEBUG
cout << "! Skip block because input state is Bottom" << endl;
@@ -199,6 +240,39 @@ void PolyAnalysis::processBB(PPLManager *man, ai::CFGGraph &graph, MyHTable<int,
if ((*ana)->isSynth()) {
/* Handle call to another function */
CFG *subCFG = (*ana)->toSynth()->callee();
+
+ /* handle crash on null CFG */
+ if (subCFG == nullptr) {
+ cout << "Error: calling a null CFG" << endl;
+ exit(1);
+ }
+
+ ROOT_CFG(subCFG) = ROOT_CFG((*ana)->cfg());
+ int oldLoop = CURRENT_LOOP(ROOT_CFG(subCFG)); //< store old loop id to restore it after return
+ //CURRENT_LOOP(ROOT_CFG(subCFG)) = -1;
+ string name = subCFG->name();
+
+ // create artificiel loop context for function calls
+ std::map<int,std::map<string,int>> currentInstancesAll = CURRENT_INSTANCES(ROOT_CFG(subCFG));
+ std::map<string,int> currentInstances;
+ if(currentInstancesAll.find(oldLoop) == currentInstancesAll.end()){
+ currentInstances = std::map<string,int>();
+ }
+ else{
+ currentInstances = currentInstancesAll.at(oldLoop);
+ currentInstancesAll.erase(oldLoop);
+ }
+ int instance = 1; // default value
+ if(currentInstances.find(name) != currentInstances.end()){
+ instance = currentInstances.at(name) + 1; //< new value
+ currentInstances.erase(name); //< to replace the value
+ }
+ currentInstances.emplace(name,instance);
+ CURRENT_LOOP(ROOT_CFG(subCFG)) = - MAX_LOOP * oldLoop + instance; // unique negative value for each loop
+ currentInstancesAll.emplace(oldLoop,currentInstances);
+ CURRENT_INSTANCES(ROOT_CFG(subCFG)) = currentInstancesAll;
+ // end of artificial loop context
+
cout << "Call from " << (*ana)->toSynth()->caller()->name() << " to " << subCFG->name() << endl;
bool compose_ok = false;
@@ -273,6 +347,7 @@ void PolyAnalysis::processBB(PPLManager *man, ai::CFGGraph &graph, MyHTable<int,
} else {
processCFG(*subCFG, s, lb, false, false);
cout << "Return from " << subCFG->name() << " to " << (*ana)->toSynth()->caller()->name() << endl;
+ CURRENT_LOOP(ROOT_CFG(subCFG)) = oldLoop;
}
}
@@ -345,7 +420,7 @@ void PolyAnalysis::processBB(PPLManager *man, ai::CFGGraph &graph, MyHTable<int,
/* Filtering: apply branch condition on edge state */
PDBG("BEFORE FILTERING: " << endl)
PDBG(edgeState)
- edgeState = edgeState.onBranch(e->isTaken());
+ edgeState = edgeState.onBranch(e->isTaken(), *ana);
if (edgeState.isBottom()) {
continue;
}
@@ -369,6 +444,11 @@ void PolyAnalysis::processBB(PPLManager *man, ai::CFGGraph &graph, MyHTable<int,
if (LOOP_EXIT_EDGE(e) != nullptr) {
/* Exit edge: remove virtual loop counter, and apply loop bound constraint on state */
Block *bb = LOOP_EXIT_EDGE(e);
+
+ // tells that we get out of a loop
+ if(LOOP_HEADER(e->source())){
+ LOOP_RESET(e->sink()) = true;
+ }
/*
* FIXME: should be bound = s.getLoopBound(bb->id()) but we need to fix the widening to make it work
@@ -380,7 +460,7 @@ void PolyAnalysis::processBB(PPLManager *man, ai::CFGGraph &graph, MyHTable<int,
PDBG("Bound on loop exit: " << bound << endl)
if (!linBound.isBottom()) {
- edgeState = edgeState.onLoopExitLinear(bb->id(), linBound);
+ edgeState = edgeState.onLoopExitLinear(bb->id(), linBound, bb);
if (edgeState.isBottom())
continue;
}
@@ -388,12 +468,14 @@ void PolyAnalysis::processBB(PPLManager *man, ai::CFGGraph &graph, MyHTable<int,
#endif
edgeState.doRemoveUselessAvatars();
edgeState.doRemoveAllAvatars();
+#ifndef LINBOUND
if (bound >= 0) {
- edgeState = edgeState.onLoopExit(bb->id(), bound);
+ edgeState = edgeState.onLoopExit(bb->id(), bound, bb);
if (edgeState.isBottom()) {
continue;
}
}
+#endif
}
edgeState.doFinalizeUpdate();
ana.check(*e, edgeState);
@@ -494,9 +576,6 @@ void PolyAnalysis::processCFG(CFG &cfg, state_t &s, MyHTable<int, PPLDomain> &lb
PDBG("Init state: " << s << endl)
cout << "Entering CFG: " << cfg.name() << endl;
- auto curname = cfgname;
- cfgname = cfg.name();
-
WorkListDriver<PPLManager, ai::CFGGraph, ai::EdgeStore<PPLManager, ai::CFGGraph>, PseudoTopoOrder> ana(*man, graph, store, _orders[cfg.index()]);
while (ana) {
@@ -505,7 +584,6 @@ void PolyAnalysis::processCFG(CFG &cfg, state_t &s, MyHTable<int, PPLDomain> &lb
}
cout << "Exiting CFG: " << cfg.name() << endl;
- cfgname = curname;
Block *bb = graph.exit();
Block::EdgeIter edge(bb->ins());
@@ -546,6 +624,9 @@ void PolyAnalysis::processWorkSpace(WorkSpace *ws) {
elm::log::Debug::setColorFlag(false);
#endif
+ ConstraintExporter exporter;
+ exporter.resetFile();
+
struct timeval now;
gettimeofday(&now, nullptr);
@@ -562,12 +643,17 @@ void PolyAnalysis::processWorkSpace(WorkSpace *ws) {
CFG *entry = coll->get(0);
+ ROOT_CFG(entry) = entry;
state_t dummy;
ASSERT(dummy.getSummary() == nullptr);
SUMMARIZE(ws) = false;
MyHTable<int, PPLDomain> bounds;
MyHTable<int, int> static_bounds;
processCFG(*entry, dummy, bounds, true /* is entry */, false /* summarize */);
+
+ // add non parametric loop bounds to the loop bounds
+ std::map<int,LoopBound> loop_bounds;
+
#ifdef LINBOUND
cout << "PARAMETRIC LOOP BOUNDS: " << endl;
for (MyHTable<int, PPLDomain>::PairIterator it(bounds); it; it++) {
@@ -590,6 +676,10 @@ void PolyAnalysis::processWorkSpace(WorkSpace *ws) {
for (CFGCollection::Iter iter2(coll); iter2; iter2++) {
for (CFG::BlockIter iter((*iter2)->blocks()); iter; iter++) {
Block *bb = (*iter);
+
+ if(loop_bounds.size() == 0 && ROOT_CFG(bb->cfg()) != nullptr)
+ loop_bounds = LOOP_BOUNDS(ROOT_CFG(bb->cfg())->entry());
+
if (LOOP_HEADER(bb)) {
if (static_bounds.hasKey(bb->id())) {
MAX_ITERATION(bb) = static_bounds[bb->id()];
@@ -600,6 +690,10 @@ void PolyAnalysis::processWorkSpace(WorkSpace *ws) {
cout << "[" << (*iter2)->name() << "]"
<< "TOTAL_ITERATION(" << bb->id() << ") = " << TOTAL_ITERATION(bb) << endl;
*/
+ if(MAX_ITERATION(bb) >= 0){ // if found without error, add non parametric loop bounds to the file
+ LoopBound lb(false, MAX_ITERATION(bb), "");
+ loop_bounds.emplace(bb->id(), lb);
+ }
}
}
delete _orders[(*iter2)->index()];
@@ -609,6 +703,10 @@ void PolyAnalysis::processWorkSpace(WorkSpace *ws) {
for (CFGCollection::Iter iter2(coll); iter2; iter2++) {
for (CFG::BlockIter iter((*iter2)->blocks()); iter; iter++) {
Block *bb = (*iter);
+
+ if(loop_bounds.size() == 0 && ROOT_CFG(bb->cfg()) != nullptr)
+ loop_bounds = LOOP_BOUNDS(ROOT_CFG(bb->cfg())->entry());
+
if (LOOP_HEADER(bb)) {
cout << "[" << (*iter2)->name() << "]"
<< "MAX_ITERATION(" << bb->id() << ") = " << MAX_ITERATION(bb) << endl;
@@ -616,11 +714,34 @@ void PolyAnalysis::processWorkSpace(WorkSpace *ws) {
cout << "[" << (*iter2)->name() << "]"
<< "TOTAL_ITERATION(" << bb->id() << ") = " << TOTAL_ITERATION(bb) << endl;
*/
+ if(MAX_ITERATION(bb) >= 0){ // if found without error, add non parametric loop bounds to the file
+ LoopBound lb(false, MAX_ITERATION(bb), "");
+ loop_bounds.emplace(bb->id(), lb);
+ }
}
}
delete _orders[(*iter2)->index()];
}
#endif
+ // export constraints
+ bool exported = false;
+ for (CFGCollection::Iter iter2(coll); iter2; iter2++) {
+ for (CFG::BlockIter iter((*iter2)->blocks()); iter; iter++) {
+ Block *bb = (*iter);
+ ConstraintExporter exp;
+ if(ROOT_CFG(bb->cfg()) == nullptr)
+ continue;
+ OrderedElements order = EXPORT_ORDER(ROOT_CFG(bb->cfg())); //< order also contains non loop conditionals
+ std::map<int,std::map<bool,Conditional>> loopConditions = LOOP_CONDITIONALS(ROOT_CFG(bb->cfg()));
+ exp.exportOrderedConstraints(order, loopConditions);
+ LoopBoundsExporter lbe;
+ lbe.exportToFile(loop_bounds);
+ exported = true;
+ break;
+ }
+ if(exported)
+ break;
+ }
cout << "Max variable count: " << max_vars << endl;
cout << "Max constraint count: " << max_cons << endl;
struct timeval after;
diff --git a/poly_PolyWrap.cpp b/poly_PolyWrap.cpp
index e5242a1..d79709e 100644
--- a/poly_PolyWrap.cpp
+++ b/poly_PolyWrap.cpp
@@ -7,6 +7,11 @@ namespace poly {
using namespace elm::io;
using namespace PPL;
+void parse(const coef_t& coef, char* buf){
+ gmp_snprintf(buf, sizeof(buf), "%Zd", &raw_value(coef));
+ buf[sizeof(buf) - 1] = 0;
+}
+
output_t& operator<< (output_t& stream, const coef_t& coef) {
char buf[128];
gmp_snprintf(buf, sizeof(buf), "%Zd", &raw_value(coef));
--
GitLab