TYPE

  SignFlattened = flat(snum)
  BoolFlattened = flat(bool)
  State          = Var -> SignFlattened

PROBLEM Sign

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


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

  evalAExp :: Expression * State -> SignFlattened
  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 (valLeft=valRight) then lift(valLeft) 
                   else if (valLeft=0 || valRight=0) then lift(valLeft+valRight) else top endif endif;
        "-" => let valLeft  <= evalAExp(expSubLeft(expression),  state),
                   valRight <= evalAExp(expSubRight(expression), state) in
                 if (valLeft=0 || valRight=0) then lift(valLeft-valRight) 
                   else if (valLeft!=valRight) then lift(valLeft) else top endif 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 if (valLeft=valRight) then lift(1) else lift(-1) endif 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 top endif endif;
        endcase;
      "ARITH_UNARY" =>
    case expOp(expression) of
          "-" => let v<=evalAExp(expSub(expression), state) in lift(-v);
        endcase;
      "VAR"   => state(expVar(expression));
      "CONST" => lift(if (expVal(expression)>0) then 1 else if (expVal(expression)<0) then -1 else 0 endif endif);
      _       => 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 (valLeft!=valRight) then lift(false) else top endif endif;
         "<>" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                     valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft=0 && valRight=0) then lift(false) 
               else if (valLeft!=valRight) then lift(true) else top endif endif;
         "<" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                    valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft<valRight) then lift(true) 
               else if (valLeft!=valRight || (valLeft=0 && valRight=0)) then lift(false) else top endif endif;
         ">" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                    valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft>valRight) then lift(true)
               else if (valLeft!=valRight || (valLeft=0 && valRight=0)) then lift(false) else top endif endif;
         "<=" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                     valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft<valRight || (valLeft=0 && valRight=0)) then lift(true) 
               else if (valLeft!=valRight) then lift(false) else top endif endif;
         ">=" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                     valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft>valRight || (valLeft=0 && valRight=0)) then lift(true) 
               else if (valLeft!=valRight) then lift(false) else top endif endif;
         _ => top;
         endcase;
       _ => top;
     endcase

evalCondExp :: Expression * State * bool -> State
   evalCondExp(expression,state,edge) = 
     case expType(expression) of 
       "TRUE" => if (edge) then state else bot endif;
       "FALSE" => if (!edge) then state else bot endif;
       "BOOL_BINARY" => let leftExp=expSubLeft(expression) in case expType(leftExp) of 
             "VAR" => let var=expVar(leftExp), valRight<=evalAExp(expSubRight(expression), state) in
                case expOp(expression) of
                    "=" => if (edge) then state\[var->lift(valRight)] else top endif;
                    "<>" => if edge then top else state\[var->lift(valRight)] endif;
                    "<" => if edge then (if (valRight<=0) then state\[var->lift(-1)] else top endif) else (if (valRight=1) then state\[var->lift(1)] else top endif) endif;
                    ">" => if edge then (if (valRight>=0) then state\[var->lift(1)] else top endif) else (if (valRight=-1) then state\[var->lift(-1)] else top endif) endif;
                    "<=" => if edge then (if (valRight=-1) then state\[var->lift(-1)] else top endif) else (if (valRight>=0) then state\[var->lift(1)] else top endif) endif;
                    ">=" => if edge then (if (valRight=1) then state\[var->lift(1)] else top endif) else (if (valRight<=0) then state\[var->lift(-1)] else top endif) endif;
                    _ => top;
                endcase;
             _ => state ;
             endcase;            
       _ => state;
     endcase

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