scheck.c - pub/scm/devel/sparse/sparse-dev - Git at Google

 // 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;
 }
	// 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;
	}