Commit Graph

18 Commits

Author SHA1 Message Date
Tom Hvitved
7024b07dd2 Java: Adapt to changes in FlowSummaryImpl
Missing manual models were added using the following code added to `FlowSummaryImpl.qll`:

```ql
    private predicate testsummaryElement(
      Input::SummarizedCallableBase c, string namespace, string type, boolean subtypes, string name,
      string signature, string ext, string originalInput, string originalOutput, string kind,
      string provenance, string model, boolean isExact
    ) {
      exists(string input, string output, Callable baseCallable |
        summaryModel(namespace, type, subtypes, name, signature, ext, originalInput, originalOutput,
          kind, provenance, model) and
        baseCallable = interpretElement(namespace, type, subtypes, name, signature, ext, isExact) and
        (
          c.asCallable() = baseCallable and input = originalInput and output = originalOutput
          or
          correspondingKotlinParameterDefaultsArgSpec(baseCallable, c.asCallable(), originalInput,
            input) and
          correspondingKotlinParameterDefaultsArgSpec(baseCallable, c.asCallable(), originalOutput,
            output)
        )
      )
    }

    private predicate testsummaryElement2(
      string namespace, string type, boolean subtypes, string name, string signature, string ext,
      string originalInput, string originalOutput, string kind, string provenance, string model,
      string namespace2, string type2
    ) {
      exists(Input::SummarizedCallableBase c |
        testsummaryElement(c, namespace2, type2, _, _, _, ext, originalInput, originalOutput, kind,
          provenance, model, false) and
        testsummaryElement(c, namespace, type, subtypes, name, _, _, _, _, _, provenance, _, true) and
        signature = paramsString(c.asCallable()) and
        not testsummaryElement(c, _, _, _, _, _, _, originalInput, originalOutput, kind, provenance,
          _, true)
      )
    }

    private string getAMissingManualModel(string namespace2, string type2) {
      exists(
        string namespace, string type, boolean subtypes, string name, string signature, string ext,
        string originalInput, string originalOutput, string kind, string provenance, string model
      |
        testsummaryElement2(namespace, type, subtypes, name, signature, ext, originalInput,
          originalOutput, kind, provenance, model, namespace2, type2) and
        result =
          "- [\"" + namespace + "\", \"" + type + "\", True, \"" + name + "\", \"" + signature +
            "\", \"\", \"" + originalInput + "\", \"" + originalOutput + "\", \"" + kind + "\", \"" +
            provenance + "\"]"
      )
    }
```
2026-01-26 12:40:15 +01:00
yoff
cbc0100675 Apply suggestion from @Copilot 2025-12-16 10:11:05 +01:00
yoff
c6240e5a99 java: understand more initializers
Whne a fiels is assigned a safe type in a constructor,
that field is not exposed.
2025-12-16 10:11:05 +01:00
yoff
f4878b3806 java: make as many predicates private as possible 2025-10-21 13:25:26 +02:00
yoff
de05bfbce3 java: address review comments
- do not use `getQualifiedName`
- use camelCase
- rework alert predicates
2025-10-21 13:25:26 +02:00
yoff
715acefacc Apply suggestions from code review
Co-authored-by: Anders Schack-Mulligen <aschackmull@users.noreply.github.com>
2025-10-21 12:52:59 +02:00
yoff
3a0a8999d5 java: fix ql alerts 2025-10-17 01:52:23 +02:00
yoff
61a3e9630f java: rewrite conflict detection
- favour unary predicates over binary ones
(the natural "conflicting access" is binary)
- switch to a dual solution to trade recursion through forall for simple existentials.

Co-authored-by: Anders Schack-Mulligen <aschackmull@github.com>
2025-10-17 01:43:04 +02:00
yoff
1ad239459f java: move shared code into Concurrency.qll 2025-10-09 13:36:35 +02:00
yoff
f90e9dbb5e java: favour inline_late over inline
This gives much greater control over the join-order
2025-10-09 13:01:25 +02:00
yoff
830f02af1f java: fixes from the CI bots 2025-10-09 09:37:31 +02:00
yoff
93fc287ef1 java: add auto-generated overlay annotations 2025-10-09 09:25:57 +02:00
yoff
a1671ea8af java: small cleanups
- add missing qldoc
- remove use of `getErasure`
- remove use of `getTypeDescriptor`
- define `ExposedField`
2025-10-09 09:16:25 +02:00
yoff
821b1de5b3 java: inline char pred 2025-10-09 09:16:25 +02:00
yoff
01ddc11fa7 java: address some review comments 2025-10-09 09:16:25 +02:00
yoff
77734f83d5 java: better detection of thread safe fields.
Identified by triage of DCA results.
Previously, we did not use the erased type, so would not recgnize `CompletableFuture<R>`.
We now also recognize safe initializers.
2025-10-09 09:16:25 +02:00
yoff
096d5f2a56 java: implement SCC contraction of the call graph
Our monitor analysis would be fooled by cycles in the call graph,
since it required all edges on a path to a conflicting access to be either
 - targetting a method where the access is monitored (recursively) or
 - monitored locally, that is the call is monitored in the calling method
For access to be monitored (first case) all outgoing edges (towards an access) need
to satisfy this property. For a loop, that is too strong, only edges out of the loop
actually need to be protected. This led to FPs.
2025-10-09 09:14:16 +02:00
yoff
fe487e8bf0 java: add ThreadSafe query (P3)
Co-authored-by: Raúl Pardo <raul.pardo@protonmail.com>
Co-authored-by: SimonJorgensenMancofi <simon.jorgensen@mancofi.dk>
Co-authored-by: Bjørnar Haugstad Jåtten <bjornjaat@hotmail.com>
2025-10-09 09:14:16 +02:00