Merge pull request #17034 from MathiasVP/more-alias-and-side-effect-models

C++: Add more alias and side effect models

cpp/ql/lib/semmle/code/cpp/models/Models.qll

@@ -27,6 +27,11 @@ private import implementations.StdPair
 private import implementations.StdMap
 private import implementations.StdSet
 private import implementations.StdString
+private import implementations.StdFunction
+private import implementations.StdException
+private import implementations.StdAllocator
+private import implementations.StdAlgorithm
+private import implementations.StdMath
 private import implementations.Swap
 private import implementations.GetDelim
 private import implementations.SmartPointer

cpp/ql/lib/semmle/code/cpp/models/implementations/Iterator.qll

@@ -86,6 +86,41 @@ private class StdIterator extends Iterator, Class {
   override Type getValueType() { result = this.getTemplateArgument(1).(Type).getUnderlyingType() }
 }
 
+private class StdReverseIterator extends Iterator, Class {
+  StdReverseIterator() { this.hasQualifiedName(["std", "bsl"], "reverse_iterator") }
+
+  override Type getValueType() { result = this.getTemplateArgument(1).(Type).getUnderlyingType() }
+}
+
+private class StdIstreamBufIterator extends Iterator, Class {
+  StdIstreamBufIterator() { this.hasQualifiedName(["std", "bsl"], "istreambuf_iterator") }
+
+  override Type getValueType() { result = this.getTemplateArgument(1).(Type).getUnderlyingType() }
+}
+
+private class StdIstreambufIteratorConstructor extends Constructor, SideEffectFunction,
+  AliasFunction
+{
+  StdIstreambufIteratorConstructor() { this.getDeclaringType() instanceof StdIstreamBufIterator }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and
+    buffer = false
+  }
+}
+
 /**
  * Gets the `FunctionInput` corresponding to an iterator parameter to
  * user-defined operator `op`, at `index`.
@@ -579,23 +614,43 @@ private class IteratorAssignmentMemberOperatorModel extends IteratorAssignmentMe
   override predicate parameterEscapesOnlyViaReturn(int index) { index = -1 }
 }
 
+private string beginName() {
+  result = ["begin", "cbegin", "rbegin", "crbegin", "before_begin", "cbefore_begin"]
+}
+
 /**
  * A `begin` member function, or a related function, that returns an iterator.
  */
-class BeginFunction extends MemberFunction {
+class BeginFunction extends Function {
   BeginFunction() {
-    this.hasName(["begin", "cbegin", "rbegin", "crbegin", "before_begin", "cbefore_begin"]) and
-    this.getType().getUnspecifiedType() instanceof Iterator
+    this.getUnspecifiedType() instanceof Iterator and
+    (
+      this.hasName(beginName()) and
+      this instanceof MemberFunction
+      or
+      this.hasGlobalOrStdOrBslName(beginName()) and
+      not this instanceof MemberFunction and
+      this.getNumberOfParameters() = 1
+    )
   }
 }
 
+private string endName() { result = ["end", "cend", "rend", "crend"] }
+
 /**
  * An `end` member function, or a related function, that returns an iterator.
  */
-class EndFunction extends MemberFunction {
+class EndFunction extends Function {
   EndFunction() {
-    this.hasName(["end", "cend", "rend", "crend"]) and
-    this.getType().getUnspecifiedType() instanceof Iterator
+    this.getUnspecifiedType() instanceof Iterator and
+    (
+      this.hasName(endName()) and
+      this instanceof MemberFunction
+      or
+      this.hasGlobalOrStdOrBslName(endName()) and
+      this instanceof MemberFunction and
+      this.getNumberOfParameters() = 1
+    )
   }
 }
 
@@ -603,7 +658,7 @@ class EndFunction extends MemberFunction {
  * A `begin` or `end` member function, or a related member function, that
  * returns an iterator.
  */
-class BeginOrEndFunction extends MemberFunction {
+class BeginOrEndFunction extends Function {
   BeginOrEndFunction() {
     this instanceof BeginFunction or
     this instanceof EndFunction

cpp/ql/lib/semmle/code/cpp/models/implementations/Printf.qll

@@ -7,6 +7,7 @@
 
 import semmle.code.cpp.models.interfaces.FormattingFunction
 import semmle.code.cpp.models.interfaces.Alias
+import semmle.code.cpp.models.interfaces.SideEffect
 
 /**
  * The standard functions `printf`, `wprintf` and their glib variants.
@@ -96,7 +97,7 @@ private class Sprintf extends FormattingFunction {
 /**
  * Implements `Snprintf`.
  */
-private class SnprintfImpl extends Snprintf {
+private class SnprintfImpl extends Snprintf, AliasFunction, SideEffectFunction {
   SnprintfImpl() {
     this instanceof TopLevelFunction and
     (
@@ -143,6 +144,26 @@ private class SnprintfImpl extends Snprintf {
   }
 
   override int getSizeParameterIndex() { result = 1 }
+
+  override predicate parameterNeverEscapes(int index) {
+    // We don't know how many parameters are passed to the function since it's varargs, but they also don't escape.
+    index = this.getFormatParameterIndex()
+  }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = this.getOutputParameterIndex(false) and buffer = true and mustWrite = false
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    // We don't know how many parameters are passed to the function since it's varargs, but they also have read side effects.
+    i = this.getFormatParameterIndex() and buffer = true
+  }
 }
 
 /**

cpp/ql/lib/semmle/code/cpp/models/implementations/StdAlgorithm.qll

@@ -0,0 +1,115 @@
+/**
+ * Provides models for C++ functions from the `algorithms` header.
+ */
+
+import semmle.code.cpp.models.interfaces.Taint
+import semmle.code.cpp.models.interfaces.DataFlow
+import semmle.code.cpp.models.interfaces.Iterator
+import semmle.code.cpp.models.interfaces.SideEffect
+import semmle.code.cpp.models.interfaces.Alias
+
+private class StdPartialSort extends Function, SideEffectFunction, AliasFunction {
+  StdPartialSort() { this.hasGlobalOrStdName("partial_sort") }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = this.getAnIteratorParameterIndex() and buffer = true and mustWrite = false
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = this.getAnIteratorParameterIndex() and
+    buffer = true and
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and
+    buffer = false
+  }
+
+  private int getAnIteratorParameterIndex() {
+    this.getParameter(result).getUnspecifiedType() instanceof Iterator
+  }
+
+  override predicate parameterNeverEscapes(int index) {
+    index = this.getAnIteratorParameterIndex()
+    or
+    this.getParameter(index).getUnspecifiedType() instanceof ReferenceType
+  }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+}
+
+private class StdSortHeap extends Function, SideEffectFunction, AliasFunction {
+  StdSortHeap() { this.hasGlobalOrStdName("sort_heap") }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = this.getAnIteratorParameterIndex() and buffer = true and mustWrite = false
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = this.getAnIteratorParameterIndex() and
+    buffer = true
+  }
+
+  private int getAnIteratorParameterIndex() {
+    this.getParameter(result).getUnspecifiedType() instanceof Iterator
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = this.getAnIteratorParameterIndex() }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+}
+
+private class StdGenerateN extends Function, SideEffectFunction, AliasFunction {
+  StdGenerateN() { this.hasGlobalOrStdName("generate_n") }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = this.getAnIteratorParameterIndex() and buffer = true and mustWrite = false
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and buffer = false
+  }
+
+  private int getAnIteratorParameterIndex() {
+    this.getParameter(result).getUnspecifiedType() instanceof Iterator
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = this.getAnIteratorParameterIndex() }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+}
+
+private class StdFindIfOrIfNot extends Function, SideEffectFunction, AliasFunction {
+  StdFindIfOrIfNot() { this.hasGlobalOrStdName(["find_if", "find_if_not"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = this.getAnIteratorParameterIndex() and buffer = true
+    or
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and buffer = false
+  }
+
+  private int getAnIteratorParameterIndex() {
+    this.getParameter(result).getUnspecifiedType() instanceof Iterator
+  }
+
+  override predicate parameterNeverEscapes(int index) {
+    this.getParameter(index).getUnspecifiedType() instanceof ReferenceType
+  }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) {
+    index = this.getAnIteratorParameterIndex()
+  }
+}

cpp/ql/lib/semmle/code/cpp/models/implementations/StdAllocator.qll

@@ -0,0 +1,256 @@
+/**
+ * Provides models for C++ `allocator` and `allocator_traits` classes.
+ */
+
+import semmle.code.cpp.models.interfaces.SideEffect
+import semmle.code.cpp.models.interfaces.Alias
+
+/** The `std::allocator` class. */
+class StdAllocator extends Class {
+  StdAllocator() { this.hasGlobalOrStdOrBslName("allocator") }
+}
+
+/** The `std::allocator_traits` class. */
+class StdAllocatorTraits extends Class {
+  StdAllocatorTraits() { this.hasGlobalOrStdOrBslName("allocator_traits") }
+}
+
+private class StdAllocatorConstructor extends Constructor, AliasFunction, SideEffectFunction {
+  StdAllocatorConstructor() { this.getDeclaringType() instanceof StdAllocator }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and
+    buffer = false and
+    mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and buffer = false
+  }
+}
+
+private class StdAllocatorDestructor extends Destructor, AliasFunction, SideEffectFunction {
+  StdAllocatorDestructor() { this.getDeclaringType() instanceof StdAllocator }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and
+    buffer = false and
+    mustWrite = true
+  }
+}
+
+private class StdAllocatorAddress extends MemberFunction, AliasFunction, SideEffectFunction {
+  StdAllocatorAddress() { this.getClassAndName("address") instanceof StdAllocator }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class StdAllocatorAllocate extends MemberFunction, AliasFunction, SideEffectFunction {
+  StdAllocatorAllocate() { this.getClassAndName("allocate") instanceof StdAllocator }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class StdAllocatorTraitsAllocate extends MemberFunction, AliasFunction, SideEffectFunction {
+  StdAllocatorTraitsAllocate() {
+    this.getClassAndName(["allocate", "allocate_at_least"]) instanceof StdAllocatorTraits
+  }
+
+  override predicate parameterNeverEscapes(int index) {
+    this.getParameter(index).getUnspecifiedType() instanceof ReferenceType
+  }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and buffer = false
+  }
+}
+
+private class StdAllocatorDeallocate extends MemberFunction, AliasFunction, SideEffectFunction {
+  StdAllocatorDeallocate() { this.getClassAndName("deallocate") instanceof StdAllocator }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = 0 and
+    buffer = false and
+    mustWrite = false
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = 0 and
+    buffer = false
+  }
+}
+
+private class StdAllocatorTraitsDeallocate extends MemberFunction, AliasFunction, SideEffectFunction
+{
+  StdAllocatorTraitsDeallocate() {
+    this.getClassAndName("deallocate") instanceof StdAllocatorTraits
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = [0, 1] }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = 1 and
+    buffer = false and
+    mustWrite = false
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = [0, 1] and
+    buffer = false
+  }
+}
+
+private class StdAllocatorMaxSize extends MemberFunction, AliasFunction, SideEffectFunction {
+  StdAllocatorMaxSize() { this.getClassAndName("max_size") instanceof StdAllocator }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class StdAllocatTraitsMaxSize extends MemberFunction, AliasFunction, SideEffectFunction {
+  StdAllocatTraitsMaxSize() { this.getClassAndName("max_size") instanceof StdAllocatorTraits }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class StdAllocatorConstruct extends MemberFunction, AliasFunction, SideEffectFunction {
+  StdAllocatorConstruct() { this.getClassAndName("construct") instanceof StdAllocator }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = 0 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and buffer = false
+  }
+}
+
+class StdAllocatorTraitsConstruct extends MemberFunction, AliasFunction, SideEffectFunction {
+  StdAllocatorTraitsConstruct() { this.getClassAndName("construct") instanceof StdAllocatorTraits }
+
+  override predicate parameterNeverEscapes(int index) {
+    index = 1 or this.getParameter(index).getUnspecifiedType() instanceof ReferenceType
+  }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = 1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and
+    buffer = false
+  }
+}
+
+class StdAllocatorDestroy extends MemberFunction, AliasFunction, SideEffectFunction {
+  StdAllocatorDestroy() { this.getClassAndName("destroy") instanceof StdAllocator }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = 0 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = 0 and buffer = false
+  }
+}
+
+class StdAllocatorTraitsDestroy extends MemberFunction, AliasFunction, SideEffectFunction {
+  StdAllocatorTraitsDestroy() { this.getClassAndName("destroy") instanceof StdAllocatorTraits }
+
+  override predicate parameterNeverEscapes(int index) { index = [0, 1] }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = 1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = 0 and buffer = false
+  }
+}

cpp/ql/lib/semmle/code/cpp/models/implementations/StdContainer.qll

@@ -4,6 +4,8 @@
 
 import semmle.code.cpp.models.interfaces.FlowSource
 import semmle.code.cpp.models.interfaces.Iterator
+import semmle.code.cpp.models.interfaces.SideEffect
+import semmle.code.cpp.models.interfaces.Alias
 
 /**
  * A sequence container template class (for example, `std::vector`) from the
@@ -58,7 +60,7 @@ private class Vector extends StdSequenceContainer {
 /**
  * The standard container functions `push_back` and `push_front`.
  */
-class StdSequenceContainerPush extends MemberFunction {
+class StdSequenceContainerPush extends MemberFunction, SideEffectFunction, AliasFunction {
   StdSequenceContainerPush() {
     this.getClassAndName("push_back") instanceof Vector or
     this.getClassAndName(["push_back", "push_front"]) instanceof Deque or
@@ -74,12 +76,115 @@ class StdSequenceContainerPush extends MemberFunction {
     this.getParameter(result).getUnspecifiedType().(ReferenceType).getBaseType() =
       this.getDeclaringType().getTemplateArgument(0).(Type).getUnspecifiedType() // i.e. the `T` of this `std::vector<T>`
   }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and
+    buffer = false and
+    mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    // the `std::vector<bool>` specialization doesn't take a reference as a
+    // parameter. So we need to check that the parameter is actually a
+    // reference.
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and
+    buffer = false
+  }
+}
+
+private class StdSequenceContainerPopFrontOrBack extends MemberFunction, SideEffectFunction,
+  AliasFunction
+{
+  StdSequenceContainerPopFrontOrBack() {
+    this.getClassAndName("pop_back") instanceof Vector or
+    this.getClassAndName("pop_front") instanceof ForwardList or
+    this.getClassAndName(["pop_front", "pop_back"]) instanceof Deque or
+    this.getClassAndName(["pop_front", "pop_back"]) instanceof List
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and
+    buffer = false and
+    mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and
+    buffer = false
+  }
+}
+
+private class StdSequenceContainerClear extends MemberFunction, SideEffectFunction, AliasFunction {
+  StdSequenceContainerClear() {
+    this.getClassAndName("clear") instanceof Vector or
+    this.getClassAndName("clear") instanceof Deque or
+    this.getClassAndName("clear") instanceof ForwardList or
+    this.getClassAndName("clear") instanceof List
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and
+    buffer = false and
+    mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and
+    buffer = false
+  }
+}
+
+private class StdVectorReserve extends MemberFunction, SideEffectFunction, AliasFunction {
+  StdVectorReserve() { this.getClassAndName("reserve") instanceof Vector }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and
+    buffer = false and
+    mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and
+    buffer = false
+  }
 }
 
 /**
  * The standard container functions `insert` and `insert_after`.
  */
-class StdSequenceContainerInsert extends MemberFunction {
+class StdSequenceContainerInsert extends MemberFunction, SideEffectFunction, AliasFunction {
   StdSequenceContainerInsert() {
     this.getClassAndName("insert") instanceof Deque or
     this.getClassAndName("insert") instanceof List or
@@ -100,17 +205,138 @@ class StdSequenceContainerInsert extends MemberFunction {
    * Gets the index of a parameter to this function that is an iterator.
    */
   int getAnIteratorParameterIndex() { this.getParameter(result).getType() instanceof Iterator }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and
+    buffer = false and
+    mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and
+    buffer = false
+  }
+}
+
+private class StdSequenceContainerFrontBack extends MemberFunction, SideEffectFunction,
+  AliasFunction
+{
+  StdSequenceContainerFrontBack() {
+    this.getClassAndName(["front", "back"]) instanceof Deque or
+    this.getClassAndName(["front", "back"]) instanceof List or
+    this.getClassAndName(["front", "back"]) instanceof Vector or
+    // forward_list does not have a 'back' member function
+    this.getClassAndName("front") instanceof ForwardList
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
 }
 
 /**
  * The standard container functions `at` and `operator[]`.
  */
-class StdSequenceContainerAt extends MemberFunction {
+class StdSequenceContainerAt extends MemberFunction, SideEffectFunction, AliasFunction {
   StdSequenceContainerAt() {
     this.getClassAndName(["at", "operator[]"]) instanceof Array or
     this.getClassAndName(["at", "operator[]"]) instanceof Deque or
     this.getClassAndName(["at", "operator[]"]) instanceof Vector
   }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    none()
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
+}
+
+private class StdSequenceContainerMemberEquals extends MemberFunction, SideEffectFunction,
+  AliasFunction
+{
+  StdSequenceContainerMemberEquals() {
+    this.getClassAndName("operator==") instanceof Array or
+    this.getClassAndName("operator==") instanceof Deque or
+    this.getClassAndName("operator==") instanceof Vector
+  }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 or index = 0 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    none()
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+    or
+    i = 0 and buffer = false
+  }
+}
+
+private class StdSequenceContainerEquals extends Function, SideEffectFunction, AliasFunction {
+  StdSequenceContainerEquals() {
+    this.hasGlobalOrStdOrBslName("operator==") and
+    not this instanceof MemberFunction and
+    this.getNumberOfParameters() = 2 and
+    (
+      this.getParameter(0).getUnspecifiedType().(ReferenceType).getBaseType() instanceof Vector and
+      this.getParameter(1).getUnspecifiedType().(ReferenceType).getBaseType() instanceof Vector
+      or
+      this.getParameter(0).getUnspecifiedType().(ReferenceType).getBaseType() instanceof List and
+      this.getParameter(1).getUnspecifiedType().(ReferenceType).getBaseType() instanceof List
+      or
+      this.getParameter(0).getUnspecifiedType().(ReferenceType).getBaseType() instanceof Deque and
+      this.getParameter(1).getUnspecifiedType().(ReferenceType).getBaseType() instanceof Deque
+    )
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = 0 or index = 1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    none()
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = [0, 1] and buffer = false
+  }
 }
 
 /**
@@ -142,6 +368,115 @@ class StdVectorEmplace extends StdSequenceEmplace {
   StdVectorEmplace() { this.getDeclaringType() instanceof Vector }
 }
 
+private class StdSequenceSize extends MemberFunction, SideEffectFunction, AliasFunction {
+  StdSequenceSize() {
+    this.getClassAndName("size") instanceof Vector
+    or
+    this.getClassAndName("size") instanceof List
+    or
+    this.getClassAndName("size") instanceof Deque
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
+}
+
+private class StdSequenceDestructor extends Destructor, SideEffectFunction, AliasFunction {
+  StdSequenceDestructor() {
+    this.getDeclaringType() instanceof Vector
+    or
+    this.getDeclaringType() instanceof List
+    or
+    this.getDeclaringType() instanceof Deque
+  }
+
+  private Destructor getElementDestructor() {
+    result.getDeclaringType() = this.getTemplateArgument(0)
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() {
+    this.getElementDestructor().(SideEffectFunction).hasOnlySpecificReadSideEffects()
+    or
+    not exists(this.getElementDestructor())
+  }
+
+  override predicate hasOnlySpecificWriteSideEffects() {
+    this.getElementDestructor().(SideEffectFunction).hasOnlySpecificWriteSideEffects()
+    or
+    not exists(this.getElementDestructor())
+  }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
+}
+
+private class StdSequenceConstructor extends Constructor, SideEffectFunction, AliasFunction {
+  StdSequenceConstructor() {
+    this.getDeclaringType() instanceof Vector
+    or
+    this.getDeclaringType() instanceof List
+    or
+    this.getDeclaringType() instanceof Deque
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and
+    buffer = false
+  }
+}
+
+private class InitializerList extends Class {
+  InitializerList() { this.hasQualifiedName(["std", "bsl"], "initializer_list") }
+
+  Type getElementType() { result = this.getTemplateArgument(0) }
+}
+
+private class InitializerListConstructor extends Constructor, SideEffectFunction, AliasFunction {
+  InitializerListConstructor() { this.getDeclaringType() instanceof InitializerList }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+}
+
 /**
  * The standard vector `emplace_back` function.
  */

cpp/ql/lib/semmle/code/cpp/models/implementations/StdException.qll

@@ -0,0 +1,38 @@
+/**
+ * Provides models for the C++ `std::exception` class and subclasses.
+ */
+
+import semmle.code.cpp.models.interfaces.Taint
+import semmle.code.cpp.models.interfaces.Alias
+import semmle.code.cpp.models.interfaces.SideEffect
+
+/** The `std::exception` class. */
+class StdException extends Class {
+  StdException() { this.hasGlobalOrStdOrBslName("exception") }
+}
+
+/** The `std::bad_alloc` class. */
+class StdBadAllocException extends Class {
+  StdBadAllocException() { this.hasGlobalOrStdOrBslName("bad_alloc") }
+}
+
+private class StdBadAllocExceptionConstructor extends Constructor, SideEffectFunction, AliasFunction
+{
+  StdBadAllocExceptionConstructor() { this.getDeclaringType() instanceof StdBadAllocException }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and buffer = false
+  }
+}

cpp/ql/lib/semmle/code/cpp/models/implementations/StdFunction.qll

@@ -0,0 +1,53 @@
+/**
+ * Provides models for C++ `std::function` class.
+ */
+
+import semmle.code.cpp.models.interfaces.SideEffect
+import semmle.code.cpp.models.interfaces.Alias
+
+/**
+ * An instantiation of the `std::function` class template.
+ */
+class StdFunction extends ClassTemplateInstantiation {
+  StdFunction() { this.hasGlobalOrStdOrBslName("function") }
+}
+
+private class StdFunctionConstructor extends Constructor, SideEffectFunction, AliasFunction {
+  StdFunctionConstructor() { this.getDeclaringType() instanceof StdFunction }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and buffer = false
+  }
+}
+
+private class StdFunctionDestructor extends Destructor, SideEffectFunction, AliasFunction {
+  StdFunctionDestructor() { this.getDeclaringType() instanceof StdFunction }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
+}

cpp/ql/lib/semmle/code/cpp/models/implementations/StdMap.qll

@@ -5,6 +5,8 @@
 import semmle.code.cpp.models.interfaces.Taint
 import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Iterator
+import semmle.code.cpp.models.interfaces.SideEffect
+import semmle.code.cpp.models.interfaces.Alias
 
 /**
  * The `std::map` and `std::unordered_map` template classes.
@@ -16,7 +18,9 @@ private class MapOrUnorderedMap extends Class {
 /**
  * Additional model for map constructors using iterator inputs.
  */
-private class StdMapConstructor extends Constructor, TaintFunction {
+private class StdMapConstructor extends Constructor, TaintFunction, AliasFunction,
+  SideEffectFunction
+{
   StdMapConstructor() { this.getDeclaringType() instanceof MapOrUnorderedMap }
 
   /**
@@ -35,6 +39,23 @@ private class StdMapConstructor extends Constructor, TaintFunction {
       output.isQualifierObject()
     )
   }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and
+    buffer = false
+  }
 }
 
 /**
@@ -133,7 +154,7 @@ class StdMapAt extends MemberFunction {
   StdMapAt() { this.getClassAndName(["at", "operator[]"]) instanceof MapOrUnorderedMap }
 }
 
-private class StdMapAtModels extends StdMapAt, TaintFunction {
+private class StdMapAtModels extends StdMapAt, TaintFunction, AliasFunction, SideEffectFunction {
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // flow from qualifier to referenced return value
     input.isQualifierObject() and
@@ -144,6 +165,18 @@ private class StdMapAtModels extends StdMapAt, TaintFunction {
     output.isQualifierObject()
   }
 
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
+
   override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
@@ -187,3 +220,63 @@ private class StdMapEqualRange extends TaintFunction {
     output.isReturnValue()
   }
 }
+
+class StdMapDestructor extends Destructor, SideEffectFunction, AliasFunction {
+  StdMapDestructor() { this.getDeclaringType() instanceof MapOrUnorderedMap }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
+}
+
+private class StdMapClear extends MemberFunction, SideEffectFunction, AliasFunction {
+  StdMapClear() { this.getClassAndName("clear") instanceof MapOrUnorderedMap }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and
+    buffer = false and
+    mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and
+    buffer = false
+  }
+}
+
+class StdMapSize extends MemberFunction, SideEffectFunction, AliasFunction {
+  StdMapSize() { this.getClassAndName("size") instanceof MapOrUnorderedMap }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and
+    buffer = false
+  }
+}

cpp/ql/lib/semmle/code/cpp/models/implementations/StdMath.qll

@@ -0,0 +1,98 @@
+/**
+ * Provides models for C++ functions from the `cmath` header.
+ */
+
+private import semmle.code.cpp.models.interfaces.SideEffect
+private import semmle.code.cpp.models.interfaces.Alias
+
+private class LdExp extends Function, SideEffectFunction {
+  LdExp() { this.hasGlobalOrStdOrBslName(["ldexp", "ldexpf", "ldexpl"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class Abs extends Function, SideEffectFunction {
+  Abs() { this.hasGlobalOrStdOrBslName(["abs", "fabs", "fabsf", "fabsl", "llabs", "imaxabs"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class Div extends Function, SideEffectFunction {
+  Div() { this.hasGlobalOrStdOrBslName(["div", "ldiv", "lldiv", "imaxdiv"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class FMod extends Function, SideEffectFunction {
+  FMod() { this.hasGlobalOrStdOrBslName(["fmod", "fmodf", "fmodl"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class Remainder extends Function, SideEffectFunction {
+  Remainder() { this.hasGlobalOrStdOrBslName(["remainder", "remainderf", "remainderl"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class Remquo extends Function, SideEffectFunction {
+  Remquo() { this.hasGlobalOrStdOrBslName(["remquo", "remquof", "remquol"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class Fma extends Function, SideEffectFunction {
+  Fma() { this.hasGlobalOrStdOrBslName(["fma", "fmaf", "fmal"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class Fmax extends Function, SideEffectFunction {
+  Fmax() { this.hasGlobalOrStdOrBslName(["fmax", "fmaxf", "fmaxl"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class Fmin extends Function, SideEffectFunction {
+  Fmin() { this.hasGlobalOrStdOrBslName(["fmin", "fminf", "fminl"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class Fdim extends Function, SideEffectFunction {
+  Fdim() { this.hasGlobalOrStdOrBslName(["fdim", "fdimf", "fdiml"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+}
+
+private class Nan extends Function, SideEffectFunction, AliasFunction {
+  Nan() { this.hasGlobalOrStdOrBslName(["nan", "nanf", "nanl"]) }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate parameterNeverEscapes(int index) { index = 0 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+}

cpp/ql/lib/semmle/code/cpp/models/implementations/StdPair.qll

@@ -3,6 +3,8 @@
  */
 
 import semmle.code.cpp.models.interfaces.Taint
+import semmle.code.cpp.models.interfaces.Alias
+import semmle.code.cpp.models.interfaces.SideEffect
 
 /**
  * An instantiation of `std::pair<T1, T2>`.
@@ -37,7 +39,9 @@ class StdPairCopyishConstructor extends Constructor, TaintFunction {
 /**
  * Additional model for `std::pair` constructors.
  */
-private class StdPairConstructor extends Constructor, TaintFunction {
+private class StdPairConstructor extends Constructor, TaintFunction, AliasFunction,
+  SideEffectFunction
+{
   StdPairConstructor() { this.getDeclaringType() instanceof StdPair }
 
   /**
@@ -59,4 +63,77 @@ private class StdPairConstructor extends Constructor, TaintFunction {
       output.isQualifierObject()
     )
   }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    // All the constructor parameters are references with the exception of this one:
+    // ```
+    // template<class... Args1, class... Args2>
+    // pair(std::piecewise_construct_t, std::tuple<Args1...> first_args, std::tuple<Args2...> second_args);
+    // ```
+    // So we need to check that the parameters are actually references
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and
+    buffer = false
+  }
+}
+
+private class StdPairDestructor extends Destructor, AliasFunction, SideEffectFunction {
+  StdPairDestructor() { this.getDeclaringType() instanceof StdPair }
+
+  private Type getFirstType() { result = this.getDeclaringType().getTemplateArgument(0) }
+
+  private Type getSecondType() { result = this.getDeclaringType().getTemplateArgument(0) }
+
+  private Type getAType() { result = [this.getFirstType(), this.getSecondType()] }
+
+  /**
+   * Gets the destructor associated with the base type of this pair
+   */
+  private Destructor getADestructor() { result.getDeclaringType() = this.getAType() }
+
+  override predicate hasOnlySpecificReadSideEffects() {
+    this.getADestructor().(SideEffectFunction).hasOnlySpecificReadSideEffects()
+    or
+    // If there's no declared destructor for the base type then it won't have
+    // any strange read side effects.
+    not exists(this.getADestructor())
+  }
+
+  override predicate hasOnlySpecificWriteSideEffects() {
+    this.getADestructor().(SideEffectFunction).hasOnlySpecificWriteSideEffects()
+    or
+    // If there's no declared destructor for the base type then it won't have
+    // any strange write side effects.
+    not exists(this.getADestructor())
+  }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate parameterNeverEscapes(int index) {
+    this.getADestructor().(AliasFunction).parameterNeverEscapes(index)
+    or
+    // If there's no declared destructor for the base type then it won't cause
+    // anything to escape.
+    not exists(this.getADestructor()) and
+    index = -1
+  }
 }

cpp/ql/lib/semmle/code/cpp/models/implementations/StdString.qll

@@ -7,6 +7,8 @@
 import semmle.code.cpp.models.interfaces.Taint
 import semmle.code.cpp.models.interfaces.Iterator
 import semmle.code.cpp.models.interfaces.DataFlow
+import semmle.code.cpp.models.interfaces.SideEffect
+import semmle.code.cpp.models.interfaces.Alias
 
 /**
  * The `std::basic_string` template class instantiations.
@@ -78,7 +80,9 @@ abstract private class StdStringTaintFunction extends TaintFunction {
  * std::string b(a.begin(), a.end());
  * ```
  */
-private class StdStringConstructor extends Constructor, StdStringTaintFunction {
+private class StdStringConstructor extends Constructor, StdStringTaintFunction, SideEffectFunction,
+  AliasFunction
+{
   StdStringConstructor() { this.getDeclaringType() instanceof StdBasicString }
 
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
@@ -94,6 +98,42 @@ private class StdStringConstructor extends Constructor, StdStringTaintFunction {
       output.isQualifierObject()
     )
   }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
+}
+
+private class StdStringDestructor extends Destructor, SideEffectFunction, AliasFunction {
+  StdStringDestructor() { this.getDeclaringType() instanceof StdBasicString }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
 }
 
 /**
@@ -164,7 +204,7 @@ private class StdStringFrontBack extends StdStringTaintFunction {
 /**
  * The (non-member) `std::string` function `operator+`.
  */
-private class StdStringPlus extends StdStringTaintFunction {
+private class StdStringPlus extends StdStringTaintFunction, SideEffectFunction, AliasFunction {
   StdStringPlus() {
     this.hasQualifiedName(["std", "bsl"], "operator+") and
     this.getUnspecifiedType() instanceof StdBasicString
@@ -178,6 +218,22 @@ private class StdStringPlus extends StdStringTaintFunction {
     ) and
     output.isReturnValue()
   }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    this.getParameter(i).getUnspecifiedType() instanceof ReferenceType and
+    buffer = false
+    or
+    this.getParameter(i).getUnspecifiedType() instanceof PointerType and
+    buffer = true
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = [0, 1] }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
 }
 
 /**
@@ -185,7 +241,7 @@ private class StdStringPlus extends StdStringTaintFunction {
  * All of these functions combine the existing string with a new
  * string (or character) from one of the arguments.
  */
-private class StdStringAppend extends StdStringTaintFunction {
+private class StdStringAppend extends StdStringTaintFunction, SideEffectFunction, AliasFunction {
   StdStringAppend() {
     this.getClassAndName(["operator+=", "append", "replace"]) instanceof StdBasicString
   }
@@ -210,6 +266,22 @@ private class StdStringAppend extends StdStringTaintFunction {
   }
 
   override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and mustWrite = false and buffer = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = [-1, 0] and buffer = true
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = [-1, 0] }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
 }
 
 /**
@@ -301,7 +373,7 @@ private class StdStringSubstr extends StdStringTaintFunction {
 /**
  * The `std::string` functions `at` and `operator[]`.
  */
-private class StdStringAt extends StdStringTaintFunction {
+private class StdStringAt extends StdStringTaintFunction, SideEffectFunction, AliasFunction {
   StdStringAt() { this.getClassAndName(["at", "operator[]"]) instanceof StdBasicString }
 
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
@@ -315,6 +387,22 @@ private class StdStringAt extends StdStringTaintFunction {
   }
 
   override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    none()
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
 }
 
 /**
@@ -324,6 +412,54 @@ private class StdBasicIStream extends ClassTemplateInstantiation {
   StdBasicIStream() { this.hasQualifiedName(["std", "bsl"], "basic_istream") }
 }
 
+private class StdBasicIfStream extends ClassTemplateInstantiation {
+  StdBasicIfStream() { this.hasQualifiedName(["std", "bsl"], "basic_ifstream") }
+}
+
+class StdBasicIfStreamConstructor extends Constructor, SideEffectFunction, AliasFunction {
+  StdBasicIfStreamConstructor() { this.getDeclaringType() instanceof StdBasicIfStream }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    exists(Type t | t = this.getParameter(i).getUnspecifiedType() |
+      t instanceof PointerType and buffer = true
+      or
+      t instanceof ReferenceType and buffer = false
+    )
+  }
+}
+
+class StdBasicIfStreamDestructor extends Destructor, SideEffectFunction, AliasFunction {
+  StdBasicIfStreamDestructor() { this.getDeclaringType() instanceof StdBasicIfStream }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
+}
+
 /**
  * The `std::istream` function `operator>>` (defined as a member function).
  */
@@ -542,6 +678,33 @@ private class StdBasicOStream extends ClassTemplateInstantiation {
   StdBasicOStream() { this.hasQualifiedName(["std", "bsl"], "basic_ostream") }
 }
 
+private class StdStringLessThan extends Function, AliasFunction, SideEffectFunction {
+  StdStringLessThan() {
+    this.hasQualifiedName(["std", "bsl"], "operator<") and
+    this.getNumberOfParameters() = 2 and
+    this.getParameter(0).getUnspecifiedType().(ReferenceType).getBaseType() instanceof
+      StdBasicString and
+    this.getParameter(1).getUnspecifiedType().(ReferenceType).getBaseType() instanceof
+      StdBasicString
+  }
+
+  override predicate parameterNeverEscapes(int index) { index = [0, 1] }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    none()
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = [0, 1] and buffer = false
+  }
+}
+
 /**
  * The `std::ostream` functions `operator<<` (defined as a member function),
  * `put` and `write`.