-
Notifications
You must be signed in to change notification settings - Fork 66
Implement Concurrency9 package #819
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
nicolaswill
merged 8 commits into
main
from
michaelrfairhurst/implement-concurrency9-package
Mar 27, 2025
Merged
Changes from all commits
Commits
Show all changes
8 commits
Select commit
Hold shift + click to select a range
713c675
Implement Concurrency9 package on top of Concurrency8 work
MichaelRFairhurst 42adff5
Formatting & json validation
MichaelRFairhurst 96171ee
cpp format
MichaelRFairhurst 8553103
regenerate query metadata
MichaelRFairhurst e1a0d6d
Merge branch 'main' into michaelrfairhurst/implement-concurrency9-pac…
nicolaswill dae8162
Address feedback
MichaelRFairhurst 00defdd
Fix typo
MichaelRFairhurst 37caf0e
Merge remote-tracking branch 'origin/main' into michaelrfairhurst/imp…
MichaelRFairhurst File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,125 @@ | ||
/** | ||
* A library that expands upon the `Objects.qll` library, to support nested "Objects" such as | ||
* `x.y.z` or `x[i][j]` within an object `x`. | ||
* | ||
* Objects in C are values in memory, that have a type and a storage duration. In the case of | ||
* array objects and struct objects, the object will contain other objects. The these subobjects | ||
* will share properties of the root object such as storage duration. This library can be used to, | ||
* for instance, find all usages of a struct member to ensure that member is initialized before it | ||
* is used. | ||
* | ||
* To use this library, select `SubObject` and find its usages in the AST via `getAnAccess()` (to | ||
* find usages of the subobject by value) or `getAnAddressOfExpr()` (to find usages of the object | ||
* by address). | ||
* | ||
* Note that a struct or array object may contain a pointer. In this case, the pointer itself is | ||
* a subobject of the struct or array object, but the object that the pointer points to is not. | ||
* This is because the pointed-to object does not necessarily have the same storage duration, | ||
* lifetime, or linkage as the pointer and the object containing the pointer. | ||
* | ||
* Note as well that `getAnAccess()` on an array subobject will return all accesses to the array, | ||
* not just accesses to a particular index. For this reason, `SubObject` exposes the predicate | ||
* `isPrecise()`. If a subobject is precise, that means all results of `getAnAccess()` will | ||
* definitely refer to the same object in memory. If it is not precise, the different accesses | ||
* may refer to the same or different objects in memory. For instance, `x[i].y` and `x[j].y` are | ||
* the same object if `i` and `j` are the same, but they are different objects if `i` and `j` are | ||
* different. | ||
*/ | ||
|
||
import codingstandards.c.Objects | ||
|
||
newtype TSubObject = | ||
TObjectRoot(ObjectIdentity i) or | ||
TObjectMember(SubObject struct, MemberVariable m) { | ||
m = struct.getType().(Struct).getAMemberVariable() | ||
} or | ||
TObjectIndex(SubObject array) { array.getType() instanceof ArrayType } | ||
nicolaswill marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
class SubObject extends TSubObject { | ||
string toString() { | ||
exists(ObjectIdentity i | | ||
this = TObjectRoot(i) and | ||
result = i.toString() | ||
) | ||
or | ||
exists(SubObject struct, Variable m | | ||
this = TObjectMember(struct, m) and | ||
result = struct.toString() + "." + m.getName() | ||
) | ||
or | ||
exists(SubObject array | | ||
this = TObjectIndex(array) and | ||
result = array.toString() | ||
) | ||
} | ||
|
||
Type getType() { | ||
exists(ObjectIdentity i | | ||
this = TObjectRoot(i) and | ||
result = i.getType() | ||
) | ||
or | ||
exists(Variable m | | ||
this = TObjectMember(_, m) and | ||
result = m.getType() | ||
) | ||
or | ||
exists(SubObject array | | ||
this = TObjectIndex(array) and | ||
result = array.getType().(ArrayType).getBaseType() | ||
) | ||
} | ||
|
||
/** | ||
* Holds for object roots and for member accesses on that root, not for array accesses. | ||
* | ||
* This is useful for cases where we do not wish to treat `x[y]` and `x[z]` as the same object. | ||
*/ | ||
predicate isPrecise() { not getParent*() = TObjectIndex(_) } | ||
|
||
SubObject getParent() { | ||
exists(SubObject struct, MemberVariable m | | ||
this = TObjectMember(struct, m) and | ||
result = struct | ||
) | ||
or | ||
exists(SubObject array | | ||
this = TObjectIndex(array) and | ||
result = array | ||
) | ||
} | ||
|
||
Expr getAnAccess() { | ||
exists(ObjectIdentity i | | ||
this = TObjectRoot(i) and | ||
result = i.getAnAccess() | ||
) | ||
or | ||
exists(MemberVariable m | | ||
this = TObjectMember(_, m) and | ||
result = m.getAnAccess() and | ||
// Only consider `DotFieldAccess`es, not `PointerFieldAccess`es, as the latter | ||
// are not subobjects of the root object: | ||
result.(DotFieldAccess).getQualifier() = getParent().getAnAccess() | ||
nicolaswill marked this conversation as resolved.
Show resolved
Hide resolved
|
||
) | ||
or | ||
this = TObjectIndex(_) and | ||
result.(ArrayExpr).getArrayBase() = getParent().getAnAccess() | ||
} | ||
|
||
AddressOfExpr getAnAddressOfExpr() { result.getOperand() = this.getAnAccess() } | ||
|
||
/** | ||
* Get the "root" object identity to which this subobject belongs. For instance, in the | ||
* expression `x.y.z`, the root object is `x`. This subobject will share properties with the root | ||
* object such as storage duration, lifetime, and linkage. | ||
*/ | ||
ObjectIdentity getRootIdentity() { | ||
exists(ObjectIdentity i | | ||
this = TObjectRoot(i) and | ||
result = i | ||
) | ||
or | ||
result = getParent().getRootIdentity() | ||
nicolaswill marked this conversation as resolved.
Show resolved
Hide resolved
|
||
} | ||
} |
95 changes: 95 additions & 0 deletions
95
c/common/src/codingstandards/c/initialization/GlobalInitializationAnalysis.qll
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,95 @@ | ||
import cpp | ||
import codingstandards.c.Objects | ||
import codingstandards.cpp.Concurrency | ||
import codingstandards.cpp.Type | ||
|
||
signature module GlobalInitializationAnalysisConfigSig { | ||
/** A function which is not called or started as a thread */ | ||
default predicate isRootFunction(Function f) { | ||
not exists(Function f2 | f2.calls(f)) and | ||
nicolaswill marked this conversation as resolved.
Show resolved
Hide resolved
|
||
not f instanceof ThreadedFunction and | ||
// Exclude functions which are used as function pointers. | ||
not exists(FunctionAccess access | f = access.getTarget()) | ||
} | ||
|
||
ObjectIdentity getAnInitializedObject(Expr e); | ||
|
||
ObjectIdentity getAUsedObject(Expr e); | ||
} | ||
|
||
module GlobalInitalizationAnalysis<GlobalInitializationAnalysisConfigSig Config> { | ||
final class FinalFunction = Function; | ||
|
||
final class FinalExpr = Expr; | ||
|
||
class RootFunction extends FinalFunction { | ||
RootFunction() { Config::isRootFunction(this) } | ||
} | ||
|
||
/** A function call which initializes a mutex or a condition */ | ||
class ObjectInit extends FinalExpr { | ||
ObjectIdentity owningObject; | ||
|
||
ObjectInit() { owningObject = Config::getAnInitializedObject(this) } | ||
|
||
ObjectIdentity getOwningObject() { result = owningObject } | ||
} | ||
|
||
/** | ||
* A function argument where that argument is used as a mutex or condition object. | ||
*/ | ||
class ObjectUse extends FinalExpr { | ||
ObjectIdentity owningObject; | ||
|
||
ObjectUse() { owningObject = Config::getAUsedObject(this) } | ||
|
||
ObjectIdentity getOwningObject() { result = owningObject } | ||
} | ||
|
||
predicate requiresInitializedMutexObject( | ||
Function func, ObjectUse mutexUse, ObjectIdentity owningObject | ||
) { | ||
mutexUse.getEnclosingFunction() = func and | ||
owningObject = mutexUse.getOwningObject() and | ||
not exists(ObjectInit init | | ||
init.getEnclosingFunction() = func and | ||
init.getOwningObject() = owningObject and | ||
mutexUse.getAPredecessor+() = init | ||
) | ||
or | ||
exists(FunctionCall call | | ||
func = call.getEnclosingFunction() and | ||
requiresInitializedMutexObject(call.getTarget(), mutexUse, owningObject) and | ||
not exists(ObjectInit init | | ||
call.getAPredecessor*() = init and | ||
init.getOwningObject() = owningObject | ||
) | ||
) | ||
or | ||
exists(C11ThreadCreateCall call | | ||
func = call.getEnclosingFunction() and | ||
not owningObject.getStorageDuration().isThread() and | ||
requiresInitializedMutexObject(call.getFunction(), mutexUse, owningObject) and | ||
not exists(ObjectInit init | | ||
call.getAPredecessor*() = init and | ||
init.getOwningObject() = owningObject | ||
) | ||
) | ||
} | ||
|
||
predicate uninitializedFrom(Expr e, ObjectIdentity obj, Function callRoot) { | ||
exists(ObjectUse use | use = e | | ||
obj = use.getOwningObject() and | ||
requiresInitializedMutexObject(callRoot, use, obj) and | ||
( | ||
if obj.getStorageDuration().isAutomatic() | ||
then obj.getEnclosingElement+() = callRoot | ||
else ( | ||
obj.getStorageDuration().isThread() and callRoot instanceof ThreadedFunction | ||
or | ||
callRoot instanceof RootFunction | ||
) | ||
) | ||
) | ||
} | ||
} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
162 changes: 162 additions & 0 deletions
162
c/misra/src/rules/DIR-5-1/PossibleDataRaceBetweenThreads.ql
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,162 @@ | ||
/** | ||
* @id c/misra/possible-data-race-between-threads | ||
* @name DIR-5-1: There shall be no data races between threads | ||
* @description Threads shall not access the same memory location concurrently without utilization | ||
* of thread synchronization objects. | ||
* @kind problem | ||
* @precision medium | ||
* @problem.severity error | ||
* @tags external/misra/id/dir-5-1 | ||
* correctness | ||
* concurrency | ||
* external/misra/c/2012/amendment4 | ||
* external/misra/obligation/required | ||
*/ | ||
|
||
import cpp | ||
import codingstandards.c.misra | ||
import codingstandards.c.Objects | ||
import codingstandards.c.SubObjects | ||
import codingstandards.cpp.Concurrency | ||
|
||
newtype TNonReentrantOperation = | ||
TReadWrite(SubObject object) { | ||
object.getRootIdentity().getStorageDuration().isStatic() | ||
or | ||
object.getRootIdentity().getStorageDuration().isAllocated() | ||
} or | ||
TStdFunctionCall(FunctionCall call) { | ||
call.getTarget() | ||
.hasName([ | ||
"setlocale", "tmpnam", "rand", "srand", "getenv", "getenv_s", "strok", "strerror", | ||
"asctime", "ctime", "gmtime", "localtime", "mbrtoc16", "c16rtomb", "mbrtoc32", | ||
"c32rtomb", "mbrlen", "mbrtowc", "wcrtomb", "mbsrtowcs", "wcsrtombs" | ||
]) | ||
} | ||
|
||
class NonReentrantOperation extends TNonReentrantOperation { | ||
string toString() { | ||
exists(SubObject object | | ||
this = TReadWrite(object) and | ||
result = object.toString() | ||
) | ||
or | ||
exists(FunctionCall call | | ||
this = TStdFunctionCall(call) and | ||
result = call.getTarget().getName() | ||
) | ||
} | ||
|
||
Expr getAReadExpr() { | ||
exists(SubObject object | | ||
this = TReadWrite(object) and | ||
result = object.getAnAccess() | ||
) | ||
or | ||
this = TStdFunctionCall(result) | ||
} | ||
|
||
Expr getAWriteExpr() { | ||
exists(SubObject object, Assignment assignment | | ||
this = TReadWrite(object) and | ||
result = assignment and | ||
assignment.getLValue() = object.getAnAccess() | ||
) | ||
or | ||
this = TStdFunctionCall(result) | ||
} | ||
|
||
string getReadString() { | ||
this = TReadWrite(_) and | ||
result = "read operation" | ||
or | ||
this = TStdFunctionCall(_) and | ||
result = "call to non-reentrant function" | ||
} | ||
|
||
string getWriteString() { | ||
this = TReadWrite(_) and | ||
result = "write to object" | ||
or | ||
this = TStdFunctionCall(_) and | ||
result = "call to non-reentrant function" | ||
} | ||
|
||
Element getSourceElement() { | ||
exists(SubObject object | | ||
this = TReadWrite(object) and | ||
result = object.getRootIdentity() | ||
) | ||
or | ||
this = TStdFunctionCall(result) | ||
} | ||
} | ||
|
||
class WritingThread extends ThreadedFunction { | ||
NonReentrantOperation aWriteObject; | ||
Expr aWriteExpr; | ||
|
||
WritingThread() { | ||
aWriteExpr = aWriteObject.getAWriteExpr() and | ||
// This function directly contains the write expression, or transitively calls the function | ||
// that contains the write expression. | ||
this.calls*(aWriteExpr.getEnclosingFunction()) and | ||
// The write isn't synchronized with a mutex or condition object. | ||
not aWriteExpr instanceof LockProtectedControlFlowNode and | ||
// The write doesn't seem to be during a special initialization phase of the program. | ||
not aWriteExpr.getEnclosingFunction().getName().matches(["%init%", "%boot%", "%start%"]) | ||
} | ||
|
||
Expr getAWriteExpr() { result = aWriteExpr } | ||
} | ||
|
||
class ReadingThread extends ThreadedFunction { | ||
Expr aReadExpr; | ||
|
||
ReadingThread() { | ||
exists(NonReentrantOperation op | | ||
aReadExpr = op.getAReadExpr() and | ||
this.calls*(aReadExpr.getEnclosingFunction()) and | ||
not aReadExpr instanceof LockProtectedControlFlowNode | ||
) | ||
} | ||
|
||
Expr getAReadExpr() { result = aReadExpr } | ||
} | ||
|
||
predicate mayBeDataRace(Expr write, Expr read, NonReentrantOperation operation) { | ||
exists(WritingThread wt | | ||
wt.getAWriteExpr() = write and | ||
write = operation.getAWriteExpr() and | ||
exists(ReadingThread rt | | ||
read = rt.getAReadExpr() and | ||
read = operation.getAReadExpr() and | ||
( | ||
wt.isMultiplySpawned() or | ||
not wt = rt | ||
) | ||
) | ||
) | ||
} | ||
|
||
from | ||
WritingThread wt, ReadingThread rt, Expr write, Expr read, NonReentrantOperation operation, | ||
string message, string writeString, string readString | ||
where | ||
not isExcluded(write, Concurrency9Package::possibleDataRaceBetweenThreadsQuery()) and | ||
mayBeDataRace(write, read, operation) and | ||
wt = min(WritingThread f | f.getAWriteExpr() = write | f order by f.getName()) and | ||
rt = min(ReadingThread f | f.getAReadExpr() = read | f order by f.getName()) and | ||
writeString = operation.getWriteString() and | ||
readString = operation.getReadString() and | ||
if wt.isMultiplySpawned() | ||
then | ||
message = | ||
"Threaded " + writeString + | ||
" $@ not synchronized from thread function $@ spawned from a loop." | ||
else | ||
message = | ||
"Threaded " + writeString + | ||
" $@ from thread function $@ is not synchronized with $@ from thread function $@." | ||
select write, message, operation.getSourceElement(), operation.toString(), wt, wt.getName(), read, | ||
"concurrent " + readString, rt, rt.getName() |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.