Lines Matching refs:insn
74 static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx)
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);
83 static BoolectorNode *zext(Btor *btor, struct instruction *insn, BoolectorNode *s)
86 int new = insn->type->bit_size;
90 static BoolectorNode *sext(Btor *btor, struct instruction *insn, BoolectorNode *s)
93 int new = insn->type->bit_size;
97 static BoolectorNode *slice(Btor *btor, struct instruction *insn, BoolectorNode *s)
100 int new = insn->type->bit_size;
104 static void binary(Btor *btor, BoolectorSort s, struct instruction *insn)
108 a = mkvar(btor, s, insn->src1);
109 b = mkvar(btor, s, insn->src2);
112 switch (insn->opcode) {
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;
137 fprintf(stderr, "unsupported insn\n");
140 insn->target->priv = t;
143 static void binop(Btor *btor, struct instruction *insn)
145 BoolectorSort s = get_sort(btor, insn->type, insn->pos);
146 binary(btor, s, insn);
149 static void icmp(Btor *btor, struct instruction *insn)
151 BoolectorSort s = get_sort(btor, insn->itype, insn->pos);
152 binary(btor, s, insn);
155 static void unop(Btor *btor, struct instruction *insn)
157 BoolectorSort s = get_sort(btor, insn->type, insn->pos);
160 a = mkvar(btor, s, insn->src1);
163 switch (insn->opcode) {
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;
170 fprintf(stderr, "unsupported insn\n");
173 insn->target->priv = t;
176 static void ternop(Btor *btor, struct instruction *insn)
178 BoolectorSort s = get_sort(btor, insn->type, insn->pos);
181 a = mkvar(btor, s, insn->src1);
182 b = mkvar(btor, s, insn->src2);
183 c = mkvar(btor, s, insn->src3);
186 switch (insn->opcode) {
193 fprintf(stderr, "unsupported insn\n");
196 insn->target->priv = t;
199 static bool add_precondition(Btor *btor, BoolectorNode **pre, struct instruction *insn)
201 BoolectorNode *a = get_arg(btor, insn, 0);
209 static bool check_btor(Btor *btor, BoolectorNode *p, BoolectorNode *n, struct instruction *insn)
221 sparse_error(insn->pos, "assertion failed");
222 show_entry(insn->bb->ep);
227 sparse_error(insn->pos, "SMT failure");
233 static bool check_assert(Btor *btor, BoolectorNode *pre, struct instruction *insn)
235 BoolectorNode *a = get_arg(btor, insn, 0);
238 return check_btor(btor, pre, n, insn);
241 static bool check_equal(Btor *btor, BoolectorNode *pre, struct instruction *insn)
243 BoolectorNode *a = get_arg(btor, insn, 0);
244 BoolectorNode *b = get_arg(btor, insn, 1);
246 return check_btor(btor, pre, n, insn);
249 static bool check_const(Btor *ctxt, struct instruction *insn)
251 pseudo_t src1 = ptr_list_nth(insn->arguments, 0);
252 pseudo_t src2 = ptr_list_nth(insn->arguments, 1);
255 sparse_error(insn->pos, "should be a constant: %s", show_pseudo(src2));
259 sparse_error(insn->pos, "not a constant: %s", show_pseudo(src1));
261 sparse_error(insn->pos, "invalid value: %s != %s", show_pseudo(src1), show_pseudo(src2));
265 static bool check_call(Btor *btor, BoolectorNode **pre, struct instruction *insn)
267 pseudo_t func = insn->func;
271 return add_precondition(btor, pre, insn);
273 return check_assert(btor, *pre, insn);
275 return check_equal(btor, *pre, insn);
277 return check_const(btor, insn);
292 struct instruction *insn;
293 FOR_EACH_PTR(bb->insns, insn) {
294 if (!insn->bb)
296 switch (insn->opcode) {
300 binop(btor, insn);
303 icmp(btor, insn);
306 unop(btor, insn);
309 ternop(btor, insn);
312 rc &= check_call(btor, &pre, insn);
317 fprintf(stderr, "unsupported insn\n");
320 } END_FOR_EACH_PTR(insn);