/* st-single.cc: check use of single and global synchronization
 */

#include "AST.h"
#include "decls.h"
#include "errors.h"

// Abrupt termination reasons
class Termination
{
public:
  enum Kind { Break=0, Continue, Return, Exception } kind;
  const char *kindStr() { 
    static const char *kindNames[] = 
      { "break", "continue", "return", "exception" };
    return kindNames[kind];
  }

  // Label or omitted for Break/Continue, exception type for Exception
    TreeNode *argument;

    SourcePosn position; 

  Termination(Kind k, TreeNode *a, SourcePosn const p) : 
     kind(k), argument(a), position(p) { }
};

// Synchronization sequences - temporarily an enum for simplicity

enum Sync { Epsilon, Fixed };

// Lists of terminations are never shared (so use destructive operations)
typedef llist<Termination> *Terminations;

// The information inferred by single analysis
// In a judgement |- node : a, s, g, T+, T-, n
//   a is { +, - } to indicate if the expression is single-valued
//   s is the synchronization sequence of node
//   g is a boolean that is true if the node must be executed by
//     all processes, i.e. the node has single side effects
//     This does not include synchronization effects, they are handled
//     separately to allow for if-multi (and switch-multi)
//   l is a boolean that is true if the node has single side effects
//     that only affect local variables (so cannot be done in an
//     if-multi, but doesn't force the function to be declared
//     single)
//   T+ is the set of abrupt terminations taken deterministically by
//     all processes that start node
//   T- is the set of abrupt terminations taken in a random fashion 
//   n is a boolean that is true if the node may terminate normally
//     (so false implies that it must terminate abruptly)
  
class TreeNode::SingleState
{
public:
  bool singleValued;		// a (+=true, -=false)
  Sync syncSeq;		// s
  bool globalEffects;		// g
  bool localEffects;		// l
  Terminations globalTerminations; // T+
  Terminations randomTerminations; // T-
  bool normalTermination;	// n

  SingleState(bool a, Sync s, bool g, bool l, Terminations T1, Terminations T2,
	      bool n) : singleValued(a), syncSeq(s), globalEffects(g),
    localEffects(l), globalTerminations(T1), randomTerminations(T2),
    normalTermination(n)
  { }
  SingleState() : singleValued(false), syncSeq(Epsilon), globalEffects(false),
    localEffects(false), globalTerminations(NULL), randomTerminations(NULL),
    normalTermination(false)
  { }
};

// Single inference context
class TreeNode::SingleContext
{
public:
  bool inConstructor;
  bool singleReturn;		// result of function is single

  SingleContext() : inConstructor(false), singleReturn(false) { }
  SingleContext(SingleContext *old) { *this = *old; }
};

// Operations on lists of terminations
// Lists of terminations are never shared to simplify memory management,
// so all operations are destructive

bool contains(Termination::Kind k, Terminations l)
{
  foreach (termination, llist<Termination>, *l)
    if ((*termination).kind == k) return true;

  return false;
}

#define union extend

Terminations filterUnlabeled(Termination::Kind k, Terminations l)
{
  Terminations *scan = &l;

  while (*scan)
    {
      if ((*scan)->front().kind == k && (*scan)->front().argument->absent())
	*scan = (*scan)->tail(); // delete
      else
	scan = &(*scan)->tail();
    }
  return l;
}

Terminations filterLabel(Termination::Kind k, TreeNode *label, Terminations l)
{
  Decl *ldecl = label->decl();
  Terminations *scan = &l;

  while (*scan)
    {
      if ((*scan)->front().kind == k &&
	  (*scan)->front().argument->decl() == ldecl)
	*scan = (*scan)->tail(); // delete
      else
	scan = &(*scan)->tail();
    }
  return l;
}

Terminations filterException(TypeNode *exception, Terminations l)
{
  Terminations *scan = &l;

  while (*scan)
    {
      if ((*scan)->front().kind == Termination::Exception &&
	  isSubClass((*scan)->front().argument->decl(), exception->decl()))
	*scan = (*scan)->tail(); // delete
      else
	scan = &(*scan)->tail();
    }
  return l;
}

Terminations duplicateTerminations(Terminations l)
{
  Terminations newl = NULL;
  Terminations *lastl = &newl;
  
  while (l)
    {
      *lastl = cons(l->front());
      lastl = &(*lastl)->tail();
      l = l->tail();
    }

  return newl;
}

// Operations on synchronization sequences

// the synchronization representing s1 followed by s2
Sync syncSequence(Sync s1, Sync s2)
{
  if (s1 == Epsilon && s2 == Epsilon) return Epsilon;
  else return Fixed;
}

// the least upper bound of s1 and s2
Sync syncMerge(Sync s1, Sync s2)
{
  if (s1 == Epsilon && s2 == Epsilon) return Epsilon;
  else return Fixed;
}

// Operations on SingleStates

bool TreeNode::hasGlobalEffects(SingleState s)
{
  return s.globalEffects || s.syncSeq != Epsilon;
}

bool TreeNode::hasSingleEffects(SingleState s)
{
  return s.localEffects || s.globalEffects || s.syncSeq != Epsilon;
}

TreeNode::SingleState TreeNode::duplicateState(SingleState s)
{
  s.randomTerminations = duplicateTerminations(s.randomTerminations);
  s.globalTerminations = duplicateTerminations(s.globalTerminations);

  return s;
}

void TreeNode::discardState(SingleState s)
{
  free_all(s.randomTerminations);
  free_all(s.globalTerminations);
}

TreeNode::SingleState TreeNode::removeLabel(SingleState s, TreeNode *label)
{
  if (label->absent())
    {
      s.randomTerminations = filterUnlabeled(Termination::Break,
			     filterUnlabeled(Termination::Continue, s.randomTerminations));
      s.globalTerminations = filterUnlabeled(Termination::Break, 
			     filterUnlabeled(Termination::Continue, s.globalTerminations));
    }
  else
    {
      s.randomTerminations = filterLabel(Termination::Break, label,
			     filterLabel(Termination::Continue, label, s.randomTerminations));
      s.globalTerminations = filterLabel(Termination::Break, label,
			     filterLabel(Termination::Continue, label, s.globalTerminations));
    }
  return s;
}

TreeNode::SingleState TreeNode::removeUnlabeledBreak(SingleState s)
{
  s.randomTerminations = filterUnlabeled(Termination::Break, s.randomTerminations);
  s.globalTerminations = filterUnlabeled(Termination::Break, s.globalTerminations);
  return s;
}

TreeNode::SingleState TreeNode::removeException(SingleState s, TypeNode *exception)
{
  s.randomTerminations = filterException(exception, s.randomTerminations);
  s.globalTerminations = filterException(exception, s.globalTerminations);
  return s;
}

TreeNode::SingleState TreeNode::mergeTerminations(SingleState s, TypeNode *methodType)
{
  foriter (thrown, methodType->throws()->allTypes(), TypeIter)
    {
      if ((*thrown)->isSingle())
	s.globalTerminations = cons(Termination(Termination::Exception, (*thrown), position()),
				    s.globalTerminations);
      else
	s.randomTerminations = cons(Termination(Termination::Exception, (*thrown), position()),
				    s.randomTerminations);
    }
  return s;
}

void TreeNode::validateTerminations(SingleState s)
{
  // no need to check global terminations, as type checking guarantees
  // that only valid exceptions can be thrown

  foreach (termination, llist<Termination>, *s.randomTerminations)
    if ((*termination).kind == Termination::Exception)
      {
	TypeNode *exception = (TypeNode *)(*termination).argument;

	// This exception must be listed as a non-single exception
	foriter (thrown, throws()->allTypes(), TypeIter)
	  {
	    if ((*thrown)->isAssignableFromType(exception) &&
		(*thrown)->isSingle())
	      error() << "non-single exception " << exception->typeName()
		      << " is assignable to declared exception "
		      << (*thrown)->typeName() << endl;
	  }
      }
}

void dumpTerminations(Terminations ts) {
  foreach(t, llist<Termination>, *ts) 
    Error((*t).position) << "non-single termination (" << (*t).kindStr() << ")" << endl;
}

// Call on the node whose effect is s2 to get correct error messages
TreeNode::SingleState TreeNode::sequenceState(SingleState s1, SingleState s2,
					      SingleContext *ctx)
{
  // s1 always terminates abruptly->s2 not executed
  if (!s1.normalTermination) return s1;

  s1.singleValued = s1.singleValued && s2.singleValued;
  s1.syncSeq = syncSequence(s1.syncSeq, s2.syncSeq);
  s1.globalEffects = s1.globalEffects || s2.globalEffects;
  s1.localEffects = s1.localEffects || s2.localEffects;
  if (hasSingleEffects(s2))
    {
      // require single termination in s1
      if (s1.randomTerminations) {
	error() << "statement with single effects is preceded by statements with non-single terminations" << endl
                << "    preceding non-single terminations follow:" << endl;
        dumpTerminations(s1.randomTerminations);
      }
    }

  if (s1.randomTerminations)
    {
      if (ctx->singleReturn && contains(Termination::Return, s2.globalTerminations)) {
	  error() << "single return is preceded by statements with non-single terminations" << endl
                  << "    preceding non-single terminations follow:" << endl;
          dumpTerminations(s1.randomTerminations);
      }
      s1.randomTerminations = union(s1.randomTerminations, s2.globalTerminations);
    }
  else
    s1.globalTerminations = union(s1.globalTerminations, s2.globalTerminations);
  s1.randomTerminations = union(s1.randomTerminations, s2.randomTerminations);

  s1.normalTermination = s2.normalTermination;

  return s1;
}

TreeNode::SingleState TreeNode::merge(SingleState s1,
				      SingleState s2,
				      bool singleSplit,
				      SingleContext *ctx)
{
  s1.singleValued = s1.singleValued && s2.singleValued && singleSplit;
  s1.syncSeq = syncMerge(s1.syncSeq, s2.syncSeq);
  s1.globalEffects = s1.globalEffects || s2.globalEffects;
  s1.localEffects = s1.localEffects || s2.localEffects;
  s1.globalTerminations = union(s1.globalTerminations, s2.globalTerminations);
  s1.randomTerminations = union(s1.randomTerminations, s2.randomTerminations);
  if (!singleSplit)
    {
      if (s1.globalEffects || s1.localEffects || s1.syncSeq == Fixed)
	error() << "non-single " << operatorName() << " has single effects" << endl;

      if (ctx->singleReturn && contains(Termination::Return, s1.globalTerminations)) {
	error() << "non-single " << operatorName() << " causes non-single return" << endl
                << "    non-single returns follow:" << endl;
        Terminations ttemp = NULL;
        foreach (t, llist<Termination>, *s1.globalTerminations)
          if ((*t).kind == Termination::Return) ttemp = cons(*t, ttemp);
        dumpTerminations(ttemp);
        free_all(ttemp);
      }
      s1.randomTerminations = union(s1.randomTerminations, s1.globalTerminations);
      s1.globalTerminations = NULL;
    }
  s1.normalTermination = s1.normalTermination || s2.normalTermination;

  return s1;
}

TreeNode::SingleState TreeNode::loopMerge(SingleState condition,
					  SingleState body,
					  SingleContext *ctx)
{
  // compute Fixed-point directly
  SingleState aLoop;

  aLoop.singleValued = false; // meaningless
  if (condition.syncSeq == Epsilon && body.syncSeq == Epsilon)
    aLoop.syncSeq = Epsilon;
  else
    aLoop.syncSeq = Fixed;
  aLoop.globalEffects = condition.globalEffects || body.globalEffects;
  aLoop.localEffects = condition.localEffects || body.localEffects;
  aLoop.randomTerminations = union(condition.randomTerminations,
				  body.randomTerminations);
  aLoop.globalTerminations = union(condition.globalTerminations,
				  body.globalTerminations);
  if (!condition.singleValued || aLoop.randomTerminations)
    {
      if (ctx->singleReturn && contains(Termination::Return, aLoop.globalTerminations)) {
	error() << "non-single loop causes non-single return" << endl
                << "    non-single returns follow:" << endl;
        dumpTerminations(aLoop.globalTerminations);
      }
      aLoop.randomTerminations =
	union(aLoop.randomTerminations, aLoop.globalTerminations);
      aLoop.globalTerminations = NULL;
    }
  aLoop.normalTermination = true; // leave it to caller

  if (hasSingleEffects(aLoop))
    {
      if (!condition.singleValued)
	error() << "loop with single effects has non-single condition" << endl;
      if (aLoop.randomTerminations) {
	error() << "loop with single effects has non-single terminations" << endl
                << "    non-single terminations follow:" << endl;
        dumpTerminations(aLoop.randomTerminations);
      }

    }

  return removeLabel(aLoop, omitted);
}

// Basic single-inference patterns

// A simple single-valued expression with no global effects, etc
TreeNode::SingleState TreeNode::iAmSingle =
  TreeNode::SingleState(true, Epsilon, false, false, NULL, NULL, true);

// Single inference on each element of a list independently
// (used at class top-level)
TreeNode::SingleState TreeNode::singleList(SingleContext *ctx)
{
  foriter (p, allChildren(), ChildIter)
    discardState((*p)->single(ctx));
  
  return SingleState();
}

// An expression (or statement) representing a sequential evaluation
// of the children, followed by a deterministic operator on their
// results
TreeNode::SingleState TreeNode::singleSequence(SingleContext *ctx)
{
  return singleSequence(ctx, iAmSingle);
}
    
// An expression (or statement) representing a sequential evaluation
// of the children, followed by a deterministic operator on their
// results
TreeNode::SingleState TreeNode::singleSequence(SingleContext *ctx, SingleState st)
{
  foriter (p, allChildren(), ChildIter)
    st = (*p)->sequenceState(st, (*p)->single(ctx), ctx);

  return st;
}

// An expression (or statement) representing a sequential evaluation
// of all children, followed by a deterministic operator on their
// results, followed by an assignment to the first child
TreeNode::SingleState TreeNode::singleAssignment(SingleContext *ctx)
{
  return child(0)->singleAssign(singleSequence(ctx), ctx);
}

TreeNode::SingleState TreeNode::singleIf(TreeNode *condition,
					 TreeNode *thenNode, TreeNode *elseNode,
					 SingleContext *ctx)
{
  SingleState sc = condition->single(ctx);
  SingleState st = thenNode->single(ctx);
  SingleState se = elseNode->single(ctx);

  return sequenceState(sc, merge(st, se, sc.singleValued, ctx), ctx);
}

Decl *isGlobalCall(Decl *method)
{
  if (method->modifiers() & Common::Sglobal) return method;
#ifdef SGLOBAL_INFERENCE
  MethodSet *overriders = method->overriders();
  iterator s = overriders->begin(), end = overriders->end();

  while (s != end)
    {
      if ((*s)->modifiers() & Common::Sglobal) return *s;
      s++;
    }
#endif
  return NULL;
}

TreeNode::SingleState TreeNode::singleCall(SingleState st,
					   bool explicitConstructorCall,
					   SingleContext *ctx)
{
  // The single-valued field of st will be true if the call matches
  // the single signature (any extra requirements are already ensured
  // in 'st' by the caller)
  Decl *cdecl = decl();
  TypeNode *ctype = cdecl->type();

  foriter2 (arg, args()->allChildren(),
	    type, ctype->paramTypes()->allChildren(),
	    ChildIter)
    {
      TypeNode *ptype = (TypeNode *)(*type);
      SingleState sa = (*arg)->single(ctx);
      bool singleOk = st.singleValued && ptype->isSingle() <= sa.singleValued;

      st = (*arg)->sequenceState(st, sa, ctx);
      st.singleValued = singleOk;
    }

  if (explicitConstructorCall) // calls to other constructor must respect signature
    if (!st.singleValued)
      error() << "call to " << cdecl->errorName()
	      << " must respect single signature" << endl;

  Decl *gmethod = isGlobalCall(cdecl);
  if (gmethod)
    {
      // A call with global effects
      if (!explicitConstructorCall && !st.singleValued)
	error() << "Call may invoke " << gmethod->errorName()
		<< " which has global effects - must respect single signature" << endl;
      st.syncSeq = Fixed;
      st.globalEffects = true;
    }

  st.singleValued = st.singleValued && ctype->declaredReturnType()->isSingle();

  return mergeTerminations(st, ctype);
}

TreeNode::SingleState TreeNode::singleAllocateArray(SingleState st,
						    SingleContext */*ctx*/)
{
#if 0
  Oops. This should only be for (the future) immutable classes
  if (decl()->modifiers() & Single)
    {
      // default constructor has global effects, dimensions must be
      // single-valued
      if (!st.singleValued)
	error() << "default constructor for " << decl()->container()->errorName()
		<< " has global effects - use single-valued dimensions" << endl;
      st.syncSeq = Fixed;
      st.globalEffects = true;
    }
  return mergeTerminations(st, decl()->type());
#else
  return st;
#endif
}

static TreeNode::SingleState singleTerminate(Termination t)
{
  return TreeNode::SingleState(true, Epsilon, false, false, cons(t), NULL, false);
}



TreeNode::SingleState TreeNode::single(SingleContext *)
{
  undefined("single");
  return SingleState();
}

TreeNode::SingleState TreeNode::singleAssign(const SingleState &, SingleContext *)
{
  undefined("singleAssign");
  return SingleState();
}

TreeNode::SingleState OmittedNode::single(SingleContext *)
{
  return iAmSingle;
}

TreeNode::SingleState CompileUnitNode::single(SingleContext *)
{
  SingleContext c;

  types()->singleList(&c);
  return SingleState();
}

TreeNode::SingleState TemplateDeclNode::single( SingleContext *context )
{
  return SingleState();
}

TreeNode::SingleState TypeDeclNode::single(SingleContext *ctx)
{
  members()->singleList(ctx);
  return SingleState();
}

// Class members

TreeNode::SingleState MethodSignatureNode::single(SingleContext *)
{
  // nothing to do
  return SingleState();
}

TreeNode::SingleState FieldDeclNode::single(SingleContext *ctx)
{
  SingleState si = initExpr()->single(ctx);

  if (dtype()->isSingle())
    {
      if (!si.singleValued)
	error() << decl()->errorName() << " is assigned a non-single value" << endl;

      // Change: static single initialisers can have initialisers because
      // we have decreed an arbitrary, but Fixed, class load order
    }

  if (hasGlobalEffects(si)) { // see PR515
    if (flags() & Static)
      warning("sglobal-static-init") << "global effects in static field initializers may not be supported in future versions" << endl;
    else 
      // we cannot allow global effects unless we propagate that to the enclosing constructors
      error() << "global effects are currently prohibited in instance field initializers" << endl;
  }

  discardState(si);

  return SingleState();
}

TreeNode::SingleState StaticInitNode::single(SingleContext *ctx)
{
  SingleState sb = block()->single(ctx);
  // Change: static single initialisers can have initialisers because
  // we have decreed an arbitrary, but fixed, class load order
  if (hasGlobalEffects(sb) && 
      strcmp(this->parent()->parent()->simpName()->ident()->c_str(),"UNIXProcess")) // temporarily disable warning for one stdlib violation
    warning("sglobal-static-init") << "global effects in static initializers may not be supported in future versions" << endl;
  discardState(sb);
  return SingleState();
}

TreeNode::SingleState InstanceInitNode::single(SingleContext *ctx)
{
  SingleState sb = block()->single(ctx);
  // we cannot allow global effects unless we propagate that to the enclosing constructors
  if (hasGlobalEffects(sb))
    error() << "global effects are currently prohibited in instance initializers" << endl;
  discardState(sb);
  return SingleState();
}

TreeNode::SingleState MethodDeclNode::single(SingleContext *ctx)
{
  bool declaredSingle = (decl()->modifiers() & Sglobal) != 0;
  SingleContext subCtx(ctx);

  // The 'void' type is single for various reasons, but that isn't so good here...
  subCtx.singleReturn = returnType()->isSingle() && returnType()->kind() != VoidKind;
  SingleState sb = body()->single(&subCtx);

  if (hasGlobalEffects(sb) && !declaredSingle)
    error() << decl()->errorName() << " has global effects - must be declared single" << endl;

  validateTerminations(sb);
  discardState(sb);

  return SingleState();
}

TreeNode::SingleState ConstructorDeclNode::single(SingleContext *ctx)
{
  bool declaredSingle = (decl()->modifiers() & Sglobal) != 0;

  SingleContext subCtx(ctx);

  subCtx.inConstructor = true;
  SingleState st = body()->sequenceState(constructorCall()->single(&subCtx),
					 body()->single(&subCtx), &subCtx);

  if (hasGlobalEffects(st) && !declaredSingle)
    error() << decl()->errorName() << " has global effects - must be declared single" << endl;

  validateTerminations(st);
  discardState(st);

  return SingleState();
}

// Statements

TreeNode::SingleState EmptyStmtNode::single(SingleContext *)
{
  return iAmSingle;
}

TreeNode::SingleState BlockNode::single(SingleContext *ctx)
{
  return stmts()->singleSequence(ctx);
}

TreeNode::SingleState ExpressionStmtNode::single(SingleContext *ctx)
{
    return expr()->single(ctx);
}

TreeNode::SingleState SynchronizedNode::single(SingleContext *ctx)
{
  return singleSequence(ctx);
}

TreeNode::SingleState LabeledStmtNode::single(SingleContext *ctx)
{
  return removeLabel(stmt()->single(ctx), label());
}

TreeNode::SingleState VarDeclNode::single(SingleContext *ctx)
{
  SingleState si = initExpr()->single(ctx);

  if (dtype()->isSingle())
    {
      if (!si.singleValued)
	error() << decl()->errorName() << " is assigned a non-single value" << endl;
    }

  return si;
}

TreeNode::SingleState IfStmtNode::single(SingleContext *ctx)
{
  return singleIf(condition(), thenPart(), elsePart(), ctx);
} 

TreeNode::SingleState AssertNode::single(SingleContext *ctx)
{
  return singleIf(condition(), value(), TreeNode::omitted, ctx);
}

TreeNode::SingleState SwitchNode::single(SingleContext *ctx)
{
  SingleState se = expr()->single(ctx);
  llist<SingleState> *branchStates = NULL;
  bool defaultPresent = false;

  // conceptually, each branch falls through to the next one
  foriter (branch, switchBlocks()->allChildren(), ChildIter)
    {
      SingleState branchEffects = (*branch)->stmts()->singleSequence(ctx);

      // add the effect to all previous branches, then add to start
      foreach (b, llist<SingleState>, *branchStates)
	if ((*b).normalTermination) // avoid excessive duplication
	  *b = (*branch)->sequenceState(*b, duplicateState(branchEffects), ctx);
      branchStates = cons(branchEffects, branchStates);

      // see if 'default' label present
      if (!defaultPresent)
	foriter (acase, (*branch)->cases()->allChildren(), ChildIter)
	  if ((*acase)->expr()->absent())
	    {
	      defaultPresent = true;
	      break;
	    }
    }

  // Special-case for useless switch
  if (!branchStates) return se;

  // merge all branches
  SingleState switchEffect = branchStates->front();
  bool lastTerminatedNormally = switchEffect.normalTermination;

  TreeNode *sblocks = switchBlocks();
  int i = sblocks->arity(); // to get better error message line numbers
  foreach (b, llist<SingleState>, *branchStates->tail())
    switchEffect = sblocks->child(--i)->merge(switchEffect, *b, se.singleValued, ctx);

  // a switch can terminate normally if there is no 'default' label or if
  // the last case can terminate normally (this ignores exhaustive switches)
  switchEffect.normalTermination =
    !defaultPresent || lastTerminatedNormally;

  free_all(branchStates);

  return sequenceState(se, removeUnlabeledBreak(switchEffect), ctx);
}

TreeNode::SingleState LoopNode::single(SingleContext *ctx)
{
  // Doesn't detect infinite loops (for setting normalTermination)
  SingleState condState = test()->single(ctx);
  SingleState bodyState = stmt()->single(ctx);

  return loopMerge(condState, bodyState, ctx);
}

TreeNode::SingleState ForNode::single(SingleContext *ctx)
{
  // Doesn't detect infinite loops (for setting normalTermination)
  SingleState condState = test()->single(ctx);
  SingleState bodyState =
    update()->sequenceState(stmt()->single(ctx),
			    update()->singleSequence(ctx), ctx);

  return stmt()->sequenceState(init()->singleSequence(ctx),
			       loopMerge(condState, bodyState, ctx), ctx);
}

TreeNode::SingleState BreakNode::single(SingleContext *)
{
  return singleTerminate(Termination(Termination::Break, label(), position()));
}

TreeNode::SingleState ContinueNode::single(SingleContext *)
{
  return singleTerminate(Termination(Termination::Continue, label(), position()));
}

TreeNode::SingleState ReturnNode::single(SingleContext *ctx)
{
  SingleState returnState = expr()->single(ctx);

  if (ctx->singleReturn && !returnState.singleValued)
    error() << "non-single-valued return" << endl;

  return sequenceState(returnState, singleTerminate(Termination(Termination::Return, omitted, position())), ctx);
}

TreeNode::SingleState ThrowNode::single(SingleContext *ctx)
{
  SingleState st = expr()->single(ctx);
  Termination t = Termination(Termination::Exception, expr()->type(), position());

  if (st.singleValued)
    return singleTerminate(t);
  else
    return SingleState(true, Epsilon, false, false, NULL, cons(t), false);
}

TreeNode::SingleState TryStmtNode::single(SingleContext *ctx)
{
  SingleState sb = block()->single(ctx);

  // catch
  if (catches()->arity() > 0)
    {
      bool singleEffectsAllowed = sb.randomTerminations == NULL;
      SingleState catchEffects = iAmSingle;

      foriter (aCatch, catches()->allChildren(), ChildIter)
	{
	  SingleState sc = (*aCatch)->block()->single(ctx);
	  TypeNode *ctype = (*aCatch)->param()->dtype();

          if (!singleEffectsAllowed && ctype->isSingle()) {
	    (*aCatch)->error() << "cannot 'single catch' a try with non-single terminations" << endl
                << "    non-single terminations follow:" << endl;
            dumpTerminations(sb.randomTerminations);
          }
	  catchEffects = (*aCatch)->merge(catchEffects, sc, singleEffectsAllowed, ctx);
	  sb = removeException(sb, ctype);
	}

      bool blockTerminates = sb.normalTermination;
      sb.normalTermination = true; // the catch clauses may execute
      sb = catches()->child(0)->sequenceState(sb, catchEffects, ctx);
      // if the block terminated normally, catches don't have any effect
      if (blockTerminates)
	sb.normalTermination = true;
    }

  // finally
  SingleState sf = finally()->single(ctx);
  if (!sf.normalTermination)
    {
      // abrupt termination in a finally clause overrides all other
      // abrupt terminations
      free_all(sb.globalTerminations);
      free_all(sb.randomTerminations);
      sb.globalTerminations = sb.randomTerminations = NULL;
      sb.normalTermination = true; // the finally clause always executes
      return finally()->sequenceState(sb, sf, ctx);
    }
  else
    {
      bool normalTermination = sb.normalTermination;
      sb.normalTermination = true; // the finally clause always executes
      sb = finally()->sequenceState(sb, sf, ctx);
      // If the finally clause can terminate normally, then it doesn't
      // effect whether the whole try block can terminate normally
      sb.normalTermination = normalTermination;
      return sb;
    }
}

TreeNode::SingleState TryNode::single(SingleContext *ctx)
{
    return block()->single(ctx);
}

TreeNode::SingleState FinallyNode::single(SingleContext *ctx)
{
    return block()->single(ctx);
}

// Titanium statements

TreeNode::SingleState ForEachStmtNode::single(SingleContext *ctx)
{
  SingleState sf = iAmSingle;
  bool allSingle = true;
  // The type of all the points (it is shared, cf st-field.c)
  TypeNode *ptype = vars()->child(0)->simpName()->decl()->type();

  foriter (var, vars()->allChildren(), ChildIter)
    {
      SingleState sv = (*var)->initExpr()->single(ctx);

      sf = (*var)->sequenceState(sf, sv, ctx);
      if (!sv.singleValued) allSingle = false;
    }

  // A foreach is 'single' if all the domains are
  if (allSingle)
    ptype->modifiers((Modifiers) (ptype->modifiers() | Single));

  return sequenceState(sf, loopMerge(SingleState(allSingle, Epsilon,
						 false, false, NULL, NULL,
						 true),
				     stmt()->single(ctx), ctx), ctx);
}

TreeNode::SingleState PartitionStmtNode::single(SingleContext *ctx)
{
  foriter (clause, cases()->allChildren(), ChildIter)
    {
      SingleState condState = (*clause)->condition()->single(ctx);
      if (hasSingleEffects(condState))
	(*clause)->condition()->error() << "partition conditions cannot have single effects" << endl;
      discardState(condState);

      SingleState clauseState = (*clause)->stmt()->single(ctx);
      if (clauseState.globalEffects || clauseState.localEffects)
	(*clause)->stmt()->warning("sglobal-partition") << "Single effects are unchecked in partition" << endl;
      discardState(clauseState);
    }

  return SingleState(true, Fixed, true, false, NULL, NULL, true);
}

// Expressions

// Operators

TreeNode::SingleState UnaryArithNode::single(SingleContext *ctx)
{
  return singleSequence(ctx);
}

TreeNode::SingleState BinaryArithNode::single(SingleContext *ctx)
{
  return singleSequence(ctx);
}

TreeNode::SingleState ShiftNode::single(SingleContext *ctx)
{
  return singleSequence(ctx);
}

TreeNode::SingleState RelationNode::single(SingleContext *ctx)
{
  return singleSequence(ctx);
}

TreeNode::SingleState EqualityNode::single(SingleContext *ctx)
{
  return singleSequence(ctx);
}

TreeNode::SingleState BitwiseNode::single(SingleContext *ctx)
{
  return singleSequence(ctx);
}

TreeNode::SingleState ComplementNode::single(SingleContext *ctx)
{
  return singleSequence(ctx);
}

TreeNode::SingleState NotNode::single(SingleContext *ctx)
{
  return singleSequence(ctx);
}

TreeNode::SingleState CastNode::single(SingleContext *ctx)
{
  SingleState st =  opnd0()->single(ctx);

  if (dtype()->isSingle()) // a 'single' cast
    st.singleValued = true;

  return st;
}

TreeNode::SingleState InstanceOfNode::single(SingleContext *ctx)
{
  return opnd0()->single(ctx);
}

TreeNode::SingleState StringConcatNode::single(SingleContext *ctx)
{
  return addends()->singleSequence(ctx);
}

// Assignment operators

TreeNode::SingleState IncrDecrNode::single(SingleContext *ctx)
{
  return singleAssignment(ctx);
}

TreeNode::SingleState BinaryArithAssignNode::single(SingleContext *ctx)
{
  return singleAssignment(ctx);
}

TreeNode::SingleState ShiftAssignNode::single(SingleContext *ctx)
{
  return singleAssignment(ctx);
}

TreeNode::SingleState BitwiseAssignNode::single(SingleContext *ctx)
{
  return singleAssignment(ctx);
}

TreeNode::SingleState AssignNode::single(SingleContext *ctx)
{
  SingleState st0 = opnd0()->single(ctx);
  SingleState st1 = opnd1()->single(ctx);
  bool isSingleValued = st1.singleValued;

  SingleState st = opnd0()->singleAssign(opnd1()->sequenceState(st0, st1, ctx), ctx);
  st.singleValued = isSingleValued; // singleness of destination doesn't affect
				    // singleness of result

  return st;
}

TreeNode::SingleState StringConcatAssignNode::single(SingleContext *ctx)
{
  SingleState left  = opnd0()->single(ctx);
  SingleState right = addends()->singleSequence(ctx, left);
  return opnd0()->singleAssign(right, ctx);
}

// Constants

TreeNode::SingleState LitNode::single(SingleContext *)
{
  return iAmSingle;
}

// Miscellaneous

TreeNode::SingleState ArrayInitNode::single(SingleContext *ctx)
{
  return initializers()->singleSequence(ctx);
}

TreeNode::SingleState ThisNode::single(SingleContext *)
{
  // this is always treated as single-valued (restrictions occur
  // in method calls)
  return iAmSingle;
}

TreeNode::SingleState IfExprNode::single(SingleContext *ctx)
{
  return singleIf(condition(), thenOpnd(), elseOpnd(), ctx);
}

TreeNode::SingleState LogCondNode::single(SingleContext *ctx)
{
  return singleIf(opnd0(), opnd1(), omitted, ctx);
}

// Assignable expressions

static TreeNode::SingleState localEffect = TreeNode::SingleState(true, Epsilon, false, true, NULL, NULL, true);
static TreeNode::SingleState globalEffect = TreeNode::SingleState(true, Epsilon, true, false, NULL, NULL, true);

TreeNode::SingleState ObjectNode::single(SingleContext *)
{
  return SingleState(decl()->type()->isSingle(), Epsilon, false, false,
		     NULL, NULL, true);
}

TreeNode::SingleState ObjectNode::singleAssign(const SingleState &value,
					       SingleContext *ctx)
{
  SingleState result = value;
  
  if (decl()->type()->isSingle())
    {
      if (!value.singleValued)
	error() << decl()->errorName() << " is assigned a non-single value" << endl;
      result = sequenceState(value, localEffect, ctx);
    }
  // Assignments to variables do not count as global effects
  return result;
}

TreeNode::SingleState ArrayAccessNode::single(SingleContext *ctx)
{
  SingleState st = singleSequence(ctx);

  if (!array()->type()->elementType()->isSingle())
    st.singleValued = false;

  return st;
}

TreeNode::SingleState ArrayAccessNode::singleAssign(const SingleState &value,
						    SingleContext *ctx)
{
  if (!array()->type()->elementType()->isSingle()) return value;

  if (!value.singleValued)
    error() << "non-single assignment to array " << array()->type()->typeName() << endl;

  return sequenceState(value, globalEffect, ctx);
}

TreeNode::SingleState FieldAccessNode::single(SingleContext *)
{
  return SingleState(decl()->type()->isSingle(), Epsilon, false, false,
		     NULL, NULL, true);
}

TreeNode::SingleState FieldAccessNode::singleAssign(const SingleState &value,
						    SingleContext *ctx)
{
  if (!decl()->type()->isSingle()) return value;

  if (!value.singleValued)
    error() << decl()->errorName() << " is assigned a non-single value" << endl;

  return sequenceState(value, globalEffect, ctx);
}

TreeNode::SingleState ThisFieldAccessNode::singleAssign(const SingleState &value,
							SingleContext *ctx)
{
  if (!decl()->type()->isSingle()) return value;

  if (!value.singleValued)
    error() << decl()->errorName() << " is assigned a non-single value" << endl;

  // Initialisation of fields in a constructor is a local effect
  // (the object cannot be accessed by a non-single pointer yet)
  if ((decl()->modifiers() & Static) || !ctx->inConstructor)
    return sequenceState(value, globalEffect, ctx);
  else return sequenceState(value, localEffect, ctx);
}

TreeNode::SingleState ObjectFieldAccessNode::single(SingleContext *ctx)
{
  return sequenceState(object()->single(ctx),
		       FieldAccessNode::single(ctx), ctx);
}

// Constructor & method calls

TreeNode::SingleState MethodCallNode::single(SingleContext *ctx)
{
  SingleState st = method()->single(ctx);

  // Calls to static method do not need a single-valued 'this'
  if (decl()->modifiers() & Static)
    st.singleValued = true;
  
  return singleCall(st, false, ctx);
}

TreeNode::SingleState MethodCallAssignNode::single(SingleContext *ctx)
{
  SingleState st = method()->single(ctx);

  // Calls to static method do not need a single-valued 'this'
  if (decl()->modifiers() & Static)
    st.singleValued = true;
  
  return method()->object()->singleAssign(singleCall(st, false, ctx), ctx);
}

TreeNode::SingleState ThisConstructorCallNode::single(SingleContext *ctx)
{
  return singleCall(iAmSingle, true, ctx);
}

TreeNode::SingleState SuperConstructorCallNode::single(SingleContext *ctx)
{
  if (decl())
    return singleCall(iAmSingle, true, ctx);
  else
    return iAmSingle;
}

TreeNode::SingleState AllocateNode::single(SingleContext *ctx)
{
  return singleCall(iAmSingle, false, ctx);
}

TreeNode::SingleState AllocateArrayNode::single(SingleContext *ctx)
{
  SingleState sa = singleAllocateArray(dimExprs()->singleSequence(ctx), ctx);
  SingleState si = initExpr()->single(ctx);
  return sequenceState(sa, si, ctx);
}

TreeNode::SingleState AllocateArrayDimensionNode::single(SingleContext *ctx)
{
  return expr()->single(ctx);
}

// Titanium expressions

TreeNode::SingleState PointNode::single(SingleContext *ctx)
{
  return args()->singleSequence(ctx);
}

TreeNode::SingleState DomainNode::single(SingleContext *ctx)
{
  SingleState st = iAmSingle;

  foriter (range, args()->allChildren(), ChildIter)
    st = (*range)->sequenceState(st, (*range)->singleSequence(ctx), ctx);

  return st;
}

TreeNode::SingleState BroadcastNode::single(SingleContext *ctx)
{
  const SingleState procState = proc()->single(ctx);
  const SingleState exprState = expr()->single(ctx);
  
  if (!procState.singleValued)
    error() << "broadcasting process must be a single-valued expression" << endl;

  if (hasSingleEffects(exprState))
    error() << "broadcast expression must not have single effects" << endl;

  if (exprState.globalTerminations || exprState.randomTerminations)
    error() << "broadcast expression must not allow exceptions to be thrown" << endl;

  SingleState state = exprState;
  state.singleValued = type()->isSingle();
  state.syncSeq = Fixed;  
  return state;
}


void singleAnalysis(CompileUnitNode *file)
{
  file->single(NULL);
}