@@ -475,12 +475,12 @@ class CPPThreadWait extends ThreadWait {
475475}
476476
477477/**
478- * Models a call to `thread_join ` in C11.
478+ * Models a call to `thrd_join ` in C11.
479479 */
480- class C11ThreadWait extends FunctionCall {
480+ class C11ThreadWait extends ThreadWait {
481481 VariableAccess var ;
482482
483- C11ThreadWait ( ) { getTarget ( ) .getName ( ) = "thread_join " }
483+ C11ThreadWait ( ) { getTarget ( ) .getName ( ) = "thrd_join " }
484484}
485485
486486abstract class MutexSource extends FunctionCall { }
@@ -507,38 +507,14 @@ class C11MutexSource extends MutexSource, FunctionCall {
507507 * came from. For example, if it is passed in from a local function to a thread.
508508 * This functionality is critical, since it allows one to inspect how the thread
509509 * behaves with respect to the owner of a resource.
510+ *
511+ * To model the myriad ways this can happen, the subclasses of this class are
512+ * responsible for implementing the various usage patterns.
510513 */
511514abstract class ThreadDependentMutex extends DataFlow:: Node {
515+
512516 DataFlow:: Node sink ;
513517
514- }
515- class FlowBasedThreadDependentMutex extends ThreadDependentMutex {
516- DataFlow:: Node sink ;
517-
518- ThreadDependentMutex ( ) {
519-
520- // this predicate captures two cases. The first being some sort of dataflow,
521- // likely through parameter passing.
522- exists ( ThreadDependentMutexTaintTrackingConfiguration config | config .hasFlow ( this , sink ) ) or
523-
524- // the second encapsulates usages from outside scopes not directly expressed
525- // in dataflow.
526- exists ( MutexSource mutexSrc , ThreadedFunction f , Variable variableSource |
527- DataFlow:: exprNode ( mutexSrc ) = this and
528-
529- // find a variable that was assigned the mutex
530- TaintTracking:: localTaint ( DataFlow:: exprNode ( mutexSrc ) , DataFlow:: exprNode ( variableSource .getAnAssignedValue ( ) ) ) and
531-
532- // find all subsequent accesses of that variable that are within a
533- // function and set those to the sink
534- exists ( VariableAccess va |
535- va = variableSource .getAnAccess ( ) and
536- va .getEnclosingFunction ( ) = f
537- and sink = DataFlow:: exprNode ( va )
538- )
539- )
540- }
541-
542518 DataFlow:: Node getASource ( ) {
543519 // the source is either the thing that declared
544520 // the mutex
@@ -584,24 +560,172 @@ class FlowBasedThreadDependentMutex extends ThreadDependentMutex {
584560 )
585561 }
586562
563+
587564 /**
588565 * Gets a set of usages of this mutex in both the local and thread scope.
589566 * In the case of scoped usage, this also captures typical accesses of variables.
590567 */
591568 DataFlow:: Node getAUsage ( ) { TaintTracking:: localTaint ( getASource ( ) , result ) }
569+
592570}
593571
572+ /**
573+ * This class models the type of thread/mutex dependency that is established
574+ * through the typical parameter passing mechanisms found in C++.
575+ */
576+ class FlowBasedThreadDependentMutex extends ThreadDependentMutex {
577+ FlowBasedThreadDependentMutex ( ) {
578+ // some sort of dataflow, likely through parameter passing.
579+ exists ( ThreadDependentMutexTaintTrackingConfiguration config | config .hasFlow ( this , sink ) )
580+ }
581+ }
582+
583+
584+ /**
585+ * This class models the type of thread/mutex dependency that is established by
586+ * either scope based accesses (e.g., global variables) or block scope differences.
587+ */
594588class AccessBasedThreadDependentMutex extends ThreadDependentMutex {
589+ Variable variableSource ;
590+
591+ AccessBasedThreadDependentMutex ( ) {
592+ // encapsulates usages from outside scopes not directly expressed
593+ // in dataflow.
594+ exists ( MutexSource mutexSrc , ThreadedFunction f |
595+ DataFlow:: exprNode ( mutexSrc ) = this and
596+
597+ // find a variable that was assigned the mutex
598+ TaintTracking:: localTaint ( DataFlow:: exprNode ( mutexSrc ) , DataFlow:: exprNode ( variableSource .getAnAssignedValue ( ) ) ) and
599+
600+ // find all subsequent accesses of that variable that are within a
601+ // function and set those to the sink
602+ exists ( VariableAccess va |
603+ va = variableSource .getAnAccess ( ) and
604+ va .getEnclosingFunction ( ) = f
605+ and sink = DataFlow:: exprNode ( va )
606+ )
607+ )
608+ }
609+
610+ override DataFlow:: Node getAUsage ( ) { DataFlow:: exprNode ( variableSource .getAnAccess ( ) ) = result }
611+ }
612+
613+
595614
615+
616+ /**
617+ * In the typical C thread model, a mutex is a created by a function that is not responsible
618+ * for creating the variable. Thus this class encodes a slightly different semantics
619+ * wherein the usage pattern is that of variables that have been both initialized
620+ * and then subsequently passed into a thread directly.
621+ */
622+ class DeclarationInitBasedThreadDependentMutex extends ThreadDependentMutex {
623+
624+ Variable variableSource ;
625+
626+ DeclarationInitBasedThreadDependentMutex ( ) {
627+
628+ exists ( MutexSource ms , ThreadCreationFunction tcf |
629+ this = DataFlow:: exprNode ( ms ) and
630+ // accessed as a mutex source
631+ TaintTracking:: localTaint ( DataFlow:: exprNode ( variableSource .getAnAccess ( ) ) , DataFlow:: exprNode ( ms .getAnArgument ( ) ) ) and
632+ // subsequently passed to a thread creation function (order not strictly
633+ // enforced for performance reasons)
634+ sink = DataFlow:: exprNode ( tcf .getAnArgument ( ) ) and
635+ TaintTracking:: localTaint ( DataFlow:: exprNode ( variableSource .getAnAccess ( ) ) , sink )
636+ )
637+ }
638+
639+ override DataFlow:: Node getAUsage ( ) { TaintTracking:: localTaint ( getASource ( ) , result ) or
640+ DataFlow:: exprNode ( variableSource .getAnAccess ( ) ) = result
641+ }
642+
643+ override DataFlow:: Node getASource ( ) {
644+ // the source is either the thing that declared
645+ // the mutex
646+ result = this
647+ or
648+ // or the thread we are using it in
649+ result = getAThreadSource ( )
650+ }
651+
652+ DataFlow:: Node getSink ( ) {
653+ result = sink
654+ }
655+
656+ /**
657+ * Gets the dataflow nodes corresponding to thread local usages of the
658+ * dependent mutex.
659+ */
660+ override DataFlow:: Node getAThreadSource ( ) {
661+ // here we line up the actual parameter at the thread creation
662+ // site with the formal parameter in the target thread.
663+ // Note that there are differences between the C and C++ versions
664+ // of the argument ordering in the thread creation function. However,
665+ // since the C version only takes one parameter (as opposed to multiple)
666+ // we can simplify this search by considering only the first argument.
667+
668+
669+ exists ( FunctionCall fc , Function f , int n | // CPP Version
670+ fc .getArgument ( n ) = sink .asExpr ( ) and
671+ f = fc .getArgument ( 0 ) .( FunctionAccess ) .getTarget ( ) and
672+ // in C++, there is an extra argument to the `std::thread` call
673+ // so we must subtract 1 since this is not passed to the thread.
674+ result = DataFlow:: exprNode ( f .getParameter ( n - 1 ) .getAnAccess ( ) )
675+ ) or
676+ exists ( FunctionCall fc , Function f | // C Version
677+ fc .getAnArgument ( ) = sink .asExpr ( ) and
678+ // in C, the second argument is the function
679+ f = fc .getArgument ( 1 ) .( FunctionAccess ) .getTarget ( ) and
680+ // in C, the passed argument is always the zeroth argument
681+ result = DataFlow:: exprNode ( f .getParameter ( 0 ) .getAnAccess ( ) )
682+ )
683+
684+ }
685+
686+ }
687+
688+
689+ /**
690+ * In the typical C model, another way to use mutexes is to work with global variables
691+ * that can be initialized at various points -- one of which must be inside a thread.
692+ * This class encapsulates this pattern.
693+ */
694+ class DeclarationInitAccessBasedThreadDependentMutex extends ThreadDependentMutex {
695+
696+ Variable variableSource ;
697+
698+ DeclarationInitAccessBasedThreadDependentMutex ( ) {
699+
700+ exists ( MutexSource ms , ThreadedFunction tf , VariableAccess va |
701+ this = DataFlow:: exprNode ( ms ) and
702+ // accessed as a mutex source
703+ TaintTracking:: localTaint ( DataFlow:: exprNode ( variableSource .getAnAccess ( ) ) , DataFlow:: exprNode ( ms .getAnArgument ( ) ) ) and
704+ // is accessed somewhere else
705+ va = variableSource .getAnAccess ( ) and
706+ sink = DataFlow:: exprNode ( va ) and
707+ // one of which must be a thread
708+ va .getEnclosingFunction ( ) = tf
709+ )
710+ }
711+
712+ override DataFlow:: Node getAUsage ( ) {
713+ result = DataFlow:: exprNode ( variableSource .getAnAccess ( ) )
714+ }
596715}
597716
598717
718+
719+
720+
599721class ThreadDependentMutexTaintTrackingConfiguration extends TaintTracking:: Configuration {
600722 ThreadDependentMutexTaintTrackingConfiguration ( ) {
601723 this = "ThreadDependentMutexTaintTrackingConfiguration"
602724 }
603725
604- override predicate isSource ( DataFlow:: Node node ) { node .asExpr ( ) instanceof MutexSource }
726+ override predicate isSource ( DataFlow:: Node node ) {
727+ node .asExpr ( ) instanceof MutexSource
728+ }
605729
606730 override predicate isSink ( DataFlow:: Node node ) {
607731 exists ( ThreadCreationFunction f | f .getAnArgument ( ) = node .asExpr ( ) )
0 commit comments