Skip to content

Commit bbde104

Browse files
d01c2d01c2
committed
fix: lint error
1 parent 5c085d3 commit bbde104

1 file changed

Lines changed: 107 additions & 45 deletions

File tree

‎src/main/scala/esmeta/solver/Reifier.scala‎

Lines changed: 107 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,10 @@ object Reifier {
3232
private val default = "undefined" // fallback witness
3333

3434
// per-sym witnesses; None if any sym cannot be reified (unsatisfiable shape)
35-
def witness(formulas: List[Formula], syms: List[Sym]): Option[Map[Sym, String]] =
35+
def witness(
36+
formulas: List[Formula],
37+
syms: List[Sym],
38+
): Option[Map[Sym, String]] =
3639
val pairs = syms.map(sym => sym -> reifyValue(model(sym, formulas)))
3740
Option.when(pairs.forall(_._2.isDefined)) {
3841
pairs.collect { case (s, Some(js)) => s -> js }.toMap
@@ -54,26 +57,36 @@ object Reifier {
5457
// result `done` constraint (then the call-return path reifies a finite
5558
// iterator on its own and this case can be deleted).
5659
case FTypeCheck(SERecord("IteratorRecord", fields), _) =>
57-
fields.get("NextMethod").fold(m)(n => narrowAt(m, sym, n)(markIteratorNext))
58-
case FTypeCheck(t, ty) => narrowAt(m, sym, t)(byTypeCheck(ty))
59-
case FEq(SELit(_), SELit(_)) => m
60+
fields
61+
.get("NextMethod")
62+
.fold(m)(n => narrowAt(m, sym, n)(markIteratorNext))
63+
case FTypeCheck(t, ty) => narrowAt(m, sym, t)(byTypeCheck(ty))
64+
case FEq(SELit(_), SELit(_)) => m
6065
// HasProperty(base, key) == bool: ordinary property presence/absence
61-
case FEq(ValueField(SECall("HasProperty", b :: rest)), SELit(EBool(exists))) =>
66+
case FEq(
67+
ValueField(SECall("HasProperty", b :: rest)),
68+
SELit(EBool(exists)),
69+
) =>
6270
hasProperty(m, sym, b, rest, exists)
63-
case FEq(SELit(EBool(exists)), ValueField(SECall("HasProperty", b :: rest))) =>
71+
case FEq(
72+
SELit(EBool(exists)),
73+
ValueField(SECall("HasProperty", b :: rest)),
74+
) =>
6475
hasProperty(m, sym, b, rest, exists)
6576
case FEq(SECall("HasProperty", b :: rest), SELit(EBool(exists))) =>
6677
hasProperty(m, sym, b, rest, exists)
6778
case FEq(SELit(EBool(exists)), SECall("HasProperty", b :: rest)) =>
6879
hasProperty(m, sym, b, rest, exists)
69-
case FEq(t, SELit(lit)) => narrowAt(m, sym, t)(byLiteral(lit))
70-
case FEq(SELit(lit), t) => narrowAt(m, sym, t)(byLiteral(lit))
80+
case FEq(t, SELit(lit)) => narrowAt(m, sym, t)(byLiteral(lit))
81+
case FEq(SELit(lit), t) => narrowAt(m, sym, t)(byLiteral(lit))
7182
// value identical to a realm intrinsic: pin its JS access expression
7283
case FEq(t, intrinsicJs(js)) => narrowAt(m, sym, t)(pinTo(js))
7384
case FEq(intrinsicJs(js), t) => narrowAt(m, sym, t)(pinTo(js))
74-
case FExists(b, k @ SELit(EStr(_))) => narrowAt(m, sym, SEField(b, k))(identity)
75-
case FNot(FExists(b, SELit(EStr(f)))) => narrowAt(m, sym, b)(absentSlot(f))
76-
case FNot(FTypeCheck(t, ty)) => narrowAt(m, sym, t)(without(ty))
85+
case FExists(b, k @ SELit(EStr(_))) =>
86+
narrowAt(m, sym, SEField(b, k))(identity)
87+
case FNot(FExists(b, SELit(EStr(f)))) =>
88+
narrowAt(m, sym, b)(absentSlot(f))
89+
case FNot(FTypeCheck(t, ty)) => narrowAt(m, sym, t)(without(ty))
7790
case FNot(FEq(t, SELit(lit))) =>
7891
negTy(lit).fold(m)(nt => narrowAt(m, sym, t)(without(nt)))
7992
case FNot(FEq(SELit(lit), t)) =>
@@ -112,7 +125,10 @@ object Reifier {
112125

113126
// the value lacks internal slot `f`
114127
private def absentSlot(f: String): Model => Model =
115-
m => m.copy(ty = m.ty.copied(record = m.ty.record.update(f, Binding.Absent, true)))
128+
m =>
129+
m.copy(ty =
130+
m.ty.copied(record = m.ty.record.update(f, Binding.Absent, true)),
131+
)
116132

117133
// [Z3] FIXME: mark an iterator's NextMethod for hardcoded finite reification
118134
private def markIteratorNext: Model => Model =
@@ -144,8 +160,9 @@ object Reifier {
144160

145161
// the access path from `sym` to `expr`, or None if `expr` is not rooted at `sym`
146162
private def pathTo(sym: Sym, expr: SymExpr): Option[List[Access]] = expr match
147-
case SESym(s) => Option.when(s == sym)(Nil)
148-
case ValueField(c @ SECall(_, _)) => pathTo(sym, c) // strip completion .Value
163+
case SESym(s) => Option.when(s == sym)(Nil)
164+
case ValueField(c @ SECall(_, _)) =>
165+
pathTo(sym, c) // strip completion .Value
149166
case SECall("Get" | "GetV" | "GetMethod", args) =>
150167
getKey(args).flatMap((b, k) => pathTo(sym, b).map(_ :+ Access.Prop(k)))
151168
case SECall(name, b :: rest) if internalMethods(name) =>
@@ -158,23 +175,33 @@ object Reifier {
158175
// applying: narrow `m` at a located position
159176

160177
// narrow `m` at `expr`'s position (relative to `sym`); no-op if not rooted at `sym`
161-
private def narrowAt(m: Model, sym: Sym, expr: SymExpr)(narrow: Model => Model): Model =
178+
private def narrowAt(m: Model, sym: Sym, expr: SymExpr)(
179+
narrow: Model => Model,
180+
): Model =
162181
pathTo(sym, expr).fold(m)(walk(m, _, narrow))
163182

164183
// walk `path` from `m`, narrowing each container's kind, applying `narrow` at the leaf
165-
private def walk(m: Model, path: List[Access], narrow: Model => Model): Model =
184+
private def walk(
185+
m: Model,
186+
path: List[Access],
187+
narrow: Model => Model,
188+
): Model =
166189
path match
167190
case Nil => narrow(m)
168191
case access :: rest => descend(m, access, walk(_, rest, narrow))
169192

170193
// one access step into `m`: narrow the container's kind, recurse into the child
171194
private def descend(m: Model, access: Access, narrow: Model => Model): Model =
172-
m.copy(ty = kindOf(m.ty, access), children = entry(m.children, access, narrow))
195+
m.copy(
196+
ty = kindOf(m.ty, access),
197+
children = entry(m.children, access, narrow),
198+
)
173199

174200
// narrow the container's ty for the access taken into it
175201
private def kindOf(ty: ValueTy, access: Access): ValueTy = access match
176-
case Access.Slot(f) => ValueTy(record = ty.record.update(f, Binding.Exist, true))
177-
case _ => ty && ObjectT // prop/method => the container is an object
202+
case Access.Slot(f) =>
203+
ValueTy(record = ty.record.update(f, Binding.Exist, true))
204+
case _ => ty && ObjectT // prop/method => the container is an object
178205

179206
// narrow one child entry (`top` if absent)
180207
private def entry(
@@ -187,16 +214,26 @@ object Reifier {
187214
// resolving keys and method names
188215

189216
// Get(base, key) | Get(base, receiver, key) -> (base, key)
190-
private def getKey(args: List[SymExpr]): Option[(SymExpr, String)] = args match
191-
case b :: k :: Nil => propKey(k).map(b -> _)
192-
case b :: _ :: k :: Nil => propKey(k).map(b -> _)
193-
case _ => None
217+
private def getKey(args: List[SymExpr]): Option[(SymExpr, String)] =
218+
args match
219+
case b :: k :: Nil => propKey(k).map(b -> _)
220+
case b :: _ :: k :: Nil => propKey(k).map(b -> _)
221+
case _ => None
194222

195223
// internal methods reached as a Method access (Get-family stays a Prop)
196224
private val internalMethods: Set[String] = Set(
197-
"Call", "Construct", "GetPrototypeOf", "SetPrototypeOf", "IsExtensible",
198-
"PreventExtensions", "OwnPropertyKeys", "Set", "HasProperty",
199-
"DefineOwnProperty", "Delete", "GetOwnProperty",
225+
"Call",
226+
"Construct",
227+
"GetPrototypeOf",
228+
"SetPrototypeOf",
229+
"IsExtensible",
230+
"PreventExtensions",
231+
"OwnPropertyKeys",
232+
"Set",
233+
"HasProperty",
234+
"DefineOwnProperty",
235+
"Delete",
236+
"GetOwnProperty",
200237
)
201238

202239
// the singleton ValueTy of a literal
@@ -218,8 +255,9 @@ object Reifier {
218255
case SELit(EMath(n)) if n.isValidInt && n >= 0 => Some(n.toInt.toString)
219256
case SELit(ENumber(d)) if d >= 0 && d == d.toLong && !d.isInfinite =>
220257
Some(d.toLong.toString)
221-
case StaticField(SEGlobal("SYMBOL"), name) => Some("@@" + name) // well-known symbol
222-
case _ => None
258+
case StaticField(SEGlobal("SYMBOL"), name) =>
259+
Some("@@" + name) // well-known symbol
260+
case _ => None
223261

224262
// a realm intrinsic reference (`...Intrinsics["%Name%"]`) -> its JS access
225263
// expression; a dotted name is itself JS, an unnameable one maps via globalAlias
@@ -237,7 +275,6 @@ object Reifier {
237275
case _ => None
238276
}
239277

240-
241278
/** reify: build a JS expression that witnesses a Model */
242279
// TODO: NEEDS CODE REVIEW
243280

@@ -248,7 +285,11 @@ object Reifier {
248285
// [Z3] FIXME: `v.iteratorNext ||` routes hardcoded finite iterators here;
249286
// remove it (revert to the line below) once Z3 supplies `done` constraints.
250287
// else if (callReturn(v).isDefined || isConstructor(v) || v.ty <= FunctionT)
251-
else if (v.iteratorNext || callReturn(v).isDefined || isConstructor(v) || v.ty <= FunctionT)
288+
else if (
289+
v.iteratorNext || callReturn(v).isDefined || isConstructor(
290+
v,
291+
) || v.ty <= FunctionT
292+
)
252293
reifyFunction(v)
253294
else if (isObjectLike(v)) reifyObject(v)
254295
else reifyPrimitive(v)
@@ -261,7 +302,9 @@ object Reifier {
261302
// method constrained to throw makes it a Proxy with a throwing trap
262303
def reifyObject(v: Model): Option[String] =
263304
if (isRevokedProxy(v))
264-
Some("(() => { const r = Proxy.revocable({}, {}); r.revoke(); return r.proxy; })()")
305+
Some(
306+
"(() => { const r = Proxy.revocable({}, {}); r.revoke(); return r.proxy; })()",
307+
)
265308
else
266309
throwingTraps(v) match
267310
case traps if traps.nonEmpty =>
@@ -303,7 +346,9 @@ object Reifier {
303346
// regular call-return path reify a terminating iterator.
304347
def reifyIteratorNext(v: Model): Option[String] =
305348
val first = callReturn(v).flatMap(reifyValue).getOrElse("{}")
306-
Some(s"(() => { let i = 0; return () => (i++ ? { done: true } : $first); })()")
349+
Some(
350+
s"(() => { let i = 0; return () => (i++ ? { done: true } : $first); })()",
351+
)
307352

308353
// creation form from the value's record type ([[Prototype]] / exotic / `{}`);
309354
// a non-object record (e.g. Symbol) is built from its own type, an ordinary
@@ -318,7 +363,8 @@ object Reifier {
318363
if (props.isEmpty) Some(base)
319364
else
320365
val rendered = props.toList.sortBy(_._1).map { (k, child) =>
321-
if (child.pin.isEmpty && child.ty.isBottom) None // unsatisfiable -> no witness
366+
if (child.pin.isEmpty && child.ty.isBottom)
367+
None // unsatisfiable -> no witness
322368
else if (child.pin.isEmpty && child.ty <= AbruptT)
323369
Some(s"get ${jsPropKey(k)}() { throw 0; }")
324370
else reifyValue(child).map(js => s"${jsPropKey(k)}: $js")
@@ -358,18 +404,28 @@ object Reifier {
358404

359405
// proxy trap names for internal methods whose result is constrained abrupt
360406
private def throwingTraps(v: Model): List[String] =
361-
v.children.toList.collect {
362-
case (Access.Method(name, _), m) if m.ty <= AbruptT && proxyTraps.contains(name) =>
363-
proxyTraps(name)
364-
}.distinct.sorted
407+
v.children.toList
408+
.collect {
409+
case (Access.Method(name, _), m)
410+
if m.ty <= AbruptT && proxyTraps.contains(name) =>
411+
proxyTraps(name)
412+
}
413+
.distinct
414+
.sorted
365415

366416
// internal method -> Proxy trap (Call/Construct omitted: those reify as functions)
367417
private val proxyTraps: Map[String, String] = Map(
368-
"Get" -> "get", "Set" -> "set", "HasProperty" -> "has",
369-
"DefineOwnProperty" -> "defineProperty", "Delete" -> "deleteProperty",
370-
"GetOwnProperty" -> "getOwnPropertyDescriptor", "OwnPropertyKeys" -> "ownKeys",
371-
"GetPrototypeOf" -> "getPrototypeOf", "SetPrototypeOf" -> "setPrototypeOf",
372-
"IsExtensible" -> "isExtensible", "PreventExtensions" -> "preventExtensions",
418+
"Get" -> "get",
419+
"Set" -> "set",
420+
"HasProperty" -> "has",
421+
"DefineOwnProperty" -> "defineProperty",
422+
"Delete" -> "deleteProperty",
423+
"GetOwnProperty" -> "getOwnPropertyDescriptor",
424+
"OwnPropertyKeys" -> "ownKeys",
425+
"GetPrototypeOf" -> "getPrototypeOf",
426+
"SetPrototypeOf" -> "setPrototypeOf",
427+
"IsExtensible" -> "isExtensible",
428+
"PreventExtensions" -> "preventExtensions",
373429
)
374430

375431
// the pinned singleton value of `ty` as JS, if any
@@ -406,8 +462,12 @@ object Reifier {
406462
// a concrete default whose instances satisfy `ty` (e.g. a union like
407463
// ArrayBuffer|SharedArrayBuffer picks ArrayBuffer, not the ObjectT catch-all)
408464
.orElse(defaults.collectFirst { case (c, js) if c <= ty => js })
409-
.orElse(defaults.collectFirst { case (c, js) if ty <= c => js }) // subtype
410-
.orElse(defaults.collectFirst { case (c, js) if !(ty && c).isBottom => js })
465+
.orElse(defaults.collectFirst {
466+
case (c, js) if ty <= c => js
467+
}) // subtype
468+
.orElse(defaults.collectFirst {
469+
case (c, js) if !(ty && c).isBottom => js
470+
})
411471

412472
private val defaults: List[(ValueTy, String)] = List(
413473
RecordT("TypedArray") -> "new Int8Array()",
@@ -487,7 +547,9 @@ object Reifier {
487547
val value = witness.getOrElse(Sym.Arg(0), default)
488548
Some(s"${descriptor(base)}.set.call($thisArg, $value);")
489549
case _ =>
490-
access(path).map(fn =>s"$fn.call(${(thisArg :: args).mkString(", ")});")
550+
access(path).map(fn =>
551+
s"$fn.call(${(thisArg :: args).mkString(", ")});",
552+
)
491553
}
492554
}
493555

0 commit comments

Comments
 (0)