Merge branch 'master' into interactive

Author: sim642

.github/workflows/docker.yml

@@ -38,18 +38,18 @@ jobs:
         uses: actions/checkout@v3
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v1 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
 
       - name: Log in to the Container registry
-        uses: docker/login-action@v1
+        uses: docker/login-action@v2
         with:
           registry: ${{ env.REGISTRY }}
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
 
       - name: Extract metadata (tags, labels) for Docker
         id: meta
-        uses: docker/metadata-action@v3
+        uses: docker/metadata-action@v4
         with:
           images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
           tags: |
@@ -59,7 +59,7 @@ jobs:
 
       - name: Build Docker image
         id: build
-        uses: docker/build-push-action@v2
+        uses: docker/build-push-action@v3
         with:
           context: .
           load: true # load into docker instead of immediately pushing
@@ -72,7 +72,7 @@ jobs:
         run: docker run --rm -v $(pwd):/data ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ steps.meta.outputs.version }} /data/tests/regression/04-mutex/01-simple_rc.c # run image by version in case multiple tags
 
       - name: Push Docker image
-        uses: docker/build-push-action@v2
+        uses: docker/build-push-action@v3
         with:
           context: .
           push: true

.github/workflows/unlocked.yml

@@ -169,11 +169,11 @@ jobs:
         uses: actions/checkout@v3
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v1 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
 
       - name: Build dev Docker image
         id: build
-        uses: docker/build-push-action@v2
+        uses: docker/build-push-action@v3
         with:
           context: .
           target: dev

src/framework/analyses.ml

@@ -451,6 +451,8 @@ type analyzed_data = {
 }
 
 type increment_data = {
+  server: bool;
+
   old_data: analyzed_data option;
   new_file: Cil.file;
   changes: CompareCIL.change_info;
@@ -460,7 +462,8 @@ type increment_data = {
   restarting: VarQuery.t list;
 }
 
-let empty_increment_data file = {
+let empty_increment_data ?(server=false) file = {
+  server;
   old_data = None;
   new_file = file;
   changes = CompareCIL.empty_change_info ();

src/framework/control.ml

@@ -8,8 +8,10 @@ open GobConfig
 open Constraints
 
 module type S2S = functor (X : Spec) -> Spec
-(* gets Spec for current options *)
-let get_spec () : (module Spec) =
+
+(* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
+let spec_module: (module Spec) Lazy.t = lazy (
+  GobConfig.building_spec := true;
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
@@ -28,7 +30,14 @@ let get_spec () : (module Spec) =
             |> lift (get_bool "ana.opt.equal" && not (get_bool "ana.opt.hashcons")) (module OptEqual)
             |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
           ) in
+  GobConfig.building_spec := false;
   (module S1)
+)
+
+(** gets Spec for current options *)
+let get_spec (): (module Spec) =
+  Lazy.force spec_module
+
 
 (** Given a [Cfg], a [Spec], and an [Inc], computes the solution to [MCP.Path] *)
 module AnalyzeCFG (Cfg:CfgBidir) (Spec:Spec) (Inc:Increment) =

src/maingoblint.ml

@@ -563,7 +563,7 @@ let diff_and_rename current_file =
       | Some cil_file, Some solver_data -> Some ({cil_file; solver_data}: Analyses.analyzed_data)
       | _, _ -> None
     in
-    {Analyses.changes = changes; restarting; old_data; new_file = current_file}
+    {server = false; Analyses.changes = changes; restarting; old_data; new_file = current_file}
   in change_info
 
 let () = (* signal for printing backtrace; other signals in Generic.SolverStats and Timeout *)

src/solvers/td3.ml

@@ -1185,7 +1185,19 @@ module WP =
          * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have
          *   the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values).
          *)
-        if loaded && GobConfig.get_bool "ana.opt.hashcons" then (
+        if loaded && S.increment.server then (
+          data.rho <- HM.copy data.rho;
+          data.stable <- HM.copy data.stable;
+          data.wpoint <- HM.copy data.wpoint;
+          data.infl <- HM.copy data.infl;
+          data.side_infl <- HM.copy data.side_infl;
+          data.side_dep <- HM.copy data.side_dep;
+          (* data.st is immutable, no need to copy *)
+          data.var_messages <- HM.copy data.var_messages;
+          data.rho_write <- HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *)
+          data.dep <- HM.copy data.dep;
+        )
+        else if loaded && GobConfig.get_bool "ana.opt.hashcons" then (
           let rho' = HM.create (HM.length data.rho) in
           HM.iter (fun k v ->
             (* call hashcons on contexts and abstract values; results in new tags *)

src/util/gobConfig.ml

@@ -28,6 +28,8 @@ exception ConfigError of string
 (* Phase of the analysis (moved from GoblintUtil b/c of circular build...) *)
 let phase = ref 0
 
+let building_spec = ref false
+
 
 module Validator = JsonSchema.Validator (struct let schema = Options.schema end)
 module ValidatorRequireAll = JsonSchema.Validator (struct let schema = Options.require_all end)
@@ -303,10 +305,16 @@ struct
     in
     drop memo_int; drop memo_bool; drop memo_string; drop memo_list
 
-  let get_int    = memo_int.get
-  let get_bool   = memo_bool.get
-  let get_string = memo_string.get
-  let get_list   = memo_list.get
+  let wrap_get f x =
+    (* self-observe options, which Spec construction depends on *)
+    if !building_spec && Tracing.tracing then Tracing.trace "config" "get during building_spec: %s\n" x;
+    (* TODO: blacklist such building_spec option from server mode modification since it will have no effect (spec is already built) *)
+    f x
+
+  let get_int    = wrap_get memo_int.get
+  let get_bool   = wrap_get memo_bool.get
+  let get_string = wrap_get memo_string.get
+  let get_list   = wrap_get memo_list.get
   let get_string_list = List.map Yojson.Safe.Util.to_string % get_list
 
   (** Helper functions for writing values. *)

src/util/server.ml

@@ -147,13 +147,13 @@ let increment_data (s: t) file reparsed = match !Serialize.server_solver_data wi
     let old_data = Some { Analyses.cil_file = s_file; solver_data } in
     s.max_ids <- UpdateCil.update_ids s_file s.max_ids file changes;
     (* TODO: get globals for restarting from config *)
-    { Analyses.changes; old_data; new_file = file; restarting = [] }, false
+    { server = true; Analyses.changes; old_data; new_file = file; restarting = [] }, false
   | Some solver_data ->
     let changes = virtual_changes file in
     let old_data = Some { Analyses.cil_file = file; solver_data } in
     (* TODO: get globals for restarting from config *)
-    { Analyses.changes; old_data; new_file = file; restarting = [] }, false
-  | _ -> Analyses.empty_increment_data file, true
+    { server = true; Analyses.changes; old_data; new_file = file; restarting = [] }, false
+  | _ -> Analyses.empty_increment_data ~server:true file, true
 
 let analyze ?(reset=false) (s: t) =
   Messages.Table.(MH.clear messages_table);
@@ -194,7 +194,6 @@ let () =
         analyze serve ~reset;
         {status = if !Goblintutil.verified = Some false then VerifyError else Success}
       with Sys.Break ->
-        assert (GobConfig.get_bool "ana.opt.hashcons"); (* TODO: TD3 doesn't copy input solver data, so will modify it in place and screw up Serialize.server_solver_data accidentally *)
         {status = Aborted}
   end);
 

tests/regression/03-practical/26-smtprc-crash.c

@@ -0,0 +1,16 @@
+// SKIP: Low Priority -- this compiles with warnings, but goblint crashes.
+#include <pthread.h>
+
+int data[10];
+
+void *t_fun(int i) {
+  int *x = &data[i];
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  int n = 0;
+  pthread_create(&id, NULL, t_fun, (int*) n);
+  return 0;
+}

tests/regression/05-lval_ls/18-website.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] symb_locks --set ana.activated[+] region --set ana.activated[+] var_eq --enable exp.region-offsets
+// PARAM: --set ana.activated[+] symb_locks
 #include <pthread.h>
 
 int data[10];
@@ -31,4 +31,3 @@ int main() {
 
   return 0;
 }
-