Add DEBT'24 (and Onward!24) demo materials

adb_examples/debt-24-demo/README.md

@@ -0,0 +1,40 @@
+# Abstract Debugging with GobPie demo (DEBT'24)
+
+This folder contains the materials for the demo presentation of Abstract Debugging
+with GobPie at the [Second Workshop on Future Debugging Techniques (DEBT'24)](https://conf.researchr.org/details/issta-ecoop-2024/debt-2024-papers/4/Abstract-Debugging-with-GobPie).
+
+:movie_camera: There is a pre-recorded [video](https://youtu.be/KtLFdxMAdD8) of using the abstract debugger on the source code of SMTP Relay Checker, showcasing how to debug and fix a data race warning using the abstract debugger.
+
+:page_facing_up: Cite with:
+```
+@inproceedings{10.1145/3678720.3685320,
+  author    = {Holter, Karoliine and Hennoste, Juhan Oskar and Saan, Simmo and Lam, Patrick and Vojdani, Vesal},
+  title     = {Abstract Debugging with GobPie},
+  year      = {2024},
+  isbn      = {9798400711107},
+  publisher = {Association for Computing Machinery},
+  address   = {New York, NY, USA},
+  url       = {https://doi.org/10.1145/3678720.3685320},
+  doi       = {10.1145/3678720.3685320},
+  booktitle = {Proceedings of the 2nd ACM International Workshop on Future Debugging Techniques},
+  pages     = {32–33},
+  numpages  = {2},
+  keywords  = {Abstract Interpretation, Automated Software Verification, Data Race Detection, Explainability, Visualization},
+  location  = {Vienna, Austria},
+  series    = {DEBT 2024}
+}
+```
+
+### Examples
+
+The directory contains the following example programs:
+
+1. The [example program](./paper-example/example.c) illustrated in the paper.
+2. An [extracted version](./smtprc-example) of the Smtp Open Relay Checker ([smtprc](https://sourceforge.net/projects/smtprc/files/smtprc/smtprc-2.0.3/)).
+   Some parts of the code in this project were omitted to speed up the analysis for demonstration purposes.
+
+Some illustrative example programs for demonstrating the abstract debugger's behavior <br>
+
+- with [context-sensitive](context-sensitivity.c) analysis results;
+- with [path-sensitive](path-sensitivity.c) analysis results;
+- in case of function calls through [function pointers](fun-pointers.c).

adb_examples/debt-24-demo/context-sensitivity.c

@@ -0,0 +1,12 @@
+void f(int x) {
+    assert(x - 1 < x); // Using breakpoint: two different contexts will be displayed in the "call stack" panel
+    if (x > 1 ) {
+        printf("Hello!");
+    }
+}
+
+int main() {
+    f(rand() % 10);
+    f(42);
+    return 0;
+}

adb_examples/debt-24-demo/fun-pointers.c

@@ -0,0 +1,17 @@
+void f(int x) {
+  printf("%i", x);
+}
+
+void g(int x) {
+  printf("%i", x + 100);
+}
+
+int main() {
+  int i = rand() % 100;
+  void (*fp)(int);
+  if (i >= 50)
+    fp = &f;
+  else
+    fp = &g;
+  fp(i - 30); // Using breakpoint: step into is unambiguous and requests "step into target"
+}

adb_examples/debt-24-demo/goblint.json

@@ -0,0 +1,25 @@
+{
+  "files": [
+    "context-sensitivity.c"
+  ],
+  "ana": {
+    "int": {
+      "def_exc" : false,
+      "interval": true
+    },
+    "activated": ["expRelation", "base", "threadid", "threadflag", "threadreturn",
+            "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp",
+            "assert", "pthreadMutexType", "apron"]
+  },
+  "sem": {
+    "lock": {
+      "fail": true
+    }
+  },
+  "warn": {
+    "imprecise": false,
+    "deadcode": false,
+    "info": false
+  },
+  "allglobs": true
+}

adb_examples/debt-24-demo/gobpie.json

@@ -0,0 +1,6 @@
+{
+    "goblintConf" : "goblint.json",
+    "abstractDebugging": true,
+    "incrementalAnalysis": false,
+    "showCfg": true
+}

adb_examples/debt-24-demo/paper-example/.vscode/launch.json

@@ -0,0 +1,28 @@
+{
+    "configurations": [
+        {
+            "name": "(gdb) Launch",
+            "type": "cppdbg",
+            "request": "launch",
+            "program": "${workspaceFolder}/a.out",
+            "args": [],
+            "stopAtEntry": false,
+            "cwd": "${fileDirname}",
+            "environment": [],
+            "externalConsole": false,
+            "MIMode": "gdb",
+            "setupCommands": [
+                {
+                    "description": "Enable pretty-printing for gdb",
+                    "text": "-enable-pretty-printing",
+                    "ignoreFailures": true
+                },
+                {
+                    "description": "Set Disassembly Flavor to Intel",
+                    "text": "-gdb-set disassembly-flavor intel",
+                    "ignoreFailures": true
+                }
+            ]
+        }
+    ]
+}

adb_examples/debt-24-demo/paper-example/example.c

@@ -0,0 +1,37 @@
+#include <stdio.h>
+#include <pthread.h>
+
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+typedef enum { PUBLISH, CACHE } ThreadAction;
+int global;
+
+int f(ThreadAction action) {
+    int cache = 0;
+    switch (action) {
+        case CACHE:
+            printf("Store in local cache!\n");
+            cache = 42;
+        case PUBLISH:
+            printf("Publish work!\n");
+            global = 42;
+    }
+}
+
+void *t(void *arg) {
+    if (pthread_mutex_trylock(&mutex)) {
+        f(CACHE);
+    } else {
+        f(PUBLISH);
+        pthread_mutex_unlock(&mutex);
+    }
+}
+
+
+int main() {
+    pthread_t t1, t2;
+    pthread_create(&t1, NULL, t, NULL);
+    pthread_create(&t2, NULL, t, NULL);
+    pthread_join(t1, NULL);
+    pthread_join(t2, NULL);
+    return 0;
+}

adb_examples/debt-24-demo/paper-example/goblint.json

@@ -0,0 +1,22 @@
+{
+  "files": [
+    "example.c"
+  ],
+  "ana": {
+    "int": {
+      "def_exc" : false,
+      "interval": true
+    }
+  },
+  "sem": {
+    "lock": {
+      "fail": true
+    }
+  },
+  "warn": {
+    "imprecise": false,
+    "deadcode": false,
+    "info": false
+  },
+  "allglobs": true
+}

adb_examples/debt-24-demo/paper-example/gobpie.json

@@ -0,0 +1,6 @@
+{
+    "goblintConf" : "goblint.json",
+    "abstractDebugging": true,
+    "showCfg": true,
+    "incrementalAnalysis": false
+}

adb_examples/debt-24-demo/path-sensitivity.c

@@ -0,0 +1,18 @@
+#include <pthread.h>
+
+pthread_mutex_t mutex; 
+
+int main(void) {
+    int do_work = rand();
+    int work = 0;
+    if (do_work) {
+        pthread_mutex_lock(&mutex);
+    }
+
+    // ...
+
+    if (do_work) {
+        work++;
+        pthread_mutex_unlock(&mutex);
+    }
+}

adb_examples/debt-24-demo/smtprc-example/gobpie.json

@@ -0,0 +1,6 @@
+{
+    "goblintConf" : "smtprc-extraction.json",
+    "abstractDebugging": true,
+    "incrementalAnalysis": false,
+    "showCfg": true
+}

adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/Makefile

@@ -0,0 +1,131 @@
+CC=gcc
+CFLAGS=-Wall -g 
+INSTALL_PROG=install -c
+MKDIR=mkdir -p
+REMOVE=rm -rf
+LIBS=-lsocket -lnsl -lrt -lpthread
+
+
+all: freebsd
+install: freebsd_install
+uninstall: freebsd_uninstall
+
+
+
+linux: freebsd_build
+linux_install: freebsd_install_start
+linux_uninstall: freebsd_uninstall_start
+
+freebsd: freebsd_build
+freebsd_install: freebsd_install_start
+freebsd_uninstall: freebsd_uninstall_start
+
+solaris: solaris_err
+solaris_install: solaris_err
+solaris_uninstall: solaris_err
+
+solaris_err: 
+	@echo " "
+	@echo " "
+	@echo " "
+	@echo "	Unfortunatly SmtpRC does not yet work correctly"
+	@echo "	under Solaris."
+	@echo " "
+	@echo " "
+	@echo "	To use SmtpRC you must run it on a *BSD or Linux"
+	@echo "	based OS"
+	@echo " "
+	@echo " "
+	@echo " "
+	@echo " "
+	@echo " "
+	@echo " "
+
+freebsd_build: smtprc.o scan_engine.o options.o utils.o parse_config_files.o parse_args.o
+	${CC} $(CFLAGS) -c smtprc.c scan_engine.c options.c utils.c parse_config_files.c parse_args.c -pthread
+	${CC} -o smtprc smtprc.o scan_engine.o options.o utils.o parse_config_files.o parse_args.o -pthread
+
+freebsd_install_start:
+	${INSTALL_PROG} smtprc /usr/local/bin/smtprc
+	${INSTALL_PROG} gsmtprc /usr/local/bin/gsmtprc
+	-${MKDIR} /usr/local/etc/smtprc
+	${INSTALL_PROG} auto.conf /usr/local/etc/smtprc/auto.conf
+	${INSTALL_PROG} email.tmpl /usr/local/etc/smtprc/email.tmpl
+	${INSTALL_PROG} rcheck.conf /usr/local/etc/smtprc/rcheck.conf
+	-${MKDIR} /usr/local/share/doc/smtprc
+	${INSTALL_PROG} README /usr/local/share/doc/smtprc/README
+	${INSTALL_PROG} FAQ /usr/local/share/doc/smtprc/FAQ
+	${INSTALL_PROG} smtprc.1 /usr/local/man/man1/smtprc.1
+	${INSTALL_PROG} gsmtprc.1 /usr/local/man/man1/gsmtprc.1
+
+freebsd_uninstall_start:
+	-${REMOVE} /usr/local/etc/smtprc
+	-${REMOVE} /usr/local/share/doc/smtprc
+	-${REMOVE} /usr/local/bin/smtprc
+	-${REMOVE} /usr/local/man/man1/smtprc.1
+	-${REMOVE} /usr/local/man/man1/gsmtprc.1
+	-${REMOVE} /usr/local/bin/gsmtprc
+
+solaris_build: smtprc.o scan_engine.o options.o utils.o parse_config_files.o parse_args.o
+				${CC} $(CFLAGS) -c smtprc.c scan_engine.c options.c utils.c parse_config_files.c parse_args.c
+				${CC} -o smtprc smtprc.o scan_engine.o options.o utils.o parse_config_files.o parse_args.o ${LIBS}
+
+solaris_install_start:
+	${INSTALL_PROG} /usr/local/bin smtprc
+	-${MKDIR} /usr/local/etc/smtprc
+	${INSTALL_PROG} /usr/local/etc/smtprc auto.conf
+	${INSTALL_PROG} /usr/local/etc/smtprc email.tmpl
+	${INSTALL_PROG} /usr/local/etc/smtprc rcheck.conf
+	-${MKDIR} /usr/local/doc/smtprc
+	${INSTALL_PROG} /usr/local/doc/smtprc README
+	${INSTALL_PROG} /usr/local/doc/smtprc FAQ
+	${INSTALL_PROG} /usr/share/man/man1 smtprc.1
+	${INSTALL_PROG} /usr/share/man/man1 gsmtprc.1
+	${INSTALL_PROG} /usr/local/bin gsmtprc
+
+solaris_uninstall_start:
+	-${REMOVE} /usr/local/etc/smtprc
+	-${REMOVE} /usr/local/share/doc/smtprc
+	-${REMOVE} /usr/local/bin/smtprc
+	-${REMOVE} /usr/local/man/man1/smtprc.1
+	-${REMOVE} /usr/local/man/man1/gsmtprc.1
+	-${REMOVE} /usr/local/bin/gsmtprc
+
+
+clean:
+	-${REMOVE} *.o smtprc
+
+message:
+	@echo " "
+	@echo " "
+	@echo " "
+	@echo "	You need to specify what OS to make...." 
+	@echo " "
+	@echo "	The three types currently supported are:"  
+	@echo " "
+	@echo " "
+	@echo "	freebsd"
+	@echo "	linux"
+	@echo " solaris"
+	@echo " "
+	@echo " "
+	@echo " "
+	@echo "	Type make <os> to bulid the package and then"
+	@echo "	make <os>_install to install the package"
+	@echo "	(Swapping <os> for one of the supported types"
+	@echo " "
+	@echo " "
+	@echo "	Example: "
+	@echo " "
+	@echo "	make freebsd"
+	@echo "	make freebsd_install"
+	@echo "	make clean"
+	@echo " "
+	@echo " "
+	@echo "	Also:"
+	@echo "	make freebsd_unistall"
+	@echo " "
+	@echo " "
+	@echo " "
+
+