Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Introducing support for Fixed-Point rational arithmetic

  • Loading branch information...
commit 8cb72a27e6d8a5b2887767e1cd0b16c852e4f5c0 1 parent 8a0a05e
Marco Pensallorto authored
1  src/common.cc
View
@@ -28,6 +28,7 @@ const char *TRUE_TOKEN = "TRUE";
const char *BOOL_TOKEN = "boolean";
const char *UNSIGNED_TOKEN = "unsigned";
const char *SIGNED_TOKEN = "signed";
+const char *FIXED_TOKEN = "fixed";
const char *INTEGER_TOKEN = "integer";
const char *TEMPORAL_TOKEN = "temporal";
const char *MAIN_TOKEN = "main";
3  src/common.hh
View
@@ -116,12 +116,13 @@ public:
class Object : public IObject {
};
-/* tokens, defined in common.cc */
+/* internal tokens, defined in common.cc */
extern const char *FALSE_TOKEN;
extern const char *TRUE_TOKEN;
extern const char *BOOL_TOKEN;
extern const char *UNSIGNED_TOKEN;
extern const char *SIGNED_TOKEN;
+extern const char *FIXED_TOKEN;
extern const char *INTEGER_TOKEN;
extern const char *TEMPORAL_TOKEN;
extern const char *MAIN_TOKEN;
3  src/enc/enc.cc
View
@@ -90,8 +90,9 @@ MonolithicEncoding::MonolithicEncoding()
{}
// algebraic encoding uses monolithic as a builing block
-AlgebraicEncoding::AlgebraicEncoding(unsigned width, bool is_signed, ADD *dds)
+AlgebraicEncoding::AlgebraicEncoding(unsigned width, unsigned fract, bool is_signed, ADD *dds)
: f_width(width)
+ , f_fract(fract)
, f_signed(is_signed)
, f_temporary(NULL != dds)
{
3  src/enc/enc.hh
View
@@ -122,9 +122,10 @@ protected:
{ assert(0); }
// width is number of *digits* here, dds is reserved for temporary encodings
- AlgebraicEncoding(unsigned width, bool is_signed, ADD *dds = NULL);
+ AlgebraicEncoding(unsigned width, unsigned fract, bool is_signed, ADD *dds = NULL);
unsigned f_width;
+ unsigned f_fract; // non-zero for fixed encodings
bool f_signed;
bool f_temporary;
};
25 src/enc/enc_mgr.cc
View
@@ -36,26 +36,37 @@ IEncoding_ptr EncodingMgr::make_encoding(Type_ptr tp)
IEncoding_ptr res = NULL;
BooleanType_ptr btype;
- AlgebraicType_ptr atype;
+ SignedAlgebraicType_ptr sa_type;
+ UnsignedAlgebraicType_ptr ua_type;
+ FixedAlgebraicType_ptr fa_type;
EnumType_ptr etype;
ArrayType_ptr vtype;
assert(NULL != tp);
if (NULL != (btype = dynamic_cast<BooleanType_ptr>(tp))) {
- DEBUG << "Encoding Boolean " << btype << endl;
+ DEBUG << "Encoding boolean " << btype << endl;
res = new BooleanEncoding();
}
- else if (NULL != (atype = dynamic_cast<AlgebraicType_ptr>(tp))) {
- DEBUG << "Encoding Algebraic " << atype << endl;
- res = new AlgebraicEncoding(atype->width(), atype->is_signed(), atype->dds());
+ else if (NULL != (sa_type = dynamic_cast<SignedAlgebraicType_ptr>(tp))) {
+ DEBUG << "Encoding signed algebraic " << sa_type << endl;
+ res = new AlgebraicEncoding(sa_type->width(), 0, true, sa_type->dds());
+ }
+ else if (NULL != (ua_type = dynamic_cast<UnsignedAlgebraicType_ptr>(tp))) {
+ DEBUG << "Encoding unsigned algebraic " << ua_type << endl;
+ res = new AlgebraicEncoding(ua_type->width(), 0, false, ua_type->dds());
+ }
+ else if (NULL != (fa_type = dynamic_cast<FixedAlgebraicType_ptr>(tp))) {
+ DEBUG << "Encoding fixed-point algebraic " << fa_type << endl;
+ res = new AlgebraicEncoding(fa_type->width(), fa_type->fract(),
+ true, fa_type->dds());
}
else if (NULL != (etype = dynamic_cast<EnumType_ptr>(tp))) {
- DEBUG << "Encoding Enum " << etype << endl;
+ DEBUG << "Encoding enum " << etype << endl;
res = new EnumEncoding(etype->literals());
}
else if (NULL != (vtype = dynamic_cast<ArrayType_ptr>(tp))) {
- DEBUG << "Encoding Array " << vtype << endl;
+ DEBUG << "Encoding array " << vtype << endl;
Encodings encs;
for (unsigned i =0; i < vtype->size(); ++ i) {
encs.push_back(make_encoding(vtype->of()));
2  src/expr/expr_mgr.cc
View
@@ -39,7 +39,7 @@ ExprMgr::ExprMgr()
// unsigned and signed base integer types identifiers
unsigned_expr = make_identifier(UNSIGNED_TOKEN);
signed_expr = make_identifier(SIGNED_TOKEN);
-
+ fixed_expr = make_identifier(FIXED_TOKEN);
integer_expr = make_identifier(INTEGER_TOKEN); // abstract
// main module identifier
11 src/expr/expr_mgr.hh
View
@@ -191,6 +191,9 @@ public:
inline Expr_ptr make_dot(Expr_ptr a, Expr_ptr b)
{ return make_expr(DOT, a, b); }
+ inline Expr_ptr make_comma(Expr_ptr a, Expr_ptr b)
+ { return make_expr(COMMA, a, b); }
+
inline Expr_ptr make_subscript(Expr_ptr a, Expr_ptr b)
{ return make_expr(SUBSCRIPT, a, b); }
@@ -217,6 +220,13 @@ public:
inline Expr_ptr make_signed_type(unsigned bits)
{ return make_params(signed_expr, make_iconst((value_t) bits)); }
+ inline Expr_ptr make_fixed_type(unsigned int_digits, unsigned fract_digits)
+ {
+ return make_params(fixed_expr,
+ make_comma(make_iconst((value_t) int_digits),
+ make_iconst((value_t) fract_digits)));
+ }
+
Expr_ptr make_enum_type(ExprSet& literals);
/* builtin identifiers */
@@ -406,6 +416,7 @@ private:
// base for (un-)signed integer
Expr_ptr unsigned_expr;
Expr_ptr signed_expr;
+ Expr_ptr fixed_expr;
Expr_ptr integer_expr; // reserved for abstract integer-type
/* shared pools */
9 src/parser/grammars/smv.g
View
@@ -718,9 +718,12 @@ type_name returns [Type_ptr res]
| { $res = tm.find_signed(width->value()); } )
- // ranges
- // | lhs=int_constant '..' rhs=int_constant
- // { $res = tm.find_range(lhs, rhs); }
+ // fixed point rational numbers
+ | 'fixed' '(' iwidth = int_constant ',' fract_width = int_constant ')' (
+ '[' size=int_constant ']'
+ { $res = tm.find_fixed_array(iwidth->value(), fract_width->value(), size->value()); }
+
+ | { $res = tm.find_fixed(iwidth->value(), fract_width->value()); } )
// enumeratives, pure symbolic
| enum_type[lits]
30 src/type/type.cc
View
@@ -38,16 +38,32 @@ IntegerType::IntegerType(TypeMgr& owner) // abstract
f_repr = f_owner.em().make_integer_type();
}
-AlgebraicType::AlgebraicType(TypeMgr& owner, unsigned width, bool is_signed, ADD *dds)
+AlgebraicType::AlgebraicType(TypeMgr& owner, ADD *dds)
: Type(owner)
- , f_width(width)
- , f_signed(is_signed)
, f_dds(dds)
{
- f_repr = f_signed
- ? f_owner.em().make_signed_type(width)
- : f_owner.em().make_unsigned_type(width)
- ;
+}
+
+SignedAlgebraicType::SignedAlgebraicType(TypeMgr& owner, unsigned width, ADD *dds)
+ : AlgebraicType(owner, dds)
+ , f_width(width)
+{
+ f_repr = f_owner.em().make_signed_type(width);
+}
+
+UnsignedAlgebraicType::UnsignedAlgebraicType(TypeMgr& owner, unsigned width, ADD *dds)
+ : AlgebraicType(owner, dds)
+ , f_width(width)
+{
+ f_repr = f_owner.em().make_unsigned_type(width);
+}
+
+FixedAlgebraicType::FixedAlgebraicType(TypeMgr& owner, unsigned width, unsigned fract, ADD *dds)
+ : AlgebraicType(owner, dds)
+ , f_width(width)
+ , f_fract(fract)
+{
+ f_repr = f_owner.em().make_fixed_type(width, fract);
}
ArrayType::ArrayType(TypeMgr& owner, Type_ptr of, unsigned size)
81 src/type/type.hh
View
@@ -23,7 +23,6 @@
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
*
**/
-
#ifndef TYPE_H
#define TYPE_H
@@ -35,10 +34,10 @@
#include <type_mgr.hh>
-/* Supported data types: boolean, integers (signed and unsigned)
- enums, module instances. */
+/* Supported data types: boolean, integers (signed and unsigned),
+ fixed-point, enums, module instances, arrays of all-of-the-above. */
-// NOTE: types are *immutable* by design!
+/* REMARK types are *immutable* by design! */
// ostream helper, uses FQExpr printer (see expr/expr.cc)
ostream& operator<<(ostream& os, Type_ptr type);
@@ -50,7 +49,7 @@ ostream& operator<<(ostream& os, const Type_ptr type);
typedef class Type* Type_ptr;
class Type : public Object {
public:
- inline Expr_ptr repr() const
+ Expr_ptr repr() const
{ return f_repr; }
virtual ~Type()
@@ -83,33 +82,83 @@ protected:
typedef class AlgebraicType* AlgebraicType_ptr;
class AlgebraicType : public Type {
public:
- inline unsigned width() const
+ virtual unsigned width() const =0;
+ virtual bool is_signed() const =0;
+
+ ADD *dds() const
+ { return f_dds; }
+
+protected:
+ friend class TypeMgr; // ctors not public
+ AlgebraicType(TypeMgr& owner, ADD *dds = NULL);
+
+ // this is reserved for temp encodings, it's NULL for ordinary algebraics
+ ADD *f_dds;
+};
+
+
+typedef class SignedAlgebraicType* SignedAlgebraicType_ptr;
+class SignedAlgebraicType : public AlgebraicType {
+public:
+ unsigned width() const
{ return f_width; }
- inline bool is_signed() const
- { return f_signed; }
+ bool is_signed() const
+ { return true; }
- inline ADD *dds() const
- { return f_dds; }
+ protected:
+ friend class TypeMgr; // ctors not public
+ SignedAlgebraicType(TypeMgr& owner, unsigned width, ADD *dds = NULL);
+
+ unsigned f_width;
+};
+
+typedef class UnsignedAlgebraicType* UnsignedAlgebraicType_ptr;
+class UnsignedAlgebraicType : public AlgebraicType {
+public:
+ unsigned width() const
+ { return f_width; }
+
+ bool is_signed() const
+ { return false; }
protected:
friend class TypeMgr; // ctors not public
- AlgebraicType(TypeMgr& owner, unsigned width, bool is_signed, ADD *dds = NULL);
+ UnsignedAlgebraicType(TypeMgr& owner, unsigned width, ADD *dds = NULL);
unsigned f_width;
- bool f_signed;
+};
- // this is reserved for temp encodings, it's NULL for ordinary algebraics
- ADD *f_dds;
+
+typedef class FixedAlgebraicType* FixedAlgebraicType_ptr;
+class FixedAlgebraicType : public AlgebraicType {
+public:
+ unsigned width() const
+ { return f_width; }
+
+ unsigned fract() const
+ { return f_fract; }
+
+ /* in current implementation fixed is signed only */
+ bool is_signed() const
+ { return true; }
+
+protected:
+ friend class TypeMgr; // ctors not public
+ FixedAlgebraicType(TypeMgr& owner, unsigned width, unsigned fract, ADD *dds = NULL);
+
+ unsigned f_width;
+ unsigned f_fract;
};
+
typedef class ArrayType* ArrayType_ptr;
class ArrayType : public Type {
public:
- inline unsigned size() const
+ unsigned size() const
{ return f_size; }
- inline Type_ptr of() const
+ Type_ptr of() const
{ return f_of; }
protected:
80 src/type/type_mgr.cc
View
@@ -48,7 +48,7 @@ const Type_ptr TypeMgr::find_unsigned(unsigned bits)
if (NULL != res) return res;
// new type, needs to be registered before returning
- res = new AlgebraicType( *this, bits, false);
+ res = new UnsignedAlgebraicType( *this, bits);
register_type(descr, res);
return res;
}
@@ -61,7 +61,8 @@ const Type_ptr TypeMgr::find_unsigned_array(unsigned digits, unsigned size)
if (NULL != res) return res;
// new type, needs to be registered before returning
- res = new ArrayType( *this, find_unsigned(digits), size);
+ res = new ArrayType( *this,
+ find_unsigned(digits), size);
register_type(descr, res);
return res;
}
@@ -73,7 +74,7 @@ const Type_ptr TypeMgr::find_signed(unsigned bits)
if (NULL != res) return res;
// new type, needs to be registered before returning
- res = new AlgebraicType( *this, bits, true); // signed
+ res = new SignedAlgebraicType( *this, bits);
register_type(descr, res);
return res;
}
@@ -86,11 +87,41 @@ const Type_ptr TypeMgr::find_signed_array(unsigned digits, unsigned size)
if (NULL != res) return res;
// new type, needs to be registered before returning
- res = new ArrayType( *this , find_signed(digits), size);
+ res = new ArrayType( *this,
+ find_signed(digits), size);
register_type(descr, res);
return res;
}
+const Type_ptr TypeMgr::find_fixed(unsigned int_digits, unsigned fract_digits)
+{
+ Expr_ptr descr(f_em.make_fixed_type(int_digits, fract_digits));
+ Type_ptr res = lookup_type(descr);
+ if (NULL != res) return res;
+
+ // new type, needs to be registered before returning
+ res = new FixedAlgebraicType( *this, int_digits, fract_digits);
+ register_type(descr, res);
+ return res;
+}
+
+const Type_ptr TypeMgr::find_fixed_array(unsigned int_digits,
+ unsigned fract_digits,
+ unsigned size)
+{
+ Expr_ptr descr(f_em.make_subscript( f_em.make_fixed_type(int_digits, fract_digits),
+ f_em.make_iconst(size)));
+ Type_ptr res = lookup_type(descr);
+ if (NULL != res) return res;
+
+ // new type, needs to be registered before returning
+ res = new ArrayType( *this,
+ find_fixed(int_digits, fract_digits), size);
+ register_type(descr, res);
+ return res;
+}
+
+
const Type_ptr TypeMgr::find_enum(ExprSet& lits)
{
/*
@@ -161,13 +192,48 @@ EnumType_ptr TypeMgr::as_enum(const Type_ptr tp) const
}
bool TypeMgr::is_algebraic(const Type_ptr tp) const
+{ return (NULL != dynamic_cast <AlgebraicType*> (tp)); }
+
+bool TypeMgr::is_signed_algebraic(const Type_ptr tp) const
+{ return (NULL != dynamic_cast <SignedAlgebraicType*> (tp)); }
+
+bool TypeMgr::is_unsigned_algebraic(const Type_ptr tp) const
+{ return (NULL != dynamic_cast <UnsignedAlgebraicType*> (tp)); }
+
+bool TypeMgr::is_fixed_algebraic(const Type_ptr tp) const
+{ return (NULL != dynamic_cast <FixedAlgebraicType*> (tp)); }
+
+AlgebraicType_ptr TypeMgr::as_algebraic(const Type_ptr tp) const
{
- return (NULL != dynamic_cast <AlgebraicType*> (tp));
+ AlgebraicType_ptr res = dynamic_cast
+ <const AlgebraicType_ptr> (tp);
+ assert(res);
+
+ return res;
}
-AlgebraicType_ptr TypeMgr::as_algebraic(const Type_ptr tp) const
+SignedAlgebraicType_ptr TypeMgr::as_signed_algebraic(const Type_ptr tp) const
+{
+ SignedAlgebraicType_ptr res = dynamic_cast
+ <const SignedAlgebraicType_ptr> (tp);
+ assert(res);
+
+ return res;
+}
+
+UnsignedAlgebraicType_ptr TypeMgr::as_unsigned_algebraic(const Type_ptr tp) const
+{
+ UnsignedAlgebraicType_ptr res = dynamic_cast
+ <const UnsignedAlgebraicType_ptr> (tp);
+ assert(res);
+
+ return res;
+}
+
+FixedAlgebraicType_ptr TypeMgr::as_fixed_algebraic(const Type_ptr tp) const
{
- AlgebraicType_ptr res = dynamic_cast <const AlgebraicType_ptr> (tp);
+ FixedAlgebraicType_ptr res = dynamic_cast
+ <const FixedAlgebraicType_ptr> (tp);
assert(res);
return res;
15 src/type/type_mgr.hh
View
@@ -74,6 +74,9 @@ public:
const Type_ptr find_signed(unsigned digits);
const Type_ptr find_signed_array(unsigned digits, unsigned size);
+ const Type_ptr find_fixed(unsigned int_digits, unsigned fract_digits);
+ const Type_ptr find_fixed_array(unsigned int_digits, unsigned fract_digits, unsigned size);
+
const Type_ptr find_enum(ExprSet& lits);
const Type_ptr find_instance(Expr_ptr identifier);
@@ -89,6 +92,9 @@ public:
// an algebraic variable
bool is_algebraic(const Type_ptr tp) const;
+ bool is_signed_algebraic(const Type_ptr tp) const;
+ bool is_unsigned_algebraic(const Type_ptr tp) const;
+ bool is_fixed_algebraic(const Type_ptr tp) const;
// an ENUM
bool is_enum(const Type_ptr tp) const;
@@ -109,6 +115,15 @@ public:
typedef class AlgebraicType* AlgebraicType_ptr;
AlgebraicType_ptr as_algebraic(const Type_ptr tp) const;
+ typedef class SignedAlgebraicType* SignedAlgebraicType_ptr;
+ SignedAlgebraicType_ptr as_signed_algebraic(const Type_ptr tp) const;
+
+ typedef class UnsignedAlgebraicType* UnsignedAlgebraicType_ptr;
+ UnsignedAlgebraicType_ptr as_unsigned_algebraic(const Type_ptr tp) const;
+
+ typedef class FixedAlgebraicType* FixedAlgebraicType_ptr;
+ FixedAlgebraicType_ptr as_fixed_algebraic(const Type_ptr tp) const;
+
typedef class EnumType* EnumType_ptr;
EnumType_ptr as_enum(const Type_ptr tp) const;
Please sign in to comment.
Something went wrong with that request. Please try again.