[sqlite] page and cache size flags and defaults

Summary:
Sqlite versions set their own default page and cache size.  Old versions use crazy-non-optimal settings.

Allow setting both from command line and set up reasonable defaults.  See, e.g.,

https://wiki.mozilla.org/Performance/Avoid_SQLite_In_Your_Next_Firefox_Feature

for page size notes.

The defaults will cost a maximum of 64Mb in cache per Infer process.  These improve merging times significantly.

Reviewed By: jvillard

Differential Revision: D17364643

fbshipit-source-id: b9abab10f

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)
 

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

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).

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
 

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).

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

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

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