TYPE

  PSign  = set(snum)
  PSignLifted  = lift(PSign)
  BoolFlattened = flat(bool)
  State  = Var -> PSignLifted

PROBLEM SignExtended

  direction  : forward
  carrier    : State
  init       : bot
  init_start : [-> top]
  combine    : nLUB


TRANSFER

// in assignments calculate the new value of the variable and add it to the state
  ASSIGN(variable, expression) =
    if @ = bot then bot else @\[variable -> evalAExp(expression, @)] endif

  // test conditions
  IF(expression), true_edge = branch(expression,@,true)
  IF(expression), false_edge = branch(expression,@,false)

  // loop conditions
  WHILE(expression), true_edge = branch(expression,@,true)  
  WHILE(expression), false_edge = branch(expression,@,false)

SUPPORT  
  mySgn :: snum-> snum
  mySgn(x) = if (x<0) then -1 else if (x=0) then 0 else 1 endif endif

  nLUB :: State*State->State
  nLUB(e1,e2) = [ [->top]\(a,b) |(a,b) in (e1 lub e2)\top; (b=bot || !(-1?drop(b) && 1?drop(b)))]

  evalAExp :: Expression * State -> PSignLifted
  evalAExp(expression, state) =
    case expType(expression) of
      "ARITH_BINARY" => case expOp(expression) of
        "+" => let valLeft  <= evalAExp(expSubLeft(expression),  state),
                   valRight <= evalAExp(expSubRight(expression), state) in
		    if ((-1?valLeft && 1?valRight) || (1?valLeft && -1?valRight)) then top 
		      else lift({mySgn(x1 + x2) | x1 in valLeft; x2 in valRight}) endif;
        "-" => let valLeft  <= evalAExp(expSubLeft(expression),  state),
                   valRight <= evalAExp(expSubRight(expression), state) in
                 if ((-1?valLeft && -1?valRight) || (1?valLeft && 1?valRight)) then top
		      else lift({mySgn(x1 - x2) | x1 in valLeft; x2 in valRight}) endif;
        "*" => let valLeft  = evalAExp(expSubLeft(expression),  state),
                   valRight = evalAExp(expSubRight(expression), state) in
                 if (valLeft=bot || valRight=bot) then bot
		      else if (valLeft=lift({0}) || valRight=lift({0})) then lift({0})
		      else if (valLeft=top || valRight=top) then top
		      else lift({mySgn(x1 * x2) | x1 in drop(valLeft); x2 in drop(valRight)}) endif endif endif;
        "/" => let valLeft  = evalAExp(expSubLeft(expression),  state),
                   valRight = evalAExp(expSubRight(expression), state) in
                 if (valLeft=bot || valRight=bot || valRight=lift({0})) then bot
                   else if (valLeft=lift({0})) then lift({0})
                   else lift(union({0},{mySgn(x1 * x2) | x1 in drop(valLeft); x2 in drop(valRight)})) endif endif;
        endcase;
      "ARITH_UNARY" => case expOp(expression) of
          "-" => let value <= evalAExp(expSub(expression), state) in lift({-x | x in value});
        endcase;
      "VAR"   => state (expVar(expression));
      "CONST" => lift({mySgn(expVal(expression))});
      _       => error("Runtime Error: evalAExp applied to nonarithmetic Expression");
    endcase

evalBExp :: Expression * State -> BoolFlattened
   evalBExp(expression,state) = 
     case expType(expression) of 
       "TRUE" => lift(true);
       "FALSE" => lift(false);
       "BOOL_UNARY" => let value <= evalBExp(expSub(expression), state) in lift(!value);
       "BOOL_BINARY" => case expOp(expression) of
	       "=" => let valLeft  <= evalAExp(expSubLeft(expression),  state),
                    valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft={0} && valRight={0}) then lift(true) 
               else if (intersect(valLeft,valRight)!={}) then top else lift(false) endif endif;
         "<>" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                    valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft={0} && valRight={0}) then lift(false) 
               else if (intersect(valLeft,valRight)!={}) then top else lift(true) endif endif;
         "<" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                   valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft={0}) then (if (valRight={1}) then lift(true) else if (valRight={0,1}) then top else lift(false) endif endif)
               else if (-1?valLeft) then (if (intersect(valLeft,valRight)={}) then lift(true) else top endif)
               else (if (1?valRight) then top else lift(false) endif) endif endif;
         ">" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                   valRight <= evalAExp(expSubRight(expression), state) in
             if (valRight={0}) then (if (valLeft={1}) then lift(true) else if (valLeft={0,1}) then top else lift(false) endif endif)
               else if (-1?valRight) then (if (intersect(valLeft,valRight)={}) then lift(true) else top endif)
               else (if (1?valLeft) then top else lift(false) endif) endif endif;
         "<=" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                    valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft={0} && valRight={0}) then lift(true) 
               else if (intersect(valLeft,valRight)!={}) then top 
               else (if (valLeft={0}) then (if (valRight={1}) then lift(true) else if (valRight={0,1}) then top else lift(false) endif endif)
                 else if (-1?valLeft) then (if (intersect(valLeft,valRight)={}) then lift(true) else top endif)
                 else (if (1?valRight) then top else lift(false) endif) endif endif)
               endif endif;
         ">=" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                    valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft={0} && valRight={0}) then lift(true) 
               else if (intersect(valLeft,valRight)!={}) then top 
               else (if (valRight={0}) then (if (valLeft={1}) then lift(true) else if (valLeft={0,1}) then top else lift(false) endif endif)
                 else if (-1?valRight) then (if (intersect(valLeft,valRight)={}) then lift(true) else top endif)
                 else (if (1?valLeft) then top else lift(false) endif) endif endif)
               endif endif;
         _ => top;
         endcase;
       _ => top;
     endcase

   branch :: Expression * State * bool -> State
   branch(expression, state, edge) = let valexp = evalBExp(expression,state) in 
      if (valexp != bot && (valexp = top || drop(valexp) = edge)) then state else bot endif