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

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

[Luc Van Oostenryck]

Some instruction simplifications can be quite tricky and thus
easy to get wrong. Often, they are lso 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. This, combined wth some assertion at the
C source level, allows to symbolically check the expressions in
these assertions. In other words, it allows to check if these
expressions 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".


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              |  52 +++++-
 builtin.h              |   4 +
 ident-list.h           |   6 +
 scheck.c               | 348 +++++++++++++++++++++++++++++++++++++++++
 validation/scheck/ko.c |  10 ++
 validation/scheck/ok.c |  22 +++
 validation/test-suite  |   6 +
 9 files changed, 472 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 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 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:
	op(T)
	op(T, T)
	op(T,T, ... T)
where T is some integer type.

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

diff --git a/builtin.c b/builtin.c
index ff03dbab9a06..f03bf109c818 100644
--- a/builtin.c
+++ b/builtin.c
@@ -390,6 +390,56 @@ static struct symbol_op overflow_p_op = {
 };
 
 
+///
+// Evaluate the arguments of 'generic' integer operators.
+//
+// All arguments must be the same basic integer type and
+// their number comes from the prototype and is already checked.
+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) {
+		struct symbol *type;
+
+		if (++n == 1) {
+			t = arg->ctype;
+			if (!arg || !(type = arg->ctype))
+				return 0;
+			if (type->type == SYM_NODE)
+				type = type->ctype.base_type;
+			if (!type)
+				return 0;
+			if (type->ctype.base_type != &int_type || type == &bool_ctype)
+				goto err;
+		} else {
+			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

[PATCH 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 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               | 302 +++++++++++++++++++++++++++++++++++++++++
 validation/scheck/ko.c |  10 ++
 validation/scheck/ok.c |  14 ++
 validation/test-suite  |   6 +
 7 files changed, 343 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..719aeea84e7c
--- /dev/null
+++ b/scheck.c
@@ -0,0 +1,302 @@
+// 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 binop(Btor *btor, struct instruction *insn)
+{
+	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
+	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 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:
+			case OP_BINCMP ... OP_BINCMP_END:
+				binop(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 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 719aeea84e7c..ff91328f681a 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 },
 	{}
 };
 
@@ -213,6 +214,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;
@@ -220,6 +229,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 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 ff91328f681a..26f88a4a028e 100644
--- a/scheck.c
+++ b/scheck.c
@@ -241,6 +241,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;
@@ -261,8 +262,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 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 26f88a4a028e..ff140aaa1e95 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 },
 	{}
 };
 
@@ -222,6 +223,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;
@@ -231,6 +248,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 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 ff140aaa1e95..b8bc9bb28498 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 },
@@ -184,11 +185,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) {
@@ -207,20 +219,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)
@@ -239,15 +251,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;
@@ -256,6 +270,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;
 
@@ -281,7 +296,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

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

[Ramsay Jones]

On 10/04/2021 14:30, Luc Van Oostenryck wrote:
> This can be used to define some generic (polymorphic) builtin
> with a signature like:
> 	op(T)
> 	op(T, T)
> 	op(T,T, ... T)
> where T is some integer type.
> 
> Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
> ---
>  builtin.c | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
>  builtin.h |  2 ++
>  2 files changed, 52 insertions(+)
> 
> diff --git a/builtin.c b/builtin.c
> index ff03dbab9a06..f03bf109c818 100644
> --- a/builtin.c
> +++ b/builtin.c
> @@ -390,6 +390,56 @@ static struct symbol_op overflow_p_op = {
>  };
>  

I must apologize in advance, I've got a head cold, I'm tired and
should probably not be commenting (especially since I am only
skimming these patches), but ...

>  
> +///
> +// Evaluate the arguments of 'generic' integer operators.
> +//
> +// All arguments must be the same basic integer type and
> +// their number comes from the prototype and is already checked.
> +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);

So, t is used to iterate over the 'fntype->arguments' (which is to say
the generic type T), ...

> +	FOR_EACH_PTR(expr->args, arg) {
> +		struct symbol *type;
> +
> +		if (++n == 1) {
> +			t = arg->ctype;

which is then set to the first argument type, here ...

> +			if (!arg || !(type = arg->ctype))
> +				return 0;
> +			if (type->type == SYM_NODE)
> +				type = type->ctype.base_type;
> +			if (!type)
> +				return 0;
> +			if (type->ctype.base_type != &int_type || type == &bool_ctype)
> +				goto err;
> +		} else {
> +			t = ctype;

... and thereafter (for 2, 3, ...) to NULL. (ctype is not set to anything
and it is initialized to NULL above).

> +		}
> +		add_ptr_list(&types, t);

... so this 'types' list is just {arg->ctype, NULL, NULL, ...}

> +		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);

here, n will only ever be 1, right? (only way to get here, via goto, from
the n == 1 conditional, above).

> +	info(arg->pos, "        %s", show_typename(arg->ctype));
> +	expr->ctype = &bad_ctype;
> +	return 0;
> +}

I stopped reading here. (I probably should have stopped sooner! ;).

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 2/8] builtin: define a symbol_op for a generic op acting on integer

[Luc Van Oostenryck]

On Sun, Apr 11, 2021 at 09:40:19PM +0100, Ramsay Jones wrote:
> On 10/04/2021 14:30, Luc Van Oostenryck wrote:
> > This can be used to define some generic (polymorphic) builtin
> > with a signature like:
> > 	op(T)
> > 	op(T, T)
> > 	op(T,T, ... T)
> > where T is some integer type.
> > 
> > Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
> > ---
> >  builtin.c | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
> >  builtin.h |  2 ++
> >  2 files changed, 52 insertions(+)
> > 
> > diff --git a/builtin.c b/builtin.c
> > index ff03dbab9a06..f03bf109c818 100644
> > --- a/builtin.c
> > +++ b/builtin.c
> > @@ -390,6 +390,56 @@ static struct symbol_op overflow_p_op = {
> >  };
> >  
> 
> I must apologize in advance, I've got a head cold, I'm tired and
> should probably not be commenting (especially since I am only
> skimming these patches), but ...

Sorry to hear this, and it's me that should apology, really.
This patch was a quick rough draft that I forget to return to it.
It's indeed very broken.

Thank you very much for noticing this.

-- Luc