diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 91dd83967..74fbac872 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -296,9 +296,17 @@ OPTIONS Activates: Enable --siof and disable all other checkers (Conversely: --no-siof-only) + --sqlite-cache-size int + SQLite cache size in pages (if positive) or kB (if negative), + follows formal of corresponding SQLite PRAGMA. + --sqlite-lock-timeout int Timeout for SQLite results database operations, in milliseconds. + --sqlite-page-size int + SQLite page size in bytes, must be a power of two between 512 and + 65536. + --no-starvation Deactivates: starvation analysis (Conversely: --starvation) diff --git a/infer/man/man1/infer-capture.txt b/infer/man/man1/infer-capture.txt index 3a1b89ae6..8b86ee47d 100644 --- a/infer/man/man1/infer-capture.txt +++ b/infer/man/man1/infer-capture.txt @@ -94,9 +94,17 @@ OPTIONS Ignore files whose path matches the given prefix (can be specified multiple times) + --sqlite-cache-size int + SQLite cache size in pages (if positive) or kB (if negative), + follows formal of corresponding SQLite PRAGMA. + --sqlite-lock-timeout int Timeout for SQLite results database operations, in milliseconds. + --sqlite-page-size int + SQLite page size in bytes, must be a power of two between 512 and + 65536. + -- Stop argument processing, use remaining arguments as a build command BUCK COMPILATION DATABASE OPTIONS diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index e461dad8e..4b6df5c00 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1025,10 +1025,18 @@ OPTIONS Deactivates: print code excerpts around trace elements (Conversely: --source-preview) See also infer-explore(1). + --sqlite-cache-size int + SQLite cache size in pages (if positive) or kB (if negative), + follows formal of corresponding SQLite PRAGMA. See also infer-analyze(1), infer-capture(1), and infer-run(1). + --sqlite-lock-timeout int Timeout for SQLite results database operations, in milliseconds. See also infer-analyze(1), infer-capture(1), and infer-run(1). + --sqlite-page-size int + SQLite page size in bytes, must be a power of two between 512 and + 65536. See also infer-analyze(1), infer-capture(1), and infer-run(1). + --no-starvation Deactivates: starvation analysis (Conversely: --starvation) See also infer-analyze(1). diff --git a/infer/man/man1/infer-run.txt b/infer/man/man1/infer-run.txt index 46100148a..9435b36c7 100644 --- a/infer/man/man1/infer-run.txt +++ b/infer/man/man1/infer-run.txt @@ -147,9 +147,17 @@ OPTIONS Ignore files whose path matches the given prefix (can be specified multiple times) + --sqlite-cache-size int + SQLite cache size in pages (if positive) or kB (if negative), + follows formal of corresponding SQLite PRAGMA. + --sqlite-lock-timeout int Timeout for SQLite results database operations, in milliseconds. + --sqlite-page-size int + SQLite page size in bytes, must be a power of two between 512 and + 65536. + --version Print version information and exit diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index d89710a6c..57e5c174e 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -1025,10 +1025,18 @@ OPTIONS Deactivates: print code excerpts around trace elements (Conversely: --source-preview) See also infer-explore(1). + --sqlite-cache-size int + SQLite cache size in pages (if positive) or kB (if negative), + follows formal of corresponding SQLite PRAGMA. See also infer-analyze(1), infer-capture(1), and infer-run(1). + --sqlite-lock-timeout int Timeout for SQLite results database operations, in milliseconds. See also infer-analyze(1), infer-capture(1), and infer-run(1). + --sqlite-page-size int + SQLite page size in bytes, must be a power of two between 512 and + 65536. See also infer-analyze(1), infer-capture(1), and infer-run(1). + --no-starvation Deactivates: starvation analysis (Conversely: --starvation) See also infer-analyze(1). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 65c338c5f..c43b2786f 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2236,6 +2236,21 @@ and specs_library = specs_library +and sqlite_cache_size = + CLOpt.mk_int ~long:"sqlite-cache-size" ~default:2000 + ~in_help: + InferCommand.[(Analyze, manual_generic); (Capture, manual_generic); (Run, manual_generic)] + "SQLite cache size in pages (if positive) or kB (if negative), follows formal of \ + corresponding SQLite PRAGMA." + + +and sqlite_page_size = + CLOpt.mk_int ~long:"sqlite-page-size" ~default:32768 + ~in_help: + InferCommand.[(Analyze, manual_generic); (Capture, manual_generic); (Run, manual_generic)] + "SQLite page size in bytes, must be a power of two between 512 and 65536." + + and sqlite_lock_timeout = (* some lame estimate: when the frontend writes CFGs to disk, it may take a few seconds to write one CFG and all the cores may be trying to write to the database at the same time. This means @@ -3165,6 +3180,10 @@ and sourcepath = !sourcepath and spec_abs_level = !spec_abs_level +and sqlite_cache_size = !sqlite_cache_size + +and sqlite_page_size = !sqlite_page_size + and sqlite_lock_timeout = !sqlite_lock_timeout and sqlite_vfs = !sqlite_vfs diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 8a3338476..e4d6df3f6 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -644,6 +644,10 @@ val spec_abs_level : int val specs_library : string list +val sqlite_cache_size : int + +val sqlite_page_size : int + val sqlite_lock_timeout : int val sqlite_vfs : string option diff --git a/infer/src/base/ResultsDatabase.ml b/infer/src/base/ResultsDatabase.ml index b34bbb30d..7ec9194e0 100644 --- a/infer/src/base/ResultsDatabase.ml +++ b/infer/src/base/ResultsDatabase.ml @@ -48,6 +48,8 @@ let create_source_files_table db = let create_db () = let temp_db = Filename.temp_file ~in_dir:Config.results_dir database_filename ".tmp" in let db = Sqlite3.db_open ~mutex:`FULL temp_db in + SqliteUtils.exec db ~log:"sqlite page size" + ~stmt:(Printf.sprintf "PRAGMA page_size=%d" Config.sqlite_page_size) ; create_procedures_table db ; create_source_files_table db ; (* This should be the default but better be sure, otherwise we cannot access the database concurrently. This has to happen before setting WAL mode. *) @@ -148,6 +150,8 @@ end = struct in Sqlite3.busy_timeout db Config.sqlite_lock_timeout ; SqliteUtils.exec db ~log:"synchronous=OFF" ~stmt:"PRAGMA synchronous=OFF" ; + SqliteUtils.exec db ~log:"sqlite cache size" + ~stmt:(Printf.sprintf "PRAGMA cache_size=%i" Config.sqlite_cache_size) ; database := Some db ; List.iter ~f:(fun callback -> callback db) !new_db_callbacks end