@@ -475,12 +475,12 @@ class CPPThreadWait extends ThreadWait {
475
475
}
476
476
477
477
/**
478
- * Models a call to `thread_join ` in C11.
478
+ * Models a call to `thrd_join ` in C11.
479
479
*/
480
- class C11ThreadWait extends FunctionCall {
480
+ class C11ThreadWait extends ThreadWait {
481
481
VariableAccess var ;
482
482
483
- C11ThreadWait ( ) { getTarget ( ) .getName ( ) = "thread_join " }
483
+ C11ThreadWait ( ) { getTarget ( ) .getName ( ) = "thrd_join " }
484
484
}
485
485
486
486
abstract class MutexSource extends FunctionCall { }
@@ -507,38 +507,14 @@ class C11MutexSource extends MutexSource, FunctionCall {
507
507
* came from. For example, if it is passed in from a local function to a thread.
508
508
* This functionality is critical, since it allows one to inspect how the thread
509
509
* 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.
510
513
*/
511
514
abstract class ThreadDependentMutex extends DataFlow:: Node {
515
+
512
516
DataFlow:: Node sink ;
513
517
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
-
542
518
DataFlow:: Node getASource ( ) {
543
519
// the source is either the thing that declared
544
520
// the mutex
@@ -584,24 +560,172 @@ class FlowBasedThreadDependentMutex extends ThreadDependentMutex {
584
560
)
585
561
}
586
562
563
+
587
564
/**
588
565
* Gets a set of usages of this mutex in both the local and thread scope.
589
566
* In the case of scoped usage, this also captures typical accesses of variables.
590
567
*/
591
568
DataFlow:: Node getAUsage ( ) { TaintTracking:: localTaint ( getASource ( ) , result ) }
569
+
592
570
}
593
571
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
+ */
594
588
class 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
+
595
614
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
+ }
596
715
}
597
716
598
717
718
+
719
+
720
+
599
721
class ThreadDependentMutexTaintTrackingConfiguration extends TaintTracking:: Configuration {
600
722
ThreadDependentMutexTaintTrackingConfiguration ( ) {
601
723
this = "ThreadDependentMutexTaintTrackingConfiguration"
602
724
}
603
725
604
- override predicate isSource ( DataFlow:: Node node ) { node .asExpr ( ) instanceof MutexSource }
726
+ override predicate isSource ( DataFlow:: Node node ) {
727
+ node .asExpr ( ) instanceof MutexSource
728
+ }
605
729
606
730
override predicate isSink ( DataFlow:: Node node ) {
607
731
exists ( ThreadCreationFunction f | f .getAnArgument ( ) = node .asExpr ( ) )
0 commit comments