[PATCH 0/5] small fixes for the symbolic checker

[PATCH 0/5] small fixes for the symbolic checker

[Luc Van Oostenryck]

From: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>

This series contains a few fixes for the symbolic checker (which
can be used internally to validate some code transformations).

Luc Van Oostenryck (5):
  scheck: better diagnostic for unsupported instructions
  scheck: ignore OP_NOP & friends
  scheck: constants are untyped
  scheck: mkvar() with target or input type
  scheck: fix type of operands in casts

 scheck.c | 48 +++++++++++++++++++++++++++++++-----------------
 1 file changed, 31 insertions(+), 17 deletions(-)

-- 
2.32.0

[PATCH 1/5] scheck: better diagnostic for unsupported instructions

[Luc Van Oostenryck]

From: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>

When reporting an unsupported instruction, display the instruction
together with the diagnostic message.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 scheck.c | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/scheck.c b/scheck.c
index 754fe76f986a..c830f56a0985 100644
--- a/scheck.c
+++ b/scheck.c
@@ -134,7 +134,7 @@ static void binary(Btor *btor, BoolectorSort s, struct instruction *insn)
 	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");
+		fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 		return;
 	}
 	insn->target->priv = t;
@@ -167,7 +167,7 @@ static void unop(Btor *btor, struct instruction *insn)
 	case OP_ZEXT:	t = zext(btor, insn, a); break;
 	case OP_TRUNC:	t = slice(btor, insn, a); break;
 	default:
-		fprintf(stderr, "unsupported insn\n");
+		fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 		return;
 	}
 	insn->target->priv = t;
@@ -190,7 +190,7 @@ static void ternop(Btor *btor, struct instruction *insn)
 		t = boolector_cond(btor, d, b, c);
 		break;
 	default:
-		fprintf(stderr, "unsupported insn\n");
+		fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 		return;
 	}
 	insn->target->priv = t;
@@ -314,7 +314,7 @@ static bool check_function(struct entrypoint *ep)
 			case OP_RET:
 				goto out;
 			default:
-				fprintf(stderr, "unsupported insn\n");
+				fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 				goto out;
 			}
 		} END_FOR_EACH_PTR(insn);
-- 
2.32.0

[PATCH 2/5] scheck: ignore OP_NOP & friends

[Luc Van Oostenryck]

From: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>

Some instructions have no effects and so can just be ignored here.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 scheck.c | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/scheck.c b/scheck.c
index c830f56a0985..d3ebddd6c2f5 100644
--- a/scheck.c
+++ b/scheck.c
@@ -313,6 +313,11 @@ static bool check_function(struct entrypoint *ep)
 				break;
 			case OP_RET:
 				goto out;
+			case OP_INLINED_CALL:
+			case OP_DEATHNOTE:
+			case OP_NOP:
+			case OP_CONTEXT:
+				continue;
 			default:
 				fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 				goto out;
-- 
2.32.0

[PATCH 3/5] scheck: constants are untyped

[Luc Van Oostenryck]

From: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>

in sparse, constants (PSEUDO_VALs) are not typed, so the same pseudo
can be used to represent 1-bit 0, 8-bit 0, 16-bit 0, ...

That's incompatible with the bit vectors used here, so we can't associate
a PSEUDO_VAL with its own bitvector like it's done for PSEUDO_REGs.
A fresh one is needed for each occurrence (we could use a small table
but won't bother).

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 scheck.c | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/scheck.c b/scheck.c
index d3ebddd6c2f5..5e2b60abb163 100644
--- a/scheck.c
+++ b/scheck.c
@@ -53,15 +53,14 @@ 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:
+		if (pseudo->priv)
+			return pseudo->priv;
 		n = boolector_var(btor, s, show_pseudo(pseudo));
 		break;
 	default:
-- 
2.32.0

[PATCH 4/5] scheck: mkvar() with target or input type

[Luc Van Oostenryck]

From: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>

Most instructions have one associated type, the 'target type'.
Some, like compares, have another one too, the 'input type'.

So, when creating a bitvector from an instruction, we need to specify
the type in some way.

So, create an helper for both cases: mktvar() and mkivar().

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 scheck.c | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/scheck.c b/scheck.c
index 5e2b60abb163..07b15a0600e3 100644
--- a/scheck.c
+++ b/scheck.c
@@ -70,6 +70,18 @@ static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo)
 	return pseudo->priv = n;
 }
 
+static BoolectorNode *mktvar(Btor *btor, struct instruction *insn, pseudo_t src)
+{
+	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
+	return mkvar(btor, s, src);
+}
+
+static BoolectorNode *mkivar(Btor *btor, struct instruction *insn, pseudo_t src)
+{
+	BoolectorSort s = get_sort(btor, insn->itype, insn->pos);
+	return mkvar(btor, s, src);
+}
+
 static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx)
 {
 	pseudo_t arg = ptr_list_nth(insn->arguments, idx);
-- 
2.32.0

[PATCH 5/5] scheck: fix type of operands in casts

[Luc Van Oostenryck]

From: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>

Casts were using the target type for their operands.

Fix this by using the new helper mkivar() for them.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 scheck.c | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/scheck.c b/scheck.c
index 07b15a0600e3..bb052d97996d 100644
--- a/scheck.c
+++ b/scheck.c
@@ -165,18 +165,16 @@ static void icmp(Btor *btor, struct instruction *insn)
 
 static void unop(Btor *btor, struct instruction *insn)
 {
-	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
-	BoolectorNode *t, *a;
+	pseudo_t src = insn->src;
+	BoolectorNode *t;
 
-	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;
+	case OP_SEXT:	t = sext(btor, insn, mkivar(btor, insn, src)); break;
+	case OP_ZEXT:	t = zext(btor, insn, mkivar(btor, insn, src)); break;
+	case OP_TRUNC:	t = slice(btor, insn, mkivar(btor, insn, src)); break;
+
+	case OP_NEG:	t = boolector_neg(btor, mktvar(btor, insn, src)); break;
+	case OP_NOT:	t = boolector_not(btor, mktvar(btor, insn, src)); break;
 	default:
 		fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 		return;
-- 
2.32.0