mirror of
https://github.com/github/codeql.git
synced 2026-04-27 01:35:13 +02:00
Merge branch 'main' into fix-join-in-isUse
This commit is contained in:
@@ -0,0 +1,183 @@
|
||||
/** Definitions for the missing function level access control query */
|
||||
|
||||
import csharp
|
||||
import semmle.code.csharp.frameworks.microsoft.AspNetCore
|
||||
import semmle.code.csharp.frameworks.system.web.UI
|
||||
import semmle.code.asp.WebConfig
|
||||
|
||||
/** A method representing an action for a web endpoint. */
|
||||
abstract class ActionMethod extends Method {
|
||||
/**
|
||||
* Gets a string that can indicate what this method does to determine if it should have an auth check;
|
||||
* such as its method name, class name, or file path.
|
||||
*/
|
||||
string getADescription() {
|
||||
result =
|
||||
[
|
||||
this.getName(), this.getDeclaringType().getBaseClass*().getName(),
|
||||
this.getDeclaringType().getFile().getRelativePath()
|
||||
]
|
||||
}
|
||||
|
||||
/** Holds if this method may need an authorization check. */
|
||||
predicate needsAuth() {
|
||||
this.getADescription()
|
||||
.regexpReplaceAll("([a-z])([A-Z])", "$1_$2")
|
||||
// separate camelCase words
|
||||
.toLowerCase()
|
||||
.regexpMatch(".*(edit|delete|modify|admin|superuser).*")
|
||||
}
|
||||
|
||||
/** Gets a callable for which if it contains an auth check, this method should be considered authenticated. */
|
||||
Callable getAnAuthorizingCallable() { result = this }
|
||||
|
||||
/**
|
||||
* Gets a possible url route that could refer to this action,
|
||||
* which would be covered by `<location>` configurations specifying a prefix of it.
|
||||
*/
|
||||
string getARoute() { result = this.getDeclaringType().getFile().getRelativePath() }
|
||||
}
|
||||
|
||||
/** An action method in the MVC framework. */
|
||||
private class MvcActionMethod extends ActionMethod {
|
||||
MvcActionMethod() { this = any(MicrosoftAspNetCoreMvcController c).getAnActionMethod() }
|
||||
}
|
||||
|
||||
/** An action method on a subclass of `System.Web.UI.Page`. */
|
||||
private class WebFormActionMethod extends ActionMethod {
|
||||
WebFormActionMethod() {
|
||||
this.getDeclaringType().getBaseClass+() instanceof SystemWebUIPageClass and
|
||||
this.getAParameter().getType().getName().matches("%EventArgs")
|
||||
}
|
||||
|
||||
override Callable getAnAuthorizingCallable() {
|
||||
result = super.getAnAuthorizingCallable()
|
||||
or
|
||||
result.getDeclaringType() = this.getDeclaringType() and
|
||||
result.getName() = "Page_Load"
|
||||
}
|
||||
|
||||
override string getARoute() {
|
||||
exists(string physicalRoute | physicalRoute = super.getARoute() |
|
||||
result = physicalRoute
|
||||
or
|
||||
exists(string absolutePhysical |
|
||||
virtualRouteMapping(result, absolutePhysical) and
|
||||
physicalRouteMatches(absolutePhysical, physicalRoute)
|
||||
)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `virtualRoute` is a URL path
|
||||
* that can map to the corresponding `physicalRoute` filepath
|
||||
* through a call to `MapPageRoute`
|
||||
*/
|
||||
private predicate virtualRouteMapping(string virtualRoute, string physicalRoute) {
|
||||
exists(MethodCall mapPageRouteCall, StringLiteral virtualLit, StringLiteral physicalLit |
|
||||
mapPageRouteCall
|
||||
.getTarget()
|
||||
.hasQualifiedName("System.Web.Routing", "RouteCollection", "MapPageRoute") and
|
||||
virtualLit = mapPageRouteCall.getArgument(1) and
|
||||
physicalLit = mapPageRouteCall.getArgument(2) and
|
||||
virtualLit.getValue() = virtualRoute and
|
||||
physicalLit.getValue() = physicalRoute
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if the filepath `route` can refer to `actual` after expanding a '~". */
|
||||
bindingset[route, actual]
|
||||
private predicate physicalRouteMatches(string route, string actual) {
|
||||
route = actual
|
||||
or
|
||||
route.charAt(0) = "~" and
|
||||
exists(string dir | actual = dir + route.suffix(1) + ".cs")
|
||||
}
|
||||
|
||||
/** An expression that indicates that some authorization/authentication check is being performed. */
|
||||
class AuthExpr extends Expr {
|
||||
AuthExpr() {
|
||||
this.(MethodCall)
|
||||
.getTarget()
|
||||
.hasQualifiedName("System.Security.Principal", "IPrincipal", "IsInRole")
|
||||
or
|
||||
this.(PropertyAccess)
|
||||
.getTarget()
|
||||
.hasQualifiedName("System.Security.Principal", "IIdentity", ["IsAuthenticated", "Name"])
|
||||
or
|
||||
this.(MethodCall).getTarget().getName().toLowerCase().matches("%auth%")
|
||||
or
|
||||
this.(PropertyAccess).getTarget().getName().toLowerCase().matches("%auth%")
|
||||
}
|
||||
}
|
||||
|
||||
/** Holds if `m` is a method that should have an auth check, and does indeed have one. */
|
||||
predicate hasAuthViaCode(ActionMethod m) {
|
||||
m.needsAuth() and
|
||||
exists(Callable caller, AuthExpr auth |
|
||||
m.getAnAuthorizingCallable().calls*(caller) and
|
||||
auth.getEnclosingCallable() = caller
|
||||
)
|
||||
}
|
||||
|
||||
/** An `<authorization>` XML element. */
|
||||
class AuthorizationXmlElement extends XmlElement {
|
||||
AuthorizationXmlElement() {
|
||||
this.getParent() instanceof SystemWebXmlElement and
|
||||
this.getName().toLowerCase() = "authorization"
|
||||
}
|
||||
|
||||
/** Holds if this element has a `<deny>` element to deny access to a resource. */
|
||||
predicate hasDenyElement() { this.getAChild().getName().toLowerCase() = "deny" }
|
||||
|
||||
/** Gets the physical filepath of this element. */
|
||||
string getPhysicalPath() { result = this.getFile().getParentContainer().getRelativePath() }
|
||||
|
||||
/** Gets the path specified by a `<location>` tag containing this element, if any. */
|
||||
string getLocationTagPath() {
|
||||
exists(LocationXmlElement loc, XmlAttribute path |
|
||||
loc = this.getParent().(SystemWebXmlElement).getParent() and
|
||||
path = loc.getAnAttribute() and
|
||||
path.getName().toLowerCase() = "path" and
|
||||
result = path.getValue()
|
||||
)
|
||||
}
|
||||
|
||||
/** Gets a route prefix that this configuration can refer to. */
|
||||
string getARoute() {
|
||||
result = this.getLocationTagPath()
|
||||
or
|
||||
result = this.getPhysicalPath() + "/" + this.getLocationTagPath()
|
||||
or
|
||||
not exists(this.getLocationTagPath()) and
|
||||
result = this.getPhysicalPath()
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the given action has an xml `authorization` tag that refers to it.
|
||||
*/
|
||||
predicate hasAuthViaXml(ActionMethod m) {
|
||||
exists(AuthorizationXmlElement el, string rest |
|
||||
el.hasDenyElement() and
|
||||
m.getARoute() = el.getARoute() + rest
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if the given action has an attribute that indications authorization. */
|
||||
predicate hasAuthViaAttribute(ActionMethod m) {
|
||||
exists(Attribute attr | attr.getType().getName().toLowerCase().matches("%auth%") |
|
||||
attr = m.getAnAttribute() or
|
||||
attr = m.getDeclaringType().getABaseType*().getAnAttribute()
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `m` is a method that should have an auth check, but is missing it. */
|
||||
predicate missingAuth(ActionMethod m) {
|
||||
m.needsAuth() and
|
||||
not hasAuthViaCode(m) and
|
||||
not hasAuthViaXml(m) and
|
||||
not hasAuthViaAttribute(m) and
|
||||
exists(m.getBody().getAChildStmt()) // exclude empty methods
|
||||
}
|
||||
13
csharp/ql/src/Security Features/CWE-285/MVC.cs
Normal file
13
csharp/ql/src/Security Features/CWE-285/MVC.cs
Normal file
@@ -0,0 +1,13 @@
|
||||
public class ProfileController : Controller {
|
||||
|
||||
// BAD: No authorization is used.
|
||||
public ActionResult Edit(int id) {
|
||||
...
|
||||
}
|
||||
|
||||
// GOOD: The `Authorize` attribute is used.
|
||||
[Authorize]
|
||||
public ActionResult Delete(int id) {
|
||||
...
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,54 @@
|
||||
<!DOCTYPE qhelp PUBLIC
|
||||
"-//Semmle//qhelp//EN"
|
||||
"qhelp.dtd">
|
||||
<qhelp>
|
||||
|
||||
<overview>
|
||||
<p>
|
||||
Sensitive actions, such as editing or deleting content, or accessing admin pages, should have authorization checks
|
||||
to ensure that they cannot be used by malicious actors.
|
||||
</p>
|
||||
|
||||
</overview>
|
||||
<recommendation>
|
||||
|
||||
<p>
|
||||
Ensure that proper authorization checks are made for sensitive actions.
|
||||
For WebForms applications, the <code>authorization</code> tag in <code>Web.config</code> XML files
|
||||
can be used to implement access control. The <code>System.Web.UI.Page.User</code> property can also be
|
||||
used to verify a user's role.
|
||||
For MVC applications, the <code>Authorize</code> attribute can be used to require authorization on specific
|
||||
action methods.
|
||||
</p>
|
||||
|
||||
</recommendation>
|
||||
<example>
|
||||
|
||||
<p>
|
||||
In the following WebForms example, the case marked BAD has no authorization checks whereas the
|
||||
case marked GOOD uses <code>User.IsInRole</code> to check for the user's role.
|
||||
</p>
|
||||
|
||||
<sample src="WebForms.cs" />
|
||||
|
||||
<p>
|
||||
The following <code>Web.config</code> file uses the <code>authorization</code> tag to deny access to anonymous users,
|
||||
in a <code>location</code> tag to have that configuration apply to a specific path.
|
||||
</p>
|
||||
|
||||
<sample src="Web.config" />
|
||||
|
||||
<p>
|
||||
In the following MVC example, the case marked BAD has no authorization
|
||||
checks whereas the case marked GOOD uses the <code>Authorize</code> attribute.
|
||||
</p>
|
||||
|
||||
<sample src="MVC.cs" />
|
||||
|
||||
</example>
|
||||
<references>
|
||||
<li><code>Page.User</code> Property - <a href="https://learn.microsoft.com/en-us/dotnet/api/system.web.ui.page.user?view=netframework-4.8.1#system-web-ui-page-user">Microsoft Learn</a>.</li>
|
||||
<li>Control authorization permissions in an ASP.NET application - <a href="https://learn.microsoft.com/en-us/troubleshoot/developer/webapps/aspnet/www-authentication-authorization/authorization-permissions">Microsoft Learn</a>.</li>
|
||||
<li>Simple authorization in ASP.NET Core - <a href="https://learn.microsoft.com/en-us/aspnet/core/security/authorization/simple?view=aspnetcore-7.0">Microsoft Learn</a>.</li>
|
||||
</references>
|
||||
</qhelp>
|
||||
@@ -0,0 +1,20 @@
|
||||
/**
|
||||
* @name Missing function level access control
|
||||
* @description Sensitive actions should have authorization checks to prevent them from being used by malicious actors.
|
||||
* @kind problem
|
||||
* @problem.severity warning
|
||||
* @security-severity 7.5
|
||||
* @precision medium
|
||||
* @id cs/web/missing-function-level-access-control
|
||||
* @tags security
|
||||
* external/cwe/cwe-285
|
||||
* external/cwe/cwe-284
|
||||
* external/cwe/cwe-862
|
||||
*/
|
||||
|
||||
import csharp
|
||||
import semmle.code.csharp.security.auth.MissingFunctionLevelAccessControlQuery
|
||||
|
||||
from Method m
|
||||
where missingAuth(m)
|
||||
select m, "This action is missing an authorization check."
|
||||
11
csharp/ql/src/Security Features/CWE-285/Web.config
Normal file
11
csharp/ql/src/Security Features/CWE-285/Web.config
Normal file
@@ -0,0 +1,11 @@
|
||||
<?xml version="1.0"?>
|
||||
|
||||
<configuration xmlns:xdt="http://schemas.microsoft.com/XML-Document-Transform">
|
||||
<location path="User/Profile">
|
||||
<system.web>
|
||||
<authorization>
|
||||
<deny users="?" />
|
||||
</authorization>
|
||||
</system.web>
|
||||
</location>
|
||||
</configuration>
|
||||
14
csharp/ql/src/Security Features/CWE-285/WebForms.cs
Normal file
14
csharp/ql/src/Security Features/CWE-285/WebForms.cs
Normal file
@@ -0,0 +1,14 @@
|
||||
class ProfilePage : System.Web.UI.Page {
|
||||
// BAD: No authorization is used
|
||||
protected void btn1_Edit_Click(object sender, EventArgs e) {
|
||||
...
|
||||
}
|
||||
|
||||
// GOOD: `User.IsInRole` checks the current user's role.
|
||||
protected void btn2_Delete_Click(object sender, EventArgs e) {
|
||||
if (!User.IsInRole("admin")) {
|
||||
return;
|
||||
}
|
||||
...
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: newQuery
|
||||
---
|
||||
* Added a new query, `cs/web/missing-function-level-access-control`, to find instances of missing authorization checks.
|
||||
@@ -0,0 +1 @@
|
||||
| ProfileController.cs:9:25:9:31 | Delete1 | This action is missing an authorization check. |
|
||||
@@ -0,0 +1 @@
|
||||
Security Features/CWE-285/MissingAccessControl.ql
|
||||
@@ -0,0 +1,30 @@
|
||||
using Microsoft.AspNetCore.Mvc;
|
||||
using Microsoft.AspNetCore.Authorization;
|
||||
|
||||
public class ProfileController : Controller {
|
||||
private void doThings() { }
|
||||
private bool isAuthorized() { return false; }
|
||||
|
||||
// BAD: This is a Delete method, but no auth is specified.
|
||||
public ActionResult Delete1(int id) {
|
||||
doThings();
|
||||
return View();
|
||||
}
|
||||
|
||||
// GOOD: isAuthorized is checked.
|
||||
public ActionResult Delete2(int id) {
|
||||
if (!isAuthorized()) {
|
||||
return null;
|
||||
}
|
||||
doThings();
|
||||
return View();
|
||||
}
|
||||
|
||||
// GOOD: The Authorize attribute is used.
|
||||
[Authorize]
|
||||
public ActionResult Delete3(int id) {
|
||||
doThings();
|
||||
return View();
|
||||
}
|
||||
|
||||
}
|
||||
@@ -0,0 +1,3 @@
|
||||
semmle-extractor-options: /nostdlib /noconfig
|
||||
semmle-extractor-options: --load-sources-from-project:${testdir}/../../../../../resources/stubs/_frameworks/Microsoft.NETCore.App/Microsoft.NETCore.App.csproj
|
||||
semmle-extractor-options: --load-sources-from-project:${testdir}/../../../../../resources/stubs/_frameworks/Microsoft.AspNetCore.App/Microsoft.AspNetCore.App.csproj
|
||||
@@ -0,0 +1,3 @@
|
||||
| Test1/EditProfile.aspx.cs:10:20:10:29 | btn1_Click | This action is missing an authorization check. |
|
||||
| Test1/ViewProfile.aspx.cs:14:20:14:36 | btn_delete1_Click | This action is missing an authorization check. |
|
||||
| Test3/B/EditProfile.aspx.cs:8:20:8:29 | btn1_Click | This action is missing an authorization check. |
|
||||
@@ -0,0 +1 @@
|
||||
Security Features/CWE-285/MissingAccessControl.ql
|
||||
@@ -0,0 +1,20 @@
|
||||
using System;
|
||||
using System.Web.UI;
|
||||
|
||||
class EditProfile : System.Web.UI.Page {
|
||||
private void doThings() { }
|
||||
|
||||
private bool isAuthorized() { return false; }
|
||||
|
||||
// BAD: The class name indicates that this may be an Edit method, but there is no auth check
|
||||
protected void btn1_Click(object sender, EventArgs e) {
|
||||
doThings();
|
||||
}
|
||||
|
||||
// GOOD: There is a call to isAuthorized
|
||||
protected void btn2_Click(object sender, EventArgs e) {
|
||||
if (isAuthorized()) {
|
||||
doThings();
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,24 @@
|
||||
using System;
|
||||
using System.Web.UI;
|
||||
using System.Web.Security;
|
||||
|
||||
class ViewProfile : System.Web.UI.Page {
|
||||
private void doThings() { }
|
||||
|
||||
// GOOD: This method and class name do not indicate a sensitive method.
|
||||
protected void btn_safe_Click(object sender, EventArgs e) {
|
||||
doThings();
|
||||
}
|
||||
|
||||
// BAD: The name indicates a Delete method, but no auth is present.
|
||||
protected void btn_delete1_Click(object sender, EventArgs e) {
|
||||
doThings();
|
||||
}
|
||||
|
||||
// GOOD: User.IsInRole is checked.
|
||||
protected void btn_delete2_Click(object sender, EventArgs e) {
|
||||
if (User.IsInRole("admin")) {
|
||||
doThings();
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,11 @@
|
||||
using System;
|
||||
using System.Web.UI;
|
||||
|
||||
class EditProfile2 : System.Web.UI.Page {
|
||||
private void doThings() { }
|
||||
|
||||
// GOOD: The Web.config file specifies auth for this path.
|
||||
protected void btn1_Click(object sender, EventArgs e) {
|
||||
doThings();
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,12 @@
|
||||
<?xml version="1.0"?>
|
||||
|
||||
<configuration xmlns:xdt="http://schemas.microsoft.com/XML-Document-Transform">
|
||||
|
||||
<system.web>
|
||||
|
||||
<authorization>
|
||||
<deny users="?" />
|
||||
</authorization>
|
||||
|
||||
</system.web>
|
||||
</configuration>
|
||||
@@ -0,0 +1,11 @@
|
||||
using System;
|
||||
using System.Web.UI;
|
||||
|
||||
class EditProfile3 : System.Web.UI.Page {
|
||||
private void doThings() { }
|
||||
|
||||
// GOOD: This is covered by the Web.config's location tag referring to A
|
||||
protected void btn1_Click(object sender, EventArgs e) {
|
||||
doThings();
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,11 @@
|
||||
using System;
|
||||
using System.Web.UI;
|
||||
|
||||
class EditProfile4 : System.Web.UI.Page {
|
||||
private void doThings() { }
|
||||
|
||||
// BAD: The Web.config file does not specify auth for this path.
|
||||
protected void btn1_Click(object sender, EventArgs e) {
|
||||
doThings();
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,11 @@
|
||||
using System;
|
||||
using System.Web.UI;
|
||||
|
||||
class EditProfile5 : System.Web.UI.Page {
|
||||
private void doThings() { }
|
||||
|
||||
// GOOD: The Web.config file specifies auth for the path Virtual, which is mapped to C in Global.asax
|
||||
protected void btn1_Click(object sender, EventArgs e) {
|
||||
doThings();
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,26 @@
|
||||
using System;
|
||||
using System.Web;
|
||||
using System.Web.Routing;
|
||||
|
||||
public class Global : System.Web.HttpApplication {
|
||||
|
||||
void Application_Start(object sender, EventArgs e) {
|
||||
RegisterRoutes(RouteTable.Routes);
|
||||
}
|
||||
|
||||
void Application_End(object sender, EventArgs e) { }
|
||||
|
||||
void Application_Error(object sender, EventArgs e) { }
|
||||
|
||||
void Session_Start(object sender, EventArgs e) { }
|
||||
|
||||
void Session_End(object sender, EventArgs e) { }
|
||||
|
||||
static void RegisterRoutes(RouteCollection routes) {
|
||||
routes.MapPageRoute("VirtualEditProfile",
|
||||
"Virtual/Edit",
|
||||
"~/C/EditProfile.aspx",
|
||||
false
|
||||
);
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0"?>
|
||||
|
||||
<configuration xmlns:xdt="http://schemas.microsoft.com/XML-Document-Transform">
|
||||
|
||||
<location path="A">
|
||||
<system.web>
|
||||
<authorization>
|
||||
<deny users="?" />
|
||||
</authorization>
|
||||
</system.web>
|
||||
</location>
|
||||
<location path="Virtual">
|
||||
<system.web>
|
||||
<authorization>
|
||||
<deny users="?" />
|
||||
</authorization>
|
||||
</system.web>
|
||||
</location>
|
||||
</configuration>
|
||||
@@ -0,0 +1,3 @@
|
||||
semmle-extractor-options: /nostdlib /noconfig
|
||||
semmle-extractor-options: --load-sources-from-project:${testdir}/../../../../../resources/stubs/_frameworks/Microsoft.NETCore.App/Microsoft.NETCore.App.csproj
|
||||
semmle-extractor-options: ${testdir}/../../../../../resources/stubs/System.Web.cs
|
||||
File diff suppressed because one or more lines are too long
@@ -48,6 +48,8 @@ namespace System.Web
|
||||
public class HttpApplication : IHttpHandler
|
||||
{
|
||||
public HttpServerUtility Server { get; }
|
||||
|
||||
public Routing.RouteTable RouteTable { get; }
|
||||
}
|
||||
}
|
||||
|
||||
@@ -79,6 +81,7 @@ namespace System.Web.UI
|
||||
|
||||
public class Page
|
||||
{
|
||||
public System.Security.Principal.IPrincipal User { get; }
|
||||
}
|
||||
|
||||
interface IPostBackDataHandler
|
||||
@@ -301,6 +304,19 @@ namespace System.Web.Routing
|
||||
public class RequestContext
|
||||
{
|
||||
}
|
||||
|
||||
public class Route
|
||||
{
|
||||
}
|
||||
|
||||
public class RouteTable {
|
||||
public RouteCollection Routes { get; }
|
||||
}
|
||||
|
||||
public class RouteCollection
|
||||
{
|
||||
public Route MapPageRoute(string routeName, string routeUrl, string physicalFile, bool checkPhysicalUrlAccess) { return null; }
|
||||
}
|
||||
}
|
||||
|
||||
namespace System.Web.Security
|
||||
|
||||
@@ -959,13 +959,18 @@ The types specified after the ``extends`` keyword are the *base types* of the cl
|
||||
|
||||
The types specified after the ``instanceof`` keyword are the *instanceof types* of the class.
|
||||
|
||||
A class type is said to *inherit* from the base types. In addition, inheritance is transitive: If a type ``A`` inherits from a type ``B``, and ``B`` inherits from a type ``C``, then ``A`` inherits from ``C``.
|
||||
A class type is said to *final inherit* from base types that are final or referenced through final aliases, and a class type is said to *inherit* from its other base types. In addition, inheritance is transitive:
|
||||
|
||||
- If a type ``A`` inherits from a type ``B``, and ``B`` inherits from a type ``C``, then ``A`` inherits from ``C``.
|
||||
- If a type ``A`` final inherits from a type ``B``, and ``B`` inherits from a type ``C``, then ``A`` final inherits from ``C``.
|
||||
- If a type ``A`` inherits from a type ``B``, and ``B`` final inherits from a type ``C``, then ``A`` final inherits from ``C``.
|
||||
- If a type ``A`` final inherits from a type ``B``, and ``B`` final inherits from a type ``C``, then ``A`` final inherits from ``C``.
|
||||
|
||||
A class adds a mapping from the class name to the class declaration to the current module's declared type environment.
|
||||
|
||||
A valid class can be annotated with ``abstract``, ``final``, ``library``, and ``private``. Any other annotation renders the class invalid.
|
||||
|
||||
A valid class may not inherit from a final class, from itself, or from more than one primitive type.
|
||||
A valid class may not inherit from itself, or from more than one primitive type. The set of types that a valid class inherits from must be disjoint from the set of types that it final inherits from.
|
||||
|
||||
A valid class must have at least one base type or instanceof type.
|
||||
|
||||
@@ -975,9 +980,10 @@ Class dependencies
|
||||
The program is invalid if there is a cycle of class dependencies.
|
||||
|
||||
The following are class dependencies:
|
||||
|
||||
- ``C`` depends on ``C.C``
|
||||
- ``C.C`` depends on ``C.extends``
|
||||
- If ``C`` is abstract then it depends on all classes ``D`` such that ``C`` is a base type of ``D``.
|
||||
- If ``C`` is abstract then it depends on all classes ``D`` such that ``C`` is a base type of ``D`` and ``D`` inherits from ``C``.
|
||||
- ``C.extends`` depends on ``D.D`` for each base type ``D`` of ``C``.
|
||||
- ``C.extends`` depends on ``D`` for each instanceof type ``D`` of ``C``.
|
||||
|
||||
@@ -1029,7 +1035,9 @@ A valid member predicate can be annotated with ``abstract``, ``cached``, ``final
|
||||
|
||||
If a type is provided before the name of the member predicate, then that type is the *result type* of the predicate. Otherwise, the predicate has no result type. The types of the variables in the ``var_decls`` are called the predicate's *argument types*.
|
||||
|
||||
A member predicate ``p`` with enclosing class ``C`` *overrides* a member predicate ``p'`` with enclosing class ``D`` when ``C`` inherits from ``D``, ``p'`` is visible in ``C``, and both ``p`` and ``p'`` have the same name and the same arity. An overriding predicate must have the same sequence of argument types as any predicates which it overrides, otherwise the program is invalid.
|
||||
A member predicate ``p`` with enclosing class ``C`` *overrides* a member predicate ``p'`` with enclosing class ``D`` when ``p`` is annotated ``overrride``, ``C`` inherits from ``D``, ``p'`` is visible in ``C``, ``p'`` is not final, and both ``p`` and ``p'`` have the same name and the same arity. An overriding predicate must have the same sequence of argument types as any predicates which it overrides, otherwise the program is invalid.
|
||||
|
||||
A member predicate ``p`` with enclosing class ``C`` *shadows* a member predicate ``p'`` with enclosing class ``D`` when ``C`` final inherits from ``D``, ``p'`` is visible in ``C``, and both ``p`` and ``p'`` have the same name and the same arity. Additionally, a member predicate ``p`` with enclosing class ``C`` *shadows* a member predicate ``p'`` with enclosing class ``D`` when ``C`` inherits from ``D``, ``p'`` is visible in ``C``, ``p'`` is final, and both ``p`` and ``p'`` have the same name and the same arity.
|
||||
|
||||
Member predicates have one or more *root definitions*. If a member predicate overrides no other member predicate, then it is its own root definition. Otherwise, its root definitions are those of any member predicate that it overrides.
|
||||
|
||||
@@ -1043,7 +1051,9 @@ A class may not inherit from a class with an abstract member predicate unless it
|
||||
|
||||
A valid class must include a non-private predicate named ``toString`` with no arguments and a result type of ``string``, or it must inherit from a class that does.
|
||||
|
||||
A valid class may not inherit from two different classes that include a predicate with the same name and number of arguments, unless either one of the predicates overrides the other, or the class defines a predicate that overrides both of them.
|
||||
A valid class may not inherit from two different classes that include a predicate with the same name and number of arguments, unless either one of the predicates overrides or shadows the other, or the class defines a predicate that overrides or shadows both of them.
|
||||
|
||||
A valid class may not final inherit from two different classes that include a predicate with the same name and number of arguments, unless either one of the predicates overrides or shadows the other, or the class defines a predicate that shadows both of them.
|
||||
|
||||
The typing environment for a member predicate or character is the same as if it were a non-member predicate, except that it additionally maps ``this`` to a type and also maps any fields on a class to a type. If the member is a character, then the typing environment maps ``this`` to the class domain type of the class. Otherwise, it maps ``this`` to the class type of the class itself.
|
||||
The typing environment also maps any field to the type of the field.
|
||||
@@ -1053,9 +1063,13 @@ Fields
|
||||
|
||||
A field declaration introduces a mapping from the field name to the field declaration in the class's declared field environment.
|
||||
|
||||
A field ``f`` with enclosing class ``C`` *overrides* a field ``f'`` with enclosing class ``D`` when ``f`` is annotated ``override``, ``C`` inherits from ``D``, ``p'`` is visible in ``C``, and both ``p`` and ``p'`` have the same name.
|
||||
A field ``f`` with enclosing class ``C`` *overrides* a field ``f'`` with enclosing class ``D`` when ``f`` is annotated ``override``, ``C`` inherits from ``D``, ``p'`` is visible in ``C``, ``p'`` is not final, and both ``p`` and ``p'`` have the same name.
|
||||
|
||||
A valid class may not inherit from two different classes that include a field with the same name, unless either one of the fields overrides the other, or the class defines a field that overrides both of them.
|
||||
A field ``f`` with enclosing class ``C`` *shadows* a field ``f'`` with enclosing class ``D`` when ``C`` final inherits from ``D``, ``p'`` is visible in ``C``, and both ``p`` and ``p'`` have the same name. Additionally, a field ``f`` with enclosing class ``C`` *shadows* a field ``f'`` with enclosing class ``D`` when ``C`` inherits from ``D``, ``p'`` is visible in ``C``, ``p'`` is final, and both ``p`` and ``p'`` have the same name.
|
||||
|
||||
A valid class may not inherit from two different classes that include a field with the same name, unless either one of the fields overrides or shadows the other, or the class defines a field that overrides or shadows both of them.
|
||||
|
||||
A valid class may not final inherit from two different classes that include a field with the same name, unless either one of the fields overrides or shadows the other, or the class defines a field that shadows both of them.
|
||||
|
||||
A valid field must override another field if it is annotated ``override``.
|
||||
|
||||
@@ -1349,9 +1363,10 @@ If the call includes a closure, then all declared predicate arguments, the enclo
|
||||
|
||||
A call to a member predicate may be a *direct* call:
|
||||
- If the receiver is not a super expression it is not direct.
|
||||
- If the receiver is ``A.super`` and ``A`` is an instanceof type and not a base type then it is not direct.
|
||||
- If the receiver is ``A.super`` and ``A`` is a base type type and not an instanceof type then it is direct.
|
||||
- If the receiver is ``A.super`` and ``A`` is a base type and an instanceof type then the call is not valid.
|
||||
- If the receiver is ``A.super`` and ``A`` is an instanceof type and not a base type that is inherited from then it is not direct.
|
||||
- If the receiver is ``A.super`` and ``A`` is a base type that is final inherited from then it is not direct.
|
||||
- If the receiver is ``A.super`` and ``A`` is a base type that is inherited from and not an instanceof type then it is direct.
|
||||
- If the receiver is ``A.super`` and ``A`` is a base type that is inherited from and an instanceof type then the call is not valid.
|
||||
- If the receiver is ``super`` and the member predicate is in the exported member predicate environment of an instanceof type and not in the exported member predicate environment of a base type then it isn't direct.
|
||||
- If the receiver is ``super`` and the member predicate is in the exported member predicate environment of a base type and not in the exported member predicate environment of an instanceof type then it is direct.
|
||||
- If the receiver is ``super`` and the member predicate is in the exported member predicate environment of a base type and in the exported member predicate environment of an instanceof type then the call is not valid.
|
||||
@@ -2123,7 +2138,7 @@ Predicates, and types can *depend* and *strictly depend* on each other. Such dep
|
||||
|
||||
- For each class ``C`` with a characteristic predicate, ``C.C`` depends on the characteristic predicate.
|
||||
|
||||
- For each abstract class ``A`` in the program, for each type ``C`` that has ``A`` as a base type, ``A.class`` depends on ``C.class``.
|
||||
- For each abstract class ``A`` in the program, for each type ``C`` that inherits from ``A`` and has ``A`` as a base type, ``A.class`` depends on ``C.class``.
|
||||
|
||||
- A predicate with a higher-order body may strictly depend or depend on each predicate reference within the body. The exact dependencies are left unspecified.
|
||||
|
||||
@@ -2175,7 +2190,7 @@ Each layer of the stratification is *populated* in order. To populate a layer, e
|
||||
|
||||
- To populate the type ``C.class`` for an abstract class type ``C``, identify each named tuple that has the following properties:
|
||||
- It is a member of ``C.C``.
|
||||
- For each class ``D`` that has ``C`` as a base type then there is a named tuple with variables from the public fields of ``C`` and ``this`` that the given tuple and a tuple in ``D.class`` both extend.
|
||||
- For each class ``D`` that inherits from ``C`` and has ``C`` as a base type then there is a named tuple with variables from the public fields of ``C`` and ``this`` that the given tuple and a tuple in ``D.class`` both extend.
|
||||
|
||||
|
||||
Query evaluation
|
||||
|
||||
@@ -24,7 +24,7 @@
|
||||
JavaScript,ECMAScript 2022 or lower,Not applicable,"``.js``, ``.jsx``, ``.mjs``, ``.es``, ``.es6``, ``.htm``, ``.html``, ``.xhtm``, ``.xhtml``, ``.vue``, ``.hbs``, ``.ejs``, ``.njk``, ``.json``, ``.yaml``, ``.yml``, ``.raml``, ``.xml`` [7]_"
|
||||
Python [8]_,"2.7, 3.5, 3.6, 3.7, 3.8, 3.9, 3.10, 3.11",Not applicable,``.py``
|
||||
Ruby [9]_,"up to 3.2",Not applicable,"``.rb``, ``.erb``, ``.gemspec``, ``Gemfile``"
|
||||
Swift [10]_,"Swift 5.4-5.7","Swift compiler","``.swift``"
|
||||
Swift [10]_,"Swift 5.4-5.8.1","Swift compiler","``.swift``"
|
||||
TypeScript [11]_,"2.6-5.1",Standard TypeScript compiler,"``.ts``, ``.tsx``, ``.mts``, ``.cts``"
|
||||
|
||||
.. container:: footnote-group
|
||||
@@ -38,5 +38,5 @@
|
||||
.. [7] JSX and Flow code, YAML, JSON, HTML, and XML files may also be analyzed with JavaScript files.
|
||||
.. [8] The extractor requires Python 3 to run. To analyze Python 2.7 you should install both versions of Python.
|
||||
.. [9] Requires glibc 2.17.
|
||||
.. [10] Swift support is currently in beta. Support for the analysis of Swift 5.4-5.7 requires macOS. Swift 5.7.3 can also be analyzed using Linux.
|
||||
.. [10] Swift support is currently in beta. Support for the analysis of Swift 5.4-5.8.1 requires macOS or Linux.
|
||||
.. [11] TypeScript analysis is performed by running the JavaScript extractor with TypeScript enabled. This is the default.
|
||||
|
||||
Reference in New Issue
Block a user