fix issue #380

ibex-team · May 24, 2019 · e9cc9d5 · e9cc9d5
1 parent d0644c6
commit e9cc9d5
Show file tree

Hide file tree

Showing 14 changed files with 170 additions and 62 deletions.
diff --git a/src/parser/ibex_CtrGenerator.cpp b/src/parser/ibex_CtrGenerator.cpp
@@ -2,10 +2,10 @@
 //                                  I B E X                                   
 // File        : ibex_CtrGenerator.cpp
 // Author      : Gilles Chabert
-// Copyright   : Ecole des Mines de Nantes (France)
+// Copyright   : IMT Atlantique (France)
 // License     : See the LICENSE file
 // Created     : Jun 12, 2012
-// Last Update : Jun 12, 2012
+// Last Update : May 22, 2019
 //============================================================================
 
 #include "ibex_CtrGenerator.h"
@@ -69,6 +69,12 @@ void CtrGenerator::visit(const P_OneConstraint& c) {
 	}
 }
 
+void CtrGenerator::visit(const P_TmpSymbolDecl& tmp) {
+	// TODO: if the temporary symbol is never used,
+	// the generated expression is a memory leak
+	scopes().top().add_expr_tmp_symbol(tmp.symbol, &tmp.expr.generate());
+}
+
 void CtrGenerator::visit(const P_ConstraintList& list) {
 	for (vector<P_NumConstraint*>::const_iterator it=list.ctrs.begin(); it!=list.ctrs.end(); it++) {
 		visit(**it);
@@ -81,15 +87,13 @@ void CtrGenerator::visit(const P_ConstraintLoop& loop) {
 	int begin=loop.first_value._2int();
 	int end=loop.last_value._2int();
 
-	scopes().push(scopes().top());
-
-	scopes().top().add_iterator(name);
-
 	for (int i=begin; i<=end; i++) {
+		scopes().push(scopes().top());
+		scopes().top().add_iterator(name);
 		scopes().top().set_iter_value(name,i);
 		visit(loop.ctrs);
+		scopes().pop();
 	}
-	scopes().pop();
 }
 
 void CtrGenerator::visit(const P_ThickEquality& eq) {

diff --git a/src/parser/ibex_CtrGenerator.h b/src/parser/ibex_CtrGenerator.h
@@ -2,10 +2,10 @@
 //                                  I B E X                                   
 // File        : ibex_CtrGenerator.h
 // Author      : Gilles Chabert
-// Copyright   : Ecole des Mines de Nantes (France)
+// Copyright   : IMT Atlantique (France)
 // License     : See the LICENSE file
 // Created     : Jun 12, 2012
-// Last Update : Jun 12, 2012
+// Last Update : May 22, 2019
 //============================================================================
 
 #ifndef __IBEX_CTR_GENERATOR_H__
@@ -27,6 +27,7 @@ namespace parser {
 
 class P_NumConstraint;
 class P_OneConstraint;
+class P_TmpSymbolDecl;
 class P_ConstraintList;
 class P_ConstraintLoop;
 class P_ThickEquality;
@@ -40,6 +41,7 @@ class CtrGenerator {
 
 	void visit(const P_NumConstraint& c);
 	void visit(const P_OneConstraint& c);
+	void visit(const P_TmpSymbolDecl& c);
 	void visit(const P_ConstraintList& l);
 	void visit(const P_ConstraintLoop& l);
 	void visit(const P_ThickEquality& e);

diff --git a/src/parser/ibex_P_ExprGenerator.cpp b/src/parser/ibex_P_ExprGenerator.cpp
@@ -244,15 +244,9 @@ void ExprGenerator::visit(const P_ExprNode& e) {
 			case P_ExprNode::INFTY:      e.lab=LabelConst::pos_infinity(); break;
 			case P_ExprNode::VAR_SYMBOL: e.lab=new LabelNode(scope.get_var(((P_ExprVarSymbol&) e).name).first); break;
 			case P_ExprNode::CST_SYMBOL: e.lab=new LabelConst(scope.get_cst(((P_ExprCstSymbol&) e).name)); break;
-			case P_ExprNode::TMP_SYMBOL:
-				{
-					const P_ExprNode& e2=scope.get_expr_tmp_expr(((P_ExprTmpSymbol&) e).name);
-					visit(e2);
-					e.lab = new LabelNode(&e2.lab->node());
-				}
-				break;
-			case P_ExprNode::CST:     e.lab=new LabelConst(((P_ExprConstant&) e).value,true); break;
-			case P_ExprNode::ITER:    e.lab=new LabelConst(scope.get_iter_value(((P_ExprIter&) e).name)); break;
+			case P_ExprNode::TMP_SYMBOL: e.lab=new LabelNode(scope.get_expr_tmp_expr(((P_ExprTmpSymbol&) e).name)); break;
+			case P_ExprNode::CST:        e.lab=new LabelConst(((P_ExprConstant&) e).value,true); break;
+			case P_ExprNode::ITER:       e.lab=new LabelConst(scope.get_iter_value(((P_ExprIter&) e).name)); break;
 			case P_ExprNode::IDX:
 			case P_ExprNode::IDX_RANGE:
 			case P_ExprNode::IDX_ALL:

diff --git a/src/parser/ibex_P_NumConstraint.cpp b/src/parser/ibex_P_NumConstraint.cpp
@@ -1,15 +1,17 @@
 //============================================================================
 //                                  I B E X                                   
-// File        : ibex_ParserNumConstraint.cpp
+// File        : ibex_P_NumConstraint.cpp
 // Author      : Gilles Chabert
-// Copyright   : Ecole des Mines de Nantes (France)
+// Copyright   : IMT Atlantique (France)
 // License     : See the LICENSE file
 // Created     : Jun 12, 2012
-// Last Update : Jun 12, 2012
+// Last Update : May 22, 2019
 //============================================================================
 
 #include "ibex_P_NumConstraint.h"
 
+#include <stdlib.h>
+
 using namespace std;
 
 namespace ibex {
@@ -30,27 +32,57 @@ P_OneConstraint::~P_OneConstraint() {
 	delete &expr;
 }
 
+P_TmpSymbolDecl::P_TmpSymbolDecl(const char* symbol, const P_ExprNode* expr) : symbol(strdup(symbol)), expr(*expr) {
+
+}
+
+void P_TmpSymbolDecl::print(std::ostream& os) const {
+	os << symbol << ":=" << expr << endl;
+}
+
+P_TmpSymbolDecl::~P_TmpSymbolDecl() {
+	free((char*) symbol);
+	delete &expr;
+}
+
+void P_OneConstraint::print(ostream& os) const {
+	os << expr << op << '0';
+}
+
 P_ConstraintList::P_ConstraintList(vector<P_NumConstraint*>* _ctrs) : ctrs(*_ctrs) {
 
 }
 
 P_ConstraintList::~P_ConstraintList() {
-	for (vector<P_NumConstraint*>::const_iterator it=ctrs.begin(); it!=ctrs.end(); it++) {
+	for (vector<P_NumConstraint*>::const_iterator it=ctrs.begin(); it!=ctrs.end(); ++it) {
 		delete *it;
 	}
 	delete &ctrs;
 }
 
+void P_ConstraintList::print(ostream& os) const {
+	for (vector<P_NumConstraint*>::const_iterator it=ctrs.begin(); it!=ctrs.end(); ++it) {
+		os << **it << endl;
+	}
+}
+
 P_ConstraintLoop::P_ConstraintLoop(const char* iter, const P_ExprNode* first_value, const P_ExprNode* last_value, vector<P_NumConstraint*>* ctrs) :
 		 iter(strdup(iter)), first_value(*first_value), last_value(*last_value), ctrs(ctrs) {
 
 }
 
 P_ConstraintLoop::~P_ConstraintLoop() {
+	free((char*) iter);
 	delete &first_value;
 	delete &last_value;
 }
 
+void P_ConstraintLoop::print(ostream& os) const {
+	os << "for " << iter << "=" << first_value << ":" << last_value << endl;
+	os << ctrs;
+	os << "end" << endl;
+}
+
 P_ThickEquality::P_ThickEquality(const P_ExprNode* expr, const Interval& d) : expr(*expr), d(d) {
 
 }
@@ -59,6 +91,10 @@ P_ThickEquality::~P_ThickEquality() {
 	delete &expr;
 }
 
+void P_ThickEquality::print(ostream& os) const {
+	os << expr << " in " << d;
+}
 
 } // end namespace parser
+
 } // end namespace ibex
diff --git a/src/parser/ibex_P_NumConstraint.h b/src/parser/ibex_P_NumConstraint.h
@@ -1,11 +1,11 @@
 //============================================================================
 //                                  I B E X                                   
-// File        : ibex_ParserNumConstraint.h
+// File        : ibex_P_NumConstraint.h
 // Author      : Gilles Chabert
-// Copyright   : Ecole des Mines de Nantes (France)
+// Copyright   : IMT Atlantique (France)
 // License     : See the LICENSE file
 // Created     : Jun 12, 2012
-// Last Update : Jun 12, 2012
+// Last Update : May 22, 2019
 //============================================================================
 
 #ifndef __IBEX_PARSER_NUM_CONSTRAINT_H__
@@ -14,6 +14,8 @@
 #include "ibex_CtrGenerator.h"
 #include "ibex_NumConstraint.h"
 
+#include <iostream>
+
 namespace ibex {
 
 namespace parser {
@@ -22,6 +24,8 @@ class P_NumConstraint {
 public:
 	virtual void acceptVisitor(CtrGenerator& g) const=0;
 
+	virtual void print(std::ostream& os) const=0;
+
 	/**
 	 * delete all the nodes of the expression *excepted symbols*
 	 */
@@ -32,10 +36,12 @@ class P_OneConstraint : public P_NumConstraint {
 public:
 	P_OneConstraint(const P_ExprNode* left, CmpOp op, const P_ExprNode* right);
 
-	void acceptVisitor(CtrGenerator& g) const {
+	virtual void acceptVisitor(CtrGenerator& g) const {
 		g.visit(*this);
 	}
 
+	virtual void print(std::ostream& os) const;
+
 	/**
 	 * delete all the nodes of the expression *excepted symbols*
 	 */
@@ -45,14 +51,33 @@ class P_OneConstraint : public P_NumConstraint {
 	CmpOp op;
 };
 
+class P_TmpSymbolDecl : public P_NumConstraint {
+public:
+	P_TmpSymbolDecl(const char* symbol, const P_ExprNode* expr);
+
+	virtual void acceptVisitor(CtrGenerator& g) const {
+		g.visit(*this);
+	}
+
+	virtual void print(std::ostream& os) const;
+
+	virtual ~P_TmpSymbolDecl();
+
+	const char* symbol;
+	const P_ExprNode& expr;
+};
+
+
 class P_ConstraintList : public P_NumConstraint {
 public:
 	P_ConstraintList(std::vector<P_NumConstraint*>* ctrs);
 
-	void acceptVisitor(CtrGenerator& g) const {
+	virtual void acceptVisitor(CtrGenerator& g) const {
 		g.visit(*this);
 	}
 
+	virtual void print(std::ostream& os) const;
+
 	/**
 	 * delete all the nodes of the expression *excepted symbols*
 	 */
@@ -66,10 +91,12 @@ class P_ConstraintLoop : public P_NumConstraint {
 public:
 	P_ConstraintLoop(const char* iter, const P_ExprNode* first_value, const P_ExprNode* last_value, std::vector<P_NumConstraint*>* ctrs);
 
-	void acceptVisitor(CtrGenerator& g) const {
+	virtual void acceptVisitor(CtrGenerator& g) const {
 		g.visit(*this);
 	}
 
+	virtual void print(std::ostream& os) const;
+
 	/**
 	 * delete all the nodes of the expression *excepted symbols*
 	 */
@@ -96,14 +123,22 @@ class P_ThickEquality : public P_NumConstraint {
 	 */
 	~P_ThickEquality();
 
-	void acceptVisitor(CtrGenerator& g) const {
+	virtual void acceptVisitor(CtrGenerator& g) const {
 		g.visit(*this);
 	}
 
+	virtual void print(std::ostream& os) const;
+
 	const P_ExprNode& expr;
 	Interval d;
 };
 
+
+inline std::ostream& operator<<(std::ostream& os, const P_NumConstraint& ctr) {
+	ctr.print(os);
+	return os;
+}
+
 } // end namespace parser
 } // end namespace ibex
 

diff --git a/src/parser/ibex_P_Source.cpp b/src/parser/ibex_P_Source.cpp
@@ -1,10 +1,10 @@
 //============================================================================
 //                                  I B E X                                   
-// File        : ibex_ParserSource.cpp
+// File        : ibex_P_Source.cpp
 // Author      : Gilles Chabert
-// Copyright   : Ecole des Mines de Nantes (France)
+// Copyright   : IMT Atlantique (France)
 // License     : See the LICENSE file
-// Created     : Jun 12, 2012
+// Created     : May 22, 2019
 // Last Update : Jun 12, 2012
 //============================================================================
 
@@ -39,5 +39,16 @@ void P_Source::cleanup() {
 	ctrs=NULL;
 }
 
+ostream& operator<<(ostream& os, const P_Source& source) {
+	if (source.goal)
+		os << "minimize " << *source.goal << endl;
+	if (source.ctrs) {
+		os << "constraints" << endl;
+		os << *source.ctrs;
+	}
+	return os;
+}
+
 } // end namespace parser
+
 } // end namespace ibex
diff --git a/src/parser/ibex_P_Source.h b/src/parser/ibex_P_Source.h
@@ -1,11 +1,11 @@
 //============================================================================
 //                                  I B E X                                   
-// File        : ibex_ParserSource.h
+// File        : ibex_P_Source.h
 // Author      : Gilles Chabert
-// Copyright   : Ecole des Mines de Nantes (France)
+// Copyright   : IMT Atlantique (France)
 // License     : See the LICENSE file
 // Created     : Jun 12, 2012
-// Last Update : Jun 12, 2012
+// Last Update : May 22, 2019
 //============================================================================
 
 #ifndef __IBEX_PARSER_SOURCE_H__
@@ -45,6 +45,8 @@ class P_Source {
 	P_ConstraintList* ctrs;
 };
 
+std::ostream& operator<<(std::ostream& os, const P_Source& source);
+
 } // end namespace parser
 } // end namespace ibex
 

diff --git a/src/parser/ibex_Scope.cpp b/src/parser/ibex_Scope.cpp
@@ -85,15 +85,15 @@ class Scope::S_Func : public Scope::S_Object {
 
 class Scope::S_ExprTmp : public Scope::S_Object {
 public:
-	S_ExprTmp(const P_ExprNode* expr) : expr(expr) { }
+	S_ExprTmp(const ExprNode* expr) : expr(expr) { }
 
 	S_Object* copy() const { return new S_ExprTmp(expr); }
 
 	int token() const { return TK_EXPR_TMP_SYMBOL; }
 
 	void print(ostream& os) const { os << "expression tmp " << *expr; }
 
-	const P_ExprNode* expr;
+	const ExprNode* expr;
 };
 
 class Scope::S_Entity : public Scope::S_Object {
@@ -188,7 +188,7 @@ void Scope::add_func(const char* id, Function* f) {
 	//cout << "[parser] add function " << *f << endl;
 }
 
-void Scope::add_expr_tmp_symbol(const char* id, const P_ExprNode* expr) {
+void Scope::add_expr_tmp_symbol(const char* id, const ExprNode* expr) {
 	tab.insert_new(id, new S_ExprTmp(expr));
 }
 
@@ -230,10 +230,10 @@ Function& Scope::get_func(const char* id) {
 	return *((const S_Func&) s).f;
 }
 
-const P_ExprNode& Scope::get_expr_tmp_expr(const char* id) const {
+const ExprNode* Scope::get_expr_tmp_expr(const char* id) const {
 	const S_Object& s=*tab[id];
 	assert(s.token()==TK_EXPR_TMP_SYMBOL);
-	return *((const S_ExprTmp&) s).expr;
+	return ((const S_ExprTmp&) s).expr;
 }
 
 std::pair<const ExprSymbol*,const Domain*> Scope::get_var(const char* id) const {