Support type guards for CompT / Add type guard for ValidateNonRevoked…

…Proxy
es-meta · Sep 14, 2024 · 67dd3a6 · 67dd3a6
1 parent 0b7298f
commit 67dd3a6
Show file tree

Hide file tree

Showing 2 changed files with 70 additions and 57 deletions.
diff --git a/src/main/scala/esmeta/analyzer/TypeAnalyzer.scala b/src/main/scala/esmeta/analyzer/TypeAnalyzer.scala
@@ -263,6 +263,17 @@ class TypeAnalyzer(
           }
           AbsValue(retTy, map)
         },
+        "ValidateNonRevokedProxy" -> { (xs, vs, retTy) =>
+          var map: Refinements = Map()
+          xs(0).map { x =>
+            map += Normal -> Map(
+              x -> ValueTy.from(
+                "Record[ProxyExoticObject { ProxyHandler : Record[Object], ProxyTarget : Record[Object] }]",
+              ),
+            )
+          }
+          AbsValue(retTy, map)
+        },
         "IsPromise" -> { (xs, vs, retTy) =>
           var map: Refinements = Map()
           xs(0).map { x => map += True -> Map(x -> RecordT("Promise")) }
@@ -491,8 +502,10 @@ class TypeAnalyzer(
       refinedValue: AbsValue,
     )(using np: NodePoint[_]): Result[List[Unit]] =
       var kinds = Vector.empty[RefinementKind]
-      if (refinedValue ⊑ AVT) kinds :+= RefinementKind.True
-      if (refinedValue ⊑ AVF) kinds :+= RefinementKind.False
+      if (refinedValue.ty <= TrueT) kinds :+= RefinementKind.True
+      if (refinedValue.ty <= FalseT) kinds :+= RefinementKind.False
+      if (refinedValue.ty <= NormalT) kinds :+= RefinementKind.Normal
+      if (refinedValue.ty <= AbruptT) kinds :+= RefinementKind.Abrupt
       join(for {
         kind <- kinds
         map <- value.refinements.get(kind).toList
@@ -667,9 +680,12 @@ class TypeAnalyzer(
       l <- transfer(x)
       v <- transfer(l)
       refinedV =
-        if (positive) v ⊓ AbsValue(ty)
+        if (positive)
+          if (v.ty <= ty.toValue) v
+          else v ⊓ AbsValue(ty)
         else v -- AbsValue(ty)
       _ <- modify(_.update(l, refinedV))
+      _ <- refine(v, refinedV)
     } yield ()
   }
 

diff --git a/src/main/scala/esmeta/ty/RecordTy.scala b/src/main/scala/esmeta/ty/RecordTy.scala
@@ -56,7 +56,7 @@ enum RecordTy extends TyElem with Lattice[RecordTy] {
           lfm = lmap.getOrElse(t, FieldMap.Top)
           rfm = rmap.getOrElse(t, FieldMap.Top)
           fm = lfm && rfm
-          pair <- update(t, fm, refine = true)
+          pair <- RecordTy.update(t, fm, refine = true)
         } yield pair)
           .groupBy(_._1)
           .map { case (t, pairs) => t -> pairs.map(_._2).reduce(_ && _) }
@@ -96,14 +96,7 @@ enum RecordTy extends TyElem with Lattice[RecordTy] {
   /** field accessor */
   def apply(f: String): Binding = this match
     case Top       => Binding.Top
-    case Elem(map) => map.map(apply(_, f)).foldLeft(Binding.Bot)(_ || _)
-
-  /** field accessor for specific record type */
-  private def apply(pair: (String, FieldMap), f: String): Binding = this match
-    case Top => Binding.Top
-    case Elem(map) =>
-      val (t, fm) = pair
-      getField(t, f) && fm(f)
+    case Elem(map) => map.map(RecordTy(_, f)).foldLeft(Binding.Bot)(_ || _)
 
   /** field update */
   def update(field: String, ty: ValueTy, refine: Boolean): RecordTy =
@@ -119,40 +112,11 @@ enum RecordTy extends TyElem with Lattice[RecordTy] {
     case Elem(map) =>
       Elem(map.foldLeft(Map[String, FieldMap]()) {
         case (map, pair) =>
-          update(pair, field, elem, refine).fold(map) { (t, fm) =>
+          RecordTy.update(pair, field, elem, refine).fold(map) { (t, fm) =>
             map + (t -> map.get(t).fold(fm)(_ || fm))
           }
       })
 
-  /** field update */
-  private def update(
-    t: String,
-    fm: FieldMap,
-    refine: Boolean,
-  ): Option[(String, FieldMap)] =
-    fm.map.foldLeft(Option(t -> FieldMap.Top)) {
-      case (None, _)               => None
-      case (Some(pair), (f, elem)) => update(pair, f, elem, refine)
-    }
-
-  /** field update */
-  private def update(
-    pair: (String, FieldMap),
-    field: String,
-    elem: Binding,
-    refine: Boolean,
-  ): Option[(String, FieldMap)] =
-    val (t, fm) = pair
-    val x = (for {
-      map <- refinerOf(t).get(field)
-      (_, u) <- map.find { case (e, _) => elem <= e }
-    } yield u).getOrElse(t)
-    if (refine)
-      val refined = elem && apply(pair, field)
-      if (refined.isBottom) None
-      else Some(normalize(x -> fm.update(field, refined)))
-    else Some(normalize(x -> fm.update(field, elem)))
-
   /** record containment check */
   def contains(record: RecordObj, heap: Heap): Boolean = this match
     case Top => true
@@ -171,11 +135,6 @@ enum RecordTy extends TyElem with Lattice[RecordTy] {
   def normalized: RecordTy = this match
     case Top       => Top
     case Elem(map) => Elem(map.map(normalize))
-
-  /** normalized type */
-  private def normalize(pair: (String, FieldMap)): (String, FieldMap) =
-    val (t, fm) = pair
-    t -> FieldMap(fm.map.filter { (f, elem) => !(getField(t, f) <= elem) })
 }
 
 object RecordTy extends Parser.From(Parser.recordTy) {
@@ -187,18 +146,56 @@ object RecordTy extends Parser.From(Parser.recordTy) {
     apply(names.toSet)
   def apply(names: Set[String]): RecordTy =
     apply(names.toList.map(_ -> FieldMap.Top).toMap)
-  def apply(name: String, fields: Map[String, ValueTy]): RecordTy = apply(
-    Map(
-      name -> FieldMap(
-        (for {
-          (field, ty) <- fields
-          elem = Binding(ty, false, false)
-        } yield field -> elem).toMap,
-      ),
-    ),
-  ).normalized
+  def apply(name: String, fields: Map[String, ValueTy]): RecordTy =
+    fields
+      .foldLeft(Option(name -> FieldMap.Top)) {
+        case (None, _) => None
+        case (Some(pair), (f, ty)) =>
+          update(pair, f, Binding(ty), refine = false)
+      }
+      .fold(Bot)(apply)
+  def apply(pair: (String, FieldMap)): RecordTy = apply(Map(pair))
   def apply(name: String, fieldMap: FieldMap): RecordTy =
     apply(Map(name -> fieldMap))
   def apply(map: Map[String, FieldMap]): RecordTy =
     Elem(map)
+
+  /** field accessor for specific record type */
+  private def apply(pair: (String, FieldMap), f: String): Binding =
+    val (t, fm) = pair
+    getField(t, f) && fm(f)
+
+  /** field update */
+  private def update(
+    t: String,
+    fm: FieldMap,
+    refine: Boolean,
+  ): Option[(String, FieldMap)] =
+    fm.map.foldLeft(Option(t -> FieldMap.Top)) {
+      case (None, _)               => None
+      case (Some(pair), (f, elem)) => update(pair, f, elem, refine)
+    }
+
+  /** field update */
+  private def update(
+    pair: (String, FieldMap),
+    field: String,
+    elem: Binding,
+    refine: Boolean,
+  ): Option[(String, FieldMap)] =
+    val (t, fm) = pair
+    val x = (for {
+      map <- refinerOf(t).get(field)
+      (_, u) <- map.find { case (e, _) => elem <= e }
+    } yield u).getOrElse(t)
+    if (refine)
+      val refined = elem && apply(pair, field)
+      if (refined.isBottom) None
+      else Some(normalize(x -> fm.update(field, refined)))
+    else Some(normalize(x -> fm.update(field, elem)))
+
+  /** normalized type */
+  private def normalize(pair: (String, FieldMap)): (String, FieldMap) =
+    val (t, fm) = pair
+    t -> FieldMap(fm.map.filter { (f, elem) => !(getField(t, f) <= elem) })
 }