From ae55b6fa1efbdfadca9bb9251f8c710279b73429 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 28 Sep 2025 13:02:05 +0300
Subject: [PATCH] add analysis

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 .github/workflows/codeql-analysis.yml       | 41 ++++++++++
 codeql/custom_queries/FindUnderspecified.ql | 87 +++++++++++++++++++++
 2 files changed, 128 insertions(+)
 create mode 100644 .github/workflows/codeql-analysis.yml
 create mode 100644 codeql/custom_queries/FindUnderspecified.ql

diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml
new file mode 100644
index 000000000..d53c5453c
--- /dev/null
+++ b/.github/workflows/codeql-analysis.yml
@@ -0,0 +1,41 @@
+name: "CodeQL"
+
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+  schedule:
+    - cron: '0 0 * * 0'
+
+jobs:
+  analyze:
+    name: Analyze
+    runs-on: ubuntu-latest
+    permissions:
+      actions: read
+      contents: read
+      security-events: write
+
+    strategy:
+      fail-fast: false
+      matrix:
+        language: [cpp]
+
+    steps:
+    - name: Checkout repository
+      uses: actions/checkout@v4
+
+    - name: Initialize CodeQL
+      uses: github/codeql-action/init@v3
+      with:
+        languages: ${{ matrix.language }}
+
+    - name: Autobuild
+      uses: github/codeql-action/autobuild@v3
+
+    - name: Run CodeQL Query
+      uses: github/codeql-action/analyze@v3
+      with:
+        category: 'custom'
+        queries: ./codeql/custom-queries
\ No newline at end of file
diff --git a/codeql/custom_queries/FindUnderspecified.ql b/codeql/custom_queries/FindUnderspecified.ql
new file mode 100644
index 000000000..0d33dc4f8
--- /dev/null
+++ b/codeql/custom_queries/FindUnderspecified.ql
@@ -0,0 +1,87 @@
+ /**
+
+  * Finds function calls with arguments that have unspecified evaluation order.
+
+  *
+
+  * @name Unspecified argument evaluation order
+
+  * @kind problem
+
+  * @problem.severity warning
+
+  * @id cpp/z3/unspecevalorder
+
+  */
+
+
+
+  import cpp
+
+
+
+  predicate isPureFunc(Function f) {
+
+    f.getName() = "m" or
+
+    not exists(Assignment a | a.getEnclosingFunction() = f) and
+
+    forall(FunctionCall g | g.getEnclosingFunction() = f | isPureFunc(g.getTarget()))
+
+  }
+
+
+
+  predicate sideEffectfulArgument(Expr a) {
+
+    exists(Function f | f = a.(FunctionCall).getTarget() |
+
+      not f instanceof ConstMemberFunction and
+
+      not isPureFunc(f)
+
+    )
+
+    or
+
+    exists(ArrayExpr b | b = a.(ArrayExpr) |
+
+      sideEffectfulArgument(b.getArrayBase()) or sideEffectfulArgument(b.getArrayOffset())
+
+    )
+
+    or
+
+    exists(Assignment b | b = a)
+
+    or
+
+    exists(BinaryOperation b | b = a | sideEffectfulArgument(b.getAnOperand()))
+
+    or
+
+    exists(UnaryOperation b | b = a | sideEffectfulArgument(b.getOperand()))
+
+  }
+
+
+
+  from FunctionCall f, Expr a, int i, Expr b, int j where
+
+    i < j and
+
+    f.getTarget().getName() != "operator&&" and
+
+    f.getTarget().getName() != "operator||" and
+
+    a = f.getArgument(i) and
+
+    b = f.getArgument(j) and
+
+    sideEffectfulArgument(a) and
+
+    sideEffectfulArgument(b)
+
+  select f, "potentially unspecified evaluation order of function arguments: $@ and $@", a,
+
+    i.toString(), b, j.toString()
\ No newline at end of file