Fix/self analysis false positives and reorder init

.ctrace-analyzer.cfg

@@ -10,6 +10,7 @@ buffer-model=models/buffer-overflow/generic.txt
 # compile-commands=build/compile_commands.json
 analysis-profile=full
 jobs=auto
+compile-ir-cache-dir=.cache/compile-ir
 
 # Output behavior
 warnings-only=true
@@ -19,8 +20,8 @@ timing=false
 # Inter-TU analysis
 resource-cross-tu=true
 uninitialized-cross-tu=true
-#resource-summary-cache-dir=.cache/resource-lifetime
-resource-summary-cache-memory-only=true
+resource-summary-cache-dir=.cache/resource-lifetime
+resource-summary-cache-memory-only=false
 
 # SMT configuration
 smt=on

.github/workflows/ci.yml

@@ -1,14 +1,16 @@
 name: Build
 
 on:
-  push:
-    branches:
-      - "**"
   pull_request:
-    branches:
-      - "**"
+    branches: [main]
+  push:
+    branches: [main]
   workflow_dispatch:
 
+concurrency:
+  group: ci-${{ github.workflow }}-${{ github.event.pull_request.head.repo.full_name || github.repository }}-${{ github.event.pull_request.head.ref || github.ref_name }}
+  cancel-in-progress: true
+
 env:
   CCACHE_DIR: ${{ github.workspace }}/.ccache
 

CMakeLists.txt

@@ -3,6 +3,7 @@ project(stack_usage_analyzer)
 
 list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake")
 include(CheckLLVMVersion OPTIONAL)
+include(CheckCXXCompilerFlag)
 
 if(COMMAND check_llvm_version)
     set(LLVM_MIN_REQUIRED_VERSION "19" CACHE STRING "Minimum required LLVM version")
@@ -51,9 +52,15 @@ message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}")
 # Options de build
 option(BUILD_CLI "Build stack_usage_analyzer CLI tool" ON)
 option(BUILD_SHARED_LIB "Build shared library variant" ON)
-option(ENABLE_STACK_USAGE "Emit per-function stack usage (.su) files" OFF)
+option(ENABLE_STACK_USAGE "Emit per-function stack usage (.su) files" ON)
+option(ENABLE_WARN_PADDED "Enable -Wpadded warnings" ON)
+option(ENABLE_WARN_REORDER_INIT_LIST "Enable -Wreorder-init-list when supported" ON)
 option(ENABLE_Z3_BACKEND "Enable optional Z3 SMT backend if Z3 is available" ON)
 
+if(ENABLE_WARN_REORDER_INIT_LIST)
+    check_cxx_compiler_flag("-Wreorder-init-list" CTRACE_STACK_HAS_WREORDER_INIT_LIST)
+endif()
+
 # ===========================
 #  Communs Sources
 # ===========================
@@ -114,7 +121,6 @@ if(ENABLE_Z3_BACKEND)
     endif()
 endif()
 
-include_directories(${LLVM_INCLUDE_DIRS})
 add_definitions(${LLVM_DEFINITIONS})
 
 # llvm_map_components_to_libnames(llvm_libs
@@ -128,6 +134,10 @@ add_library(stack_usage_analyzer_lib STATIC
     ${STACK_ANALYZER_SOURCES}
 )
 
+if(ENABLE_WARN_REORDER_INIT_LIST AND CTRACE_STACK_HAS_WREORDER_INIT_LIST)
+    target_compile_options(stack_usage_analyzer_lib PRIVATE -Wreorder-init-list)
+endif()
+
 if(CTRACE_STACK_HAVE_Z3_BACKEND)
     target_compile_definitions(stack_usage_analyzer_lib PUBLIC CTRACE_STACK_ENABLE_Z3_BACKEND=1)
     if(TARGET z3::libz3)
@@ -137,7 +147,7 @@ if(CTRACE_STACK_HAVE_Z3_BACKEND)
     elseif(DEFINED Z3_LIBRARIES)
         target_link_libraries(stack_usage_analyzer_lib PUBLIC ${Z3_LIBRARIES})
         if(DEFINED Z3_INCLUDE_DIRS)
-            target_include_directories(stack_usage_analyzer_lib PUBLIC ${Z3_INCLUDE_DIRS})
+            target_include_directories(stack_usage_analyzer_lib SYSTEM PUBLIC ${Z3_INCLUDE_DIRS})
         endif()
     endif()
 endif()
@@ -162,9 +172,21 @@ target_include_directories(stack_usage_analyzer_lib
     PUBLIC
         $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include>
         $<INSTALL_INTERFACE:include>
+)
+
+target_include_directories(stack_usage_analyzer_lib SYSTEM
+    PUBLIC
         ${LLVM_INCLUDE_DIRS}
 )
 
+# Treat external dependency headers as system includes to reduce warning noise
+# from third-party code when project warning levels are strict.
+target_include_directories(stack_usage_analyzer_lib SYSTEM
+    PUBLIC
+        $<TARGET_PROPERTY:cc::compilerlib_static,INTERFACE_INCLUDE_DIRECTORIES>
+        $<TARGET_PROPERTY:coretrace::logger,INTERFACE_INCLUDE_DIRECTORIES>
+)
+
 # ALIAS FOR USE WITH FETCHCONTENT
 add_library(coretrace::stack_usage_analyzer_lib ALIAS stack_usage_analyzer_lib)
 
@@ -215,6 +237,10 @@ if(BUILD_CLI)
       main.cpp
     )
 
+    if(ENABLE_WARN_REORDER_INIT_LIST AND CTRACE_STACK_HAS_WREORDER_INIT_LIST)
+        target_compile_options(stack_usage_analyzer PRIVATE -Wreorder-init-list)
+    endif()
+
     target_link_libraries(stack_usage_analyzer
       PRIVATE
         stack_usage_analyzer_lib
@@ -226,6 +252,11 @@ if(BUILD_CLI)
         target_compile_options(stack_usage_analyzer PRIVATE -fstack-usage)
     endif()
 
+    if(ENABLE_WARN_PADDED AND CMAKE_CXX_COMPILER_ID MATCHES "Clang|GNU")
+        target_compile_options(stack_usage_analyzer_lib PRIVATE -Wpadded)
+        target_compile_options(stack_usage_analyzer PRIVATE -Wpadded)
+    endif()
+
     if(ENABLE_DEBUG_ASAN)
         target_compile_options(stack_usage_analyzer PRIVATE -fsanitize=address -fno-omit-frame-pointer -g)
         target_link_options(stack_usage_analyzer PRIVATE -fsanitize=address)

README.md

@@ -239,6 +239,7 @@ Ready-to-adapt workflow examples:
 --no-resource-cross-tu disables cross-TU resource summaries
 --resource-summary-cache-dir=<path> sets cache directory for cross-TU resource summaries (default: .cache/resource-lifetime)
 --resource-summary-cache-memory-only keeps cross-TU summary cache in memory only (process-local, no files)
+--compile-ir-cache-dir=<path> enables dependency-aware LLVM IR compile cache for unchanged source files
 --timing prints compile/analysis timings to stderr
 --config=<path> loads optional key=value config file (CLI flags override config values)
 --print-effective-config prints resolved runtime config to stderr
@@ -268,6 +269,8 @@ To generate `compile_commands.json` with CMake, configure with
 If analysis feels slow, `--compdb-fast` disables heavy flags (optimizations,
 sanitizers, profiling) while keeping include paths and macros.
 For multi-file runs, `--jobs=<N|auto>` parallelizes input loading; with cross-TU enabled it also parallelizes summary construction.
+`--compile-ir-cache-dir=<path>` reuses compiled LLVM IR for unchanged translation units
+based on source/dependency stamps, which reduces repeated C/C++ frontend cost across runs.
 When inputs are auto-discovered from `compile_commands.json`, `_deps` entries are skipped by default
 to keep analysis focused on project code; use `--include-compdb-deps` to opt back in.
 
@@ -305,6 +308,7 @@ Supported keys:
 - `uninitialized-cross-tu`
 - `resource-summary-cache-dir`
 - `resource-summary-cache-memory-only`
+- `compile-ir-cache-dir`
 
 Example file:
 
@@ -315,6 +319,7 @@ buffer-model=models/buffer-overflow/generic.txt
 compile-commands=build/compile_commands.json
 analysis-profile=full
 jobs=auto
+compile-ir-cache-dir=.cache/compile-ir
 smt=on
 smt-backend=z3
 smt-rules=recursion,integer-overflow,size-minus-k,stack-buffer,oob-read

docs/architecture/smt-implementation-plans.md

@@ -0,0 +1,151 @@
+Voici comment je vois l'évolution, ordonnée par ROI décroissant et dépendances techniques.
+
+---
+
+## Phase 1 — Encoder LLVM IR → ConstraintIR expressif
+*Le verrou qui bloque tout le reste*
+
+Aujourd'hui `encodeRangeConstraints` ne sait encoder que des intervalles. Pour que Z3 apporte une vraie valeur sur les autres analyses, il faut un encoder qui traduit les instructions LLVM en expressions symboliques.
+
+**Ce qu'il faut couvrir :**
+
+| LLVM IR | ConstraintIR |
+|---|---|
+| `add nsw i32 %a, %b` | `Add(sym_a, sym_b, 32)` + assertion overflow = poison |
+| `icmp slt i32 %x, 42` | `Slt(sym_x, Const(42, 32))` |
+| `br i1 %cond, label %then, label %else` | Edge constraint sur les deux branches |
+| `phi [%v1, %bb1], [%v2, %bb2]` | Disjonction : `Or(And(from_bb1, eq(sym, v1)), And(from_bb2, eq(sym, v2)))` |
+| `getelementptr [10 x i32], ptr %p, i64 0, i64 %idx` | `Add(base, Mul(idx, 4))` avec bound `0 ≤ idx < 10` |
+| `select i1 %c, i32 %a, i32 %b` | `ITE(cond, sym_a, sym_b)` (nécessite ajout `ExprKind::Select`) |
+| `llvm.assume(i1 %x)` | Assertion directe |
+| `freeze` | Marquer le symbole comme "valeur définie" |
+
+**Livrable :** un `LlvmConstraintEncoder` qui prend un chemin de blocs basiques et produit un `ConstraintIR` complet. Le `ConstraintIrBuilder` est déjà prêt — c'est la traversée LLVM qui manque.
+
+---
+
+## Phase 2 — Onboarding IntegerOverflow + SizeMinusK
+*Le plus gros gisement de FP réductibles*
+
+Avec l'encoder de la phase 1, on peut brancher le SMT sur les analyses à fort FP :
+
+**IntegerOverflowAnalysis** — Aujourd'hui l'analyse détecte les overflows sur les arguments de `malloc`/`memcpy`. Le pattern type de FP :
+```c
+size_t n = get_count();    // range inconnu
+void *p = malloc(n * sizeof(int));  // flaggé overflow
+```
+Avec Z3 : encoder `n * 4` en bitvector 64 bits, vérifier si l'overflow est satisfiable sous les contraintes de chemin. Si `UNSAT` → supprimer le diagnostic.
+
+**SizeMinusKWrites** — Même principe : les off-by-one sont souvent des FP quand la taille est prouvablement > k.
+
+**Point d'intégration :** après la passe heuristique existante, avant émission. Exactement ce que le doc prévoit. Le `RecursionConstraintEvaluator` sert de modèle — créer un `OverflowConstraintEvaluator` analogue.
+
+---
+
+## Phase 3 — StackBuffer + OOBRead path-sensitive
+*Précision sur les accès mémoire*
+
+L'analyse de buffer overflow actuelle est flow-insensitive — elle ne suit pas les contraintes de chemin sur les indices. Avec le SMT :
+
+```c
+int buf[10];
+int idx = get_index();
+if (idx >= 0 && idx < 10) {
+    buf[idx] = 42;  // aujourd'hui : flaggé potentiel overflow
+                     // avec SMT : UNSAT → sûr
+}
+```
+
+C'est le même pattern que la récursion : BFS avec accumulation de contraintes, sauf que la question est "cet accès est-il dans les bornes ?" au lieu de "cette base case est-elle atteignable ?".
+
+**Possibilité de factoriser** la traversée path-sensitive de `hasFeasibleNonRecursiveReturnPath` en un framework réutilisable :
+
+```
+PathExplorer<Question>
+  - traverse le CFG en BFS
+  - accumule les contraintes
+  - pose une Question à chaque point d'intérêt
+  - retourne Feasible / Infeasible / Inconclusive
+```
+
+---
+
+## Phase 4 — TypeConfusion avec raisonnement struct-layout
+*Les 91 FPs documentés*
+
+C'est le plus gros lot de FP en volume mais le plus complexe à encoder. Il faut :
+
+1. Encoder les layouts de structs (offsets des champs, tailles) comme contraintes
+2. Pour chaque "conflit de type" détecté, vérifier si les deux vues sont sur des sous-objets légalement imbriqués
+3. Si Z3 prouve que `offset_A + size_A ≤ offset_B` ou que les deux accès sont au même sous-objet → `UNSAT` → supprimer
+
+Ça nécessite probablement un ajout au `ConstraintIR` : des contraintes de type mémoire/layout, pas seulement arithmétiques.
+
+---
+
+## Phase 5 — DiagnosticRefiner comme composant autonome
+*Quand plusieurs analyses utilisent le SMT*
+
+Dès que 3+ analyses passent par le SMT, la logique de décision (keep/suppress/downgrade/tag inconclusive) mérite d'être extraite :
+
+```cpp
+class DiagnosticRefiner {
+    RefinementDecision refine(const Diagnostic& original,
+                              const SmtDecision& decision,
+                              const RulePolicy& policy) const;
+};
+
+enum class RefinementDecision {
+    Keep,           // SAT ou pas de SMT
+    Suppress,       // UNSAT confirmé
+    Downgrade,      // UNSAT mais confidence < seuil → Warning→Info
+    MarkInconclusive // Unknown/Timeout
+};
+```
+
+Avec des politiques par rule :
+- `recursion` : suppress agressif (UNSAT = pas de bug)
+- `integer-overflow` : downgrade plutôt que suppress (risque d'encoding bug)
+- `type-confusion` : suppress seulement en dual-consensus
+
+---
+
+## Phase 6 — Cache + Observabilité
+*Quand le volume de queries justifie l'investissement*
+
+**Cache :**
+- Clé : hash du `ConstraintIR` normalisé + mode/backend
+- Valeur : `SmtStatus`
+- Portée : process-local (un seul run d'analyse)
+- ROI : significatif en mode portfolio/cross-check ou quand plusieurs analyses posent des questions similaires sur les mêmes fonctions
+
+**Observabilité :**
+- Compteurs : queries total / sat / unsat / unknown / timeout / error
+- Latence : P50/P95/P99 par backend
+- Suppressions : count par rule
+- Format : JSON ou intégration dans le `--timing` existant
+
+---
+
+## Phase 7 — Améliorations Z3 avancées
+*Optimisations pour passer à l'échelle*
+
+- **Incremental solving** : réutiliser le `z3::solver` avec `push/pop` au lieu de recréer un contexte par query. Gros gain sur les traversées de chemin où les queries partagent un préfixe commun
+- **Tactics** : utiliser `z3::tactic("simplify") & z3::tactic("solve-eqs") & z3::tactic("bit-blast") & z3::tactic("sat")` pour les formules bitvector plutôt que le solveur par défaut
+- **Parallel portfolio réel** : `std::async` pour lancer Z3 et cvc5 en parallèle dans le mode portfolio (aujourd'hui c'est séquentiel)
+
+---
+
+## Résumé visuel
+
+```
+Phase 1: Encoder LLVM→ConstraintIR    ← verrou technique
+Phase 2: IntegerOverflow + SizeMinusK  ← plus gros ROI en FP
+Phase 3: StackBuffer + OOBRead         ← path-sensitive generalisé
+Phase 4: TypeConfusion                 ← 91 FPs mais complexe
+Phase 5: DiagnosticRefiner autonome    ← quand 3+ rules utilisent SMT
+Phase 6: Cache + Observabilité         ← quand le volume le justifie
+Phase 7: Incrémental + tactics + //    ← scaling
+```
+
+Les phases 1-2 sont les plus urgentes. Les phases 3-4 dépendent de la qualité de l'encoder. Les phases 5-7 sont de l'optimisation.