Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -119,27 +119,67 @@ module SemanticExprConfig {
result = block.getDisplayIndex()
}

class SsaVariable instanceof IR::Instruction {
SsaVariable() { super.hasMemoryResult() }
newtype TSsaVariable =
TSsaInstruction(IR::Instruction instr) { instr.hasMemoryResult() } or
TSsaOperand(IR::Operand op) { op.isDefinitionInexact() }

final string toString() { result = super.toString() }
class SsaVariable extends TSsaVariable {
string toString() { none() }

final Location getLocation() { result = super.getLocation() }
Location getLocation() { none() }

IR::Instruction asInstruction() { none() }

IR::Operand asOperand() { none() }
}

private class SsaInstructionVariable extends SsaVariable, TSsaInstruction {
IR::Instruction instr;

SsaInstructionVariable() { this = TSsaInstruction(instr) }

final override string toString() { result = instr.toString() }

final override Location getLocation() { result = instr.getLocation() }

final override IR::Instruction asInstruction() { result = instr }
}

private class SsaOperandVariable extends SsaVariable, TSsaOperand {
IR::Operand op;

SsaOperandVariable() { this = TSsaOperand(op) }

final override string toString() { result = op.toString() }

final override Location getLocation() { result = op.getLocation() }

final override IR::Operand asOperand() { result = op }
}

predicate explicitUpdate(SsaVariable v, Expr sourceExpr) { v = sourceExpr }
predicate explicitUpdate(SsaVariable v, Expr sourceExpr) { v.asInstruction() = sourceExpr }

predicate phi(SsaVariable v) { v instanceof IR::PhiInstruction }
predicate phi(SsaVariable v) { v.asInstruction() instanceof IR::PhiInstruction }

SsaVariable getAPhiInput(SsaVariable v) { result = v.(IR::PhiInstruction).getAnInput() }
SsaVariable getAPhiInput(SsaVariable v) {
exists(IR::PhiInstruction instr | v.asInstruction() = instr |
result.asInstruction() = instr.getAnInput()
or
result.asOperand() = instr.getAnInputOperand()
)
}

Expr getAUse(SsaVariable v) { result.(IR::LoadInstruction).getSourceValue() = v }
Expr getAUse(SsaVariable v) { result.(IR::LoadInstruction).getSourceValue() = v.asInstruction() }

SemType getSsaVariableType(SsaVariable v) {
result = getSemanticType(v.(IR::Instruction).getResultIRType())
result = getSemanticType(v.asInstruction().getResultIRType())
}

BasicBlock getSsaVariableBasicBlock(SsaVariable v) { result = v.(IR::Instruction).getBlock() }
BasicBlock getSsaVariableBasicBlock(SsaVariable v) {
result = v.asInstruction().getBlock()
or
result = v.asOperand().getUse().getBlock()
}

private newtype TReadPosition =
TReadPositionBlock(IR::IRBlock block) or
Expand Down Expand Up @@ -169,7 +209,12 @@ module SemanticExprConfig {

final override predicate hasRead(SsaVariable v) {
exists(IR::Operand operand |
operand.getDef() = v and not operand instanceof IR::PhiInputOperand
operand.getDef() = v.asInstruction() and
not operand instanceof IR::PhiInputOperand and
operand.getUse().getBlock() = block
or
operand = v.asOperand() and
operand.getUse().getBlock() = block
)
}
}
Expand All @@ -186,7 +231,7 @@ module SemanticExprConfig {

final override predicate hasRead(SsaVariable v) {
exists(IR::PhiInputOperand operand |
operand.getDef() = v and
operand.getDef() = v.asInstruction() and
operand.getPredecessorBlock() = pred and
operand.getUse().getBlock() = succ
)
Expand All @@ -205,15 +250,22 @@ module SemanticExprConfig {
exists(IR::PhiInputOperand operand |
pos = TReadPositionPhiInputEdge(operand.getPredecessorBlock(), operand.getUse().getBlock())
|
phi = operand.getUse() and input = operand.getDef()
phi.asInstruction() = operand.getUse() and
(
input.asInstruction() = operand.getDef()
or
input.asOperand() = operand
)
)
}

class Bound instanceof IRBound::Bound {
Bound() {
this instanceof IRBound::ZeroBound
or
this.(IRBound::ValueNumberBound).getValueNumber().getAnInstruction() instanceof SsaVariable
exists(SsaVariable v |
this.(IRBound::ValueNumberBound).getValueNumber().getAnInstruction() = v.asInstruction()
)
}

string toString() { result = super.toString() }
Expand All @@ -228,21 +280,21 @@ module SemanticExprConfig {

override string toString() {
result =
min(SsaVariable instr |
instr = bound.getValueNumber().getAnInstruction()
min(SsaVariable v |
v.asInstruction() = bound.getValueNumber().getAnInstruction()
|
instr
v
order by
instr.(IR::Instruction).getBlock().getDisplayIndex(),
instr.(IR::Instruction).getDisplayIndexInBlock()
v.asInstruction().getBlock().getDisplayIndex(),
v.asInstruction().getDisplayIndexInBlock()
).toString()
}
}

predicate zeroBound(Bound bound) { bound instanceof IRBound::ZeroBound }

predicate ssaBound(Bound bound, SsaVariable v) {
v = bound.(IRBound::ValueNumberBound).getValueNumber().getAnInstruction()
v.asInstruction() = bound.(IRBound::ValueNumberBound).getValueNumber().getAnInstruction()
}

Expr getBoundExpr(Bound bound, int delta) {
Expand Down Expand Up @@ -284,9 +336,13 @@ SemBasicBlock getSemanticBasicBlock(IR::IRBlock block) { result = block }

IR::IRBlock getCppBasicBlock(SemBasicBlock block) { block = result }

SemSsaVariable getSemanticSsaVariable(IR::Instruction instr) { result = instr }
SemSsaVariable getSemanticSsaVariable(IR::Instruction instr) {
result.(SemanticExprConfig::SsaVariable).asInstruction() = instr
}

IR::Instruction getCppSsaVariableInstruction(SemSsaVariable v) { v = result }
IR::Instruction getCppSsaVariableInstruction(SemSsaVariable var) {
var.(SemanticExprConfig::SsaVariable).asInstruction() = result
}

SemBound getSemanticBound(IRBound::Bound bound) { result = bound }

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
| test.cpp:33:10:33:10 | Load: i | false | test.cpp:29:14:29:14 | Phi: i | IR gives 0 but sem is unbounded |
| test.cpp:40:10:40:14 | Load: begin | false | test.cpp:38:16:38:20 | InitializeParameter: begin | IR gives 0 but sem is unbounded |
| test.cpp:40:10:40:14 | Load: begin | true | test.cpp:38:28:38:30 | InitializeParameter: end | IR gives -1 but sem gives 0 |
| test.cpp:62:10:62:13 | Load: iter | false | test.cpp:60:17:60:17 | InitializeParameter: p | IR gives 0 but sem is unbounded |
| test.cpp:62:10:62:13 | Load: iter | true | test.cpp:60:17:60:17 | InitializeParameter: p | IR gives 3 but sem is unbounded |
| test.cpp:62:10:62:13 | Load: iter | true | test.cpp:61:39:61:51 | Convert: (char *)... | IR gives -1 but sem gives 0 |
| test.cpp:67:10:67:13 | Load: iter | false | test.cpp:60:17:60:17 | InitializeParameter: p | IR gives 0 but sem is unbounded |
| test.cpp:67:10:67:13 | Load: iter | true | test.cpp:60:17:60:17 | InitializeParameter: p | IR gives 3 but sem is unbounded |
| test.cpp:67:10:67:13 | Load: iter | true | test.cpp:61:32:61:35 | Phi: iter | IR gives -1 but sem is unbounded |
| test.cpp:67:10:67:13 | Load: iter | true | test.cpp:61:39:61:51 | Convert: (char *)... | IR gives -1 but sem gives 0 |
| test.cpp:73:12:73:21 | Mul: new[] | false | test.cpp:73:12:73:21 | Mul: new[] | IR gives 0 but sem is unbounded |
| test.cpp:73:12:73:21 | Mul: new[] | true | test.cpp:73:12:73:21 | Mul: new[] | IR gives 0 but sem is unbounded |
| test.cpp:130:10:130:10 | Load: i | false | file://:0:0:0:0 | 0 | IR gives 0 but sem is unbounded |
| test.cpp:149:10:149:10 | Store: i | false | file://:0:0:0:0 | 0 | IR is unbounded but sem gives 1 |
| test.cpp:149:10:149:10 | Store: i | true | file://:0:0:0:0 | 0 | IR is unbounded but sem gives 1 |
| test.cpp:200:10:200:10 | Load: i | true | test.cpp:198:25:198:25 | InitializeParameter: l | IR gives -1 but sem is unbounded |
| test.cpp:203:11:203:11 | Load: i | true | test.cpp:198:25:198:25 | InitializeParameter: l | IR gives -3 but sem is unbounded |
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
import experimental.semmle.code.cpp.rangeanalysis.RangeAnalysis
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
import semmle.code.cpp.ir.IR
import semmle.code.cpp.ir.ValueNumbering

from Instruction i, string diff, boolean upper, Bound b
where
(
i.getAUse() instanceof ArgumentOperand
or
exists(ReturnValueInstruction retInstr | retInstr.getReturnValueOperand() = i.getAUse())
) and
(
exists(int irDelta, int semDelta |
boundedInstruction(i, b, irDelta, upper, _) and
semBounded(i, b, semDelta, upper, _) and
irDelta != semDelta and
diff = "IR gives " + irDelta + " but sem gives " + semDelta
)
or
exists(int irDelta |
boundedInstruction(i, b, irDelta, upper, _) and
not exists(int semDelta | semBounded(i, b, semDelta, upper, _)) and
diff = "IR gives " + irDelta + " but sem is unbounded"
)
or
exists(int semDelta |
not exists(int irDelta | boundedInstruction(i, b, irDelta, upper, _)) and
semBounded(i, b, semDelta, upper, _) and
diff = "IR is unbounded but sem gives " + semDelta
)
)
select i, upper, b, diff
6 changes: 6 additions & 0 deletions cpp/ql/test/library-tests/ir/modulus-analysis/test.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -58,3 +58,9 @@ void loops(int cap)
for (int k = 0; k < cap; k += 3)
mod(k); // $ mod=0,0,3
}

int loops2 (unsigned int *i) {
for (; *i <= 2; (*i)++) {
}
return *i;
}
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
import cpp
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
import experimental.semmle.code.cpp.semantic.Semantic
import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
import semmle.code.cpp.ir.IR as IR
import TestUtilities.InlineExpectationsTest

Expand Down Expand Up @@ -37,8 +38,9 @@ private string getBoundString(SemBound b, int delta) {
b instanceof SemZeroBound and result = delta.toString()
or
result =
strictconcat(b.(SemSsaBound).getAVariable().(IR::Instruction).getAst().toString(), ":") +
getOffsetString(delta)
strictconcat(getCppSsaVariableInstruction(b.(SemSsaBound).getAVariable()).getAst().toString(),
":"
) + getOffsetString(delta)
}

private string getARangeString(SemExpr e) {
Expand Down
Loading