← nischoy.ai

sqlite Verification

SMT2 formal verification of security-critical code paths

ALL VERIFIED
Overall
22
Properties Checked
22
Verified
0
Failed

SQLite3 Limit ID Bounds (0-12)

🌳 tree-sitter VERIFIED

Function: sqlite3_limit · Z3 solved in 0.1ms

sqlite3_limit() limitId must be 0-SQLITE_N_LIMIT(12). Extracted from main.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun limitId () Int)
(assert
 (<= limitId 12))
(assert
 (>= limitId 0))
(assert
 (or (< limitId 0) (> limitId 12)))
(check-sat)

SQLite3 Page Size Bounds (512-65536)

🌳 tree-sitter (partial) VERIFIED

Function: sqlite3BtreeSetPageSize · Z3 solved in 0.0ms

Page size must be power of 2 between 512 and SQLITE_MAX_PAGE_SIZE(65536). From btree.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun pageSize () Int)
(assert
 (<= pageSize 65536))
(assert
 (>= pageSize 512))
(assert
 (or (< pageSize 512) (> pageSize 65536)))
(check-sat)

SQLite3 SQL Statement Length Bounds

🌳 tree-sitter (partial) VERIFIED

Function: sqlite3LockAndPrepare · Z3 solved in 0.0ms

SQL length ≤ SQLITE_MAX_SQL_LENGTH (1,000,000,000). From prepare.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun sql_len () Int)
(assert
 (<= sql_len 1000000000))
(assert
 (>= sql_len 0))
(assert
 (or (< sql_len 0) (> sql_len 1000000000)))
(check-sat)

SQLite3 Expression Tree Depth Bounds (0-1000)

🌳 tree-sitter (partial) VERIFIED

Function: sqlite3ExprCheckHeight · Z3 solved in 0.0ms

Expression depth ≤ SQLITE_MAX_EXPR_DEPTH (1000). From expr.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun expr_depth () Int)
(assert
 (<= expr_depth 1000))
(assert
 (>= expr_depth 0))
(assert
 (or (< expr_depth 0) (> expr_depth 1000)))
(check-sat)

SQLite3 Column Count Bounds (1-32767)

🌳 tree-sitter (partial) VERIFIED

Function: sqlite3AddColumn · Z3 solved in 0.0ms

Column count ≤ SQLITE_MAX_COLUMN (hard max 32767). From build.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun nColumn () Int)
(assert
 (<= nColumn 32767))
(assert
 (>= nColumn 1))
(assert
 (or (< nColumn 1) (> nColumn 32767)))
(check-sat)

SQLite3 Attached Database Index Bounds (0-125)

🌳 tree-sitter (partial) VERIFIED

Function: sqlite3_limit · Z3 solved in 0.0ms

Attached DB index 0-SQLITE_MAX_ATTACHED(125). From main.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun iDb () Int)
(assert
 (<= iDb 125))
(assert
 (>= iDb 0))
(assert
 (or (< iDb 0) (> iDb 125)))
(check-sat)

SQLite3 BLOB/String Length Bounds

🌳 tree-sitter (partial) VERIFIED

Function: sqlite3_result_blob · Z3 solved in 0.0ms

BLOB/string length ≤ SQLITE_MAX_LENGTH (1,000,000,000).

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun blob_len () Int)
(assert
 (<= blob_len 1000000000))
(assert
 (>= blob_len 0))
(assert
 (or (< blob_len 0) (> blob_len 1000000000)))
(check-sat)

SQLite3 Function Argument Count Bounds (-1 to 127)

🌳 tree-sitter VERIFIED

Function: sqlite3CreateFunc · Z3 solved in 0.0ms

nArg must be -1 (any) to SQLITE_MAX_FUNCTION_ARG (127). From sqlite3CreateFunc() in main.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun nArg () Int)
(assert
 (<= nArg 127))
(assert
 (>= nArg (- 1)))
(assert
 (or (< nArg (- 1)) (> nArg 127)))
(check-sat)

SQLite3 Memory-Mapped I/O Size Bounds

🌳 tree-sitter (partial) VERIFIED

Function: sqlite3_config · Z3 solved in 0.0ms

mxMmap must be non-negative. From sqlite3_config().

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun mxMmap () Int)
(assert
 (>= mxMmap 0))
(assert
 (< mxMmap 0))
(check-sat)

SQLite3 SQL Parameter Index Bounds (1-32766)

🌳 tree-sitter (partial) VERIFIED

Function: sqlite3ExprCodeTarget · Z3 solved in 0.0ms

SQL parameter index (?NNN) must be 1-SQLITE_MAX_VARIABLE_NUMBER (32766). From expr.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun variable_number () Int)
(assert
 (<= variable_number 32766))
(assert
 (>= variable_number 1))
(assert
 (or (< variable_number 1) (> variable_number 32766)))
(check-sat)

SQLite3 Trigger Recursion Depth Bounds (0-1000)

🌳 tree-sitter (partial) VERIFIED

Function: sqlite3CodeRowTriggerDirect · Z3 solved in 0.0ms

Trigger depth ≤ SQLITE_MAX_TRIGGER_DEPTH (1000). From trigger.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun trigger_depth () Int)
(assert
 (<= trigger_depth 1000))
(assert
 (>= trigger_depth 0))
(assert
 (or (< trigger_depth 0) (> trigger_depth 1000)))
(check-sat)

SQLite3 Worker Thread Count Bounds (0-8)

🌳 tree-sitter (partial) VERIFIED

Function: sqlite3VdbeSorterInit · Z3 solved in 0.0ms

Worker thread count ≤ SQLITE_MAX_WORKER_THREADS (8). From vdbesort.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun nWorker () Int)
(assert
 (<= nWorker 8))
(assert
 (>= nWorker 0))
(assert
 (or (< nWorker 0) (> nWorker 8)))
(check-sat)

SQLite3 Compound SELECT Depth Bounds (2-500)

📋 stub VERIFIED

Function: compound_select_check · Z3 solved in 0.0ms

Compound SELECT limit ≤ SQLITE_MAX_COMPOUND_SELECT (500). From parse.y.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun mxSelect () Int)
(assert
 (<= mxSelect 500))
(assert
 (>= mxSelect 2))
(assert
 (or (< mxSelect 2) (> mxSelect 500)))
(check-sat)

SQLite3 LIKE Pattern Length Bounds (1-50000)

📋 stub VERIFIED

Function: like_pattern_length_check · Z3 solved in 0.0ms

LIKE/GLOB pattern length ≤ SQLITE_MAX_LIKE_PATTERN_LENGTH (50000). Prevents DoS via deep recursion in patternCompare(). From func.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun nPat () Int)
(assert
 (<= nPat 50000))
(assert
 (>= nPat 1))
(assert
 (or (< nPat 1) (> nPat 50000)))
(check-sat)

SQLite3 Parser Depth Bounds (0-2500)

📋 stub VERIFIED

Function: parser_depth_check · Z3 solved in 0.0ms

Parser depth ≤ SQLITE_MAX_PARSER_DEPTH (2500). sqlite3_limit() clamps to hard limit, preventing stack overflow from deeply nested SQL. From main.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun depth () Int)
(assert
 (<= depth 2500))
(assert
 (>= depth 0))
(assert
 (or (< depth 0) (> depth 2500)))
(check-sat)

SQLite3 Schema Retry Limit (0-50)

📋 stub VERIFIED

Function: schema_retry_check · Z3 solved in 0.0ms

Schema retry counter ≤ SQLITE_MAX_SCHEMA_RETRY (50). sqlite3_step() and sqlite3_blob_open() cap re-parse attempts, preventing infinite loops on concurrent schema changes. From vdbeapi.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun cnt () Int)
(assert
 (<= cnt 50))
(assert
 (>= cnt 0))
(assert
 (or (< cnt 0) (> cnt 50)))
(check-sat)

SQLite3 VDBE Opcode Limit (40-250000000)

📋 stub VERIFIED

Function: vdbe_op_limit · Z3 solved in 0.0ms

VDBE opcode limit ∈ [40, 250000000]. SQLITE_MAX_VDBE_OP caps opcodes per prepared statement, preventing DoS via complex queries. Compile-time check enforces ≥ 40. From main.c/sqliteLimit.h.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun limit () Int)
(assert
 (<= limit 250000000))
(assert
 (>= limit 40))
(assert
 (or (< limit 40) (> limit 250000000)))
(check-sat)

SQLite3 Lookaside Slot Size (8-65528)

📋 stub VERIFIED

Function: lookaside_slot_size · Z3 solved in 0.0ms

Lookaside slot size ∈ [8, 65528]. SQLite's lookaside allocator uses fixed-size memory slots. Must be > sizeof(pointer) (8) and ≤ 65528 (u16 cap). Default 1200. From main.c setupLookaside().

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun sz () Int)
(assert
 (<= sz 65528))
(assert
 (>= sz 8))
(assert
 (or (< sz 8) (> sz 65528)))
(check-sat)

SQLite3 Lookaside Slot Count (0-268369920)

📋 stub VERIFIED

Function: lookaside_slot_count · Z3 solved in 0.0ms

Lookaside slot count ∈ [0, 268369920]. SQLite clamps cnt<1 to 0 and caps at 0x7fff0000/sz. Absolute max is 0x7fff0000/8 (min slot size=8) = 268369920. Prevents OOM via excessive lookaside allocation. From main.c setupLookaside().

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun cnt () Int)
(assert
 (<= cnt 268369920))
(assert
 (>= cnt 0))
(assert
 (or (< cnt 0) (> cnt 268369920)))
(check-sat)

SQLite3 WAL Autocheckpoint Threshold (0-2147483647)

📋 stub VERIFIED

Function: wal_autocheckpoint · Z3 solved in 0.0ms

WAL autocheckpoint threshold ∈ [0, 2147483647]. sqlite3_wal_autocheckpoint(nFrame) enables auto-checkpoint when nFrame>0, disables when ≤0. Default 1000. Prevents unbounded WAL growth that can exhaust disk space. From main.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun nFrame () Int)
(assert
 (<= nFrame 2147483647))
(assert
 (>= nFrame 0))
(assert
 (or (< nFrame 0) (> nFrame 2147483647)))
(check-sat)

SQLite3 FTS5 Tombstone Array Allocation Domain

🌳 tree-sitter (partial) VERIFIED

Function: fts5SegIterAllocTombstone · Z3 solved in 0.0ms

FTS5 tombstone page-count used for allocation must remain in 64-bit-safe sizing domain under the nPgTombstone>0 allocation path. Generalizes CVE-2025-7709 integer-overflow/under-allocation class for corrupted FTS5 index metadata. From ext/fts5/fts5_index.c.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun nPgTombstone () Int)
(assert
 (<= nPgTombstone 2147483647))
(assert
 (>= nPgTombstone 0))
(assert
 (and (> nPgTombstone 0) (> nPgTombstone 2147483647)))
(check-sat)

SQLite3 Max Page Count (1-4294967294)

📋 stub VERIFIED

Function: max_page_count · Z3 solved in 0.0ms

Max page count ∈ [1, 4294967294]. SQLITE_MAX_PAGE_COUNT caps the number of pages in a database, limiting max DB size (~16TB at 4096-byte pages). Default 0xFFFFFFFE. From pager.c/sqliteLimit.h.

View SMT2 Constraints 
; benchmark generated from python API
(set-info :status unknown)
(declare-fun mxpg () Int)
(assert
 (<= mxpg 4294967294))
(assert
 (>= mxpg 1))
(assert
 (or (< mxpg 1) (> mxpg 4294967294)))
(check-sat)

Last verified: 2026-03-26 00:04:02 UTC · Solver: Z3 4.16.0