Traces article implementation

.gitignore

@@ -52,3 +52,5 @@ goblint.bc.js
 *.orig
 
 sv-comp/goblint.zip
+
+privPrecCompare*/

conf/traces.json

@@ -0,0 +1,43 @@
+{
+  "ana": {
+    "int": {
+      "def_exc": true,
+      "interval": false,
+      "enums": true
+    }
+  },
+  "sem": {
+    "unknown_function": {
+      "invalidate": {
+        "globals": false
+      },
+      "spawn": true
+    },
+    "builtin_unreachable": {
+      "dead_code": true
+    }
+  },
+  "exp": {
+    "priv-distr-init": false,
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc"
+      ]
+    }
+  }
+}

scripts/privPrecCompare-creduce.sh

@@ -0,0 +1,32 @@
+#!/bin/bash
+
+# creduce ./scripts/privPrecCompare-creduce.sh ./pfscan_comb.c
+
+set -e
+
+gcc -c -Werror=implicit-function-declaration ./tegra20.c
+
+GOBLINTDIR="/home/simmo/dev/goblint/sv-comp/goblint"
+# OPTS="./pfscan_comb.c --enable custom_libc"
+OPTS="./tegra20.c --conf $GOBLINTDIR/conf/traces.json --enable ana.sv-comp.functions"
+# PRIVS=(protection protection-read write mine-W lock write+lock)
+PRIVS=(protection write)
+INTERESTING="protection more precise than write"
+OUTDIR="privPrecCompare-creduce"
+
+
+mkdir -p $OUTDIR
+
+for PRIV in "${PRIVS[@]}"; do
+    echo $PRIV
+    PRIVDUMP="$OUTDIR/$PRIV"
+    LOG="$OUTDIR/$PRIV.log"
+    rm -f $PRIVDUMP
+    $GOBLINTDIR/goblint --sets exp.privatization $PRIV --sets exp.priv-prec-dump $PRIVDUMP $OPTS -v --enable dbg.debug &> $LOG
+    grep -F "Function definition missing" $LOG && exit 1
+done
+
+PRIVDUMPS=("${PRIVS[*]/#/$OUTDIR/}") # why [*] here?
+$GOBLINTDIR/_build/default/src/privPrecCompare.exe $PRIVDUMPS 2>&1 | tee "$OUTDIR/compare.txt"
+
+grep -F "$INTERESTING" "$OUTDIR/compare.txt"

scripts/privPrecCompare.sh

@@ -0,0 +1,17 @@
+#!/bin/bash
+
+# ./scripts/privPrecCompare.sh ../goblint-bench/pthread/pfscan_comb.c --enable custom_libc
+
+PRIVS=(protection protection-read write mine-W lock write+lock)
+OUTDIR="privPrecCompare"
+
+mkdir -p $OUTDIR
+
+for PRIV in "${PRIVS[@]}"; do
+    echo $PRIV
+    PRIVDUMP="$OUTDIR/$PRIV"
+    ./goblint --sets exp.privatization $PRIV --sets exp.priv-prec-dump $PRIVDUMP "$@"
+done
+
+PRIVDUMPS=("${PRIVS[*]/#/$OUTDIR/}") # why [*] here?
+./_build/default/src/privPrecCompare.exe $PRIVDUMPS 2>&1 | tee "$OUTDIR/compare.txt"

scripts/update_suite.rb

@@ -1,5 +1,7 @@
 #!/usr/bin/env ruby
 
+# gobopt environment variable can be used to override goblint defaults and PARAMs
+
 require 'find'
 require 'fileutils'
 require 'timeout'
@@ -116,6 +118,7 @@ def to_s
   next unless thegroup.nil? or groupname == thegroup or # group x = only group x
     (thegroup.start_with?"-" and groupname != thegroup[1..-1]) # group -x = all groups but x
   grouppath = File.expand_path(d, testfiles)
+  next unless File.directory?(grouppath)
   group = Dir.open(grouppath)
   group.sort.each do |f|
     next if File.basename(f)[0] == ?.
@@ -230,7 +233,7 @@ def to_s
     pgid = Process.getpgid(pid)
     puts "\t #{id} reached timeout of #{timeout}s!".red + " Killing pgid #{pgid}..."
     timedout.push id
-    Process.kill('INT', -1*pgid)
+    Process.kill('KILL', -1*pgid)
     p.ok = false
     return p
   end

src/analyses/arinc.ml

@@ -32,16 +32,16 @@ module Functions = struct
     else
       match List.last args with
       | AddrOf lv ->
-        Some (fun set ->
+        Some (
             let ret = if GobConfig.get_bool "ana.arinc.assume_success" then ret_success else if List.mem fname with_timeout then ret_any else ret_no_timeout in
             let v = vd ret in
             debug_doc @@ Pretty.dprintf "effect of %s: set %a to %a" fname d_lval lv ValueDomain.Compound.pretty v;
-            set lv v
+            [(lv, v)]
           )
       | _ -> None
 end
 
-module Spec : Analyses.Spec =
+module Spec : Analyses.MCPSpec =
 struct
   include Analyses.DefaultSpec
 
@@ -260,7 +260,8 @@ struct
     (* M.debug_each @@ "BODY " ^ f.svar.vname ^" @ "^ string_of_int (!Tracing.current_loc).line; *)
     (* if not (is_single ctx || !Goblintutil.global_initialization || fst (ctx.global part_mode_var)) then raise Analyses.Deadcode; *)
     (* checkPredBot ctx.local "body" f.svar [] *)
-    let base_context = Base.Main.context_cpa @@ Obj.obj @@ List.assoc "base" ctx.presub in
+    let module BaseMain = (val Base.get_main ()) in
+    let base_context = BaseMain.context_cpa @@ Obj.obj @@ List.assoc "base" ctx.presub in
     let context_hash = Hashtbl.hash (base_context, ctx.local.pid) in
     { ctx.local with ctx = Ctx.of_int (Int64.of_int context_hash) }
 
@@ -662,10 +663,10 @@ struct
       ) tasks
     in
     let f_d = snd (Tasks.choose tasks_f) in
-    { f_d with pre = d.pre }
+    [{ f_d with pre = d.pre }]
 
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
 end
 
 let _ =
-  MCP.register_analysis ~dep:["base"] (module Spec : Spec)
+  MCP.register_analysis ~dep:["base"] (module Spec : MCPSpec)