/**

* Provides classes for identifying and reasoning about Microsoft source code

* annotation language (SAL) macros.

*/

import cpp

/**

* A SAL macro defined in `sal.h` or a similar header file.

*/

class SalMacro extends Macro {

SalMacro() {

this.getFile().getBaseName() =

["sal.h", "specstrings_strict.h", "specstrings.h", "w32p.h", "minwindef.h"] and

(

// Dialect for Windows 8 and above

this.getName().matches("\\_%\\_")

or

// Dialect for Windows 7

this.getName().matches("\\_\\_%")

)

}

}

pragma[noinline]

private predicate isTopLevelMacroAccess(MacroAccess ma) { not exists(ma.getParentInvocation()) }

/**

* An invocation of a SAL macro (excluding invocations inside other macros).

*/

class SalAnnotation extends MacroInvocation {

SalAnnotation() {

this.getMacro() instanceof SalMacro and

isTopLevelMacroAccess(this)

}

/** Gets the `Declaration` annotated by `this`. */

Declaration getDeclaration() {

annotatesAt(this, result.getADeclarationEntry(), _, _) and

not result instanceof Type // exclude typedefs

}

/** Gets the `DeclarationEntry` annotated by `this`. */

DeclarationEntry getDeclarationEntry() {

annotatesAt(this, result, _, _) and

not result instanceof TypeDeclarationEntry // exclude typedefs

}

}

/**

* A SAL macro indicating that the return value of a function should always be

* checked.

*/

class SalCheckReturn extends SalAnnotation {

SalCheckReturn() {

this.getMacro().(SalMacro).getName() = ["_Check_return_", "_Must_inspect_result_"]

}

}

/**

* A SAL macro indicating that a pointer variable or return value should not be

* `NULL`.

*/

class SalNotNull extends SalAnnotation {

SalNotNull() {

exists(SalMacro m | m = this.getMacro() |

not m.getName().matches("%\\_opt\\_%") and

(

m.getName().matches("_In%") or

m.getName().matches("_Out%") or

m.getName() = "_Ret_notnull_"

)

) and

exists(Type t |

t = this.getDeclaration().(Variable).getType() or

t = this.getDeclaration().(Function).getType()

|

t.getUnspecifiedType() instanceof PointerType

)

}

}

/**

* A SAL macro indicating that a value may be `NULL`.

*/

class SalMaybeNull extends SalAnnotation {

SalMaybeNull() {

exists(SalMacro m | m = this.getMacro() |

m.getName().matches("%\\_opt\\_%") or

m.getName().matches("\\_Ret_maybenull\\_%") or

m.getName() = "_Result_nullonfailure_"

)

}

}

/**

* A parameter annotated by one or more SAL annotations.

*/

class SalParameter extends Parameter {

/** One of this parameter's annotations. */

SalAnnotation a;

SalParameter() { annotatesAt(a, this.getADeclarationEntry(), _, _) }

predicate isIn() { a.getMacroName().toLowerCase().matches("%\\_in%") }

predicate isOut() { a.getMacroName().toLowerCase().matches("%\\_out%") }

predicate isInOut() { a.getMacroName().toLowerCase().matches("%\\_inout%") }

}

///////////////////////////////////////////////////////////////////////////////

// Implementation details

/**

* Holds if `a` annotates the declaration entry `d` and

* its start position is the `idx`th position in `file` that holds a SAL element.

*/

private predicate annotatesAt(SalAnnotation a, DeclarationEntry d, File file, int idx) {

annotatesAtPosition(a.(SalElement).getStartPosition(), d, file, idx)

}

/**

* Holds if `pos` is the `idx`th position in `file` that holds a SAL element,

* which annotates the declaration entry `d` (by occurring before it without

* any other declaration entries in between).

*/

// For performance reasons, do not mention the annotation itself here,

// but compute with positions instead. This performs better on databases

// with many annotations at the same position.

private predicate annotatesAtPosition(SalPosition pos, DeclarationEntry d, File file, int idx) {

pos = salRelevantPositionAt(file, idx) and

salAnnotationPos(pos) and

(

// Base case: `pos` right before `d`

d.(SalElement).getStartPosition() = salRelevantPositionAt(file, idx + 1)

or

// Recursive case: `pos` right before some annotation on `d`

annotatesAtPosition(_, d, file, idx + 1)

)

}

/**

* A SAL element, that is, a SAL annotation or a declaration entry

* that may have SAL annotations.

*/

class SalElement extends Element {

SalElement() {

containsSalAnnotation(this.(DeclarationEntry).getFile()) or

this instanceof SalAnnotation

}

predicate hasStartPosition(File file, int line, int col) {

exists(Location loc | loc = this.getLocation() |

file = loc.getFile() and

line = loc.getStartLine() and

col = loc.getStartColumn()

)

}

predicate hasEndPosition(File file, int line, int col) {

exists(Location loc |

loc = this.(FunctionDeclarationEntry).getBlock().getLocation()

or

this =

any(VariableDeclarationEntry vde |

vde.isDefinition() and

loc = vde.getVariable().getInitializer().getLocation()

)

|

file = loc.getFile() and

line = loc.getEndLine() and

col = loc.getEndColumn()

)

}

SalPosition getStartPosition() {

exists(File file, int line, int col |

this.hasStartPosition(file, line, col) and

result = MkSalPosition(file, line, col)

)

}

}

/** Holds if `file` contains a SAL annotation. */

pragma[noinline]

private predicate containsSalAnnotation(File file) { any(SalAnnotation a).getFile() = file }

/**

* A source-file position of a `SALElement`. Unlike location, this denotes a

* point in the file rather than a range.

*/

private newtype SalPosition =

MkSalPosition(File file, int line, int col) {

exists(SalElement e |

e.hasStartPosition(file, line, col)

or

e.hasEndPosition(file, line, col)

)

}

/** Holds if `pos` is the start position of a SAL annotation. */

pragma[noinline]

private predicate salAnnotationPos(SalPosition pos) {

any(SalAnnotation a).(SalElement).getStartPosition() = pos

}

/**

* Gets the `idx`th position in `file` that holds a SAL element,

* ordering positions lexicographically by their start line and start column.

*/

private SalPosition salRelevantPositionAt(File file, int idx) {

result =

rank[idx](SalPosition pos, int line, int col |

pos = MkSalPosition(file, line, col)

|

pos order by line, col

)

}