Complete tutorial

Author: michael-schwarz

src/analyses/tutorials/gStoreWidening.ml

@@ -3,61 +3,63 @@ open SimplifiedAnalysis
 open GStoreWideningHelper
 
 (**
-  This analysis proceeds in steps, with the steps building on each other.
+   This analysis proceeds in steps, with the steps building on each other.
 
-  For the sake of this analysis, we are assuming that all variables are of integer type.
-  This allows us to keep the analysis simple in the beginning.
+   For the sake of this analysis, we are assuming that all variables are of integer type.
+   This allows us to keep the analysis simple in the beginning.
 
 
-  1) First, a simple  interval analysis is implemented which tracks intervals
-     for local variables only. 
+   1) First, a simple  interval analysis is implemented which tracks intervals
+     for local variables only.
 
     The majority of the code is already provided, there is one place where
-    changes need to be made, namely the handling of branches. 
+    changes need to be made, namely the handling of branches.
     It is marked with TODO: 1).
 
-  2) Then the analysis is extended to also track values for globals via global store widening
+   2) Then the analysis is extended to also track values for globals via global store widening
 
     To this end, one should fix which set of globals to track, and their domain.
     Then, assignment and evaluation functions should be changed appropriately.
     These are marked with TODO: 2).
-  
-  3) Define a helper analysis which tracks for each variable which thread ids are used to write to it,
+
+   3) Define a helper analysis which tracks for each variable which thread ids are used to write to it,
     and use this information to determine whether a variable is effectively local
     (i.e., only written by one thread).
 
-    This requires modifying the domain to store thread ids, and modifying the assign function 
-    to record thread ids for global variables. 
+    This requires modifying the domain to store thread ids, and modifying the assign function
+    to record thread ids for global variables.
     Then, the query function should be modified to check whether there is only one thread
-    accessing this variable, and whether it is the current one. 
+    accessing this variable, and whether it is the current one.
     These are marked with TODO: 3).
-  
-  4) Modify the first analysis to exploit the information from the helper analysis to
+
+   4) Modify the first analysis to exploit the information from the helper analysis to
      track the values of effectively local variables more precisely in the thread that
      owns them, while keeping applying global store widening to obtain the perspective
      of other threads.
 
      This will amount to modifying some of the places changed in step 2)
 
-  
-  After modifying things, don't forget to compile by running `make`
+
+   After modifying things, don't forget to compile by running `make`
 
     There are regression tests for this analysis, which you can run by calling:
    -  ./regtest.sh 99 05
    -  ./regtest.sh 99 06
+   -  ./regtest.sh 99 07
 
-  After fixing the TODO: 1), the first regression test should pass.
-  After fixing the TODO: 2), both the first and the second tests should pass.
+   After fixing the TODO: 1), the first regression test should pass.
+   After fixing the TODO: 2), both the first and the second tests should pass.
+   After fixing the last TODO:, all three tests should pass
 
-  Running a regression test also produces a visualization of the analysis results as a HTML file in the folder
-  result.
+   Running a regression test also produces a visualization of the analysis results as a HTML file in the folder
+   result.
 
-  You can access these by spinning up a HTTP server for the result directory, 
-  e.g., by calling `python3 -m http.server --directory result`.
-  Then open `index.xml` in your browser.
+   You can access these by spinning up a HTTP server for the result directory,
+   e.g., by calling `python3 -m http.server --directory result`.
+   Then open `index.xml` in your browser.
 
-  (When using devcontainer, VSCode will automatically detect the server and 
-  provide a link to open the visualization in your browser.)
+   (When using devcontainer, VSCode will automatically detect the server and
+   provide a link to open the visualization in your browser.)
 
 *)
 
@@ -80,7 +82,7 @@ module GStoreWideningAnalysis: SimplifiedSpec = struct
   (* Evaluate a single variable given a local state *)
   let eval_varinfo man state v =
     if v.vglob then
-      (** TODO: 2) Modify so that we store values for globals *)
+      (* TODO: 2) Modify so that we get values for globals *)
       top_of_var v
     else
       D.find v state
@@ -236,7 +238,7 @@ module GStoreWideningAnalysis: SimplifiedSpec = struct
       ) (D.bot ()) f.sformals
 end
 
-module ThreadSet = ConcDomain.ThreadSet 
+module ThreadSet = ConcDomain.ThreadSet
 
 module EffectivelyLocalAnalysis:SimplifiedSpec = struct
   let name = "effectivelyLocal"
@@ -252,20 +254,24 @@ module EffectivelyLocalAnalysis:SimplifiedSpec = struct
   let startcontext = ()
 
   let assign man state lval rval =
-    let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in
-    let singleton_set = ThreadSet.singleton tid in
-    match is_tracked_lval lval with
-    | Some v ->
-      (* TODO: 3) check if this is a global variable and if it is, record the thread id *)
+    (* When the global initializers are evaluated, no threads exists yet *)
+    if !AnalysisState.global_initialization then
       state
-    | None ->
-      state
-  
+    else
+      let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in
+      let singleton_set = ThreadSet.singleton tid in
+      match is_tracked_lval lval with
+      | Some v ->
+        (* TODO: 3) check if this is a global variable and if it is, record the thread id *)
+        state
+      | None ->
+        state
+
   let query man state (type a) (q: a Queries.t): a Queries.result =
     match q with
     | Queries.TutorialEffectivelyLocal v ->
       (* TODO: 3) Get the current thread id, and check whether there is only one thread
-       accessing this variable, and whether it is the current one *)
+         accessing this variable, and whether it is the current one *)
       Queries.Result.top q
     | _ -> Queries.Result.top q
 

src/analyses/tutorials/gStoreWideningSol.ml

@@ -8,20 +8,6 @@ open GStoreWideningHelper
   **    THIS IS THE SOLUTION TO THIS TUTORIAL ANALYSIS, READING THIS BEFORE DOING THE TUTORIAL WILL SPOIL THE FUN.    **
   **                                          YOU HAVE BEEN WARNED.                                                   **
   **********************************************************************************************************************
-
-   There are two regression tests for this analysis, which you can run by calling:
-   -  ./regtest.sh 99 05
-   -  ./regtest.sh 99 06
-
-   Running these scripts also produces a visualization of the analysis results as a HTML file in the folder
-   result.
-
-   You can access these by spinning up a HTTP server, e.g., by calling `python3 -m http.server`
-
-   First fix the TODO: 1) to ensure unreachable code is marked as dead.
-   Then, tackle TODO: 2) to change this analysis so it tracks global variables
-
-   After modifying things, don't forget to compile by running `make`
 *)
 
 
@@ -42,7 +28,8 @@ module Analysis: SimplifiedSpec = struct
 
   (* Evaluate a single variable given a local state *)
   let eval_varinfo man state v =
-    if v.vglob then
+    if v.vglob &&  not (man.ask (Queries.TutorialEffectivelyLocal v))  then
+      (* TODO: 2) Modify so that we get values for globals *)
       man.global v
     else
       D.find v state
@@ -145,7 +132,10 @@ module Analysis: SimplifiedSpec = struct
       else
         (** TODO: 2) Modify so that we store values for globals *)
         (man.sideg v (cast_to_typ v.vtype (eval man state rval));
-         state)
+         if man.ask (Queries.TutorialEffectivelyLocal v) then
+           D.add v (cast_to_typ v.vtype (eval man state rval)) state
+         else
+           state)
     | None ->
       state
 
@@ -201,5 +191,70 @@ module Analysis: SimplifiedSpec = struct
       ) (D.bot ()) f.sformals
 end
 
+module ThreadSet = ConcDomain.ThreadSet
+
+module EffectivelyLocalAnalysis:SimplifiedSpec = struct
+  let name = "effectivelyLocalSol"
+
+  module D = Lattice.Unit
+  module C = Printable.Unit
+
+  (** TODO: 3) Modify so we store for each variable which thread ids are used to write to it *)
+  module V = Basetype.Variables
+  module G = ThreadSet
+
+  let startstate = ()
+  let startcontext = ()
+
+  let assign man state lval rval =
+    (* When the global initializers are evaluated, no threads exists yet *)
+    if !AnalysisState.global_initialization then
+      state
+    else
+      let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in
+      let singleton_set = ThreadSet.singleton tid in
+      match is_tracked_lval lval with
+      | Some v ->
+        (* TODO: 3) check if this is a global variable and if it is, record the thread id *)
+        if v.vglob then
+          (man.sideg v singleton_set; state)
+        else
+          state
+      | None ->
+        state
+
+  let query man state (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | Queries.TutorialEffectivelyLocal v when not !AnalysisState.global_initialization ->
+      (* TODO: 3) Get the current thread id, and check whether there is only one thread
+         accessing this variable, and whether it is the current one *)
+      let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in
+      let singleton_set = ThreadSet.singleton tid in
+      let writers = man.global v in
+      ThreadSet.equal singleton_set writers
+    | _ -> Queries.Result.top q
+
+  let branch man state e tv = state
+
+  let return _ state _ _ =
+    state
+
+  let body _ state f = ()
+
+  let enter man state _ f args = ()
+
+  let combine _ state _ lval _ _ = ()
+  let special man state lval _ _ = ()
+
+  let context _ (_, c) _ _ =
+    c
+
+  let threadenter _ _ f _ = ()
+end
+
+
+
+
 let _ =
-  MCPRegistry.registered_simplified_analysis (module Analysis:SimplifiedSpec)
+  MCPRegistry.registered_simplified_analysis (module Analysis:SimplifiedSpec);
+  MCPRegistry.registered_simplified_analysis (module EffectivelyLocalAnalysis:SimplifiedSpec)

tests/regression/99-tutorials/05-gstore-zero.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated '["gStoreWidening","assert"]'
+// SKIP PARAM: --set ana.activated '["gStoreWidening","assert","escape"]'
 #include <goblint.h>
 
 int main() {

tests/regression/99-tutorials/06-gstore-thread.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated '["gStoreWidening","assert","base","mallocWrapper"]' --set ana.base.privatization none --enable exp.globs_are_top
+// SKIP PARAM: --set ana.activated '["gStoreWidening","assert","base","mallocWrapper","escape"]' --set ana.base.privatization none --enable exp.globs_are_top
 // Additional analyses are activated so framework can handle thread creation
 #include <goblint.h>
 #include <pthread.h>
@@ -16,6 +16,7 @@ void* thread(void* arg) {
 }
 
 int main() {
+  global = 0;
   int x = 11;
 
   pthread_t t;

tests/regression/99-tutorials/07-gstore-mixed.c

@@ -0,0 +1,51 @@
+// SKIP PARAM: --set ana.activated '["gStoreWidening","effectivelyLocal","assert","base","mallocWrapper","thread","threadid","escape"]' --set ana.base.privatization none --enable exp.globs_are_top
+// Additional analyses are activated so framework can handle thread creation
+#include <goblint.h>
+#include <pthread.h>
+int global = 0;
+int thread_owned = 0;
+
+void* thread(void* arg) {
+
+  thread_owned = 42;
+  __goblint_check(thread_owned == 42);
+
+  if(global < 0) {
+     global = -58;
+  } else {
+    global = 1;
+  }
+
+  thread_owned = 11;
+  __goblint_check(thread_owned == 11);
+
+  return NULL;
+}
+
+int main() {
+  int x = 11;
+  global = 0;
+
+  pthread_t t;
+  pthread_create(&t, NULL, &thread, NULL);
+
+  global = x*x;
+
+  if(global > 200) {
+    global = -12;
+  }
+
+  __goblint_check(global < 200);
+  __goblint_check(global >= 0);
+  __goblint_check(thread_owned >= 0);
+
+
+  pthread_join(t, NULL);
+
+  global = 42;
+
+  // This is out of reach here
+  __goblint_check(global == 42);
+
+  return 0;
+}