Tasks

examples/varsize.tip

@@ -0,0 +1,13 @@
+main() {
+    var a, b, c, d, cond, r;
+    a = 100;
+    b = a;
+    while (1000 > b) {
+        b = b * a;
+    }
+    c = b * b;
+    d = c / b / a;
+    if (d > 100) cond = 1;
+    else cond = 0;
+    return cond;
+}

src/tip/Tip.scala

@@ -336,7 +336,7 @@ object Tip extends App {
           options.andersen = true
         case "-steensgaard" =>
           options.steensgaard = true
-        case "-sign" | "-livevars" | "-available" | "-vbusy" | "-reaching" | "-constprop" | "-interval" | "-copyconstprop" | "-uninitvars" | "-taint" =>
+        case "-sign" | "-livevars" | "-available" | "-vbusy" | "-reaching" | "-constprop" | "-interval" | "-varsize" | "-copyconstprop" | "-uninitvars" | "-taint" =>
           options.dfAnalysis += dfa.withName(args(i).drop(1)) -> {
             if (i + 1 < args.length && dfo.values.map(_.toString()).contains(args(i + 1))) {
               i = i + 1

src/tip/analysis/FlowSensitiveAnalysis.scala

@@ -40,7 +40,7 @@ object FlowSensitiveAnalysis {
           case Analysis.livevars => new LiveVarsAnalysisSimpleSolver(typedCfg.left.get)
           case Analysis.available => new AvailableExpAnalysisSimpleSolver(typedCfg.left.get)
           //case Analysis.vbusy => new VeryBusyExpAnalysisSimpleSolver(typedCfg.left.get) <--- Complete here
-          //case Analysis.reaching => new ReachingDefAnalysisSimpleSolver(typedCfg.left.get) <--- Complete here
+          case Analysis.reaching => new ReachingDefAnalysisSimpleSolver(typedCfg.left.get)
           case Analysis.constprop => new ConstantPropagationAnalysis.Intraprocedural.SimpleSolver(typedCfg.left.get)
           case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
         })
@@ -50,7 +50,7 @@ object FlowSensitiveAnalysis {
           case Analysis.livevars => new LiveVarsAnalysisWorklistSolver(typedCfg.left.get)
           case Analysis.available => new AvailableExpAnalysisWorklistSolver(typedCfg.left.get)
           //case Analysis.vbusy => new VeryBusyExpAnalysisWorklistSolver(typedCfg.left.get) <--- Complete here
-          //case Analysis.reaching => new ReachingDefAnalysisWorklistSolver(typedCfg.left.get) <--- Complete here
+          case Analysis.reaching => new ReachingDefAnalysisWorklistSolver(typedCfg.left.get)
           case Analysis.constprop => new ConstantPropagationAnalysis.Intraprocedural.WorklistSolver(typedCfg.left.get)
           case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
         })
@@ -63,11 +63,13 @@ object FlowSensitiveAnalysis {
       case AnalysisOption.`wlrw` =>
         Some(kind match {
           case Analysis.interval => new IntervalAnalysis.Intraprocedural.WorklistSolverWithWidening(typedCfg.left.get)
+          case Analysis.varsize => new VariableSizeAnalysis.Intraprocedural.WorklistSolverWithWidening(typedCfg.left.get)
           case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
         })
       case AnalysisOption.`wlrwn` =>
         Some(kind match {
           case Analysis.interval => new IntervalAnalysis.Intraprocedural.WorklistSolverWithWideningAndNarrowing(typedCfg.left.get)
+          case Analysis.varsize => new VariableSizeAnalysis.Intraprocedural.WorklistSolverWithWideningAndNarrowing(typedCfg.left.get)
           case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
         })
       case AnalysisOption.`wlrp` =>
@@ -166,6 +168,6 @@ object FlowSensitiveAnalysis {
     * A flow sensitive analysis kind
     */
   object Analysis extends Enumeration {
-    val sign, livevars, available, vbusy, reaching, constprop, interval, copyconstprop, uninitvars, taint = Value
+    val sign, livevars, available, vbusy, reaching, constprop, interval, varsize, copyconstprop, uninitvars, taint = Value
   }
 }

src/tip/analysis/IntervalAnalysis.scala

@@ -19,7 +19,7 @@ trait IntervalAnalysisWidening extends ValueAnalysisMisc with Dependencies[CfgNo
   /**
     * Int values occurring in the program, plus -infinity and +infinity.
     */
-  private val B = cfg.nodes.flatMap { n =>
+  protected val B = cfg.nodes.flatMap { n =>
     n.appearingConstants.map { x =>
       IntNum(x.value): Num
     } + MInf + PInf
@@ -35,7 +35,7 @@ trait IntervalAnalysisWidening extends ValueAnalysisMisc with Dependencies[CfgNo
     (x, y) match {
       case (IntervalLattice.EmptyInterval, _) => y
       case (_, IntervalLattice.EmptyInterval) => x
-      case ((l1, h1), (l2, h2)) => ??? //<--- Complete here
+      case ((l1, h1), (l2, h2)) => (maxB(if (l1 < l2) l1 else l2), minB(if (h1 > h2) h1 else h2))
     }
 
   def widen(x: liftedstatelattice.Element, y: liftedstatelattice.Element): liftedstatelattice.Element =

src/tip/analysis/LiveVarsAnalysis.scala

@@ -3,6 +3,7 @@ package tip.analysis
 import tip.ast._
 import tip.lattices._
 import tip.ast.AstNodeData.DeclarationData
+import tip.ast.AstOps.AstOp
 import tip.solvers._
 import tip.cfg._
 
@@ -20,24 +21,26 @@ abstract class LiveVarsAnalysis(cfg: IntraproceduralProgramCfg)(implicit declDat
   NoPointers.assertContainsProgram(cfg.prog)
   NoRecords.assertContainsProgram(cfg.prog)
 
-  def transfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element =
+  def transfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element = {
+    def vars(n: AExpr): Set[ADeclaration] = n.appearingIds
     n match {
       case _: CfgFunExitNode => lattice.sublattice.bottom
       case r: CfgStmtNode =>
         r.data match {
-          case cond: AExpr => ??? //<--- Complete here
+          case cond: AExpr => s ++ vars(cond)
           case as: AAssignStmt =>
             as.left match {
-              case id: AIdentifier => ??? //<--- Complete here
+              case id: AIdentifier => (s - id) ++ vars(as.right)
               case _ => ???
             }
-          case varr: AVarStmt => ??? //<--- Complete here
-          case ret: AReturnStmt => ??? //<--- Complete here
-          case out: AOutputStmt => ??? //<--- Complete here
+          case varr: AVarStmt => s -- varr.declIds
+          case ret: AReturnStmt => s ++ vars(ret.exp)
+          case out: AOutputStmt => s ++ vars(out.exp)
           case _ => s
         }
       case _ => s
     }
+  }
 }
 
 /**

src/tip/analysis/ReachingDefAnalysisSimpleSolver.scala

@@ -0,0 +1,53 @@
+package tip.analysis
+
+import tip.ast._
+import tip.lattices._
+import tip.ast.AstNodeData.DeclarationData
+import tip.ast.AstOps.AstOp
+import tip.solvers._
+import tip.cfg._
+import scala.collection.immutable.Set
+
+abstract class ReachingDefAnalysis(cfg: IntraproceduralProgramCfg)(implicit declData: DeclarationData) extends FlowSensitiveAnalysis(false) {
+  val lattice: MapLattice[CfgNode, PowersetLattice[AStmt]] = new MapLattice(new PowersetLattice())
+
+  val domain: Set[CfgNode] = cfg.nodes
+
+  NoPointers.assertContainsProgram(cfg.prog)
+  NoRecords.assertContainsProgram(cfg.prog)
+
+  def transfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element = {
+    def removerefs(S: lattice.sublattice.Element, x: AIdentifier) =
+      S.filterNot {
+        case as: AAssignStmt => as.left match {
+          case id: AIdentifier => id.name == x.name
+        }
+        case varr: AVarStmt => varr.declIds.last.name == x.name
+      }
+
+    n match {
+      case _: CfgFunExitNode => lattice.sublattice.bottom
+      case r: CfgStmtNode =>
+        r.data match {
+          case as: AAssignStmt =>
+            as.left match {
+              case id: AIdentifier => removerefs(s, id) + as
+              case _ => s
+            }
+          case varr: AVarStmt => s ++ varr.declIds.map(v => AVarStmt(List(v), v.loc)).toSet[AStmt];
+          case _ => s
+        }
+      case _ => s
+    }
+  }
+}
+
+class ReachingDefAnalysisSimpleSolver(cfg: IntraproceduralProgramCfg)(implicit declData: DeclarationData)
+  extends ReachingDefAnalysis(cfg)
+    with SimpleMapLatticeFixpointSolver[CfgNode]
+    with ForwardDependencies
+
+class ReachingDefAnalysisWorklistSolver(cfg: IntraproceduralProgramCfg)(implicit declData: DeclarationData)
+  extends ReachingDefAnalysis(cfg)
+    with SimpleWorklistFixpointSolver[CfgNode]
+    with ForwardDependencies

src/tip/analysis/SimpleSignAnalysis.scala

@@ -85,10 +85,10 @@ class SimpleSignAnalysis(cfg: ProgramCfg)(implicit declData: DeclarationData) ex
       case r: CfgStmtNode =>
         r.data match {
           // var declarations
-          case varr: AVarStmt => ??? //<--- Complete here
+          case varr: AVarStmt => s ++ varr.declIds.map(_ -> SignLattice.top)
 
           // assignments
-          case AAssignStmt(id: AIdentifier, right, _) => ??? //<--- Complete here
+          case AAssignStmt(id: AIdentifier, right, _) => s + (declData(id) -> eval(right, s))
 
           // all others: like no-ops
           case _ => s

src/tip/analysis/TypeAnalysis.scala

@@ -100,34 +100,42 @@ class TypeAnalysis(program: AProgram)(implicit declData: DeclarationData) extend
     */
   def visit(node: AstNode, arg: Unit): Unit = {
     log.verb(s"Visiting ${node.getClass.getSimpleName} at ${node.loc}")
+    def createRecType(field: String, right: AstNode): RecordType = {
+      RecordType(allFieldNames.map { f =>
+        if (f == field) VarType(right) else FreshVarType()
+      })
+    }
     node match {
-      case program: AProgram => ??? // <--- Complete here
-      case _: ANumber => ??? // <--- Complete here
-      case _: AInput => ??? // <--- Complete here
-      case is: AIfStmt => ??? // <--- Complete here
-      case os: AOutputStmt => ??? // <--- Complete here
-      case ws: AWhileStmt => ??? // <--- Complete here
+      case program: AProgram => ()
+      case _: ANumber => unify(node, IntType())
+      case _: AInput => unify(node, IntType())
+      case is: AIfStmt => unify(is.guard, IntType())
+      case os: AOutputStmt => unify(os.exp, IntType())
+      case ws: AWhileStmt => unify(ws.guard, IntType())
       case as: AAssignStmt =>
         as.left match {
-          case id: AIdentifier => ??? // <--- Complete here
-          case dw: ADerefWrite => ??? // <--- Complete here
-          case dfw: ADirectFieldWrite => ??? // <--- Complete here
-          case ifw: AIndirectFieldWrite => ??? // <--- Complete here
+          case id: AIdentifier => unify(id.declaration, as.right)
+          case dw: ADerefWrite => unify(dw.exp, PointerType(as.right))
+          case dfw: ADirectFieldWrite => unify(dfw.id, createRecType(dfw.field, as.right))
+          case ifw: AIndirectFieldWrite => unify(ifw.exp, PointerType(createRecType(ifw.field, as.right)))
         }
       case bin: ABinaryOp =>
+        unify(bin, IntType())
         bin.operator match {
-          case Eqq => ??? // <--- Complete here
-          case _ => ??? // <--- Complete here
+          case Eqq => unify(bin.left, bin.right)
+          case _ =>
+            unify(bin.left, IntType())
+            unify(bin.right, IntType())
         }
       case un: AUnaryOp =>
         un.operator match {
-          case DerefOp => ??? // <--- Complete here
+          case DerefOp => unify(un.subexp, PointerType(un))
         }
-      case alloc: AAlloc => ??? // <--- Complete here
-      case ref: AVarRef => ??? // <--- Complete here
-      case _: ANull => ??? // <--- Complete here
-      case fun: AFunDeclaration => ??? // <--- Complete here
-      case call: ACallFuncExpr => ??? // <--- Complete here
+      case alloc: AAlloc => unify(alloc, PointerType(alloc.exp))
+      case ref: AVarRef => unify(ref, PointerType(ref.id))
+      case _: ANull => unify(node, PointerType(FreshVarType()))
+      case fun: AFunDeclaration => unify(fun, FunctionType(fun.params, fun.stmts.ret.exp))
+      case call: ACallFuncExpr => unify(call.targetFun, FunctionType(call.args, call))
       case _: AReturnStmt =>
       case rec: ARecord =>
         val fieldmap = rec.fields.foldLeft(Map[String, Term[Type]]()) { (a, b) =>

src/tip/analysis/ValueAnalysis.scala

@@ -69,10 +69,10 @@ trait ValueAnalysisMisc {
       case r: CfgStmtNode =>
         r.data match {
           // var declarations
-          case varr: AVarStmt => ??? //<--- Complete here
+          case varr: AVarStmt => s ++ varr.declIds.map(_ -> valuelattice.top)
 
           // assignments
-          case AAssignStmt(id: AIdentifier, right, _) => ??? //<--- Complete here
+          case AAssignStmt(id: AIdentifier, right, _) => s + (declData(id) -> eval(right, s))
 
           // all others: like no-ops
           case _ => s

src/tip/analysis/VariableSizeAnalysis.scala

@@ -0,0 +1,43 @@
+package tip.analysis
+
+import tip.ast.AstNodeData.DeclarationData
+import tip.cfg.{CfgNode, IntraproceduralProgramCfg}
+import tip.lattices.IntervalLattice
+import tip.solvers.{WorklistFixpointSolverWithReachabilityAndWidening, WorklistFixpointSolverWithReachabilityAndWideningAndNarrowing}
+
+trait VariableSizeAnalysisWidening extends IntervalAnalysisWidening {
+
+  override protected val B: Set[IntervalLattice.Num] = Set(
+    0, 1,
+    Byte.MinValue, Byte.MaxValue,
+    Char.MinValue, Char.MaxValue,
+    Int.MinValue, Int.MaxValue,
+    IntervalLattice.MInf, IntervalLattice.PInf
+  )
+}
+
+object VariableSizeAnalysis {
+
+  object Intraprocedural {
+
+    /**
+     * Interval analysis, using the worklist solver with init and widening.
+     */
+    class WorklistSolverWithWidening(cfg: IntraproceduralProgramCfg)(implicit declData: DeclarationData)
+      extends IntraprocValueAnalysisWorklistSolverWithReachability(cfg, IntervalLattice)
+        with WorklistFixpointSolverWithReachabilityAndWidening[CfgNode]
+        with VariableSizeAnalysisWidening
+
+    /**
+     * Interval analysis, using the worklist solver with init, widening, and narrowing.
+     */
+    class WorklistSolverWithWideningAndNarrowing(cfg: IntraproceduralProgramCfg)(implicit declData: DeclarationData)
+      extends IntraprocValueAnalysisWorklistSolverWithReachability(cfg, IntervalLattice)
+        with WorklistFixpointSolverWithReachabilityAndWideningAndNarrowing[CfgNode]
+        with VariableSizeAnalysisWidening {
+
+      val narrowingSteps = 5
+    }
+  }
+}
+

src/tip/lattices/GenericLattices.scala

@@ -146,9 +146,9 @@ class PowersetLattice[A] extends Lattice {
 
   type Element = Set[A]
 
-  val bottom: Element = ??? //<--- Complete here
+  val bottom: Element = Set.empty[A]
 
-  def lub(x: Element, y: Element): Element = ??? //<--- Complete here
+  def lub(x: Element, y: Element): Element = x.union(y)
 }
 
 /**

theory/L2.md

@@ -0,0 +1,71 @@
+- Что будет, если в нашу систему ввести тип Bool?
+- Попробуйте переписать все правила подходящим образом
+
+Необходимо будет добавить новые правила для грамматики языка:  
+```
+<expr> = <bool_const>
+<expr> = <expr><cmp><expr>
+<bool_const> = 'true' | 'false'
+<cmp> = ('<' | '<=' | '==' | '!=' | '>' | '>=')
+```
+Также, необходимо переписать правила для анализа типов:  
+```
+E1 cmp E2              [[E1]] = [[E2]] = int ^ [[E1 cmp E2]] = bool
+if(E) {S}              [[E]] = bool
+if(E) {S1} else {S2}   [[E]] = bool
+while(E) {S}           [[E]] = bool
+```
+- Будет ли анализ
+  - более полным?
+  - более точным?
+
+Полнота - упадет. Семантика языка допускает конструкции по типу if(1) {S1}, а правила анализа типов - нет
+Точность - останется такой же, т.к. анализ типов soundness.
+
+- Что будет, если в нашу систему ввести тип Array?
+- Придумайте правила вывода для новых операторов
+```
+{}                      [[{}]] = α[]
+{E1,..., En}            [[E1]] = ... = [[En]] ^ [[{E1,..., En}]] = [[E1]][]
+E1[E2]                  [[E1]] = α[] ^ [[E2]] = int ^ [[E1[E2]]] = α
+E1[E2] = E3             [[E1]] = α[] ^ [[E2]] = int ^ [[E3]] = α
+```
+
+- Попробуйте протипизировать программу со слайда
+```
+main() {
+    var x,y,z,t;
+    x = {2,4,8,16,32,64};
+    // [[x]] = [[{2,4,8,16,32,64}]], [[2]] = ... = [[64]] ^ [[{2,4,8,16,32,64}]] = [[2]][]
+
+    y = x[x[3]];
+    // [[y]] = [[x[x[3]]]]
+    // [[x]] = α1[] ^ [[x[3]]] = int ^ [[x[x[3]]]] = α1
+    // [[x]] = α2[] ^ [[3]] = int ^ [[x[3]]] = α2
+
+    z = {{},x};
+    // [[z]] = [[{{}, x}]]
+    // [[{}]] = [[x]] ^ [[{}, x}]] = [[{}]][]
+    // [[{}]] = α3[]
+
+    t = z[1];
+    // [[t]] = [[z[1]]]
+    // [[z]] = α4[] ^ [[1]] = int ^ [[z[1]]] = α4
+
+    t[2] = y;
+    // [[t]] = α5[] ^ [[2]] = int ^ [[y]] = α5
+}
+```
+Решение:  
+```
+  α1 = int
+  α2 = int
+  α3 = int[]
+  α4 = int[]
+  α5 = int
+
+  [[x]] = int[]
+  [[y]] = int
+  [[z]] = int[][]
+  [[t]] = int[]  
+```