diff --git a/adb_examples/debt-24-demo/README.md b/adb_examples/debt-24-demo/README.md new file mode 100644 index 0000000..1dd870d --- /dev/null +++ b/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
+ +- 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). diff --git a/adb_examples/debt-24-demo/context-sensitivity.c b/adb_examples/debt-24-demo/context-sensitivity.c new file mode 100644 index 0000000..1ce25d0 --- /dev/null +++ b/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; +} \ No newline at end of file diff --git a/adb_examples/debt-24-demo/fun-pointers.c b/adb_examples/debt-24-demo/fun-pointers.c new file mode 100644 index 0000000..0dc16b1 --- /dev/null +++ b/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" +} \ No newline at end of file diff --git a/adb_examples/debt-24-demo/goblint.json b/adb_examples/debt-24-demo/goblint.json new file mode 100644 index 0000000..d9bcb0f --- /dev/null +++ b/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 +} diff --git a/adb_examples/debt-24-demo/gobpie.json b/adb_examples/debt-24-demo/gobpie.json new file mode 100644 index 0000000..577abd1 --- /dev/null +++ b/adb_examples/debt-24-demo/gobpie.json @@ -0,0 +1,6 @@ +{ + "goblintConf" : "goblint.json", + "abstractDebugging": true, + "incrementalAnalysis": false, + "showCfg": true +} diff --git a/adb_examples/debt-24-demo/paper-example/.vscode/launch.json b/adb_examples/debt-24-demo/paper-example/.vscode/launch.json new file mode 100644 index 0000000..03dacaa --- /dev/null +++ b/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 + } + ] + } + ] +} \ No newline at end of file diff --git a/adb_examples/debt-24-demo/paper-example/example.c b/adb_examples/debt-24-demo/paper-example/example.c new file mode 100644 index 0000000..065aee5 --- /dev/null +++ b/adb_examples/debt-24-demo/paper-example/example.c @@ -0,0 +1,37 @@ +#include +#include + +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; +} diff --git a/adb_examples/debt-24-demo/paper-example/goblint.json b/adb_examples/debt-24-demo/paper-example/goblint.json new file mode 100644 index 0000000..5c67c82 --- /dev/null +++ b/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 +} diff --git a/adb_examples/debt-24-demo/paper-example/gobpie.json b/adb_examples/debt-24-demo/paper-example/gobpie.json new file mode 100644 index 0000000..0283899 --- /dev/null +++ b/adb_examples/debt-24-demo/paper-example/gobpie.json @@ -0,0 +1,6 @@ +{ + "goblintConf" : "goblint.json", + "abstractDebugging": true, + "showCfg": true, + "incrementalAnalysis": false +} diff --git a/adb_examples/debt-24-demo/path-sensitivity.c b/adb_examples/debt-24-demo/path-sensitivity.c new file mode 100644 index 0000000..165fd3b --- /dev/null +++ b/adb_examples/debt-24-demo/path-sensitivity.c @@ -0,0 +1,18 @@ +#include + +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); + } +} \ No newline at end of file diff --git a/adb_examples/debt-24-demo/smtprc-example/gobpie.json b/adb_examples/debt-24-demo/smtprc-example/gobpie.json new file mode 100644 index 0000000..5c58477 --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/gobpie.json @@ -0,0 +1,6 @@ +{ + "goblintConf" : "smtprc-extraction.json", + "abstractDebugging": true, + "incrementalAnalysis": false, + "showCfg": true +} diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/Makefile b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/Makefile new file mode 100644 index 0000000..142ff93 --- /dev/null +++ b/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 to bulid the package and then" + @echo " make _install to install the package" + @echo " (Swapping 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 " " + + diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/compile_commands.json b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/compile_commands.json new file mode 100644 index 0000000..175d609 --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/compile_commands.json @@ -0,0 +1,88 @@ +[ + { + "arguments": [ + "/usr/bin/gcc", + "-Wall", + "-g", + "-c", + "-o", + "scan_engine.o", + "scan_engine.c" + ], + "directory": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction", + "file": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/scan_engine.c", + "output": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/scan_engine.o" + }, + { + "arguments": [ + "/usr/bin/gcc", + "-Wall", + "-g", + "-c", + "-pthread", + "smtprc.c" + ], + "directory": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction", + "file": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/smtprc.c" + }, + { + "arguments": [ + "/usr/bin/gcc", + "-Wall", + "-g", + "-c", + "-pthread", + "scan_engine.c" + ], + "directory": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction", + "file": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/scan_engine.c" + }, + { + "arguments": [ + "/usr/bin/gcc", + "-Wall", + "-g", + "-c", + "-pthread", + "options.c" + ], + "directory": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction", + "file": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/options.c" + }, + { + "arguments": [ + "/usr/bin/gcc", + "-Wall", + "-g", + "-c", + "-pthread", + "utils.c" + ], + "directory": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction", + "file": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/utils.c" + }, + { + "arguments": [ + "/usr/bin/gcc", + "-Wall", + "-g", + "-c", + "-pthread", + "parse_config_files.c" + ], + "directory": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction", + "file": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_config_files.c" + }, + { + "arguments": [ + "/usr/bin/gcc", + "-Wall", + "-g", + "-c", + "-pthread", + "parse_args.c" + ], + "directory": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction", + "file": "/home/ubuntu/GobPie/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_args.c" + } +] diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/options.c b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/options.c new file mode 100644 index 0000000..474834c --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/options.c @@ -0,0 +1,24 @@ +/*************************************************************************** + options.c - description + ------------------- + begin : Wed May 21 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + + +#include "options.h" +#include "utils.h" + +extern struct options o; +extern struct flags f; + diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/options.h b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/options.h new file mode 100644 index 0000000..62aa32d --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/options.h @@ -0,0 +1,113 @@ +/*************************************************************************** + options.h - description + ------------------- + begin : Wed May 21 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + +#ifndef SMTPRC_OPTIONS_H +#define SMTPRC_OPTIONS_H + +/****************************includes**************************************/ + +#include +#include +#include +#include + + +/*****************************structures***********************************/ + +struct options { + + //config options + unsigned int time; //timestamp + unsigned short int number_of_threads; //max number of threads + unsigned short int c_timeout; //connect timeout + unsigned short int r_timeout; //read timeout + unsigned short int m_timeout; //wait for mail timeout + unsigned short int cur_threads; //current number of threads + unsigned short int no_rules; //number of rules to scan with; + unsigned long no_hostnames; //number of hosts to scan + unsigned long cur_host; //current host being scanned + + pthread_t *tid; + + char *email_address; //email_addres to relay to + char *ip_range; //ip address range + char *ip_list; //ip list file + char *mailbox; //mailbox file + char *auto_config_file; //auto config filename + char *generate_file; //filename to generate auto config file + char *config_file; //relay check config file + char *email_template; //email template to be sent through servers being checked + char *name; //name part of the email address specified with -b + char *domain; //domain part of the email address specified with -b + + //output file formats + char *html_file; //output html filename + char *html_path; //path to output html file + char *xml_file; //output xml filename + char *xml_path; //path to xml file + char *machine_file; //output machine readable filename + char *machine_path; //path to machine file + char *text_file; //output text filename + char *text_path; //path to text file + + //email template //email body to send through servers + char *email; //email subject to send through servers + char *email_subject; + + //total time taken + unsigned char hours; + unsigned char mins; + unsigned char seconds; + +}; + + +//If a flag is set to TRUE then that option +//has been selected. +struct flags { + + unsigned char debug; //debugging mode + unsigned char verbose; //be verbose + unsigned char check_mailbox; //check mailbox after scanning + unsigned char maildir; //mailbox format is maildir + unsigned char mbox; //mailbox format is maildir + unsigned char pop; //mailbox format is maildir + unsigned char auto_config; //auto config file specified + unsigned char generate_config; //generate a suto config file + unsigned char output_html; //output to html + unsigned char output_text; //output to text file + unsigned char output_machine; //output to machine readable format + unsigned char output_xml; //output to xml + unsigned char resolve_hostnames; //try to resolve ips to hostnames + unsigned char display_only_ips; //only output ips not hostnames + unsigned char ip_range; //ip list file specified. + unsigned char ip_list; //got ip list + unsigned char send_email; //send email through servers + unsigned char config_file; //got config file + unsigned char email_template; //got email template + unsigned char got_name_macro; //--NAME-- macro specified in the config file + unsigned char got_email; //got email address specified with -b + unsigned char threads; //threads have been specified + unsigned char display_all; //display all results even those that fail + +}; + + +/*****************************prototypes************************************/ + +#endif + diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/options.o b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/options.o new file mode 100644 index 0000000..21a1e3a Binary files /dev/null and b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/options.o differ diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_args.c b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_args.c new file mode 100644 index 0000000..ec83e33 --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_args.c @@ -0,0 +1,126 @@ +/*************************************************************************** + parse_args.c - description + ------------------- + begin : Wed May 21 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + +#include "parse_args.h" +#include "utils.h" + +struct options o; +struct flags f; + + +void parse_args(int argc, char * const *argv) { + + + char c; + + while((c = getopt(argc, argv, "ab:c:de:f:g:hi:j:k:l:m:no:p:qr:s:tu:vw:x:y:"))!=-1) { + + + switch(c) { + case 'a': //display all results even those that pass + f.display_all = TRUE; + break; + case 'b': //email addy to use to replace --NAME-- --DOMAIN-- + f.send_email = TRUE; + o.email_address=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.email_address, optarg, strlen(optarg)); + o.email_address[strlen(optarg)] = '\0'; + break; + case 'c': //Specify the config file to use + f.config_file = TRUE; + //o.config_file=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.config_file, optarg, strlen(optarg)); + o.config_file[strlen(optarg)] = '\0'; + break; + case 'd': //Switch on DEBUG MODE + f.debug = TRUE; + break; + case 'e': //Specify a local mailbox + f.check_mailbox = TRUE; + f.mbox = TRUE; + o.mailbox=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.mailbox, optarg, strlen(optarg)); + o.mailbox[strlen(optarg)] = '\0'; + break; + case 'i': //specify an ip list + f.ip_list = TRUE; + o.ip_list=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.ip_list, optarg, strlen(optarg)); + o.ip_list[strlen(optarg)] = '\0'; + break; + case 'j': //specify an auto config file + f.auto_config = TRUE; + o.auto_config_file=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.auto_config_file, optarg, strlen(optarg)); + o.auto_config_file[strlen(optarg)] = '\0'; + break; + case 'k': //generate a config file + f.generate_config = TRUE; + o.generate_file=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.generate_file, optarg, strlen(optarg)); + o.generate_file[strlen(optarg)] = '\0'; + break; + case 'm': //TIME OUT before checking mail file + o.m_timeout = atoi(optarg); + break; + case 'n': //Resolve hostnames + f.resolve_hostnames = TRUE; + break; + case 'o': //PRINT OUTPUT IN MACHINE READABLE FORMAT + f.output_machine = TRUE; + o.machine_file=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.machine_file, optarg, strlen(optarg)); + o.machine_file[strlen(optarg)] = '\0'; + break; + case 'p': //NUMBER OF THREADS + o.number_of_threads = atoi(optarg); + break; + case 'q': + f.display_only_ips = TRUE; + break; + case 's': //IP RANGE TO SCAN + f.ip_range = TRUE; + o.ip_range=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.ip_range, optarg, strlen(optarg)); + o.ip_range[strlen(optarg)] = '\0'; + break; + case 'u': //maildir mailbox + f.check_mailbox = TRUE; + f.maildir = TRUE; + o.mailbox=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.mailbox, optarg, strlen(optarg)); + o.mailbox[strlen(optarg)] = '\0'; + break; + case 'y': //specify email file + f.email_template = TRUE; + //o.email_template=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.email_template, optarg, strlen(optarg)); + o.email_template[strlen(optarg)] = '\0';; + break; + case 'z': //output to html file + f.output_machine = TRUE; + o.machine_file=s_malloc((strlen(optarg)+1) * sizeof(char)); + strncpy(o.machine_file, optarg, strlen(optarg)); + o.machine_file[strlen(optarg)] = '\0'; + default: + return; + } + } + + return; + +} diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_args.h b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_args.h new file mode 100644 index 0000000..05cc42f --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_args.h @@ -0,0 +1,43 @@ +/*************************************************************************** + parse_args.h - description + ------------------- + begin : Wed May 21 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + + +#ifndef SMTPRC_PARSE_ARGS_H +#define SMTPRC_PARSE_ARGS_H + +#include "options.h" +#include "utils.h" +#include +#include +#include + +/********************************defines************************************/ + +#ifndef FALSE +#define FALSE 0 +#endif + +#ifndef TRUE +#define TRUE 1 +#endif + +/******************************prototypes***********************************/ + +void parse_args(int argc, char * const *argv); + +#endif + diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_args.o b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_args.o new file mode 100644 index 0000000..3ce0e73 Binary files /dev/null and b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_args.o differ diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_config_files.c b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_config_files.c new file mode 100644 index 0000000..8e5dfdc --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_config_files.c @@ -0,0 +1,57 @@ +/*************************************************************************** + parse_config_files.c - description + ------------------- + begin : Wed May 21 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + +#include "utils.h" +#include "options.h" + +extern struct options o; +extern struct flags f; + + +/* + * Parse ip address range into individual ip addresses + * + * This is really quite messy and could do with a rewrite + * but it's staying for now. + * + */ + +int get_ip_range(char *iprange) { + + int start[4]; + int end[4]; + int i = 0; + + for(i=0;i<4;i++) { + start[i] = 1; + end[i] = 255; + } + + for(i=0;i<1;i++) { + for(;start[i]<=end[i];start[i]++) { + for(;start[i+1]<=end[i+1];start[i+1]++) { + for(;start[i+2]<=end[i+2];start[i+2]++) { + for(;start[i+3]<=end[i+3];start[i+3]++) { + o.no_hostnames++; + } + } + } + } + } + + return(0); +} \ No newline at end of file diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_config_files.h b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_config_files.h new file mode 100644 index 0000000..1bf0e9f --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_config_files.h @@ -0,0 +1,31 @@ +/*************************************************************************** + parse_config_files.h - description + ------------------- + begin : Wed May 21 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + + +#ifndef SMTPRC_PARSE_CONFIG_FILES_H +#define SMTPRC_PARSE_CONFIG_FILES_H + +#include +#include +#include + +/******************************prototypes************************************/ + +int get_ip_range(char *iprange); + +#endif + diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_config_files.o b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_config_files.o new file mode 100644 index 0000000..ffe8952 Binary files /dev/null and b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/parse_config_files.o differ diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/relay.h b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/relay.h new file mode 100644 index 0000000..f210caf --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/relay.h @@ -0,0 +1,134 @@ +/*************************************************************************** + relay.h - description + ------------------- + begin : Wed May 21 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + + +#ifndef SMTPRC_RELAY_H +#define SMTPRC_RELAY_H + +/*****************************INCLUDES**************************************/ + + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + + +/****************************DEFINES****************************************/ + +#ifndef _REENTRANT +#define _REENTRANT +#endif +#ifndef MSG_NOSIGNAL +#define MSG_NOSIGNAL 0x4000 +#endif + +#define PORT 25 //SMTP Port +#define MAXDATA 8192 //Max data size +#define LARGESTRING 65535 //Large string size +#define CTIMEOUT 10 //Default connect timeout +#define RTIMEOUT 60 //Default read timeout +#define MTIMEOUT 60 //Default wait for email timeout +#define THREAD_DEFAULT 1000 //default number of threads to scan with +#define CONFIG_FILE "/usr/local/etc/smtprc/rcheck.conf" +#define EMAIL_TEMPLATE "/usr/local/etc/smtprc/email.tmpl" + +#define RSET "RSET\r\n" +#define DATA "DATA\r\n" +#define QUIT "QUIT\r\n" + +#define SLASHDOT "./" + +#define PADDING 60 + + + +/****************************DATA STRUCTURES*********************************/ + +typedef struct _check { //This structure will hole all of the check info + + unsigned char failed; + unsigned char passed; + unsigned char error_code; + + char *helo; //helo sent to the sever + char *mail_from; //mail from sent to the server + char *rcpt_to; //rcpt to sent to the server + + char *r_banner; //banner reply + char *r_helo; //helo reply etc etc + char *r_mail_from; + char *r_rcpt_to; + char *r_data_start; + char *r_data_end; + char *r_reset; + +} +check; + +typedef struct _host { //this struct will hold all of the host info. + + unsigned char smtp_open; //this indicates if the server has port 25 open + unsigned char resolved; //this indicates wether the ip address was resolved + unsigned char fatal_error; //this indicates a fatal error + unsigned char fatal; + + char *ip_address; + char *hostname; + + char *r_quit; + + check **smtp_check; + +} +host; + +typedef struct _rule { + + char *helo; + char *mail_from; + char *rcpt_to; + +} +rule; + + + + + + +#endif + diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/scan_engine.c b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/scan_engine.c new file mode 100644 index 0000000..b2ca7e4 --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/scan_engine.c @@ -0,0 +1,124 @@ +/*************************************************************************** + scan_engine.c - description + ------------------- + begin : Mon May 26 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + +/* Some code is omitted for a faster analysis to illustrate the example */ + +#include "scan_engine.h" +#include "options.h" +#include "utils.h" + +extern struct options o; +extern struct flags f; + +pthread_mutex_t main_thread_count_mutex; //mutex for the main thread counter + +void start_scan(void) { + + struct timespec tv; + pthread_t c_tid; + pthread_attr_t attr; + unsigned char flag = 0; + unsigned char res = 0; + int x = 0; + size_t stack_size; + tv.tv_sec = 0; + tv.tv_nsec = 500000000; + + + /* use if we want to start in a detached state but im not going to do this for now + * im going to try and join the threads instead + * + * pthread_attr_init(&attr); + * pthread_attr_setdetachstate(&attr, PTHREAD_CREATE_DETACHED); + * + */ + + pthread_mutex_init(&main_thread_count_mutex, NULL); + + debug("\n\nstack size: %d\n", stack_size); + + stack_size = (PTHREAD_STACK_MIN + 0x3000); + + debug("\n\nstack size: %d\n", stack_size); + + o.tid=s_malloc((o.no_hostnames + 1) * sizeof(pthread_t)); + + for(x=0;x=o.number_of_threads) { + pthread_mutex_unlock(&main_thread_count_mutex); + debug("Sleeping cur child == %d, max child == %d\n", o.cur_threads, o.number_of_threads); + nanosleep(&tv, NULL); + } + pthread_mutex_unlock(&main_thread_count_mutex); + while((res = pthread_create(&c_tid, &attr, (void *)thread_start, (int *)o.cur_host)) != 0) { + usleep(200000); + } + //printf("c_tid: %d\n", c_tid); + debug("Created thread\n"); + pthread_mutex_lock(&main_thread_count_mutex); + o.cur_threads++; + pthread_mutex_unlock(&main_thread_count_mutex); + } + flag = 0; + pthread_mutex_lock(&main_thread_count_mutex); + + return; + +} + + +int cleaner_start(void) { + + /* + * This is the cleaner thread it scans the + * thread exit global variable for any threads + * that have exited and then joins them clearing + * up any resources they've used. + * + */ + + int x = 0; + + + while(1) { + for(x=0;x +#include +#include + + +void start_scan(void); +int thread_start(long cur_host); +int cleaner_start(void); + +#endif + diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/scan_engine.o b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/scan_engine.o new file mode 100644 index 0000000..5728e04 Binary files /dev/null and b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/scan_engine.o differ diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/smtprc.c b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/smtprc.c new file mode 100644 index 0000000..7668765 --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/smtprc.c @@ -0,0 +1,39 @@ +/*************************************************************************** + smtprc.c - description + ------------------- + begin : Wed May 21 08:13:08 BST 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + +#include "utils.h" +#include "parse_args.h" +#include "parse_config_files.h" +#include "scan_engine.h" + +extern struct options o; +extern struct flags f; + +int main(int argc, char *argv[]) { + + parse_args(argc, argv); //parses the command line args + get_ip_range(o.ip_range); //parse the ip range and save into memory + /* ..... */ + + printf("Starting the scan....... Please wait!\n\n\n"); + + start_scan(); + + /* ..... */ + + return EXIT_SUCCESS; +} diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/smtprc.o b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/smtprc.o new file mode 100644 index 0000000..fde2f9e Binary files /dev/null and b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/smtprc.o differ diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/utils.c b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/utils.c new file mode 100644 index 0000000..7f14473 --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/utils.c @@ -0,0 +1,62 @@ +/*************************************************************************** + utils.c - description + ------------------- + begin : Wed May 21 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + + +#include "utils.h" +#include "relay.h" +#include "options.h" + +extern struct options o; +extern struct flags f; + +extern host **hosts; + + +/* + * Safe malloc routine. checks for errors etc.. + * + */ + +void *s_malloc(unsigned long size) { + + void *mymem; + mymem=malloc(size); + return(mymem); + +} + +/* + * prints debugging information only if the + * debugging flag is set + * + */ + +void debug(char *fmt, ...) { + + if(f.debug) { + va_list ap; + va_start(ap, fmt); + fflush(stdout); + fprintf(stdout, "DEBUG: "); + vfprintf(stderr, fmt, ap); + fprintf(stderr, "\n"); + va_end(ap); + } + + return; + +} diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/utils.h b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/utils.h new file mode 100644 index 0000000..1978f8d --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/utils.h @@ -0,0 +1,57 @@ +/*************************************************************************** + utils.h - description + ------------------- + begin : Wed May 21 2003 + copyright : (C) 2003 by Spencer Hardy + email : diceman@dircon.co.uk + ***************************************************************************/ + +/*************************************************************************** + * * + * This program is free software; you can redistribute it and/or modify * + * it under the terms of the GNU General Public License as published by * + * the Free Software Foundation; either version 2 of the License, or * + * (at your option) any later version. * + * * + ***************************************************************************/ + +#ifndef SMTPRC_UTILS_H +#define SMTPRC_UTILS_H + + +/*****************************includes*************************/ + +#include +#include +#include +#include +#include +#include +#include + + +/****************************defines*****************************/ + +#ifndef MAX +#define MAX(x,y) (((x)>(y))?(x):(y)) +#endif + +#ifndef MIN +#define MIN(x,y) (((x)<(y))?(x):(y)) +#endif + +#ifndef FALSE +#define FALSE 0 +#endif + +#ifndef TRUE +#define TRUE 1 +#endif + +/***************************prototypes***************************/ + +void *s_malloc(unsigned long size); +void debug(char *fmt, ...); + +#endif + diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/utils.o b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/utils.o new file mode 100644 index 0000000..c16b459 Binary files /dev/null and b/adb_examples/debt-24-demo/smtprc-example/smtprc-2.0.3-extraction/utils.o differ diff --git a/adb_examples/debt-24-demo/smtprc-example/smtprc-extraction.json b/adb_examples/debt-24-demo/smtprc-example/smtprc-extraction.json new file mode 100644 index 0000000..8c45938 --- /dev/null +++ b/adb_examples/debt-24-demo/smtprc-example/smtprc-extraction.json @@ -0,0 +1,82 @@ +{ + "files": ["smtprc-2.0.3-extraction"], + "ana": { + "activated": [ + "expRelation", "base", "threadid", "threadflag", "threadreturn", + "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp", + "symb_locks", "var_eq", "mallocFresh", "threadJoins" + ], + "ctx_insens": [ + "var_eq" + ], + "base": { + "privatization": "none", + "context": { + "non-ptr": false, + "int": false, + "interval": false + } + }, + "thread": { + "domain": "plain", + "include-node": false + }, + "malloc": { + "wrappers": [ + "s_malloc", + "s_zmalloc" + ] + }, + "race": { + "free": false + } + }, + "sem": { + "unknown_function": { + "spawn": false, + "invalidate": { + "globals": false, + "args": false + }, + "read": { + "args": false + } + } + }, + "incremental": { + "restart": { + "sided": { + "enabled": true, + "vars": "global" + } + } + }, + "exp": { + "earlyglobs": true + }, + "cil": { + "merge": { + "inlines": false + } + }, + "dbg": { + "timing": { + "enabled": true + } + }, + "warn": { + "assert": false, + "behavior": false, + "integer": false, + "cast": false, + "race": true, + "deadlock": false, + "deadcode": true, + "analyzer": false, + "unsound": true, + "imprecise": false, + "unknown": false, + "race-threshold": 110, + "info": false + } +}