From 5b1071d9f46bbb6083b1e6dd6f7975aaa64d0a9a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Jul 2020 15:26:11 +0200 Subject: making progress on prepass --- test/monniaux/rules.mk | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test') diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk index c0594ef9..95d57f80 100644 --- a/test/monniaux/rules.mk +++ b/test/monniaux/rules.mk @@ -21,7 +21,7 @@ MEASURES?=time ALL_CFLAGS+=-Wall -D__KVX_COS__ -DMAX_MEASURES=$(MAX_MEASURES) #ALL_CFLAGS+=-g ALL_GCCFLAGS+=$(ALL_CFLAGS) -std=c99 -Wextra -Werror=implicit -ALL_CCOMPFLAGS+=$(ALL_CFLAGS) +ALL_CCOMPFLAGS+=$(ALL_CFLAGS) -fprepass # The compilers KVX_CC?=kvx-cos-gcc -- cgit From 2ff09832c0c3a2c50d51ec90566ad74e093ab3da Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Jul 2020 17:25:44 +0200 Subject: trapping loads are irreversible --- test/monniaux/rules.mk | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test') diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk index 95d57f80..8549e367 100644 --- a/test/monniaux/rules.mk +++ b/test/monniaux/rules.mk @@ -21,7 +21,7 @@ MEASURES?=time ALL_CFLAGS+=-Wall -D__KVX_COS__ -DMAX_MEASURES=$(MAX_MEASURES) #ALL_CFLAGS+=-g ALL_GCCFLAGS+=$(ALL_CFLAGS) -std=c99 -Wextra -Werror=implicit -ALL_CCOMPFLAGS+=$(ALL_CFLAGS) -fprepass +ALL_CCOMPFLAGS+=$(ALL_CFLAGS) -fduplicate 2 -fprepass -fallnontrap # The compilers KVX_CC?=kvx-cos-gcc -- cgit From fe7e30495c1690068e1df8aded85404299aaf329 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Jul 2020 18:21:22 +0200 Subject: proper ordering on calls etc. ? --- test/monniaux/rules.mk | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test') diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk index 8549e367..63582f96 100644 --- a/test/monniaux/rules.mk +++ b/test/monniaux/rules.mk @@ -21,7 +21,7 @@ MEASURES?=time ALL_CFLAGS+=-Wall -D__KVX_COS__ -DMAX_MEASURES=$(MAX_MEASURES) #ALL_CFLAGS+=-g ALL_GCCFLAGS+=$(ALL_CFLAGS) -std=c99 -Wextra -Werror=implicit -ALL_CCOMPFLAGS+=$(ALL_CFLAGS) -fduplicate 2 -fprepass -fallnontrap +ALL_CCOMPFLAGS+=$(ALL_CFLAGS) -fduplicate 2 -fprepass -fall-loads-nontrap # The compilers KVX_CC?=kvx-cos-gcc -- cgit From 509015c29fe083b1e85b326b3dfa71d82636c9e2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 15 Jul 2020 20:27:38 +0200 Subject: flags --- test/monniaux/rules.mk | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test') diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk index 63582f96..a5754574 100644 --- a/test/monniaux/rules.mk +++ b/test/monniaux/rules.mk @@ -21,7 +21,7 @@ MEASURES?=time ALL_CFLAGS+=-Wall -D__KVX_COS__ -DMAX_MEASURES=$(MAX_MEASURES) #ALL_CFLAGS+=-g ALL_GCCFLAGS+=$(ALL_CFLAGS) -std=c99 -Wextra -Werror=implicit -ALL_CCOMPFLAGS+=$(ALL_CFLAGS) -fduplicate 2 -fprepass -fall-loads-nontrap +ALL_CCOMPFLAGS+=$(ALL_CFLAGS) -fduplicate 2 -fprepass -fprepass= list -fall-loads-nontrap # The compilers KVX_CC?=kvx-cos-gcc -- cgit From 3c8429b030efcaba205b8d0faf7fdd1f174ea1e7 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 24 Jul 2020 14:04:27 +0200 Subject: Temporary prepass flags in test/regression --- test/regression/Makefile | 2 ++ 1 file changed, 2 insertions(+) (limited to 'test') diff --git a/test/regression/Makefile b/test/regression/Makefile index 744a2c03..87827282 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -1,6 +1,8 @@ include ../../Makefile.config CCOMP=../../ccomp +# TODO - temporary +CCOMPOPTS:=$(CCOMPOPTS) -fall-loads-nontrap -fduplicate 2 -fprepass CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime \ -dparse -dc -dclight -dasm -fall \ -DARCH_$(ARCH) -DMODEL_$(MODEL) -- cgit From 9a8fcdd29d763d2b5650166ddd5b359a8bfed373 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 24 Jul 2020 14:33:57 +0200 Subject: trace quand le simulateur est appele --- test/c/Makefile | 2 ++ test/regression/Makefile | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) (limited to 'test') diff --git a/test/c/Makefile b/test/c/Makefile index 726631d2..a728d182 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -1,6 +1,8 @@ include ../../Makefile.config CCOMP=../../ccomp +# TODO - temporary +# CCOMPOPTS:=$(CCOMPOPTS) -fall-loads-nontrap -fduplicate 2 -fprepass CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime -dc -dclight -dasm CFLAGS+=-O2 -Wall diff --git a/test/regression/Makefile b/test/regression/Makefile index 87827282..8b2f4021 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -2,7 +2,7 @@ include ../../Makefile.config CCOMP=../../ccomp # TODO - temporary -CCOMPOPTS:=$(CCOMPOPTS) -fall-loads-nontrap -fduplicate 2 -fprepass +# CCOMPOPTS:=$(CCOMPOPTS) -fall-loads-nontrap -fduplicate 2 -fprepass CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime \ -dparse -dc -dclight -dasm -fall \ -DARCH_$(ARCH) -DMODEL_$(MODEL) -- cgit From 1e93ef5453d4f9a6c3108b1d43b3b9f3f4fb9d13 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 24 Jul 2020 15:01:39 +0200 Subject: Coq 8.11.2 --- test/monniaux/picosat-965/small.dat | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 test/monniaux/picosat-965/small.dat (limited to 'test') diff --git a/test/monniaux/picosat-965/small.dat b/test/monniaux/picosat-965/small.dat new file mode 100644 index 00000000..ff3d7081 --- /dev/null +++ b/test/monniaux/picosat-965/small.dat @@ -0,0 +1,2 @@ +p cnf 2 1 +1 2 0 -- cgit From d073f1901e1ddf012bc2ac607e230d8156eeefe1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 24 Jul 2020 17:36:56 +0200 Subject: smaller example --- test/monniaux/picosat-965/small.dat | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test') diff --git a/test/monniaux/picosat-965/small.dat b/test/monniaux/picosat-965/small.dat index ff3d7081..accb9054 100644 --- a/test/monniaux/picosat-965/small.dat +++ b/test/monniaux/picosat-965/small.dat @@ -1,2 +1,2 @@ -p cnf 2 1 -1 2 0 +p cnf 1 1 +1 0 -- cgit From 18988711111bd57900567b032aead1c17997cb7f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 24 Jul 2020 17:40:29 +0200 Subject: even smaller --- test/monniaux/picosat-965/tiny.dat | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 test/monniaux/picosat-965/tiny.dat (limited to 'test') diff --git a/test/monniaux/picosat-965/tiny.dat b/test/monniaux/picosat-965/tiny.dat new file mode 100644 index 00000000..030df0e5 --- /dev/null +++ b/test/monniaux/picosat-965/tiny.dat @@ -0,0 +1,2 @@ +p cnf 1 1 +0 -- cgit From cffd805ea0c06710605565fae3d0e885a7943f74 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 24 Jul 2020 17:41:31 +0200 Subject: also crashes with 0 variables --- test/monniaux/picosat-965/tiny.dat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test') diff --git a/test/monniaux/picosat-965/tiny.dat b/test/monniaux/picosat-965/tiny.dat index 030df0e5..1d89b303 100644 --- a/test/monniaux/picosat-965/tiny.dat +++ b/test/monniaux/picosat-965/tiny.dat @@ -1,2 +1,2 @@ -p cnf 1 1 +p cnf 0 1 0 -- cgit From 9464136be3904db1b227327cec0d8670b1fc164f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 24 Jul 2020 17:53:38 +0200 Subject: picosat in one file for testing purposes --- test/monniaux/picosat-965/onefile/picosat.c | 9765 +++++++++++++++++++++++++++ 1 file changed, 9765 insertions(+) create mode 100644 test/monniaux/picosat-965/onefile/picosat.c (limited to 'test') diff --git a/test/monniaux/picosat-965/onefile/picosat.c b/test/monniaux/picosat-965/onefile/picosat.c new file mode 100644 index 00000000..b255f3ee --- /dev/null +++ b/test/monniaux/picosat-965/onefile/picosat.c @@ -0,0 +1,9765 @@ +#define NALARM 1 +#define NZIP 1 +#define NGETRUSAGE 1 +#define NDEBUG 1 + +#include "picosat.h" + +#include +#include +#include +#include +#include +#include +#include + +#define GUNZIP "gunzip -c %s" +#define BUNZIP2 "bzcat %s" +#define GZIP "gzip -c -f > %s" + +#ifndef NZIP +FILE * popen (const char *, const char*); +int pclose (FILE *); +#endif + +static PicoSAT * picosat; + +static int lineno; +static FILE *input; +static int inputid; +static FILE *output; +static int verbose; +static int sargc; +static char ** sargv; +static char buffer[100]; +static char *bhead = buffer; +static const char *eob = buffer + 80; +static FILE * incremental_rup_file; +static signed char * sol; + +extern void picosat_enter (PicoSAT *); +extern void picosat_leave (PicoSAT *); + +static int +next (void) +{ + int res = getc (input); + if (res == '\n') + lineno++; + + return res; +} + +static const char * +parse (PicoSAT * picosat, int force) +{ + int ch, sign, lit, vars, clauses; + + lineno = 1; + /* DM inputid = fileno (input); */ + +SKIP_COMMENTS: + ch = next (); + if (ch == 'c') + { + while ((ch = next ()) != EOF && ch != '\n') + ; + goto SKIP_COMMENTS; + } + + if (isspace (ch)) + goto SKIP_COMMENTS; + + if (ch != 'p') +INVALID_HEADER: + return "missing or invalid 'p cnf ' header"; + + if (!isspace (next ())) + goto INVALID_HEADER; + + while (isspace (ch = next ())) + ; + + if (ch != 'c' || next () != 'n' || next () != 'f' || !isspace (next ())) + goto INVALID_HEADER; + + while (isspace (ch = next ())) + ; + + if (!isdigit (ch)) + goto INVALID_HEADER; + + vars = ch - '0'; + while (isdigit (ch = next ())) + vars = 10 * vars + (ch - '0'); + + if (!isspace (ch)) + goto INVALID_HEADER; + + while (isspace (ch = next ())) + ; + + if (!isdigit (ch)) + goto INVALID_HEADER; + + clauses = ch - '0'; + while (isdigit (ch = next ())) + clauses = 10 * clauses + (ch - '0'); + + if (!isspace (ch) && ch != '\n' ) + goto INVALID_HEADER; + + if (verbose) + { + fprintf (output, "c parsed header 'p cnf %d %d'\n", vars, clauses); + fflush (output); + } + + picosat_adjust (picosat, vars); + + if (incremental_rup_file) + picosat_set_incremental_rup_file (picosat, incremental_rup_file, vars, clauses); + + lit = 0; +READ_LITERAL: + ch = next (); + + if (ch == 'c') + { + while ((ch = next ()) != EOF && ch != '\n') + ; + goto READ_LITERAL; + } + + if (ch == EOF) + { + if (lit) + return "trailing 0 missing"; + + if (clauses && !force) + return "clause missing"; + + return 0; + } + + if (isspace (ch)) + goto READ_LITERAL; + + sign = 1; + if (ch == '-') + { + sign = -1; + ch = next (); + } + + if (!isdigit (ch)) + return "expected number"; + + lit = ch - '0'; + while (isdigit (ch = next ())) + lit = 10 * lit + (ch - '0'); + + if (!clauses && !force) + return "too many clauses"; + + if (lit) + { + if (lit > vars && !force) + return "maximal variable index exceeded"; + + lit *= sign; + } + else + clauses--; + + picosat_add (picosat, lit); + + goto READ_LITERAL; +} + +static void +bflush (void) +{ + *bhead = 0; + fputs (buffer, output); + fputc ('\n', output); + bhead = buffer; +} + +static void +printi (int i) +{ + char *next; + int l; + +REENTER: + if (bhead == buffer) + *bhead++ = 'v'; + + l = sprintf (bhead, " %d", i); + next = bhead + l; + + if (next >= eob) + { + bflush (); + goto REENTER; + } + else + bhead = next; +} + +static void +printa (PicoSAT * picosat, int partial) +{ + int max_idx = picosat_variables (picosat), i, lit, val; + + assert (bhead == buffer); + + for (i = 1; i <= max_idx; i++) + { + if (partial) + { + val = picosat_deref_partial (picosat, i); + if (!val) + continue; + } + else + val = picosat_deref (picosat, i); + lit = (val > 0) ? i : -i; + printi (lit); + } + + printi (0); + if (bhead > buffer) + bflush (); +} + +static void +blocksol (PicoSAT * picosat) +{ + int max_idx = picosat_variables (picosat), i; + + if (!sol) + { + sol = malloc (max_idx + 1); + memset (sol, 0, max_idx + 1); + } + + for (i = 1; i <= max_idx; i++) + sol[i] = (picosat_deref (picosat, i) > 0) ? 1 : -1; + + for (i = 1; i <= max_idx; i++) + picosat_add (picosat, (sol[i] < 0) ? i : -i); + + picosat_add (picosat, 0); +} + +static int +has_suffix (const char *str, const char *suffix) +{ + const char *tmp = strstr (str, suffix); + if (!tmp) + return 0; + + return str + strlen (str) - strlen (suffix) == tmp; +} + +static void +write_core_variables (PicoSAT * picosat, FILE * file) +{ + int i, max_idx = picosat_variables (picosat), count = 0; + for (i = 1; i <= max_idx; i++) + if (picosat_corelit (picosat, i)) + { + fprintf (file, "%d\n", i); + count++; + } + + if (verbose) + fprintf (output, "c found and wrote %d core variables\n", count); +} + +static int +next_assumption (int start) +{ + char * arg, c; + int res; + res = start + 1; + while (res < sargc) + { + arg = sargv[res++]; + if (!strcmp (arg, "-a")) + { + assert (res < sargc); + break; + } + + if (arg[0] == '-') { + c = arg[1]; + if (c == 'l' || c == 'i' || c == 's' || c == 'o' || c == 't' || + c == 'T' || c == 'r' || c == 'R' || c == 'c' || c == 'V' || + c == 'U' || c == 'A') res++; + } + } + if (res >= sargc) res = 0; + return res; +} + +static void +write_failed_assumptions (PicoSAT * picosat, FILE * file) +{ + int i, lit, count = 0; +#ifndef NDEBUG + int max_idx = picosat_variables (picosat); +#endif + i = 0; + while ((i = next_assumption (i))) { + lit = atoi (sargv[i]); + if (!picosat_failed_assumption (picosat, lit)) continue; + fprintf (file, "%d\n", lit); + count++; + } + if (verbose) + fprintf (output, "c found and wrote %d failed assumptions\n", count); +#ifndef NDEBUG + for (i = 1; i <= max_idx; i++) + if (picosat_failed_assumption (picosat, i)) + count--; +#endif + assert (!count); +} + +static void +write_to_file (PicoSAT * picosat, + const char *name, + const char *type, + void (*writer) (PicoSAT *, FILE *)) +{ + int pclose_file, zipped = has_suffix (name, ".gz"); + FILE *file; + char *cmd; + + if (zipped) + { +#ifdef NZIP + file = NULL; +#else + cmd = malloc (strlen (GZIP) + strlen (name)); + sprintf (cmd, GZIP, name); + file = popen (cmd, "w"); + free (cmd); + pclose_file = 1; +#endif + } + else + { + file = fopen (name, "w"); + pclose_file = 0; + } + + if (file) + { + if (verbose) + fprintf (output, + "c\nc writing %s%s to '%s'\n", + zipped ? "gzipped " : "", type, name); + + writer (picosat, file); + +#ifndef NZIP + if (pclose_file) + pclose (file); + else +#endif + fclose (file); + } + else + fprintf (output, "*** picosat: can not write to '%s'\n", name); +} + +static int catched; + +static void (*sig_int_handler); +static void (*sig_segv_handler); +static void (*sig_abrt_handler); +static void (*sig_term_handler); +#ifndef NALLSIGNALS +static void (*sig_kill_handler); +static void (*sig_xcpu_handler); +static void (*sig_xfsz_handler); +#endif + +static void +resetsighandlers (void) +{ + (void) signal (SIGINT, sig_int_handler); + (void) signal (SIGSEGV, sig_segv_handler); + (void) signal (SIGABRT, sig_abrt_handler); + (void) signal (SIGTERM, sig_term_handler); +#ifndef NALLSIGNALS + (void) signal (SIGKILL, sig_kill_handler); + (void) signal (SIGXCPU, sig_xcpu_handler); + (void) signal (SIGXFSZ, sig_xfsz_handler); +#endif +} + +static int time_limit_in_seconds; +static void (*sig_alarm_handler); +static int ought_to_be_interrupted, interrupt_notified; + +static void +alarm_triggered (int sig) +{ + (void) sig; + assert (sig == SIGALRM); + assert (time_limit_in_seconds); + assert (!ought_to_be_interrupted); + ought_to_be_interrupted = 1; + assert (!interrupt_notified); +} + +static int +interrupt_call_back (void * dummy) +{ + (void) dummy; + if (!ought_to_be_interrupted) + return 0; + if (!interrupt_notified) + { + if (verbose) + { + picosat_message (picosat, 1, ""); + picosat_message (picosat, 1, + "*** TIME LIMIT OF %d SECONDS REACHED ***", + time_limit_in_seconds); + picosat_message (picosat, 1, ""); + } + interrupt_notified = 1; + } + return 1; +} + +static void +setalarm () +{ +#ifndef NALARM + assert (time_limit_in_seconds > 0); + sig_alarm_handler = signal (SIGALRM, alarm_triggered); + alarm (time_limit_in_seconds); + assert (picosat); + picosat_set_interrupt (picosat, 0, interrupt_call_back); +#endif +} + +static void +resetalarm () +{ + assert (time_limit_in_seconds > 0); + (void) signal (SIGALRM, sig_term_handler); +} + +static void +message (int sig) +{ + picosat_message (picosat, 1, ""); + picosat_message (picosat, 1, "*** CAUGHT SIGNAL %d ***", sig); + picosat_message (picosat, 1, ""); +} + +static void +catch (int sig) +{ + if (!catched) + { + message (sig); + catched = 1; + picosat_stats (picosat); + message (sig); + } + + resetsighandlers (); + raise (sig); +} + +static void +setsighandlers (void) +{ + sig_int_handler = signal (SIGINT, catch); + sig_segv_handler = signal (SIGSEGV, catch); + sig_abrt_handler = signal (SIGABRT, catch); + sig_term_handler = signal (SIGTERM, catch); +#ifndef NALLSIGNALS + sig_kill_handler = signal (SIGKILL, catch); + sig_xcpu_handler = signal (SIGXCPU, catch); + sig_xfsz_handler = signal (SIGXFSZ, catch); +#endif +} + +#define USAGE \ +"usage: picosat [