mirror of
https://github.com/github/codeql.git
synced 2026-05-27 01:21:23 +02:00
Python: introduce shared-SSA adapter on the new CFG
Adds 'python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll', a
minimal Python SSA implementation built on the shared SSA library
('codeql.ssa.Ssa::Make<Location, Cfg, Input>'). The structure mirrors
Java's adapter at 'java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll'.
Key design choices:
* 'SourceVariable' wraps 'Py::Variable'. Only variables that are read
or deleted somewhere are tracked - write-only variables don't
benefit from SSA construction.
* Variable references are positional ('BasicBlock', 'int') pairs
looked up via 'Cfg::NameNode.defines'/'.uses'/'.deletes' (which
themselves are one-line bridges to AST-level 'Name.defines' etc.).
* Parameter writes are not synthesised: parameter Name nodes are
already wired into the CFG (per the earlier C#-style parameter
extension in 'AstNodeImpl.qll'), so the regular 'variableWrite'
path handles them at their natural CFG index.
* Non-local / captured / global / builtin variables read in a scope
but not written in it receive a synthetic entry definition at
index '-1' of the scope's entry basic block. This matches Java's
'hasEntryDef'.
* 'del x' is modelled as a certain write at the deletion site.
Includes an inline-expectations test under
'python/ql/test/library-tests/dataflow-new-ssa/' covering:
plain parameter pass-through, simple assignment + read, reassignment
with dead-write pruning, if/else with phi insertion at the join, and
an undefined-name read (currently a known limitation - no SSA flow
without an enclosing definition).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
59
python/ql/test/library-tests/dataflow-new-ssa/SsaTest.ql
Normal file
59
python/ql/test/library-tests/dataflow-new-ssa/SsaTest.ql
Normal file
@@ -0,0 +1,59 @@
|
||||
/**
|
||||
* Inline-expectations test for the new-CFG SSA adapter
|
||||
* (`semmle.python.dataflow.new.internal.SsaImpl`).
|
||||
*
|
||||
* Tags:
|
||||
* - `def=<var>`: there is an SSA write definition of `<var>` at this
|
||||
* line (parameter init, plain assignment, augmented assignment,
|
||||
* exception-handler binding, deletion, etc.).
|
||||
* - `use=<var>`: `<var>` is used at this line, and some SSA definition
|
||||
* of `<var>` reaches the read.
|
||||
* - `phi=<var>`: there is an SSA phi definition of `<var>` whose BB
|
||||
* starts on this line.
|
||||
*/
|
||||
|
||||
import python
|
||||
import semmle.python.dataflow.new.internal.SsaImpl as SsaImpl
|
||||
import semmle.python.controlflow.internal.AstNodeImpl as CfgImpl
|
||||
import semmle.python.controlflow.internal.Cfg as Cfg
|
||||
import utils.test.InlineExpectationsTest
|
||||
|
||||
module SsaTest implements TestSig {
|
||||
string getARelevantTag() { result = ["def", "use", "phi"] }
|
||||
|
||||
predicate hasActualResult(Location location, string element, string tag, string value) {
|
||||
// A `def=<id>` fires when an SSA WriteDefinition is at a CFG node
|
||||
// on the given line.
|
||||
exists(SsaImpl::Ssa::WriteDefinition def, CfgImpl::BasicBlock bb, int i, Cfg::NameNode n |
|
||||
def.definesAt(_, bb, i) and
|
||||
bb.getNode(i) = n and
|
||||
tag = "def" and
|
||||
location = n.getLocation() and
|
||||
element = n.toString() and
|
||||
value = n.getId()
|
||||
)
|
||||
or
|
||||
// A `use=<id>` fires when an SSA Definition reaches a read at this
|
||||
// CFG node.
|
||||
exists(SsaImpl::Ssa::Definition def, CfgImpl::BasicBlock bb, int i, Cfg::NameNode n |
|
||||
SsaImpl::Ssa::ssaDefReachesRead(_, def, bb, i) and
|
||||
bb.getNode(i) = n and
|
||||
tag = "use" and
|
||||
location = n.getLocation() and
|
||||
element = n.toString() and
|
||||
value = n.getId()
|
||||
)
|
||||
or
|
||||
// A `phi=<id>` fires when there is a phi node whose BB's first
|
||||
// CFG node is on the given line.
|
||||
exists(SsaImpl::Ssa::PhiNode phi, CfgImpl::BasicBlock bb |
|
||||
phi.definesAt(_, bb, _) and
|
||||
tag = "phi" and
|
||||
location = bb.getNode(0).getLocation() and
|
||||
element = bb.toString() and
|
||||
value = phi.getSourceVariable().(SsaImpl::SsaSourceVariable).getVariable().getId()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
import MakeTest<SsaTest>
|
||||
40
python/ql/test/library-tests/dataflow-new-ssa/test.py
Normal file
40
python/ql/test/library-tests/dataflow-new-ssa/test.py
Normal file
@@ -0,0 +1,40 @@
|
||||
# Basic SSA tests for the new-CFG SSA adapter.
|
||||
#
|
||||
# The shared SSA implementation prunes its construction by liveness:
|
||||
# definitions of variables that are not read are never materialised.
|
||||
# This is by design — write-only variables would only bloat the SSA
|
||||
# graph. Tests therefore must always include a read of each variable
|
||||
# being verified.
|
||||
#
|
||||
# Annotations:
|
||||
# def=<var>: there is an SSA write definition of <var> at this line
|
||||
# use=<var>: <var> is used here and the read resolves to some def
|
||||
|
||||
|
||||
def basic_param(x): # $ def=x
|
||||
return x # $ use=x
|
||||
|
||||
|
||||
def basic_assign():
|
||||
y = 1 # $ def=y
|
||||
return y # $ use=y
|
||||
|
||||
|
||||
def reassignment():
|
||||
x = 1
|
||||
x = 2 # $ def=x
|
||||
return x # $ use=x
|
||||
|
||||
|
||||
def if_else_phi(cond): # $ def=cond
|
||||
if cond: # $ use=cond phi=x
|
||||
x = 1 # $ def=x
|
||||
else:
|
||||
x = 2 # $ def=x
|
||||
return x # $ use=x
|
||||
|
||||
|
||||
def use_global():
|
||||
return some_undefined # known limitation: undefined globals not resolved here
|
||||
|
||||
|
||||
Reference in New Issue
Block a user