Skip to content

Commit

Permalink
Add some additional materials
Browse files Browse the repository at this point in the history
  • Loading branch information
@karoliineh
karoliineh committed Sep 13, 2024
1 parent bce39b4 commit 0b8cdc7
Show file tree
Hide file tree
Showing 27 changed files with 1,322 additions and 0 deletions.
43 changes: 43 additions & 0 deletions adb_examples/debt-24-demo/README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
# 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 = {Karoliine Holter and Juhan Oskar Hennoste and Simmo Saan and Patrick Lam and Vesal Vojdani},
title = {Abstract Debugging with GobPie},
year = {2024},
isbn = {979-8-4007-1110-7/24/09},
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},
numpages = {2},
keywords = {Automated Software Verification, Abstract Interpretation, Explainability, Visualization, Data Race Detection},
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).
12 changes: 12 additions & 0 deletions adb_examples/debt-24-demo/context-sensitivity.c
View file
Original file line number Diff line number Diff line change
@@ -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;
}
17 changes: 17 additions & 0 deletions adb_examples/debt-24-demo/fun-pointers.c
View file
Original file line number Diff line number Diff line change
@@ -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"
}
18 changes: 18 additions & 0 deletions adb_examples/debt-24-demo/path-sensitivity.c
View file
Original file line number Diff line number Diff line change
@@ -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);
}
}
6 changes: 6 additions & 0 deletions adb_examples/debt-24-demo/smtprc-example/gobpie.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
{
"goblintConf" : "smtprc.json",
"abstractDebugging": true,
"incrementalAnalysis": false,
"showCfg": true
}
131 changes: 131 additions & 0 deletions adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/Makefile
View file
Original file line number Diff line number Diff line change
@@ -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 " "


158 changes: 158 additions & 0 deletions adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/compile_commands.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,158 @@
[
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-o",
"smtprc.o",
"smtprc.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/smtprc.c",
"output": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/smtprc.o"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-o",
"scan_engine.o",
"scan_engine.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/scan_engine.c",
"output": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/scan_engine.o"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-o",
"options.o",
"options.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/options.c",
"output": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/options.o"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-o",
"utils.o",
"utils.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/utils.c",
"output": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/utils.o"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-o",
"parse_config_files.o",
"parse_config_files.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/parse_config_files.c",
"output": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/parse_config_files.o"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-o",
"parse_args.o",
"parse_args.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/parse_args.c",
"output": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/parse_args.o"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-pthread",
"smtprc.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/smtprc.c"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-pthread",
"scan_engine.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/scan_engine.c"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-pthread",
"options.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/options.c"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-pthread",
"utils.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/utils.c"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-pthread",
"parse_config_files.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/parse_config_files.c"
},
{
"arguments": [
"/usr/bin/gcc",
"-Wall",
"-g",
"-c",
"-pthread",
"parse_args.c"
],
"directory": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3",
"file": "/home/ubuntu/goblint/gobpie-demo-debt-24/smtprc-example/smtprc-2.0.3/parse_args.c"
}
]
Loading

0 comments on commit 0b8cdc7

Please sign in to comment.