|
| 1 | +/** |
| 2 | + * @id c/misra/possible-data-race-between-threads |
| 3 | + * @name DIR-5-1: There shall be no data races between threads |
| 4 | + * @description Threads shall not access the same memory location concurrently without utilization |
| 5 | + * of thread synchronization objects. |
| 6 | + * @kind problem |
| 7 | + * @precision medium |
| 8 | + * @problem.severity error |
| 9 | + * @tags external/misra/id/dir-5-1 |
| 10 | + * correctness |
| 11 | + * concurrency |
| 12 | + * external/misra/c/2012/amendment4 |
| 13 | + * external/misra/obligation/required |
| 14 | + */ |
| 15 | + |
| 16 | +import cpp |
| 17 | +import codingstandards.c.misra |
| 18 | +import codingstandards.c.Objects |
| 19 | +import codingstandards.c.SubObjects |
| 20 | +import codingstandards.cpp.Concurrency |
| 21 | + |
| 22 | +newtype TNonReentrantOperation = |
| 23 | + TReadWrite(SubObject object) { |
| 24 | + object.getRootIdentity().getStorageDuration().isStatic() |
| 25 | + or |
| 26 | + object.getRootIdentity().getStorageDuration().isAllocated() |
| 27 | + } or |
| 28 | + TStdFunctionCall(FunctionCall call) { |
| 29 | + call.getTarget() |
| 30 | + .hasName([ |
| 31 | + "setlocale", "tmpnam", "rand", "srand", "getenv", "getenv_s", "strok", "strerror", |
| 32 | + "asctime", "ctime", "gmtime", "localtime", "mbrtoc16", "c16rtomb", "mbrtoc32", |
| 33 | + "c32rtomb", "mbrlen", "mbrtowc", "wcrtomb", "mbsrtowcs", "wcsrtombs" |
| 34 | + ]) |
| 35 | + } |
| 36 | + |
| 37 | +class NonReentrantOperation extends TNonReentrantOperation { |
| 38 | + string toString() { |
| 39 | + exists(SubObject object | |
| 40 | + this = TReadWrite(object) and |
| 41 | + result = object.toString() |
| 42 | + ) |
| 43 | + or |
| 44 | + exists(FunctionCall call | |
| 45 | + this = TStdFunctionCall(call) and |
| 46 | + result = call.getTarget().getName() |
| 47 | + ) |
| 48 | + } |
| 49 | + |
| 50 | + Expr getAReadExpr() { |
| 51 | + exists(SubObject object | |
| 52 | + this = TReadWrite(object) and |
| 53 | + result = object.getAnAccess() |
| 54 | + ) |
| 55 | + or |
| 56 | + this = TStdFunctionCall(result) |
| 57 | + } |
| 58 | + |
| 59 | + Expr getAWriteExpr() { |
| 60 | + exists(SubObject object, Assignment assignment | |
| 61 | + this = TReadWrite(object) and |
| 62 | + result = assignment and |
| 63 | + assignment.getLValue() = object.getAnAccess() |
| 64 | + ) |
| 65 | + or |
| 66 | + this = TStdFunctionCall(result) |
| 67 | + } |
| 68 | + |
| 69 | + string getReadString() { |
| 70 | + this = TReadWrite(_) and |
| 71 | + result = "read operation" |
| 72 | + or |
| 73 | + this = TStdFunctionCall(_) and |
| 74 | + result = "call to non-reentrant function" |
| 75 | + } |
| 76 | + |
| 77 | + string getWriteString() { |
| 78 | + this = TReadWrite(_) and |
| 79 | + result = "write to object" |
| 80 | + or |
| 81 | + this = TStdFunctionCall(_) and |
| 82 | + result = "call to non-reentrant function" |
| 83 | + } |
| 84 | + |
| 85 | + Element getSourceElement() { |
| 86 | + exists(SubObject object | |
| 87 | + this = TReadWrite(object) and |
| 88 | + result = object.getRootIdentity() |
| 89 | + ) |
| 90 | + or |
| 91 | + this = TStdFunctionCall(result) |
| 92 | + } |
| 93 | +} |
| 94 | + |
| 95 | +class WritingThread extends ThreadedFunction { |
| 96 | + NonReentrantOperation aWriteObject; |
| 97 | + Expr aWriteExpr; |
| 98 | + |
| 99 | + WritingThread() { |
| 100 | + aWriteExpr = aWriteObject.getAWriteExpr() and |
| 101 | + // This function directly contains the write expression, or transitively calls the function |
| 102 | + // that contains the write expression. |
| 103 | + this.calls*(aWriteExpr.getEnclosingFunction()) and |
| 104 | + // The write isn't synchronized with a mutex or condition object. |
| 105 | + not aWriteExpr instanceof LockProtectedControlFlowNode and |
| 106 | + // The write doesn't seem to be during a special initialization phase of the program. |
| 107 | + not aWriteExpr.getEnclosingFunction().getName().matches(["%init%", "%boot%", "%start%"]) |
| 108 | + } |
| 109 | + |
| 110 | + Expr getAWriteExpr() { result = aWriteExpr } |
| 111 | +} |
| 112 | + |
| 113 | +class ReadingThread extends ThreadedFunction { |
| 114 | + Expr aReadExpr; |
| 115 | + |
| 116 | + ReadingThread() { |
| 117 | + exists(NonReentrantOperation op | |
| 118 | + aReadExpr = op.getAReadExpr() and |
| 119 | + this.calls*(aReadExpr.getEnclosingFunction()) and |
| 120 | + not aReadExpr instanceof LockProtectedControlFlowNode |
| 121 | + ) |
| 122 | + } |
| 123 | + |
| 124 | + Expr getAReadExpr() { result = aReadExpr } |
| 125 | +} |
| 126 | + |
| 127 | +predicate mayBeDataRace(Expr write, Expr read, NonReentrantOperation operation) { |
| 128 | + exists(WritingThread wt | |
| 129 | + wt.getAWriteExpr() = write and |
| 130 | + write = operation.getAWriteExpr() and |
| 131 | + exists(ReadingThread rt | |
| 132 | + read = rt.getAReadExpr() and |
| 133 | + read = operation.getAReadExpr() and |
| 134 | + ( |
| 135 | + wt.isMultiplySpawned() or |
| 136 | + not wt = rt |
| 137 | + ) |
| 138 | + ) |
| 139 | + ) |
| 140 | +} |
| 141 | + |
| 142 | +from |
| 143 | + WritingThread wt, ReadingThread rt, Expr write, Expr read, NonReentrantOperation operation, |
| 144 | + string message, string writeString, string readString |
| 145 | +where |
| 146 | + not isExcluded(write, Concurrency9Package::possibleDataRaceBetweenThreadsQuery()) and |
| 147 | + mayBeDataRace(write, read, operation) and |
| 148 | + wt = min(WritingThread f | f.getAWriteExpr() = write | f order by f.getName()) and |
| 149 | + rt = min(ReadingThread f | f.getAReadExpr() = read | f order by f.getName()) and |
| 150 | + writeString = operation.getWriteString() and |
| 151 | + readString = operation.getReadString() and |
| 152 | + if wt.isMultiplySpawned() |
| 153 | + then |
| 154 | + message = |
| 155 | + "Threaded " + writeString + |
| 156 | + " $@ not synchronized from thread function $@ spawned from a loop." |
| 157 | + else |
| 158 | + message = |
| 159 | + "Threaded " + writeString + |
| 160 | + " $@ from thread function $@ is not synchronized with $@ from thread function $@." |
| 161 | +select write, message, operation.getSourceElement(), operation.toString(), wt, wt.getName(), read, |
| 162 | + "concurrent " + readString, rt, rt.getName() |
0 commit comments