Transition.h

Go to the documentation of this file.

/*
 * Copyright (c) 2013 Jonathan Anderson
 * All rights reserved.
 *
 * This software was developed by SRI International and the University of
 * Cambridge Computer Laboratory under DARPA/AFRL contract (FA8750-10-C-0237)
 * ("CTSRD"), as part of the DARPA CRASH research programme.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions
 * are met:
 * 1. Redistributions of source code must retain the above copyright
 *    notice, this list of conditions and the following disclaimer.
 * 2. Redistributions in binary form must reproduce the above copyright
 *    notice, this list of conditions and the following disclaimer in the
 *    documentation and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
 * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
 * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
 * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
 * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
 * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
 * SUCH DAMAGE.
 */

#ifndef TRANSITION_H
#define TRANSITION_H

#include "Names.h"
#include "Protocol.h"
#include "Types.h"

#include <llvm/ADT/ArrayRef.h>
#include <llvm/ADT/OwningPtr.h>
#include <llvm/ADT/SmallPtrSet.h>
#include <llvm/Support/Casting.h>

#include <string>

namespace tesla {

// TESLA IR classes
class FieldAssignment;
class FunctionEvent;
class Identifier;
class Location;
class NowEvent;

typedef llvm::MutableArrayRef<const Argument*> MutableReferenceVector;

typedef llvm::SmallVector<Transition*,10> TransitionVector;

typedef llvm::SmallPtrSet<const Transition*,4> TEquivalenceClass;

typedef std::vector<TEquivalenceClass> TransitionSets;

typedef llvm::SmallVector<llvm::SmallVector<Transition*, 16>, 4> TransitionVectors;

class Transition {
public:
  static void Create(State& From, State& To, TransitionVector& Transitions,
                     bool Init = false, bool Cleanup = false);

  static void Create(State& From, State& To, const FunctionEvent& Ev,
                     TransitionVector&, bool Init, bool Cleanup,
                     bool OutOfScope = false);

  static void Create(State& From, State& To, const FieldAssignment& A,
                     TransitionVector&, bool Init, bool Cleanup,
                     bool OutOfScope = false);

  static void Create(State& From, State& To, const NowEvent&,
                     const AutomatonDescription&, TransitionVector&,
                     bool Init, bool Cleanup);

  static void CreateSubAutomaton(State& From, State& To,
                                 const Identifier&, TransitionVector&);

  static void Copy(State &From, State& To, const Transition* Other,
                   TransitionVector &, bool OutOfScope = false);

  static void GroupClasses(const TransitionVector&, TransitionSets&);

  virtual ~Transition() {}

  const State& Source() const { return From; }
  const State& Destination() const { return To; }

  virtual bool EquivalentTo(const Transition &T) const = 0;

  bool RequiresInit() const { return Init; }

  bool RequiresCleanup() const { return Cleanup; }

  virtual bool IsStrict() const { return false; }

  virtual const ReferenceVector Arguments() const = 0;

  llvm::SmallVector<const Argument*,4> NewArguments() const;

  int NewArgMask() const;

  void ReferencesThusFar(llvm::OwningArrayPtr<const Argument*>& Args,
                         ReferenceVector& Ref) const;

  virtual bool IsRealisable() const = 0;

  virtual std::string ShortLabel() const = 0;

  virtual std::string DotLabel() const = 0;

  virtual std::string String() const;

  bool InScope() const { return !OutOfScope; }

  enum TransitionKind { Null, Now, Fn, FieldAssign, SubAutomaton };
  virtual TransitionKind getKind() const = 0;

protected:
  static void Register(llvm::OwningPtr<Transition>&, State& From, State& To,
                       TransitionVector&);

  static void Append(const llvm::OwningPtr<Transition>&, TransitionSets&);

  Transition(const State& From, const State& To, bool Init, bool Cleanup,
             bool OutOfScope)
    : From(From), To(To), Init(Init), Cleanup(Cleanup),
      OutOfScope(OutOfScope)
  {
    // An out-of-scope event cannot cause initialisation.
    assert(!Init || !OutOfScope);
  }

  const State& From;
  const State& To;

  bool Init;            
  bool Cleanup;         

  const bool OutOfScope;
};


class NullTransition : public Transition {
public:
  bool IsRealisable() const { return false; }
  std::string ShortLabel() const { return "ε"; }
  std::string DotLabel() const { return "&#949;"; }    // epsilon

  const ReferenceVector Arguments() const {
    return ReferenceVector();
  }

  bool EquivalentExpression(const Transition* Other) const {
    return llvm::isa<NullTransition>(Other);
  }

  static bool classof(const Transition *T) {
    return T->getKind() == Null;
  }
  virtual TransitionKind getKind() const { return Null; };

protected:
  virtual bool EquivalentTo(const Transition &T) const {
    return T.getKind() == Null;
  }

private:
  NullTransition(const State& From, const State& To, bool Init, bool Cleanup)
    : Transition(From, To, Init, Cleanup, false) {}

  friend class Transition;
};


class NowTransition : public Transition {
public:
  bool IsRealisable() const { return true; }
  std::string ShortLabel() const { return "NOW"; }
  std::string DotLabel() const { return "NOW"; }

  const ReferenceVector Arguments() const { return Refs; }
  const Location& Location() const { return Ev.location(); }

  bool EquivalentExpression(const Transition* Other) const {
    auto *T = llvm::dyn_cast<NowTransition>(Other);
    if (!T) return false;

    return T->Ev == Ev;
  }

  static bool classof(const Transition *T) {
    return T->getKind() == Now;
  }
  virtual TransitionKind getKind() const { return Now; };

protected:
  virtual bool EquivalentTo(const Transition &T) const {
    return T.getKind() == Now;
  }

private:
  NowTransition(const State& From, const State& To, const NowEvent& Ev,
                const ReferenceVector& Refs, bool Init, bool Cleanup)
    : Transition(From, To, Init, Cleanup, false), Ev(Ev), Refs(Refs)
  {
  }

  const NowEvent& Ev;
  const ReferenceVector Refs;

  friend class Transition;
};


class FnTransition : public Transition {
public:
  bool IsRealisable() const { return true; }
  std::string ShortLabel() const;
  std::string DotLabel() const;

  const FunctionEvent& FnEvent() const { return Ev; }
  const ReferenceVector Arguments() const;
  bool IsStrict() const { return Ev.strict(); }

  bool EquivalentExpression(const Transition* Other) const {
    auto *T = llvm::dyn_cast<FnTransition>(Other);
    if (!T) return false;

    return T->Ev == Ev;
  }

  static bool classof(const Transition *T) {
    return T->getKind() == Fn;
  }

  virtual TransitionKind getKind() const { return Fn; };

protected:
  virtual bool EquivalentTo(const Transition &T) const {
    return (T.getKind() == Fn) &&
        (Ev == llvm::cast<FnTransition>(&T)->FnEvent());
  }

private:
  FnTransition(const State& From, const State& To, const FunctionEvent& Ev,
               bool Init, bool Cleanup, bool OutOfScope)
    : Transition(From, To, Init, Cleanup, OutOfScope), Ev(Ev) {}

  const FunctionEvent& Ev;

  friend class Transition;
};


class FieldAssignTransition : public Transition {
public:
  bool IsRealisable() const { return true; }
  std::string ShortLabel() const;
  std::string DotLabel() const;

  const ReferenceVector Arguments() const { return Refs; }
  const FieldAssignment& Assignment() const { return Assign; }
  bool IsStrict() const { return Assign.strict(); }

  bool EquivalentExpression(const Transition* Other) const {
    auto *T = llvm::dyn_cast<FieldAssignTransition>(Other);
    if (!T) return false;

    return T->Assign == Assign;
  }

  static bool classof(const Transition *T) {
    return T->getKind() == FieldAssign;
  }

  virtual TransitionKind getKind() const { return FieldAssign; };

protected:
  virtual bool EquivalentTo(const Transition &T) const {
    return (T.getKind() == FieldAssign) &&
        (Assign == llvm::cast<FieldAssignTransition>(&T)->Assignment());
  }

private:
  FieldAssignTransition(const State& From, const State& To,
                        const FieldAssignment& A, bool Init, bool Cleanup,
                        bool OutOfScope);

  static const char *OpString(FieldAssignment::AssignType);

  const FieldAssignment& Assign;

  llvm::OwningArrayPtr<const Argument*> ReferencedVariables;
  ReferenceVector Refs;

  friend class Transition;
};


class SubAutomatonTransition : public Transition {
public:
  bool IsRealisable() const { return false; }
  std::string ShortLabel() const { return ShortName(ID); }
  std::string DotLabel() const { return ShortName(ID); }

  const ReferenceVector Arguments() const;
  const Identifier& GetID() const { return ID; }

  bool EquivalentExpression(const Transition* Other) const {
    auto *T = llvm::dyn_cast<SubAutomatonTransition>(Other);
    if (!T) return false;

    return T->ID == ID;
  }

  static bool classof(const Transition *T) {
    return T->getKind() == SubAutomaton;
  }

  virtual TransitionKind getKind() const { return SubAutomaton; };

protected:
  virtual bool EquivalentTo(const Transition &T) const {
    return (T.getKind() == SubAutomaton) &&
        (ID == llvm::cast<SubAutomatonTransition>(&T)->ID);
  }

private:
  SubAutomatonTransition(const State& From, const State& To,
                         const Identifier& ID)
    : Transition(From, To, false, false, false), ID(ID) {}

  const Identifier& ID;

  friend class Transition;
};


} // namespace tesla

#endif  // TRANSITION_H