[PATCH v2 0/8] scheck: add a symbolic checker

[PATCH v2 0/8] scheck: add a symbolic checker

[Luc Van Oostenryck]

Some instruction simplifications can be quite tricky and thus
easy to get wrong. Often, they are also hard to test (for example,
you can test them with a few input values but of course not all
combinations, it's not clear what are the conditions for which
they're valid, ...).

This series add a tool, scheck, which feeds Sparse's IR into a
bitvector SMT solver (Boolector). This, together with assertions
added at C level, allows to symbolically check the validity of these
assertions. In other words, it allows to check if these assertions
are valid for all possible values (but these expressions are limited
to pure integer expressions, so no floats, no branches, no memory
accesses, no functions calls).

Now, you may ask yourself "Nice, but how can I be sure that this
checker is working correctly?". And the answer to this question
is obviously "You should write another checker, of course. And
then another one, all the way down!".

Notes: This needs to have the SMT solver's librarie installed
       and having 'BOOLECTORDIR' and 'HAVE_BOOLECTOR' configured.

Changes since v1:
* Rewrite evaluate_generic_int_op() which was very broken
  (thanks to Ramsay Jones for noticing it).
* When translating compare instructions, the input bitvectors
  must use the instructions' input type, not the target type).


Luc Van Oostenryck (8):
  export declare_builtins()
  builtin: define a symbol_op for a generic op acting on integer
  .gitignore is a bit too greedy
  scheck: add a symbolic checker
  scheck: assert_eq()
  scheck: allow multiple assertions
  scheck: assert_const()
  scheck: support pre-conditions via __assume()

 .gitignore             |  35 ++--
 Makefile               |   7 +
 builtin.c              |  63 ++++++-
 builtin.h              |   4 +
 ident-list.h           |   6 +
 scheck.c               | 361 +++++++++++++++++++++++++++++++++++++++++
 validation/scheck/ko.c |  10 ++
 validation/scheck/ok.c |  22 +++
 validation/test-suite  |   6 +
 9 files changed, 496 insertions(+), 18 deletions(-)
 create mode 100644 scheck.c
 create mode 100644 validation/scheck/ko.c
 create mode 100644 validation/scheck/ok.c

-- 
2.31.1

[PATCH v2 1/8] export declare_builtins()

[Luc Van Oostenryck]

Make declare_builtins() extern so that it can be used from other files.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 builtin.c | 2 +-
 builtin.h | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/builtin.c b/builtin.c
index c7e7da3b1b7b..ff03dbab9a06 100644
--- a/builtin.c
+++ b/builtin.c
@@ -559,7 +559,7 @@ static void declare_builtin(int stream, const struct builtin_fn *entry)
 	}
 }
 
-static void declare_builtins(int stream, const struct builtin_fn tbl[])
+void declare_builtins(int stream, const struct builtin_fn tbl[])
 {
 	if (!tbl)
 		return;
diff --git a/builtin.h b/builtin.h
index d0d3fd2ccf87..9cb6728444fe 100644
--- a/builtin.h
+++ b/builtin.h
@@ -12,4 +12,6 @@ struct builtin_fn {
 	struct symbol_op *op;
 };
 
+void declare_builtins(int stream, const struct builtin_fn tbl[]);
+
 #endif
-- 
2.31.1

[PATCH v2 2/8] builtin: define a symbol_op for a generic op acting on integer

[Luc Van Oostenryck]

This can be used to define some generic (polymorphic) builtin
with a signature like:
	<name>(int)
	<name>(T, T)
	<name>(int, T)
	<name>(int, T, long, T, ... T)
where T is some integer type which will be instantiated at each call.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 builtin.c | 61 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 builtin.h |  2 ++
 2 files changed, 63 insertions(+)

diff --git a/builtin.c b/builtin.c
index ff03dbab9a06..928e03050375 100644
--- a/builtin.c
+++ b/builtin.c
@@ -390,6 +390,67 @@ static struct symbol_op overflow_p_op = {
 };
 
 
+///
+// Evaluate the arguments of 'generic' integer operators.
+//
+// Parameters with a complete type are used like in a normal prototype.
+// The first parameter with a 'dynamic' type will be consider
+// as polymorphic and for each calls will be instancied with the type
+// of its effective argument.
+// The next dynamic parameters will the use this polymorphic type.
+// This allows to declare functions with some parameters having
+// a type variably defined at call time:
+//	int foo(int, T, T);
+static int evaluate_generic_int_op(struct expression *expr)
+{
+	struct symbol *fntype = expr->fn->ctype->ctype.base_type;
+	struct symbol_list *types = NULL;
+	struct symbol *ctype = NULL;
+	struct expression *arg;
+	struct symbol *t;
+	int n = 0;
+
+	PREPARE_PTR_LIST(fntype->arguments, t);
+	FOR_EACH_PTR(expr->args, arg) {
+		if (!is_dynamic_type(t)) {
+			;
+		} else if (!ctype) {
+			// fist 'dynamic' type, chat that it is an integer
+			t = arg->ctype;
+			if (!t)
+				return 0;
+			if (t->type == SYM_NODE)
+				t = t->ctype.base_type;
+			if (!t)
+				return 0;
+			if (t->ctype.base_type != &int_type)
+				goto err;
+
+			// next 'dynamic' arguments will use this type
+			ctype = t;
+		} else {
+			// use the previous 'dynamic' type
+			t = ctype;
+		}
+		add_ptr_list(&types, t);
+		NEXT_PTR_LIST(t);
+	} END_FOR_EACH_PTR(arg);
+	FINISH_PTR_LIST(t);
+	return evaluate_arguments(types, expr->args);
+
+err:
+	sparse_error(arg->pos, "non-integer type for argument %d:", n);
+	info(arg->pos, "        %s", show_typename(arg->ctype));
+	expr->ctype = &bad_ctype;
+	return 0;
+}
+
+struct symbol_op generic_int_op = {
+	.args = args_prototype,
+	.evaluate = evaluate_generic_int_op,
+};
+
+
 static int eval_atomic_common(struct expression *expr)
 {
 	struct symbol *fntype = expr->fn->ctype->ctype.base_type;
diff --git a/builtin.h b/builtin.h
index 9cb6728444fe..5fe77c926244 100644
--- a/builtin.h
+++ b/builtin.h
@@ -14,4 +14,6 @@ struct builtin_fn {
 
 void declare_builtins(int stream, const struct builtin_fn tbl[]);
 
+extern struct symbol_op generic_int_op;
+
 #endif
-- 
2.31.1

Re: [PATCH v2 2/8] builtin: define a symbol_op for a generic op acting on integer

[Ramsay Jones]

On 12/04/2021 22:21, Luc Van Oostenryck wrote:
> This can be used to define some generic (polymorphic) builtin
> with a signature like:
> 	<name>(int)
> 	<name>(T, T)
> 	<name>(int, T)
> 	<name>(int, T, long, T, ... T)
> where T is some integer type which will be instantiated at each call.
> 
> Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
> ---
>  builtin.c | 61 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
>  builtin.h |  2 ++
>  2 files changed, 63 insertions(+)
> 
> diff --git a/builtin.c b/builtin.c
> index ff03dbab9a06..928e03050375 100644
> --- a/builtin.c
> +++ b/builtin.c
> @@ -390,6 +390,67 @@ static struct symbol_op overflow_p_op = {
>  };
>  
>  
> +///
> +// Evaluate the arguments of 'generic' integer operators.
> +//
> +// Parameters with a complete type are used like in a normal prototype.
> +// The first parameter with a 'dynamic' type will be consider
> +// as polymorphic and for each calls will be instancied with the type
> +// of its effective argument.
> +// The next dynamic parameters will the use this polymorphic type.
> +// This allows to declare functions with some parameters having
> +// a type variably defined at call time:
> +//	int foo(int, T, T);
> +static int evaluate_generic_int_op(struct expression *expr)
> +{
> +	struct symbol *fntype = expr->fn->ctype->ctype.base_type;
> +	struct symbol_list *types = NULL;
> +	struct symbol *ctype = NULL;
> +	struct expression *arg;
> +	struct symbol *t;
> +	int n = 0;
> +
> +	PREPARE_PTR_LIST(fntype->arguments, t);
> +	FOR_EACH_PTR(expr->args, arg) {

Hmm, now n is always 0 in the error message, so:
		n++;
here?

> +		if (!is_dynamic_type(t)) {
> +			;
> +		} else if (!ctype) {
> +			// fist 'dynamic' type, chat that it is an integer

s/chat/check/

> +			t = arg->ctype;
> +			if (!t)
> +				return 0;
> +			if (t->type == SYM_NODE)
> +				t = t->ctype.base_type;
> +			if (!t)
> +				return 0;
> +			if (t->ctype.base_type != &int_type)
> +				goto err;
> +
> +			// next 'dynamic' arguments will use this type
> +			ctype = t;
> +		} else {
> +			// use the previous 'dynamic' type
> +			t = ctype;
> +		}
> +		add_ptr_list(&types, t);
> +		NEXT_PTR_LIST(t);
> +	} END_FOR_EACH_PTR(arg);
> +	FINISH_PTR_LIST(t);
> +	return evaluate_arguments(types, expr->args);

Hmm, does this do the usual argument promotions, so e.g. an 'generic'
'short' gets promoted to 'int' in the prototype? I guess not, that
would have to be done above, while adding to the types list, right?
Hmm, I would have to study evaluate_arguments(), but it may be worth
a comment here?

> +
> +err:
> +	sparse_error(arg->pos, "non-integer type for argument %d:", n);
> +	info(arg->pos, "        %s", show_typename(arg->ctype));
> +	expr->ctype = &bad_ctype;
> +	return 0;
> +}

So, this certainly looks better. Thanks! ;-)

ATB,
Ramsay Jones

> +
> +struct symbol_op generic_int_op = {
> +	.args = args_prototype,
> +	.evaluate = evaluate_generic_int_op,
> +};
> +
> +
>  static int eval_atomic_common(struct expression *expr)
>  {
>  	struct symbol *fntype = expr->fn->ctype->ctype.base_type;
> diff --git a/builtin.h b/builtin.h
> index 9cb6728444fe..5fe77c926244 100644
> --- a/builtin.h
> +++ b/builtin.h
> @@ -14,4 +14,6 @@ struct builtin_fn {
>  
>  void declare_builtins(int stream, const struct builtin_fn tbl[]);
>  
> +extern struct symbol_op generic_int_op;
> +
>  #endif
> 

Re: [PATCH v2 2/8] builtin: define a symbol_op for a generic op acting on integer

[Luc Van Oostenryck]

On Tue, Apr 13, 2021 at 01:23:00AM +0100, Ramsay Jones wrote:
> On 12/04/2021 22:21, Luc Van Oostenryck wrote:
> > +	int n = 0;
> > +
> > +	PREPARE_PTR_LIST(fntype->arguments, t);
> > +	FOR_EACH_PTR(expr->args, arg) {
> 
> Hmm, now n is always 0 in the error message, so:
> 		n++;
> here?

Hehe, yes indeed.
 
> > +		if (!is_dynamic_type(t)) {
> > +			;
> > +		} else if (!ctype) {
> > +			// fist 'dynamic' type, chat that it is an integer
> 
> s/chat/check/

fixed.

> > +	return evaluate_arguments(types, expr->args);
> 
> Hmm, does this do the usual argument promotions, so e.g. an 'generic'
> 'short' gets promoted to 'int' in the prototype? I guess not, that
> would have to be done above, while adding to the types list, right?

Well, evaluate_arguments() is the normal function used to evaluate
the arguments of all function calls, so, yes, it does arguments
promotion but only when the type is not specified (so either the
'...' of varadic function or an argument of a variadic builtin's
which is declared as NULL in the corresponding struct builtin_fn
(non-variadic builtins can't have such NULL arguments because the
first NULL is used to determine its arity and this is then normaly
checked in the .args method before the evaluation)).

> Hmm, I would have to study evaluate_arguments(), but it may be worth
> a comment here?

Not here, because there is nothing special but sure, evaluate_arguments()
should be documented and even more so how struct builtin_fn should be
used (because it's much more complex since a lot of builtins doesn't
follow the way normal C declarations rules).

> 
> So, this certainly looks better. Thanks! ;-)

Thanks to you!
-- Luc

[PATCH v2 3/8] .gitignore is a bit too greedy

[Luc Van Oostenryck]

The current .gitignore specifies that the generated programs
must be ignored. Good.

However, this is done by just specifying the name of the program
which has the effect of having any files or directories with the
same name to be ignored too. This is not intended.

Fix this using the pattern '/<name>' instead so that they match
in the root folder.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 .gitignore | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/.gitignore b/.gitignore
index 63c74afdb156..6a28fa50f8bb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,25 +8,25 @@
 .*.swp
 
 # generated
-version.h
+/version.h
 
 # programs
-c2xml
-compile
-ctags
-example
-graph
-obfuscate
-sparse
-sparse-llvm
-semind
-test-dissect
-test-inspect
-test-lexing
-test-linearize
-test-parsing
-test-show-type
-test-unssa
+/c2xml
+/compile
+/ctags
+/example
+/graph
+/obfuscate
+/semind
+/sparse
+/sparse-llvm
+/test-dissect
+/test-inspect
+/test-lexing
+/test-linearize
+/test-parsing
+/test-show-type
+/test-unssa
 
 # tags
 tags
-- 
2.31.1

[PATCH v2 4/8] scheck: add a symbolic checker

[Luc Van Oostenryck]

Some instruction simplifications can be quite tricky and thus easy to
get wrong. Often, they also are hard to test (for example, you can
test it with a few input values but of course not all combinations).

I'm used to validate some of these with an independent tool
(Alive cfr. [1], [2]) which is quite neat but has some issues:
1) This tool doesn't work with Sparse's IR or C source but it needs to
   have the tests written in its own language (very close to LLVM's IR).
   So it can be used to test if the logic of a simplification but
   not if implemented correctly.
2) This tool isn't maintained anymore (has some bugs too) and it's
   successor (Alive2 [3]) is not quite as handy to me (I miss the
   pre-conditions a lot).

So, this patch implement the same idea but fully integrated with
Sparse. This mean that you can write a test in C, let Sparse process
and simplify it and then directly validate it and not only for
a few values but symbolically, for all possible values.

Note: Of course, this is not totally stand-alone and depends on
      an external library for the solver (Boolector, see [4], [5]).

Note: Currently, it's just a proof of concept and, except the
      included tests, it's only very slightly tested (and untested
      with anything more complex than a few instructions).

[1] https://blog.regehr.org/archives/1170
[2] https://www.cs.utah.edu/~regehr/papers/pldi15.pdf
[3] https://blog.regehr.org/archives/1722
[4] https://boolector.github.io/
[5] https://boolector.github.io/papers/BrummayerBiere-TACAS09.pdf

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 .gitignore             |   1 +
 Makefile               |   7 +
 ident-list.h           |   3 +
 scheck.c               | 315 +++++++++++++++++++++++++++++++++++++++++
 validation/scheck/ko.c |  10 ++
 validation/scheck/ok.c |  14 ++
 validation/test-suite  |   6 +
 7 files changed, 356 insertions(+)
 create mode 100644 scheck.c
 create mode 100644 validation/scheck/ko.c
 create mode 100644 validation/scheck/ok.c

diff --git a/.gitignore b/.gitignore
index 6a28fa50f8bb..b22f86b1ddfb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,6 +17,7 @@
 /example
 /graph
 /obfuscate
+/scheck
 /semind
 /sparse
 /sparse-llvm
diff --git a/Makefile b/Makefile
index f9883da101c7..a0178a65a11a 100644
--- a/Makefile
+++ b/Makefile
@@ -227,6 +227,13 @@ else
 $(warning Your system does not have llvm, disabling sparse-llvm)
 endif
 
+ifeq ($(HAVE_BOOLECTOR),yes)
+PROGRAMS += scheck
+scheck-cflags  := -I${BOOLECTORDIR}/include/boolector
+scheck-ldflags := -L${BOOLECTORDIR}/lib
+scheck-ldlibs  := -lboolector -llgl -lbtor2parser
+endif
+
 ########################################################################
 LIBS := libsparse.a
 OBJS := $(LIB_OBJS) $(EXTRA_OBJS) $(PROGRAMS:%=%.o)
diff --git a/ident-list.h b/ident-list.h
index 8049b6940745..918f54d75fc4 100644
--- a/ident-list.h
+++ b/ident-list.h
@@ -78,6 +78,9 @@ IDENT(memset); IDENT(memcpy);
 IDENT(copy_to_user); IDENT(copy_from_user);
 IDENT(main);
 
+/* used by the symbolic checker */
+IDENT(__assert);
+
 #undef __IDENT
 #undef IDENT
 #undef IDENT_RESERVED
diff --git a/scheck.c b/scheck.c
new file mode 100644
index 000000000000..63cbfa2d3404
--- /dev/null
+++ b/scheck.c
@@ -0,0 +1,315 @@
+// SPDX-License-Identifier: MIT
+// Copyright (C) 2021 Luc Van Oostenryck
+
+///
+// Symbolic checker for Sparse's IR
+// --------------------------------
+//
+// This is an example client program with a dual purpose:
+//	# It shows how to translate Sparse's IR into the language
+//	  of SMT solvers (only the part concerning integers,
+//	  floating-point and memory is ignored).
+//	# It's used as a simple symbolic checker for the IR.
+//	  The idea is to create a mini-language that allows to
+//	  express some assertions with some pre-conditions.
+
+#include <stdarg.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <ctype.h>
+#include <unistd.h>
+#include <fcntl.h>
+
+#include <boolector.h>
+#include "lib.h"
+#include "expression.h"
+#include "linearize.h"
+#include "symbol.h"
+#include "builtin.h"
+
+
+#define dyntype incomplete_ctype
+static const struct builtin_fn builtins_scheck[] = {
+	{ "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op },
+	{}
+};
+
+
+static BoolectorSort get_sort(Btor *btor, struct symbol *type, struct position pos)
+{
+	if (!is_int_type(type)) {
+		sparse_error(pos, "invalid type");
+		return NULL;
+	}
+	return boolector_bitvec_sort(btor, type->bit_size);
+}
+
+static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo)
+{
+	static char buff[33];
+	BoolectorNode *n;
+
+	if (pseudo->priv)
+		return pseudo->priv;
+
+	switch (pseudo->type) {
+	case PSEUDO_VAL:
+		sprintf(buff, "%llx", pseudo->value);
+		return boolector_consth(btor, s, buff);
+	case PSEUDO_ARG:
+	case PSEUDO_REG:
+		n = boolector_var(btor, s, show_pseudo(pseudo));
+		break;
+	default:
+		fprintf(stderr, "invalid pseudo: %s\n", show_pseudo(pseudo));
+		return NULL;
+	}
+	return pseudo->priv = n;
+}
+
+static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx)
+{
+	pseudo_t arg = ptr_list_nth(insn->arguments, idx);
+	struct symbol *type = ptr_list_nth(insn->fntypes, idx + 1);
+	BoolectorSort s = get_sort(btor, type, insn->pos);
+
+	return mkvar(btor, s, arg);
+}
+
+static BoolectorNode *zext(Btor *btor, struct instruction *insn, BoolectorNode *s)
+{
+	int old = boolector_get_width(btor, s);
+	int new = insn->type->bit_size;
+	return boolector_uext(btor, s, new - old);
+}
+
+static BoolectorNode *sext(Btor *btor, struct instruction *insn, BoolectorNode *s)
+{
+	int old = boolector_get_width(btor, s);
+	int new = insn->type->bit_size;
+	return boolector_sext(btor, s, new - old);
+}
+
+static BoolectorNode *slice(Btor *btor, struct instruction *insn, BoolectorNode *s)
+{
+	int old = boolector_get_width(btor, s);
+	int new = insn->type->bit_size;
+	return boolector_slice(btor, s, old - new - 1, 0);
+}
+
+static void binary(Btor *btor, BoolectorSort s, struct instruction *insn)
+{
+	BoolectorNode *t, *a, *b;
+
+	a = mkvar(btor, s, insn->src1);
+	b = mkvar(btor, s, insn->src2);
+	if (!a || !b)
+		return;
+	switch (insn->opcode) {
+	case OP_ADD:	t = boolector_add(btor, a, b); break;
+	case OP_SUB:	t = boolector_sub(btor, a, b); break;
+	case OP_MUL:	t = boolector_mul(btor, a, b); break;
+	case OP_AND:	t = boolector_and(btor, a, b); break;
+	case OP_OR:	t = boolector_or (btor, a, b); break;
+	case OP_XOR:	t = boolector_xor(btor, a, b); break;
+	case OP_SHL:	t = boolector_sll(btor, a, b); break;
+	case OP_LSR:	t = boolector_srl(btor, a, b); break;
+	case OP_ASR:	t = boolector_sra(btor, a, b); break;
+	case OP_DIVS:	t = boolector_sdiv(btor, a, b); break;
+	case OP_DIVU:	t = boolector_udiv(btor, a, b); break;
+	case OP_MODS:	t = boolector_srem(btor, a, b); break;
+	case OP_MODU:	t = boolector_urem(btor, a, b); break;
+	case OP_SET_EQ:	t = zext(btor, insn, boolector_eq(btor, a, b)); break;
+	case OP_SET_NE:	t = zext(btor, insn, boolector_ne(btor, a, b)); break;
+	case OP_SET_LT:	t = zext(btor, insn, boolector_slt(btor, a, b)); break;
+	case OP_SET_LE:	t = zext(btor, insn, boolector_slte(btor, a, b)); break;
+	case OP_SET_GE:	t = zext(btor, insn, boolector_sgte(btor, a, b)); break;
+	case OP_SET_GT:	t = zext(btor, insn, boolector_sgt(btor, a, b)); break;
+	case OP_SET_B:	t = zext(btor, insn, boolector_ult(btor, a, b)); break;
+	case OP_SET_BE:	t = zext(btor, insn, boolector_ulte(btor, a, b)); break;
+	case OP_SET_AE:	t = zext(btor, insn, boolector_ugte(btor, a, b)); break;
+	case OP_SET_A:	t = zext(btor, insn, boolector_ugt(btor, a, b)); break;
+	default:
+		fprintf(stderr, "unsupported insn\n");
+		return;
+	}
+	insn->target->priv = t;
+}
+
+static void binop(Btor *btor, struct instruction *insn)
+{
+	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
+	binary(btor, s, insn);
+}
+
+static void icmp(Btor *btor, struct instruction *insn)
+{
+	BoolectorSort s = get_sort(btor, insn->itype, insn->pos);
+	binary(btor, s, insn);
+}
+
+static void unop(Btor *btor, struct instruction *insn)
+{
+	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
+	BoolectorNode *t, *a;
+
+	a = mkvar(btor, s, insn->src1);
+	if (!a)
+		return;
+	switch (insn->opcode) {
+	case OP_NEG:	t = boolector_neg(btor, a); break;
+	case OP_NOT:	t = boolector_not(btor, a); break;
+	case OP_SEXT:	t = sext(btor, insn, a); break;
+	case OP_ZEXT:	t = zext(btor, insn, a); break;
+	case OP_TRUNC:	t = slice(btor, insn, a); break;
+	default:
+		fprintf(stderr, "unsupported insn\n");
+		return;
+	}
+	insn->target->priv = t;
+}
+
+static void ternop(Btor *btor, struct instruction *insn)
+{
+	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
+	BoolectorNode *t, *a, *b, *c, *z, *d;
+
+	a = mkvar(btor, s, insn->src1);
+	b = mkvar(btor, s, insn->src2);
+	c = mkvar(btor, s, insn->src3);
+	if (!a || !b || !c)
+		return;
+	switch (insn->opcode) {
+	case OP_SEL:
+		z = boolector_zero(btor, s);
+		d = boolector_ne(btor, a, z);
+		t = boolector_cond(btor, d, b, c);
+		break;
+	default:
+		fprintf(stderr, "unsupported insn\n");
+		return;
+	}
+	insn->target->priv = t;
+}
+
+static bool check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn)
+{
+	char model_format[] = "btor";
+	int res;
+
+	boolector_assert(btor, boolector_not(btor, n));
+	res = boolector_sat(btor);
+	switch (res) {
+	case BOOLECTOR_UNSAT:
+		return 1;
+	case BOOLECTOR_SAT:
+		sparse_error(insn->pos, "assertion failed");
+		show_entry(insn->bb->ep);
+		boolector_dump_btor(btor, stdout);
+		boolector_print_model(btor, model_format, stdout);
+		break;
+	default:
+		sparse_error(insn->pos, "SMT failure");
+		break;
+	}
+	return 0;
+}
+
+static bool check_assert(Btor *btor, struct instruction *insn)
+{
+	BoolectorNode *a = get_arg(btor, insn, 0);
+	BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
+	BoolectorNode *n = boolector_ne(btor, a, z);
+	return check_btor(btor, n, insn);
+}
+
+static bool check_call(Btor *btor, struct instruction *insn)
+{
+	pseudo_t func = insn->func;
+	struct ident *ident = func->ident;
+
+	if (ident == &__assert_ident)
+		return check_assert(btor, insn);
+	return 0;
+}
+
+static bool check_function(struct entrypoint *ep)
+{
+	Btor *btor = boolector_new();
+	struct basic_block *bb;
+	int rc = 0;
+
+	boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1);
+
+	FOR_EACH_PTR(ep->bbs, bb) {
+		struct instruction *insn;
+		FOR_EACH_PTR(bb->insns, insn) {
+			if (!insn->bb)
+				continue;
+			switch (insn->opcode) {
+			case OP_ENTRY:
+				continue;
+			case OP_BINARY ... OP_BINARY_END:
+				binop(btor, insn);
+				break;
+			case OP_BINCMP ... OP_BINCMP_END:
+				icmp(btor, insn);
+				break;
+			case OP_UNOP ... OP_UNOP_END:
+				unop(btor, insn);
+				break;
+			case OP_SEL:
+				ternop(btor, insn);
+				break;
+			case OP_CALL:
+				rc = check_call(btor, insn);
+				goto out;
+			case OP_RET:
+				goto out;
+			default:
+				fprintf(stderr, "unsupported insn\n");
+				goto out;
+			}
+		} END_FOR_EACH_PTR(insn);
+	} END_FOR_EACH_PTR(bb);
+	fprintf(stderr, "unterminated function\n");
+
+out:
+	boolector_release_all(btor);
+	boolector_delete(btor);
+	return rc;
+}
+
+static void check_functions(struct symbol_list *list)
+{
+	struct symbol *sym;
+
+	FOR_EACH_PTR(list, sym) {
+		struct entrypoint *ep;
+
+		expand_symbol(sym);
+		ep = linearize_symbol(sym);
+		if (!ep || !ep->entry)
+			continue;
+		check_function(ep);
+	} END_FOR_EACH_PTR(sym);
+}
+
+int main(int argc, char **argv)
+{
+	struct string_list *filelist = NULL;
+	char *file;
+
+	Wdecl = 0;
+
+	sparse_initialize(argc, argv, &filelist);
+
+	declare_builtins(0, builtins_scheck);
+
+	// Expand, linearize and check.
+	FOR_EACH_PTR(filelist, file) {
+		check_functions(sparse(file));
+	} END_FOR_EACH_PTR(file);
+	return 0;
+}
diff --git a/validation/scheck/ko.c b/validation/scheck/ko.c
new file mode 100644
index 000000000000..dbd861ea17fd
--- /dev/null
+++ b/validation/scheck/ko.c
@@ -0,0 +1,10 @@
+static void ko(int x)
+{
+	__assert((~x) == (~0 + x));
+}
+
+/*
+ * check-name: scheck-ko
+ * check-command: scheck $file
+ * check-known-to-fail
+ */
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c
new file mode 100644
index 000000000000..113912e01aad
--- /dev/null
+++ b/validation/scheck/ok.c
@@ -0,0 +1,14 @@
+static void ok(int x)
+{
+	__assert((~x) == (~0 - x));	// true but not simplified yet
+}
+
+static void always(int x)
+{
+	__assert((x - x) == 0);		// true and simplified
+}
+
+/*
+ * check-name: scheck-ok
+ * check-command: scheck $file
+ */
diff --git a/validation/test-suite b/validation/test-suite
index 1b05c75e9f74..2f7950ef50a4 100755
--- a/validation/test-suite
+++ b/validation/test-suite
@@ -13,6 +13,9 @@ prog_name=`basename $0`
 if [ ! -x "$default_path/sparse-llvm" ]; then
 	disabled_cmds="sparsec sparsei sparse-llvm sparse-llvm-dis"
 fi
+if [ ! -x "$default_path/scheck" ]; then
+	disabled_cmds="$disabled_cmds scheck"
+fi
 
 # flags:
 #	- some tests gave an unexpected result
@@ -513,6 +516,7 @@ echo "    -a                         append the created test to the input file"
 echo "    -f                         write a test known to fail"
 echo "    -l                         write a test for linearized code"
 echo "    -p                         write a test for pre-processing"
+echo "    -s                         write a test for symbolic checking"
 echo
 echo "argument(s):"
 echo "    file                       file containing the test case(s)"
@@ -540,6 +544,8 @@ do_format()
 			linear=1 ;;
 		-p)
 			def_cmd='sparse -E $file' ;;
+		-s)
+			def_cmd='scheck $file' ;;
 
 		help|-*)
 			do_format_help
-- 
2.31.1

[PATCH v2 5/8] scheck: assert_eq()

[Luc Van Oostenryck]

Testing the equivalence of two sub-expressions can be done with
with a single assertion like __assert(A == B).

However, in some cases, Sparse can use the equality to simplify
the whole expression although it's unable to simplify one of
the two sub-expressions into the other.

So, add a new assertion, __assert_eq(), testing the equality of
the two expressions given in argument independently of each other.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 ident-list.h           |  1 +
 scheck.c               | 11 +++++++++++
 validation/scheck/ok.c |  5 +++++
 3 files changed, 17 insertions(+)

diff --git a/ident-list.h b/ident-list.h
index 918f54d75fc4..ab5bc5f52e01 100644
--- a/ident-list.h
+++ b/ident-list.h
@@ -80,6 +80,7 @@ IDENT(main);
 
 /* used by the symbolic checker */
 IDENT(__assert);
+IDENT(__assert_eq);
 
 #undef __IDENT
 #undef IDENT
diff --git a/scheck.c b/scheck.c
index 63cbfa2d3404..c64e865136c5 100644
--- a/scheck.c
+++ b/scheck.c
@@ -32,6 +32,7 @@
 #define dyntype incomplete_ctype
 static const struct builtin_fn builtins_scheck[] = {
 	{ "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op },
+	{ "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
 	{}
 };
 
@@ -224,6 +225,14 @@ static bool check_assert(Btor *btor, struct instruction *insn)
 	return check_btor(btor, n, insn);
 }
 
+static bool check_equal(Btor *btor, struct instruction *insn)
+{
+	BoolectorNode *a = get_arg(btor, insn, 0);
+	BoolectorNode *b = get_arg(btor, insn, 1);
+	BoolectorNode *n = boolector_eq(btor, a, b);
+	return check_btor(btor, n, insn);
+}
+
 static bool check_call(Btor *btor, struct instruction *insn)
 {
 	pseudo_t func = insn->func;
@@ -231,6 +240,8 @@ static bool check_call(Btor *btor, struct instruction *insn)
 
 	if (ident == &__assert_ident)
 		return check_assert(btor, insn);
+	if (ident == &__assert_eq_ident)
+		return check_equal(btor, insn);
 	return 0;
 }
 
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c
index 113912e01aad..76c04c4f6870 100644
--- a/validation/scheck/ok.c
+++ b/validation/scheck/ok.c
@@ -3,6 +3,11 @@ static void ok(int x)
 	__assert((~x) == (~0 - x));	// true but not simplified yet
 }
 
+static void also_ok(int x)
+{
+	__assert_eq(~x, ~0 - x);
+}
+
 static void always(int x)
 {
 	__assert((x - x) == 0);		// true and simplified
-- 
2.31.1

[PATCH v2 6/8] scheck: allow multiple assertions

[Luc Van Oostenryck]

With the SMT solver used here, by default, once an expression is
checked it's kinda consumed by the process and can't be reused
anymore for another check.

So, enable the incremental mode: it allows to call boolecter_sat()
several times.

Note: Another would be, of course, to just AND together all assertions
      and just check this but then we would lost the finer grained
      diagnostic in case of failure.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 scheck.c               | 5 +++--
 validation/scheck/ok.c | 4 ----
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/scheck.c b/scheck.c
index c64e865136c5..efa5c1c3247b 100644
--- a/scheck.c
+++ b/scheck.c
@@ -252,6 +252,7 @@ static bool check_function(struct entrypoint *ep)
 	int rc = 0;
 
 	boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1);
+	boolector_set_opt(btor, BTOR_OPT_INCREMENTAL, 1);
 
 	FOR_EACH_PTR(ep->bbs, bb) {
 		struct instruction *insn;
@@ -274,8 +275,8 @@ static bool check_function(struct entrypoint *ep)
 				ternop(btor, insn);
 				break;
 			case OP_CALL:
-				rc = check_call(btor, insn);
-				goto out;
+				rc &= check_call(btor, insn);
+				break;
 			case OP_RET:
 				goto out;
 			default:
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c
index 76c04c4f6870..f4a0daabfe9a 100644
--- a/validation/scheck/ok.c
+++ b/validation/scheck/ok.c
@@ -1,10 +1,6 @@
 static void ok(int x)
 {
 	__assert((~x) == (~0 - x));	// true but not simplified yet
-}
-
-static void also_ok(int x)
-{
 	__assert_eq(~x, ~0 - x);
 }
 
-- 
2.31.1

[PATCH v2 7/8] scheck: assert_const()

[Luc Van Oostenryck]

Since, the symbolic checker check expressions at the ... symbolic
level, this can be used to check if two expressions are equivalent
but not if this equivalence is effectively used.

So, add a new assertion (this time not at the symbolic level) to
check if an expression which is expected to simplify to a constant
is effectively simplified to this constant.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 ident-list.h           |  1 +
 scheck.c               | 19 +++++++++++++++++++
 validation/scheck/ok.c |  1 +
 3 files changed, 21 insertions(+)

diff --git a/ident-list.h b/ident-list.h
index ab5bc5f52e01..6264fd062534 100644
--- a/ident-list.h
+++ b/ident-list.h
@@ -81,6 +81,7 @@ IDENT(main);
 /* used by the symbolic checker */
 IDENT(__assert);
 IDENT(__assert_eq);
+IDENT(__assert_const);
 
 #undef __IDENT
 #undef IDENT
diff --git a/scheck.c b/scheck.c
index efa5c1c3247b..f5ea4cf11902 100644
--- a/scheck.c
+++ b/scheck.c
@@ -33,6 +33,7 @@
 static const struct builtin_fn builtins_scheck[] = {
 	{ "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op },
 	{ "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
+	{ "__assert_const", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
 	{}
 };
 
@@ -233,6 +234,22 @@ static bool check_equal(Btor *btor, struct instruction *insn)
 	return check_btor(btor, n, insn);
 }
 
+static bool check_const(Btor *ctxt, struct instruction *insn)
+{
+	pseudo_t src1 = ptr_list_nth(insn->arguments, 0);
+	pseudo_t src2 = ptr_list_nth(insn->arguments, 1);
+
+	if (src2->type != PSEUDO_VAL)
+		sparse_error(insn->pos, "should be a constant: %s", show_pseudo(src2));
+	if (src1 == src2)
+		return 1;
+	if (src1->type != PSEUDO_VAL)
+		sparse_error(insn->pos, "not a constant: %s", show_pseudo(src1));
+	else
+		sparse_error(insn->pos, "invalid value: %s != %s", show_pseudo(src1), show_pseudo(src2));
+	return 0;
+}
+
 static bool check_call(Btor *btor, struct instruction *insn)
 {
 	pseudo_t func = insn->func;
@@ -242,6 +259,8 @@ static bool check_call(Btor *btor, struct instruction *insn)
 		return check_assert(btor, insn);
 	if (ident == &__assert_eq_ident)
 		return check_equal(btor, insn);
+	if (ident == &__assert_const_ident)
+		return check_const(btor, insn);
 	return 0;
 }
 
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c
index f4a0daabfe9a..8f65013e1618 100644
--- a/validation/scheck/ok.c
+++ b/validation/scheck/ok.c
@@ -2,6 +2,7 @@ static void ok(int x)
 {
 	__assert((~x) == (~0 - x));	// true but not simplified yet
 	__assert_eq(~x, ~0 - x);
+	__assert_const(x & 0, 0);
 }
 
 static void always(int x)
-- 
2.31.1

[PATCH v2 8/8] scheck: support pre-conditions via __assume()

[Luc Van Oostenryck]

A lot of simplifications are only valid when their variables
satisfy to some conditions (like "is within a given range" or
"is a power of two").

So, allow to add such pre-conditions via new _assume() statements.
Internally, all such preconditions are ANDed together and what is
checked is they imply the assertions:
	AND(pre-condition) implies assertion 1
	...

Note: IIUC, it seems that boolector has a native mechanism for such
      things but I'm not sure if t can be used here.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 ident-list.h           |  1 +
 scheck.c               | 33 ++++++++++++++++++++++++---------
 validation/scheck/ok.c |  6 ++++++
 3 files changed, 31 insertions(+), 9 deletions(-)

diff --git a/ident-list.h b/ident-list.h
index 6264fd062534..3c08e8ca9aa4 100644
--- a/ident-list.h
+++ b/ident-list.h
@@ -79,6 +79,7 @@ IDENT(copy_to_user); IDENT(copy_from_user);
 IDENT(main);
 
 /* used by the symbolic checker */
+IDENT(__assume);
 IDENT(__assert);
 IDENT(__assert_eq);
 IDENT(__assert_const);
diff --git a/scheck.c b/scheck.c
index f5ea4cf11902..6752b9d9baaf 100644
--- a/scheck.c
+++ b/scheck.c
@@ -31,6 +31,7 @@
 
 #define dyntype incomplete_ctype
 static const struct builtin_fn builtins_scheck[] = {
+	{ "__assume", &void_ctype, 0, { &dyntype }, .op = &generic_int_op },
 	{ "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op },
 	{ "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
 	{ "__assert_const", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
@@ -195,11 +196,22 @@ static void ternop(Btor *btor, struct instruction *insn)
 	insn->target->priv = t;
 }
 
-static bool check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn)
+static bool add_precondition(Btor *btor, BoolectorNode **pre, struct instruction *insn)
+{
+	BoolectorNode *a = get_arg(btor, insn, 0);
+	BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
+	BoolectorNode *n = boolector_ne(btor, a, z);
+	BoolectorNode *p = boolector_and(btor, *pre, n);
+	*pre = p;
+	return true;
+}
+
+static bool check_btor(Btor *btor, BoolectorNode *p, BoolectorNode *n, struct instruction *insn)
 {
 	char model_format[] = "btor";
 	int res;
 
+	n = boolector_implies(btor, p, n);
 	boolector_assert(btor, boolector_not(btor, n));
 	res = boolector_sat(btor);
 	switch (res) {
@@ -218,20 +230,20 @@ static bool check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn)
 	return 0;
 }
 
-static bool check_assert(Btor *btor, struct instruction *insn)
+static bool check_assert(Btor *btor, BoolectorNode *pre, struct instruction *insn)
 {
 	BoolectorNode *a = get_arg(btor, insn, 0);
 	BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
 	BoolectorNode *n = boolector_ne(btor, a, z);
-	return check_btor(btor, n, insn);
+	return check_btor(btor, pre, n, insn);
 }
 
-static bool check_equal(Btor *btor, struct instruction *insn)
+static bool check_equal(Btor *btor, BoolectorNode *pre, struct instruction *insn)
 {
 	BoolectorNode *a = get_arg(btor, insn, 0);
 	BoolectorNode *b = get_arg(btor, insn, 1);
 	BoolectorNode *n = boolector_eq(btor, a, b);
-	return check_btor(btor, n, insn);
+	return check_btor(btor, pre, n, insn);
 }
 
 static bool check_const(Btor *ctxt, struct instruction *insn)
@@ -250,15 +262,17 @@ static bool check_const(Btor *ctxt, struct instruction *insn)
 	return 0;
 }
 
-static bool check_call(Btor *btor, struct instruction *insn)
+static bool check_call(Btor *btor, BoolectorNode **pre, struct instruction *insn)
 {
 	pseudo_t func = insn->func;
 	struct ident *ident = func->ident;
 
+	if (ident == &__assume_ident)
+		return add_precondition(btor, pre, insn);
 	if (ident == &__assert_ident)
-		return check_assert(btor, insn);
+		return check_assert(btor, *pre, insn);
 	if (ident == &__assert_eq_ident)
-		return check_equal(btor, insn);
+		return check_equal(btor, *pre, insn);
 	if (ident == &__assert_const_ident)
 		return check_const(btor, insn);
 	return 0;
@@ -267,6 +281,7 @@ static bool check_call(Btor *btor, struct instruction *insn)
 static bool check_function(struct entrypoint *ep)
 {
 	Btor *btor = boolector_new();
+	BoolectorNode *pre = boolector_true(btor);
 	struct basic_block *bb;
 	int rc = 0;
 
@@ -294,7 +309,7 @@ static bool check_function(struct entrypoint *ep)
 				ternop(btor, insn);
 				break;
 			case OP_CALL:
-				rc &= check_call(btor, insn);
+				rc &= check_call(btor, &pre, insn);
 				break;
 			case OP_RET:
 				goto out;
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c
index 8f65013e1618..1e5314f24ded 100644
--- a/validation/scheck/ok.c
+++ b/validation/scheck/ok.c
@@ -10,6 +10,12 @@ static void always(int x)
 	__assert((x - x) == 0);		// true and simplified
 }
 
+static void assumed(int x, int a, int b)
+{
+	__assume((a & ~b) == 0);
+	__assert_eq((x ^ a) | b, x | b);
+}
+
 /*
  * check-name: scheck-ok
  * check-command: scheck $file
-- 
2.31.1