Merge branch 'main' into post-release-prep/codeql-cli-2.8.0

java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll

@@ -78,10 +78,12 @@ private import FlowSummary
 private module Frameworks {
   private import internal.ContainerFlow
   private import semmle.code.java.frameworks.android.Android
+  private import semmle.code.java.frameworks.android.ContentProviders
   private import semmle.code.java.frameworks.android.Intent
   private import semmle.code.java.frameworks.android.Notifications
   private import semmle.code.java.frameworks.android.Slice
   private import semmle.code.java.frameworks.android.SQLite
+  private import semmle.code.java.frameworks.android.Widget
   private import semmle.code.java.frameworks.android.XssSinks
   private import semmle.code.java.frameworks.ApacheHttp
   private import semmle.code.java.frameworks.apache.Collections

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplCommon.qll

@@ -1290,7 +1290,7 @@ class DataFlowCallOption extends TDataFlowCallOption {
   }
 }
 
-/** Content tagged with the type of a containing object. */
+/** A `Content` tagged with the type of a containing object. */
 class TypedContent extends MkTypedContent {
   private Content c;
   private DataFlowType t;

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowUtil.qll

@@ -74,12 +74,14 @@ private module ThisFlow {
  * Holds if data can flow from `node1` to `node2` in zero or more
  * local (intra-procedural) steps.
  */
+pragma[inline]
 predicate localFlow(Node node1, Node node2) { localFlowStep*(node1, node2) }
 
 /**
  * Holds if data can flow from `e1` to `e2` in zero or more
  * local (intra-procedural) steps.
  */
+pragma[inline]
 predicate localExprFlow(Expr e1, Expr e2) { localFlow(exprNode(e1), exprNode(e2)) }
 
 /**

java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll

@@ -90,7 +90,9 @@ module Public {
     predicate contains(SummaryComponent c) { c = this.drop(_).head() }
 
     /** Gets the bottom element of this stack. */
-    SummaryComponent bottom() { result = this.drop(this.length() - 1).head() }
+    SummaryComponent bottom() {
+      this = TSingletonSummaryComponentStack(result) or result = this.tail().bottom()
+    }
 
     /** Gets a textual representation of this stack. */
     string toString() {

java/ql/lib/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll

@@ -21,12 +21,14 @@ private import semmle.code.java.frameworks.JaxWS
  * Holds if taint can flow from `src` to `sink` in zero or more
  * local (intra-procedural) steps.
  */
+pragma[inline]
 predicate localTaint(DataFlow::Node src, DataFlow::Node sink) { localTaintStep*(src, sink) }
 
 /**
  * Holds if taint can flow from `src` to `sink` in zero or more
  * local (intra-procedural) steps.
  */
+pragma[inline]
 predicate localExprTaint(Expr src, Expr sink) {
   localTaint(DataFlow::exprNode(src), DataFlow::exprNode(sink))
 }

java/ql/lib/semmle/code/java/frameworks/Thrift.qll

@@ -25,6 +25,7 @@ class ThriftIface extends Interface {
     this.getFile() instanceof ThriftGeneratedFile
   }
 
+  /** Gets an implementation of a method of this interface. */
   Method getAnImplementingMethod() {
     result.getDeclaringType().(Class).getASupertype+() = this and
     result.overrides+(this.getAMethod()) and

java/ql/lib/semmle/code/java/frameworks/android/Android.qll

@@ -177,42 +177,6 @@ private class UriModel extends SummaryModelCsv {
   }
 }
 
-private class ContentProviderSourceModels extends SourceModelCsv {
-  override predicate row(string row) {
-    row =
-      [
-        // ContentInterface models are here for backwards compatibility (it was removed in API 28)
-        "android.content;ContentInterface;true;call;(String,String,String,Bundle);;Parameter[0..3];contentprovider",
-        "android.content;ContentProvider;true;call;(String,String,String,Bundle);;Parameter[0..3];contentprovider",
-        "android.content;ContentProvider;true;call;(String,String,Bundle);;Parameter[0..2];contentprovider",
-        "android.content;ContentProvider;true;delete;(Uri,String,String[]);;Parameter[0..2];contentprovider",
-        "android.content;ContentInterface;true;delete;(Uri,Bundle);;Parameter[0..1];contentprovider",
-        "android.content;ContentProvider;true;delete;(Uri,Bundle);;Parameter[0..1];contentprovider",
-        "android.content;ContentInterface;true;getType;(Uri);;Parameter[0];contentprovider",
-        "android.content;ContentProvider;true;getType;(Uri);;Parameter[0];contentprovider",
-        "android.content;ContentInterface;true;insert;(Uri,ContentValues,Bundle);;Parameter[0];contentprovider",
-        "android.content;ContentProvider;true;insert;(Uri,ContentValues,Bundle);;Parameter[0..2];contentprovider",
-        "android.content;ContentProvider;true;insert;(Uri,ContentValues);;Parameter[0..1];contentprovider",
-        "android.content;ContentInterface;true;openAssetFile;(Uri,String,CancellationSignal);;Parameter[0];contentprovider",
-        "android.content;ContentProvider;true;openAssetFile;(Uri,String,CancellationSignal);;Parameter[0];contentprovider",
-        "android.content;ContentProvider;true;openAssetFile;(Uri,String);;Parameter[0];contentprovider",
-        "android.content;ContentInterface;true;openTypedAssetFile;(Uri,String,Bundle,CancellationSignal);;Parameter[0..2];contentprovider",
-        "android.content;ContentProvider;true;openTypedAssetFile;(Uri,String,Bundle,CancellationSignal);;Parameter[0..2];contentprovider",
-        "android.content;ContentProvider;true;openTypedAssetFile;(Uri,String,Bundle);;Parameter[0..2];contentprovider",
-        "android.content;ContentInterface;true;openFile;(Uri,String,CancellationSignal);;Parameter[0];contentprovider",
-        "android.content;ContentProvider;true;openFile;(Uri,String,CancellationSignal);;Parameter[0];contentprovider",
-        "android.content;ContentProvider;true;openFile;(Uri,String);;Parameter[0];contentprovider",
-        "android.content;ContentInterface;true;query;(Uri,String[],Bundle,CancellationSignal);;Parameter[0..2];contentprovider",
-        "android.content;ContentProvider;true;query;(Uri,String[],Bundle,CancellationSignal);;Parameter[0..2];contentprovider",
-        "android.content;ContentProvider;true;query;(Uri,String[],String,String[],String);;Parameter[0..4];contentprovider",
-        "android.content;ContentProvider;true;query;(Uri,String[],String,String[],String,CancellationSignal);;Parameter[0..4];contentprovider",
-        "android.content;ContentInterface;true;update;(Uri,ContentValues,Bundle);;Parameter[0..2];contentprovider",
-        "android.content;ContentProvider;true;update;(Uri,ContentValues,Bundle);;Parameter[0..2];contentprovider",
-        "android.content;ContentProvider;true;update;(Uri,ContentValues,String,String[]);;Parameter[0..3];contentprovider"
-      ]
-  }
-}
-
 /** Interface for classes whose instances can be written to and restored from a Parcel. */
 class TypeParcelable extends Interface {
   TypeParcelable() { this.hasQualifiedName("android.os", "Parcelable") }

java/ql/lib/semmle/code/java/frameworks/android/ContentProviders.qll

@@ -0,0 +1,59 @@
+/**
+ * Provides classes and predicates for working with Content Providers.
+ */
+
+import java
+import semmle.code.java.dataflow.ExternalFlow
+
+/** The class `android.content.ContentValues`. */
+class ContentValues extends Class {
+  ContentValues() { this.hasQualifiedName("android.content", "ContentValues") }
+}
+
+private class ContentProviderSourceModels extends SourceModelCsv {
+  override predicate row(string row) {
+    row =
+      [
+        // ContentInterface models are here for backwards compatibility (it was removed in API 28)
+        "android.content;ContentInterface;true;call;(String,String,String,Bundle);;Parameter[0..3];contentprovider",
+        "android.content;ContentProvider;true;call;(String,String,String,Bundle);;Parameter[0..3];contentprovider",
+        "android.content;ContentProvider;true;call;(String,String,Bundle);;Parameter[0..2];contentprovider",
+        "android.content;ContentProvider;true;delete;(Uri,String,String[]);;Parameter[0..2];contentprovider",
+        "android.content;ContentInterface;true;delete;(Uri,Bundle);;Parameter[0..1];contentprovider",
+        "android.content;ContentProvider;true;delete;(Uri,Bundle);;Parameter[0..1];contentprovider",
+        "android.content;ContentInterface;true;getType;(Uri);;Parameter[0];contentprovider",
+        "android.content;ContentProvider;true;getType;(Uri);;Parameter[0];contentprovider",
+        "android.content;ContentInterface;true;insert;(Uri,ContentValues,Bundle);;Parameter[0];contentprovider",
+        "android.content;ContentProvider;true;insert;(Uri,ContentValues,Bundle);;Parameter[0..2];contentprovider",
+        "android.content;ContentProvider;true;insert;(Uri,ContentValues);;Parameter[0..1];contentprovider",
+        "android.content;ContentInterface;true;openAssetFile;(Uri,String,CancellationSignal);;Parameter[0];contentprovider",
+        "android.content;ContentProvider;true;openAssetFile;(Uri,String,CancellationSignal);;Parameter[0];contentprovider",
+        "android.content;ContentProvider;true;openAssetFile;(Uri,String);;Parameter[0];contentprovider",
+        "android.content;ContentInterface;true;openTypedAssetFile;(Uri,String,Bundle,CancellationSignal);;Parameter[0..2];contentprovider",
+        "android.content;ContentProvider;true;openTypedAssetFile;(Uri,String,Bundle,CancellationSignal);;Parameter[0..2];contentprovider",
+        "android.content;ContentProvider;true;openTypedAssetFile;(Uri,String,Bundle);;Parameter[0..2];contentprovider",
+        "android.content;ContentInterface;true;openFile;(Uri,String,CancellationSignal);;Parameter[0];contentprovider",
+        "android.content;ContentProvider;true;openFile;(Uri,String,CancellationSignal);;Parameter[0];contentprovider",
+        "android.content;ContentProvider;true;openFile;(Uri,String);;Parameter[0];contentprovider",
+        "android.content;ContentInterface;true;query;(Uri,String[],Bundle,CancellationSignal);;Parameter[0..2];contentprovider",
+        "android.content;ContentProvider;true;query;(Uri,String[],Bundle,CancellationSignal);;Parameter[0..2];contentprovider",
+        "android.content;ContentProvider;true;query;(Uri,String[],String,String[],String);;Parameter[0..4];contentprovider",
+        "android.content;ContentProvider;true;query;(Uri,String[],String,String[],String,CancellationSignal);;Parameter[0..4];contentprovider",
+        "android.content;ContentInterface;true;update;(Uri,ContentValues,Bundle);;Parameter[0..2];contentprovider",
+        "android.content;ContentProvider;true;update;(Uri,ContentValues,Bundle);;Parameter[0..2];contentprovider",
+        "android.content;ContentProvider;true;update;(Uri,ContentValues,String,String[]);;Parameter[0..3];contentprovider"
+      ]
+  }
+}
+
+private class SummaryModels extends SummaryModelCsv {
+  override predicate row(string row) {
+    row =
+      [
+        "android.content;ContentValues;false;put;;;Argument[0];MapKey of Argument[-1];value",
+        "android.content;ContentValues;false;put;;;Argument[1];MapValue of Argument[-1];value",
+        "android.content;ContentValues;false;putAll;;;MapKey of Argument[0];MapKey of Argument[-1];value",
+        "android.content;ContentValues;false;putAll;;;MapValue of Argument[0];MapValue of Argument[-1];value"
+      ]
+  }
+}

java/ql/lib/semmle/code/java/frameworks/android/SQLite.qll

@@ -1,3 +1,5 @@
+/** Provides classes and predicates for working with SQLite databases. */
+
 import java
 import Android
 import semmle.code.java.dataflow.FlowSteps
@@ -24,6 +26,20 @@ class TypeDatabaseUtils extends Class {
   TypeDatabaseUtils() { hasQualifiedName("android.database", "DatabaseUtils") }
 }
 
+/**
+ * The class `android.database.sqlite.SQLiteOpenHelper`.
+ */
+class TypeSQLiteOpenHelper extends Class {
+  TypeSQLiteOpenHelper() { this.hasQualifiedName("android.database.sqlite", "SQLiteOpenHelper") }
+}
+
+/**
+ * The class `android.database.sqlite.SQLiteStatement`.
+ */
+class TypeSQLiteStatement extends Class {
+  TypeSQLiteStatement() { this.hasQualifiedName("android.database.sqlite", "SQLiteStatement") }
+}
+
 private class SQLiteSinkCsv extends SinkModelCsv {
   override predicate row(string row) {
     row =

java/ql/lib/semmle/code/java/frameworks/android/Widget.qll

@@ -0,0 +1,23 @@
+/** Provides classes and predicates for working with Android widgets. */
+
+import java
+import semmle.code.java.dataflow.ExternalFlow
+import semmle.code.java.dataflow.FlowSources
+
+private class AndroidWidgetSourceModels extends SourceModelCsv {
+  override predicate row(string row) {
+    row = "android.widget;EditText;true;getText;;;ReturnValue;android-widget"
+  }
+}
+
+private class DefaultAndroidWidgetSources extends RemoteFlowSource {
+  DefaultAndroidWidgetSources() { sourceNode(this, "android-widget") }
+
+  override string getSourceType() { result = "Android widget source" }
+}
+
+private class AndroidWidgetSummaryModels extends SummaryModelCsv {
+  override predicate row(string row) {
+    row = "android.widget;EditText;true;getText;;;Argument[-1];ReturnValue;taint"
+  }
+}

java/ql/lib/semmle/code/java/frameworks/struts/StrutsAnnotations.qll

@@ -15,6 +15,7 @@ class StrutsAnnotation extends Annotation {
 class StrutsActionAnnotation extends StrutsAnnotation {
   StrutsActionAnnotation() { this.getType().hasName("Action") }
 
+  /** Gets a callable annotated with this annotation. */
   Callable getActionCallable() {
     result = this.getAnnotatedElement()
     or

java/ql/lib/semmle/code/java/security/CleartextStorageAndroidDatabaseQuery.qll

@@ -0,0 +1,131 @@
+/** Provides classes and predicates to reason about cleartext storage in Android databases. */
+
+import java
+import semmle.code.java.dataflow.DataFlow
+import semmle.code.java.frameworks.android.ContentProviders
+import semmle.code.java.frameworks.android.Intent
+import semmle.code.java.frameworks.android.SQLite
+import semmle.code.java.security.CleartextStorageQuery
+
+private class LocalDatabaseCleartextStorageSink extends CleartextStorageSink {
+  LocalDatabaseCleartextStorageSink() { localDatabaseInput(_, this.asExpr()) }
+}
+
+private class LocalDatabaseCleartextStorageStep extends CleartextStorageAdditionalTaintStep {
+  override predicate step(DataFlow::Node n1, DataFlow::Node n2) {
+    // EditText.getText() return type is parsed as `Object`, so we need to
+    // add a taint step for `Object.toString` to model `editText.getText().toString()`
+    exists(MethodAccess ma, Method m |
+      ma.getMethod() = m and
+      m.getDeclaringType() instanceof TypeObject and
+      m.hasName("toString")
+    |
+      n1.asExpr() = ma.getQualifier() and n2.asExpr() = ma
+    )
+  }
+}
+
+/** The creation of an object that can be used to store data in a local database. */
+class LocalDatabaseOpenMethodAccess extends Storable, Call {
+  LocalDatabaseOpenMethodAccess() {
+    exists(Method m | this.(MethodAccess).getMethod() = m |
+      m.getDeclaringType().getASupertype*() instanceof TypeSQLiteOpenHelper and
+      m.hasName("getWritableDatabase")
+      or
+      m.getDeclaringType() instanceof TypeSQLiteDatabase and
+      m.hasName(["create", "openDatabase", "openOrCreateDatabase", "compileStatement"])
+      or
+      m.getDeclaringType().getASupertype*() instanceof TypeContext and
+      m.hasName("openOrCreateDatabase")
+    )
+    or
+    this.(ClassInstanceExpr).getConstructedType() instanceof ContentValues
+  }
+
+  override Expr getAnInput() {
+    exists(LocalDatabaseFlowConfig config, DataFlow::Node database |
+      localDatabaseInput(database, result) and
+      config.hasFlow(DataFlow::exprNode(this), database)
+    )
+  }
+
+  override Expr getAStore() {
+    exists(LocalDatabaseFlowConfig config, DataFlow::Node database |
+      localDatabaseStore(database, result) and
+      config.hasFlow(DataFlow::exprNode(this), database)
+    )
+  }
+}
+
+/** A method that is both a database input and a database store. */
+private class LocalDatabaseInputStoreMethod extends Method {
+  LocalDatabaseInputStoreMethod() {
+    this.getDeclaringType() instanceof TypeSQLiteDatabase and
+    this.getName().matches("exec%SQL")
+  }
+}
+
+/**
+ * Holds if `input` is a value being prepared for being stored into the SQLite dataabse `database`.
+ * This can be done using prepared statements, using the class `ContentValues`, or directly
+ * appending `input` to a SQL query.
+ */
+private predicate localDatabaseInput(DataFlow::Node database, Argument input) {
+  exists(Method m | input.getCall().getCallee() = m |
+    m instanceof LocalDatabaseInputStoreMethod and
+    database.asExpr() = input.getCall().getQualifier()
+    or
+    m.getDeclaringType() instanceof TypeSQLiteDatabase and
+    m.hasName("compileStatement") and
+    database.asExpr() = input.getCall()
+    or
+    m.getDeclaringType() instanceof ContentValues and
+    m.hasName("put") and
+    input.getPosition() = 1 and
+    database.asExpr() = input.getCall().getQualifier()
+  )
+}
+
+/**
+ * Holds if `store` is a method call for storing a previously appended input value,
+ * either through the use of prepared statements, via the `ContentValues` class, or
+ * directly executing a raw SQL query.
+ */
+private predicate localDatabaseStore(DataFlow::Node database, MethodAccess store) {
+  exists(Method m | store.getMethod() = m |
+    m instanceof LocalDatabaseInputStoreMethod and
+    database.asExpr() = store.getQualifier()
+    or
+    m.getDeclaringType() instanceof TypeSQLiteDatabase and
+    m.getName().matches(["insert%", "replace%", "update%"]) and
+    database.asExpr() = store.getAnArgument() and
+    database.getType() instanceof ContentValues
+    or
+    m.getDeclaringType() instanceof TypeSQLiteStatement and
+    m.hasName(["executeInsert", "executeUpdateDelete"]) and
+    database.asExpr() = store.getQualifier()
+  )
+}
+
+private class LocalDatabaseFlowConfig extends DataFlow::Configuration {
+  LocalDatabaseFlowConfig() { this = "LocalDatabaseFlowConfig" }
+
+  override predicate isSource(DataFlow::Node source) {
+    source.asExpr() instanceof LocalDatabaseOpenMethodAccess
+  }
+
+  override predicate isSink(DataFlow::Node sink) {
+    localDatabaseInput(sink, _) or
+    localDatabaseStore(sink, _)
+  }
+
+  override predicate isAdditionalFlowStep(DataFlow::Node n1, DataFlow::Node n2) {
+    // Adds a step for tracking databases through field flow, that is, a database is opened and
+    // assigned to a field, and then an input or store method is called on that field elsewhere.
+    exists(Field f |
+      f.getType() instanceof TypeSQLiteDatabase and
+      f.getAnAssignedValue() = n1.asExpr() and
+      f = n2.asExpr().(FieldRead).getField()
+    )
+  }
+}

java/ql/lib/semmle/code/java/security/SensitiveActions.qll

@@ -14,7 +14,11 @@
 import java
 
 private string suspicious() {
-  result = ["%password%", "%passwd%", "%account%", "%accnt%", "%trusted%"]
+  result =
+    [
+      "%password%", "%passwd%", "pwd", "%account%", "%accnt%", "%trusted%", "%refresh%token%",
+      "%secret%token"
+    ]
 }
 
 private string nonSuspicious() {

java/ql/lib/tutorial.qll

@@ -6,122 +6,22 @@
  */
 class Person extends string {
   Person() {
-    this = "Ronil" or
-    this = "Dina" or
-    this = "Ravi" or
-    this = "Bruce" or
-    this = "Jo" or
-    this = "Aida" or
-    this = "Esme" or
-    this = "Charlie" or
-    this = "Fred" or
-    this = "Meera" or
-    this = "Maya" or
-    this = "Chad" or
-    this = "Tiana" or
-    this = "Laura" or
-    this = "George" or
-    this = "Will" or
-    this = "Mary" or
-    this = "Almira" or
-    this = "Susannah" or
-    this = "Rhoda" or
-    this = "Cynthia" or
-    this = "Eunice" or
-    this = "Olive" or
-    this = "Virginia" or
-    this = "Angeline" or
-    this = "Helen" or
-    this = "Cornelia" or
-    this = "Harriet" or
-    this = "Mahala" or
-    this = "Abby" or
-    this = "Margaret" or
-    this = "Deb" or
-    this = "Minerva" or
-    this = "Severus" or
-    this = "Lavina" or
-    this = "Adeline" or
-    this = "Cath" or
-    this = "Elisa" or
-    this = "Lucretia" or
-    this = "Anne" or
-    this = "Eleanor" or
-    this = "Joanna" or
-    this = "Adam" or
-    this = "Agnes" or
-    this = "Rosanna" or
-    this = "Clara" or
-    this = "Melissa" or
-    this = "Amy" or
-    this = "Isabel" or
-    this = "Jemima" or
-    this = "Cordelia" or
-    this = "Melinda" or
-    this = "Delila" or
-    this = "Jeremiah" or
-    this = "Elijah" or
-    this = "Hester" or
-    this = "Walter" or
-    this = "Oliver" or
-    this = "Hugh" or
-    this = "Aaron" or
-    this = "Reuben" or
-    this = "Eli" or
-    this = "Amos" or
-    this = "Augustus" or
-    this = "Theodore" or
-    this = "Ira" or
-    this = "Timothy" or
-    this = "Cyrus" or
-    this = "Horace" or
-    this = "Simon" or
-    this = "Asa" or
-    this = "Frank" or
-    this = "Nelson" or
-    this = "Leonard" or
-    this = "Harrison" or
-    this = "Anthony" or
-    this = "Louis" or
-    this = "Milton" or
-    this = "Noah" or
-    this = "Cornelius" or
-    this = "Abdul" or
-    this = "Warren" or
-    this = "Harvey" or
-    this = "Dennis" or
-    this = "Wesley" or
-    this = "Sylvester" or
-    this = "Gilbert" or
-    this = "Sullivan" or
-    this = "Edmund" or
-    this = "Wilson" or
-    this = "Perry" or
-    this = "Matthew" or
-    this = "Simba" or
-    this = "Nala" or
-    this = "Rafiki" or
-    this = "Shenzi" or
-    this = "Ernest" or
-    this = "Gertrude" or
-    this = "Oscar" or
-    this = "Lilian" or
-    this = "Raymond" or
-    this = "Elgar" or
-    this = "Elmer" or
-    this = "Herbert" or
-    this = "Maude" or
-    this = "Mae" or
-    this = "Otto" or
-    this = "Edwin" or
-    this = "Ophelia" or
-    this = "Parsley" or
-    this = "Sage" or
-    this = "Rosemary" or
-    this = "Thyme" or
-    this = "Garfunkel" or
-    this = "King Basil" or
-    this = "Stephen"
+    this =
+      [
+        "Ronil", "Dina", "Ravi", "Bruce", "Jo", "Aida", "Esme", "Charlie", "Fred", "Meera", "Maya",
+        "Chad", "Tiana", "Laura", "George", "Will", "Mary", "Almira", "Susannah", "Rhoda",
+        "Cynthia", "Eunice", "Olive", "Virginia", "Angeline", "Helen", "Cornelia", "Harriet",
+        "Mahala", "Abby", "Margaret", "Deb", "Minerva", "Severus", "Lavina", "Adeline", "Cath",
+        "Elisa", "Lucretia", "Anne", "Eleanor", "Joanna", "Adam", "Agnes", "Rosanna", "Clara",
+        "Melissa", "Amy", "Isabel", "Jemima", "Cordelia", "Melinda", "Delila", "Jeremiah", "Elijah",
+        "Hester", "Walter", "Oliver", "Hugh", "Aaron", "Reuben", "Eli", "Amos", "Augustus",
+        "Theodore", "Ira", "Timothy", "Cyrus", "Horace", "Simon", "Asa", "Frank", "Nelson",
+        "Leonard", "Harrison", "Anthony", "Louis", "Milton", "Noah", "Cornelius", "Abdul", "Warren",
+        "Harvey", "Dennis", "Wesley", "Sylvester", "Gilbert", "Sullivan", "Edmund", "Wilson",
+        "Perry", "Matthew", "Simba", "Nala", "Rafiki", "Shenzi", "Ernest", "Gertrude", "Oscar",
+        "Lilian", "Raymond", "Elgar", "Elmer", "Herbert", "Maude", "Mae", "Otto", "Edwin",
+        "Ophelia", "Parsley", "Sage", "Rosemary", "Thyme", "Garfunkel", "King Basil", "Stephen"
+      ]
   }
 
   /** Gets the hair color of the person. If the person is bald, there is no result. */
@@ -936,25 +836,12 @@ class Person extends string {
 
   /** Holds if the person is deceased. */
   predicate isDeceased() {
-    this = "Ernest" or
-    this = "Gertrude" or
-    this = "Oscar" or
-    this = "Lilian" or
-    this = "Edwin" or
-    this = "Raymond" or
-    this = "Elgar" or
-    this = "Elmer" or
-    this = "Herbert" or
-    this = "Maude" or
-    this = "Mae" or
-    this = "Otto" or
-    this = "Ophelia" or
-    this = "Parsley" or
-    this = "Sage" or
-    this = "Rosemary" or
-    this = "Thyme" or
-    this = "Garfunkel" or
-    this = "King Basil"
+    this =
+      [
+        "Ernest", "Gertrude", "Oscar", "Lilian", "Edwin", "Raymond", "Elgar", "Elmer", "Herbert",
+        "Maude", "Mae", "Otto", "Ophelia", "Parsley", "Sage", "Rosemary", "Thyme", "Garfunkel",
+        "King Basil"
+      ]
   }
 
   /** Gets a parent of the person (alive or deceased). */
@@ -1195,12 +1082,7 @@ class Person extends string {
   }
 
   /** Holds if the person is allowed in the region. Initially, all villagers are allowed in every region. */
-  predicate isAllowedIn(string region) {
-    region = "north" or
-    region = "south" or
-    region = "east" or
-    region = "west"
-  }
+  predicate isAllowedIn(string region) { region = ["north", "south", "east", "west"] }
 }
 
 /** Returns a parent of the person. */