Merge branch 'schecker'

* add a symbolic checker

9 files changed, 499 insertions, 18 deletions

diff --git a/.gitignore b/.gitignore
index 63c74afd..b22f86b1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,25 +8,26 @@
 .*.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
+/scheck
+/semind
+/sparse
+/sparse-llvm
+/test-dissect
+/test-inspect
+/test-lexing
+/test-linearize
+/test-parsing
+/test-show-type
+/test-unssa
 
 # tags
 tags
diff --git a/Makefile b/Makefile
index 6ad14375..69d20e72 100644
--- a/Makefile
+++ b/Makefile
@@ -226,6 +226,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/builtin.c b/builtin.c
index c7e7da3b..8e1d2d7e 100644
--- a/builtin.c
+++ b/builtin.c
@@ -390,6 +390,69 @@ 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) {
+		n++;
+
+		if (!is_dynamic_type(t)) {
+			;
+		} else if (!ctype) {
+			// first 'dynamic' type, check that it's 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;
@@ -559,7 +622,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 d0d3fd2c..5fe77c92 100644
--- a/builtin.h
+++ b/builtin.h
@@ -12,4 +12,8 @@ struct builtin_fn {
 	struct symbol_op *op;
 };
 
+void declare_builtins(int stream, const struct builtin_fn tbl[]);
+
+extern struct symbol_op generic_int_op;
+
 #endif
diff --git a/ident-list.h b/ident-list.h
index 8049b694..3c08e8ca 100644
--- a/ident-list.h
+++ b/ident-list.h
@@ -78,6 +78,12 @@ IDENT(memset); IDENT(memcpy);
 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);
+
 #undef __IDENT
 #undef IDENT
 #undef IDENT_RESERVED
diff --git a/scheck.c b/scheck.c
new file mode 100644
index 00000000..754fe76f
--- /dev/null
+++ b/scheck.c
@@ -0,0 +1,362 @@
+// 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[] = {
+	{ "__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 },
+	{}
+};
+
+
+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 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) {
+	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, 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, pre, n, 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, pre, 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, 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, *pre, insn);
+	if (ident == &__assert_eq_ident)
+		return check_equal(btor, *pre, insn);
+	if (ident == &__assert_const_ident)
+		return check_const(btor, insn);
+	return 0;
+}
+
+static bool check_function(struct entrypoint *ep)
+{
+	Btor *btor = boolector_new();
+	BoolectorNode *pre = boolector_true(btor);
+	struct basic_block *bb;
+	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;
+		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, &pre, insn);
+				break;
+			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);
+	predefine_strong("__SYMBOLIC_CHECKER__");
+
+	// 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 00000000..dbd861ea
--- /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 00000000..1e5314f2
--- /dev/null
+++ b/validation/scheck/ok.c
@@ -0,0 +1,22 @@
+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)
+{
+	__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
+ */
diff --git a/validation/test-suite b/validation/test-suite
index 370cd35a..305edd1f 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
@@ -514,6 +517,7 @@ echo "    -f                         write a test known to fail"
 echo "    -l                         write a test for linearized code"
 echo "    -r                         write a test for linearized code returning 1"
 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)"
@@ -545,6 +549,8 @@ do_format()
 			ret=1 ;;
 		-p)
 			def_cmd='sparse -E $file' ;;
+		-s)
+			def_cmd='scheck $file' ;;
 
 		help|-*)
 			do_format_help