1// SPDX-License-Identifier: MIT
2// Copyright (C) 2021 Luc Van Oostenryck
3
4///
5// Symbolic checker for Sparse's IR
6// --------------------------------
7//
8// This is an example client program with a dual purpose:
9//	# It shows how to translate Sparse's IR into the language
10//	  of SMT solvers (only the part concerning integers,
11//	  floating-point and memory is ignored).
12//	# It's used as a simple symbolic checker for the IR.
13//	  The idea is to create a mini-language that allows to
14//	  express some assertions with some pre-conditions.
15
16#include <stdarg.h>
17#include <stdlib.h>
18#include <stdio.h>
19#include <string.h>
20#include <ctype.h>
21#include <unistd.h>
22#include <fcntl.h>
23
24#include <boolector.h>
25#include "lib.h"
26#include "expression.h"
27#include "linearize.h"
28#include "symbol.h"
29#include "builtin.h"
30
31
32#define dyntype incomplete_ctype
33static const struct builtin_fn builtins_scheck[] = {
34	{ "__assume", &void_ctype, 0, { &dyntype }, .op = &generic_int_op },
35	{ "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op },
36	{ "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
37	{ "__assert_const", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
38	{}
39};
40
41
42static BoolectorSort get_sort(Btor *btor, struct symbol *type, struct position pos)
43{
44	if (!is_int_type(type)) {
45		sparse_error(pos, "invalid type");
46		return NULL;
47	}
48	return boolector_bitvec_sort(btor, type->bit_size);
49}
50
51static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo)
52{
53	static char buff[33];
54	BoolectorNode *n;
55
56	if (pseudo->priv)
57		return pseudo->priv;
58
59	switch (pseudo->type) {
60	case PSEUDO_VAL:
61		sprintf(buff, "%llx", pseudo->value);
62		return boolector_consth(btor, s, buff);
63	case PSEUDO_ARG:
64	case PSEUDO_REG:
65		n = boolector_var(btor, s, show_pseudo(pseudo));
66		break;
67	default:
68		fprintf(stderr, "invalid pseudo: %s\n", show_pseudo(pseudo));
69		return NULL;
70	}
71	return pseudo->priv = n;
72}
73
74static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx)
75{
76	pseudo_t arg = ptr_list_nth(insn->arguments, idx);
77	struct symbol *type = ptr_list_nth(insn->fntypes, idx + 1);
78	BoolectorSort s = get_sort(btor, type, insn->pos);
79
80	return mkvar(btor, s, arg);
81}
82
83static BoolectorNode *zext(Btor *btor, struct instruction *insn, BoolectorNode *s)
84{
85	int old = boolector_get_width(btor, s);
86	int new = insn->type->bit_size;
87	return boolector_uext(btor, s, new - old);
88}
89
90static BoolectorNode *sext(Btor *btor, struct instruction *insn, BoolectorNode *s)
91{
92	int old = boolector_get_width(btor, s);
93	int new = insn->type->bit_size;
94	return boolector_sext(btor, s, new - old);
95}
96
97static BoolectorNode *slice(Btor *btor, struct instruction *insn, BoolectorNode *s)
98{
99	int old = boolector_get_width(btor, s);
100	int new = insn->type->bit_size;
101	return boolector_slice(btor, s, old - new - 1, 0);
102}
103
104static void binary(Btor *btor, BoolectorSort s, struct instruction *insn)
105{
106	BoolectorNode *t, *a, *b;
107
108	a = mkvar(btor, s, insn->src1);
109	b = mkvar(btor, s, insn->src2);
110	if (!a || !b)
111		return;
112	switch (insn->opcode) {
113	case OP_ADD:	t = boolector_add(btor, a, b); break;
114	case OP_SUB:	t = boolector_sub(btor, a, b); break;
115	case OP_MUL:	t = boolector_mul(btor, a, b); break;
116	case OP_AND:	t = boolector_and(btor, a, b); break;
117	case OP_OR:	t = boolector_or (btor, a, b); break;
118	case OP_XOR:	t = boolector_xor(btor, a, b); break;
119	case OP_SHL:	t = boolector_sll(btor, a, b); break;
120	case OP_LSR:	t = boolector_srl(btor, a, b); break;
121	case OP_ASR:	t = boolector_sra(btor, a, b); break;
122	case OP_DIVS:	t = boolector_sdiv(btor, a, b); break;
123	case OP_DIVU:	t = boolector_udiv(btor, a, b); break;
124	case OP_MODS:	t = boolector_srem(btor, a, b); break;
125	case OP_MODU:	t = boolector_urem(btor, a, b); break;
126	case OP_SET_EQ:	t = zext(btor, insn, boolector_eq(btor, a, b)); break;
127	case OP_SET_NE:	t = zext(btor, insn, boolector_ne(btor, a, b)); break;
128	case OP_SET_LT:	t = zext(btor, insn, boolector_slt(btor, a, b)); break;
129	case OP_SET_LE:	t = zext(btor, insn, boolector_slte(btor, a, b)); break;
130	case OP_SET_GE:	t = zext(btor, insn, boolector_sgte(btor, a, b)); break;
131	case OP_SET_GT:	t = zext(btor, insn, boolector_sgt(btor, a, b)); break;
132	case OP_SET_B:	t = zext(btor, insn, boolector_ult(btor, a, b)); break;
133	case OP_SET_BE:	t = zext(btor, insn, boolector_ulte(btor, a, b)); break;
134	case OP_SET_AE:	t = zext(btor, insn, boolector_ugte(btor, a, b)); break;
135	case OP_SET_A:	t = zext(btor, insn, boolector_ugt(btor, a, b)); break;
136	default:
137		fprintf(stderr, "unsupported insn\n");
138		return;
139	}
140	insn->target->priv = t;
141}
142
143static void binop(Btor *btor, struct instruction *insn)
144{
145	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
146	binary(btor, s, insn);
147}
148
149static void icmp(Btor *btor, struct instruction *insn)
150{
151	BoolectorSort s = get_sort(btor, insn->itype, insn->pos);
152	binary(btor, s, insn);
153}
154
155static void unop(Btor *btor, struct instruction *insn)
156{
157	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
158	BoolectorNode *t, *a;
159
160	a = mkvar(btor, s, insn->src1);
161	if (!a)
162		return;
163	switch (insn->opcode) {
164	case OP_NEG:	t = boolector_neg(btor, a); break;
165	case OP_NOT:	t = boolector_not(btor, a); break;
166	case OP_SEXT:	t = sext(btor, insn, a); break;
167	case OP_ZEXT:	t = zext(btor, insn, a); break;
168	case OP_TRUNC:	t = slice(btor, insn, a); break;
169	default:
170		fprintf(stderr, "unsupported insn\n");
171		return;
172	}
173	insn->target->priv = t;
174}
175
176static void ternop(Btor *btor, struct instruction *insn)
177{
178	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
179	BoolectorNode *t, *a, *b, *c, *z, *d;
180
181	a = mkvar(btor, s, insn->src1);
182	b = mkvar(btor, s, insn->src2);
183	c = mkvar(btor, s, insn->src3);
184	if (!a || !b || !c)
185		return;
186	switch (insn->opcode) {
187	case OP_SEL:
188		z = boolector_zero(btor, s);
189		d = boolector_ne(btor, a, z);
190		t = boolector_cond(btor, d, b, c);
191		break;
192	default:
193		fprintf(stderr, "unsupported insn\n");
194		return;
195	}
196	insn->target->priv = t;
197}
198
199static bool add_precondition(Btor *btor, BoolectorNode **pre, struct instruction *insn)
200{
201	BoolectorNode *a = get_arg(btor, insn, 0);
202	BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
203	BoolectorNode *n = boolector_ne(btor, a, z);
204	BoolectorNode *p = boolector_and(btor, *pre, n);
205	*pre = p;
206	return true;
207}
208
209static bool check_btor(Btor *btor, BoolectorNode *p, BoolectorNode *n, struct instruction *insn)
210{
211	char model_format[] = "btor";
212	int res;
213
214	n = boolector_implies(btor, p, n);
215	boolector_assert(btor, boolector_not(btor, n));
216	res = boolector_sat(btor);
217	switch (res) {
218	case BOOLECTOR_UNSAT:
219		return 1;
220	case BOOLECTOR_SAT:
221		sparse_error(insn->pos, "assertion failed");
222		show_entry(insn->bb->ep);
223		boolector_dump_btor(btor, stdout);
224		boolector_print_model(btor, model_format, stdout);
225		break;
226	default:
227		sparse_error(insn->pos, "SMT failure");
228		break;
229	}
230	return 0;
231}
232
233static bool check_assert(Btor *btor, BoolectorNode *pre, struct instruction *insn)
234{
235	BoolectorNode *a = get_arg(btor, insn, 0);
236	BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
237	BoolectorNode *n = boolector_ne(btor, a, z);
238	return check_btor(btor, pre, n, insn);
239}
240
241static bool check_equal(Btor *btor, BoolectorNode *pre, struct instruction *insn)
242{
243	BoolectorNode *a = get_arg(btor, insn, 0);
244	BoolectorNode *b = get_arg(btor, insn, 1);
245	BoolectorNode *n = boolector_eq(btor, a, b);
246	return check_btor(btor, pre, n, insn);
247}
248
249static bool check_const(Btor *ctxt, struct instruction *insn)
250{
251	pseudo_t src1 = ptr_list_nth(insn->arguments, 0);
252	pseudo_t src2 = ptr_list_nth(insn->arguments, 1);
253
254	if (src2->type != PSEUDO_VAL)
255		sparse_error(insn->pos, "should be a constant: %s", show_pseudo(src2));
256	if (src1 == src2)
257		return 1;
258	if (src1->type != PSEUDO_VAL)
259		sparse_error(insn->pos, "not a constant: %s", show_pseudo(src1));
260	else
261		sparse_error(insn->pos, "invalid value: %s != %s", show_pseudo(src1), show_pseudo(src2));
262	return 0;
263}
264
265static bool check_call(Btor *btor, BoolectorNode **pre, struct instruction *insn)
266{
267	pseudo_t func = insn->func;
268	struct ident *ident = func->ident;
269
270	if (ident == &__assume_ident)
271		return add_precondition(btor, pre, insn);
272	if (ident == &__assert_ident)
273		return check_assert(btor, *pre, insn);
274	if (ident == &__assert_eq_ident)
275		return check_equal(btor, *pre, insn);
276	if (ident == &__assert_const_ident)
277		return check_const(btor, insn);
278	return 0;
279}
280
281static bool check_function(struct entrypoint *ep)
282{
283	Btor *btor = boolector_new();
284	BoolectorNode *pre = boolector_true(btor);
285	struct basic_block *bb;
286	int rc = 0;
287
288	boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1);
289	boolector_set_opt(btor, BTOR_OPT_INCREMENTAL, 1);
290
291	FOR_EACH_PTR(ep->bbs, bb) {
292		struct instruction *insn;
293		FOR_EACH_PTR(bb->insns, insn) {
294			if (!insn->bb)
295				continue;
296			switch (insn->opcode) {
297			case OP_ENTRY:
298				continue;
299			case OP_BINARY ... OP_BINARY_END:
300				binop(btor, insn);
301				break;
302			case OP_BINCMP ... OP_BINCMP_END:
303				icmp(btor, insn);
304				break;
305			case OP_UNOP ... OP_UNOP_END:
306				unop(btor, insn);
307				break;
308			case OP_SEL:
309				ternop(btor, insn);
310				break;
311			case OP_CALL:
312				rc &= check_call(btor, &pre, insn);
313				break;
314			case OP_RET:
315				goto out;
316			default:
317				fprintf(stderr, "unsupported insn\n");
318				goto out;
319			}
320		} END_FOR_EACH_PTR(insn);
321	} END_FOR_EACH_PTR(bb);
322	fprintf(stderr, "unterminated function\n");
323
324out:
325	boolector_release_all(btor);
326	boolector_delete(btor);
327	return rc;
328}
329
330static void check_functions(struct symbol_list *list)
331{
332	struct symbol *sym;
333
334	FOR_EACH_PTR(list, sym) {
335		struct entrypoint *ep;
336
337		expand_symbol(sym);
338		ep = linearize_symbol(sym);
339		if (!ep || !ep->entry)
340			continue;
341		check_function(ep);
342	} END_FOR_EACH_PTR(sym);
343}
344
345int main(int argc, char **argv)
346{
347	struct string_list *filelist = NULL;
348	char *file;
349
350	Wdecl = 0;
351
352	sparse_initialize(argc, argv, &filelist);
353
354	declare_builtins(0, builtins_scheck);
355	predefine_strong("__SYMBOLIC_CHECKER__");
356
357	// Expand, linearize and check.
358	FOR_EACH_PTR(filelist, file) {
359		check_functions(sparse(file));
360	} END_FOR_EACH_PTR(file);
361	return 0;
362}
363