Swift: Expand and improve models of Set and Sequence.

This commit is contained in:
Geoffrey White
2023-10-12 22:32:23 +01:00
parent 04c90a684c
commit 60b27a4e69
4 changed files with 69 additions and 31 deletions

View File

@@ -14,21 +14,47 @@ private class SequenceSummaries extends SummaryModelCsv {
override predicate row(string row) {
row =
[
";Sequence;true;sorted();;;Argument[-1];ReturnValue;taint",
";Sequence;true;sorted();;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;sorted(by:);;;Argument[-1];ReturnValue;taint",
";Sequence;true;sorted(by:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;reversed();;;Argument[-1];ReturnValue;taint",
";Sequence;true;reversed();;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;shuffled();;;Argument[-1];ReturnValue;taint",
";Sequence;true;shuffled();;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;shuffled(using:);;;Argument[-1].CollectionElement;ReturnValue;taint",
";Sequence;true;shuffled(using:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;prefix(_:);;;Argument[-1];ReturnValue;taint",
";Sequence;true;prefix(_:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;prefix(while:);;;Argument[-1];ReturnValue;taint",
";Sequence;true;prefix(while:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;suffix(_:);;;Argument[-1];ReturnValue;taint",
";Sequence;true;suffix(_:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;dropFirst(_:);;;Argument[-1];ReturnValue;taint",
";Sequence;true;dropFirst(_:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;dropLast(_:);;;Argument[-1];ReturnValue;taint",
";Sequence;true;dropLast(_:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;drop(while:);;;Argument[-1];ReturnValue;taint",
";Sequence;true;drop(while:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;split(maxSplits:omittingEmptySubsequences:whereSeparator:);;;Argument[-1];ReturnValue;taint",
";Sequence;true;split(maxSplits:omittingEmptySubsequences:whereSeparator:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;split(separator:maxSplits:omittingEmptySubsequences:);;;Argument[-1];ReturnValue;taint",
";Sequence;true;split(separator:maxSplits:omittingEmptySubsequences:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;joined();;;Argument[-1];ReturnValue;taint",
";Sequence;true;joined(separator:);;;Argument[-1..0];ReturnValue;taint",
";Sequence;true;first(where:);;;Argument[-1];ReturnValue;taint",
";Sequence;true;joined();;;Argument[-1].CollectionElement;ReturnValue;taint",
";Sequence;true;joined();;;Argument[-1].CollectionElement.CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;joined(separator:);;;Argument[0..-1];ReturnValue;taint",
";Sequence;true;joined(separator:);;;Argument[-1].CollectionElement;ReturnValue;taint",
";Sequence;true;first(where:);;;Argument[-1].CollectionElement;ReturnValue;value",
";Sequence;true;withContiguousStorageIfAvailable(_:);;;Argument[-1];Argument[0].Parameter[0].CollectionElement;taint",
";Sequence;true;withContiguousStorageIfAvailable(_:);;;Argument[-1].CollectionElement;Argument[0].Parameter[0].CollectionElement;value",
";Sequence;true;withContiguousStorageIfAvailable(_:);;;Argument[0].ReturnValue;ReturnValue.OptionalSome;value",
";Sequence;true;makeIterator();;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value"
";Sequence;true;makeIterator();;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;value",
";Sequence;true;min();;;Argument[-1].CollectionElement;ReturnValue.OptionalSome;taint",
";Sequence;true;min(by:);;;Argument[-1].CollectionElement;ReturnValue.OptionalSome;taint",
";Sequence;true;max();;;Argument[-1].CollectionElement;ReturnValue.OptionalSome;taint",
";Sequence;true;max(by:);;;Argument[-1].CollectionElement;ReturnValue.OptionalSome;taint",
";Sequence;true;formatted();;;Argument[-1].CollectionElement;ReturnValue;taint",
]
}
}

View File

@@ -11,10 +11,22 @@ private class SetSummaries extends SummaryModelCsv {
override predicate row(string row) {
row =
[
";Set;true;insert(_:);;;Argument[-1].CollectionElement;ReturnValue.TupleElement[1];value",
";Set;true;init(_:);;;Argument[0];ReturnValue;taint",
";Set;true;init(_:);;;Argument[0].CollectionElement;ReturnValue.CollectionElement;value",
";Set;true;insert(_:);;;Argument[0];Argument[-1].CollectionElement;value",
";Set;true;insert(_:);;;Argument[0];ReturnValue.TupleElement[1];value",
";Set;true;init(_:);;;Argument[0].CollectionElement;ReturnValue.CollectionElement;value"
";Set;true;insert(_:);;;Argument[0];ReturnValue.TupleElement[1];taint",
";Set;true;update(with:);;;Argument[0];Argument[-1].CollectionElement;value",
";Set;true;update(with:);;;Argument[0];ReturnValue.OptionalSome;taint",
";Set;true;remove(_:);;;Argument[0];ReturnValue.OptionalSome;taint",
";Set;true;removeFirst();;;Argument[-1].CollectionElement;ReturnValue;value",
";Set;true;remove(at:);;;Argument[-1].CollectionElement;ReturnValue;value",
";Set;true;filter(_:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;taint",
";Set;true;union(_:);;;Argument[-1..0].CollectionElement;ReturnValue.CollectionElement;value",
";Set;true;formUnion(_:);;;Argument[0].CollectionElement;Argument[-1].CollectionElement;value",
";Set;true;symmetricDifference(_:);;;Argument[-1..0].CollectionElement;ReturnValue.CollectionElement;taint",
";Set;true;formSymmetricDifference(_:);;;Argument[0].CollectionElement;Argument[-1].CollectionElement;taint",
";Set;true;intersection(_:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;taint",
";Set;true;subtracting(_:);;;Argument[-1].CollectionElement;ReturnValue.CollectionElement;taint",
]
}
}

View File

@@ -24,8 +24,8 @@ func testSet(ix: Int) {
let taintedSet = Set([1, 2, source("t1")])
sink(arg: taintedSet) // $ tainted=t1
sink(arg: taintedSet.randomElement()!) // $ tainted=t1
sink(arg: taintedSet.min()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.max()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.min()!) // $ tainted=t1
sink(arg: taintedSet.max()!) // $ tainted=t1
sink(arg: taintedSet.firstIndex(of: source("t2"))!)
sink(arg: taintedSet[taintedSet.firstIndex(of: source("t3"))!]) // $ tainted=t1
sink(arg: taintedSet.first!) // $ tainted=t1
@@ -53,52 +53,52 @@ func testSet(ix: Int) {
var set2 = Set<Int>()
set2.update(with: source("t5"))
sink(arg: set2.randomElement()!) // $ MISSING: tainted=t5
sink(arg: set2.randomElement()!) // $ tainted=t5
var set3 = Set([source("t6")])
sink(arg: set3.randomElement()!) // $ tainted=t6
let (inserted, previous) = set3.insert(source("t7"))
sink(arg: inserted)
sink(arg: previous) // $ tainted=t6 tainted=t7
sink(arg: previous) // $ tainted=t7
let previous2 = set3.update(with: source("t8"))
sink(arg: previous2!) // $ MISSING: tainted=t8
sink(arg: previous2!) // $ tainted=t8
let previous3 = set3.remove(source("t9"))
sink(arg: previous3!) // $ MISSING: tainted=t9
sink(arg: previous3!) // $ tainted=t9
let previous4 = set3.removeFirst()
sink(arg: previous4) // $ MISSING: tainted=t6
sink(arg: previous4) // $ tainted=t6 tainted=t7 tainted=t8
let previous5 = set3.remove(at: set3.firstIndex(of: source("t10"))!)
sink(arg: previous5) // $ MISSING: tainted=t6
sink(arg: previous5) // $ tainted=t6 tainted=t7 tainted=t8
sink(arg: goodSet.union(goodSet).randomElement()!)
sink(arg: goodSet.union(taintedSet).randomElement()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.union(goodSet).randomElement()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.union(taintedSet).randomElement()!) // $ MISSING: tainted=t1
sink(arg: goodSet.union(taintedSet).randomElement()!) // $ tainted=t1
sink(arg: taintedSet.union(goodSet).randomElement()!) // $ tainted=t1
sink(arg: taintedSet.union(taintedSet).randomElement()!) // $ tainted=t1
var set4 = Set<Int>()
set4.formUnion(goodSet)
sink(arg: set4.randomElement()!)
set4.formUnion(taintedSet)
sink(arg: set4.randomElement()!) // $ MISSING: tainted=t1
sink(arg: set4.randomElement()!) // $ tainted=t1
set4.formUnion(goodSet)
sink(arg: set4.randomElement()!) // $ MISSING: tainted=t1
sink(arg: set4.randomElement()!) // $ tainted=t1
sink(arg: goodSet.intersection(goodSet).randomElement()!)
sink(arg: goodSet.intersection(taintedSet).randomElement()!)
sink(arg: taintedSet.intersection(goodSet).randomElement()!)
sink(arg: taintedSet.intersection(taintedSet).randomElement()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.intersection(goodSet).randomElement()!) // $ SPURIOUS: tainted=t1
sink(arg: taintedSet.intersection(taintedSet).randomElement()!) // $ tainted=t1
sink(arg: goodSet.symmetricDifference(goodSet).randomElement()!)
sink(arg: goodSet.symmetricDifference(taintedSet).randomElement()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.symmetricDifference(goodSet).randomElement()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.symmetricDifference(taintedSet).randomElement()!) // $ MISSING: tainted=t1
sink(arg: goodSet.symmetricDifference(taintedSet).randomElement()!) // $ tainted=t1
sink(arg: taintedSet.symmetricDifference(goodSet).randomElement()!) // $ tainted=t1
sink(arg: taintedSet.symmetricDifference(taintedSet).randomElement()!) // $ tainted=t1
sink(arg: goodSet.subtracting(goodSet).randomElement()!)
sink(arg: goodSet.subtracting(taintedSet).randomElement()!)
sink(arg: taintedSet.subtracting(goodSet).randomElement()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.subtracting(taintedSet).randomElement()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.subtracting(goodSet).randomElement()!) // $ tainted=t1
sink(arg: taintedSet.subtracting(taintedSet).randomElement()!) // $ tainted=t1
sink(arg: taintedSet.sorted().randomElement()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.shuffled().randomElement()!) // $ MISSING: tainted=t1
sink(arg: taintedSet.sorted().randomElement()!) // $ tainted=t1
sink(arg: taintedSet.shuffled().randomElement()!) // $ tainted=t1
sink(arg: taintedSet.lazy[taintedSet.firstIndex(of: source("t11"))!]) // $ tainted=t1

View File

@@ -267,9 +267,9 @@ func taintThroughSimpleStringOperations() {
}))
sink(arg: [clean, clean].joined())
sink(arg: [tainted, clean].joined()) // $ MISSING: tainted=217
sink(arg: [clean, tainted].joined()) // $ MISSING: tainted=217
sink(arg: [tainted, tainted].joined()) // $ MISSING: tainted=217
sink(arg: [tainted, clean].joined()) // $ tainted=217
sink(arg: [clean, tainted].joined()) // $ tainted=217
sink(arg: [tainted, tainted].joined()) // $ tainted=217
sink(arg: clean.description)
sink(arg: tainted.description) // $ tainted=217