Skip to content


Subversion checkout URL

You can clone with
Download ZIP
tree: 8cb72a27e6
Fetching contributors…

Cannot retrieve contributors at this time

172 lines (129 sloc) 5.904 kB
* @file type_mgr.hh
* @brief Type system classes (TypeMgr)
* This module contains definitions and services that implement an
* optimized storage for expressions. Expressions are stored in a
* Directed Acyclic Graph (DAG) for data sharing.
* Copyright (C) 2012 Marco Pensallorto < marco AT pensallorto DOT gmail DOT com >
* This library is free software; you can redistribute it and/or
* modify it under the terms of the GNU Lesser General Public
* License as published by the Free Software Foundation; either
* version 2.1 of the License, or (at your option) any later version.
* This library is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* Lesser General Public License for more details.
* You should have received a copy of the GNU Lesser General Public
* License along with this library; if not, write to the Free Software
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
#ifndef TYPE_MGR_H
#define TYPE_MGR_H
#include <expr.hh>
#include <expr_mgr.hh>
typedef class Type* Type_ptr; // fwd
typedef unordered_map<Expr_ptr, Type_ptr, PtrHash, PtrEq> TypeMap;
typedef pair<TypeMap::iterator, bool> TypeHit;
The TypeMgr has two well-defined responsibilites:
1. It keeps track of types that has been defined;
2. It instantiates (and owns) type descriptors (Type objects);
NOTE: there at distinct concepts of type that should not be mixed
together: Here we talk about the type of an expression from a
static analysis PoV. An expression can be boolean, integer, a
particular enum (TODO: prohibit intersection) or an instance of a
certain module. And that's final.
When it comes to encoding though, a variable can be either signed
or unsigned, with a given number of bits. But this, *by design* is
completely ignored by the type inferrer.
Moreover, a wff temporal formula is considered boolean w.r.t. type
inference, it will be responsibility of the formula-analyzer to
determine whether its a CTL/LTL/INVAR, and in different section of
the system different actions can be taken according to this.
typedef class TypeMgr* TypeMgr_ptr;
class TypeMgr {
/* -- inference --------------------------------------------------------- */
inline const Type_ptr find_boolean()
{ return f_register[ f_em.make_boolean_type() ]; }
inline const Type_ptr find_integer()
{ return f_register[ f_em.make_integer_type() ]; }
/* -- decls ------------------------------------------------------------- */
const Type_ptr find_unsigned(unsigned digits);
const Type_ptr find_unsigned_array(unsigned digits, unsigned size);
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);
// -- is_xxx predicates ----------------------------------------------------
/* int_enum is an important subcase of enumeratives. An
all-integer valued enumerative can safely be treated as an
integer w.r.t. type inferring. */
bool is_boolean(const Type_ptr tp) const;
// 42 is an integer constant
bool is_integer(const Type_ptr tp) const;
// 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;
bool is_instance(const Type_ptr tp) const;
// an ARRAY
bool is_array(const Type_ptr tp) const;
// -- as_xxx accessors ------------------------------------------------------
typedef class BooleanType* BooleanType_ptr;
BooleanType_ptr as_boolean(const Type_ptr tp) const;
typedef class IntegerType* IntegerType_ptr;
IntegerType_ptr as_integer(const Type_ptr tp) const;
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;
typedef class Instance* Instance_ptr;
Instance_ptr as_instance(const Type_ptr tp) const;
typedef class ArrayType* ArrayType_ptr;
ArrayType_ptr as_array(const Type_ptr tp) const;
// singleton instance accessor
static inline TypeMgr& INSTANCE() {
if (! f_instance) {
f_instance = new TypeMgr();
return (*f_instance);
inline ExprMgr& em() const
{ return f_em; }
static TypeMgr_ptr f_instance;
/* --- low-level services ----------------------------------------------- */
// register a type
void register_type(const Expr_ptr expr, Type_ptr vtype);
// lookup up a type, returns NULL if not found
inline Type_ptr lookup_type(const Expr_ptr expr)
{ return f_register [ expr ]; }
/* local data */
TypeMap f_register;
// ref to expr manager
ExprMgr& f_em;
Jump to Line
Something went wrong with that request. Please try again.