From 0887a8215c6e1a13107458d101119dda60d84a2b Mon Sep 17 00:00:00 2001
From: Dan Carpenter <dan.carpenter@oracle.com>
Date: Fri, 25 Nov 2016 23:05:25 +0300
Subject: [PATCH] implied: fix a bug with borrowed implications

This bug was, of course, found parsing real code.  Then I built
sm_implied19.c as a test case.  Originally, it printed that "vbus"
was 0.  After this patch is applied it prints that "vbus" is s32min-s32max.

I'm 80% sure that this fix is the correct approach.

This bug has to do with borrowed implications.  When we merge an sm_state
then we get ->left and ->right pointers.  Then when we assign an int to
an int, for example "a = b;"  we want to preserve that history so we can
figure out the implications of "if (a == 42) "later using the merge
history of b.  So when you look at the ->left and ->right pointers the
variable can actually be different than the variable you started out with.

Pools are a collection of states before a merge.  They are linked by ->left
and ->right sm_states which have a ->pool pointer.  When we start out the
->left and ->right states have the same estate ->state as they do in the
pool that they point to.  But later, when we're figuring out the implications
of stuff we start mangling the ->left and ->right pointers so now they
might be a subset of the estate in the pool.

The problem here (I think) is that we're mangling borrowed states.  And the
fix for that is to clone the sm_states before mangling them so we don't
affect the other users.  I also changed the ->name and ->sym because why
not?

I wish that I were more certain of this fix but it definitely fixes my test
case.

Signed-off-by: Dan Carpenter <dan.carpenter@oracle.com>
---
 smatch_implied.c          | 10 ++++++++++
 validation/sm_implied19.c | 34 ++++++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+)
 create mode 100644 validation/sm_implied19.c

diff --git a/smatch_implied.c b/smatch_implied.c
index 7630443b..fbb744ce 100644
--- a/smatch_implied.c
+++ b/smatch_implied.c
@@ -469,6 +469,16 @@ struct sm_state *filter_pools(struct sm_state *sm,
 		ret->left = left;
 		ret->right = NULL;
 	} else {
+		if (left->sym != sm->sym || strcmp(left->name, sm->name) != 0) {
+			left = clone_sm(left);
+			left->sym = sm->sym;
+			left->name = sm->name;
+		}
+		if (right->sym != sm->sym || strcmp(right->name, sm->name) != 0) {
+			right = clone_sm(right);
+			right->sym = sm->sym;
+			right->name = sm->name;
+		}
 		ret = merge_sm_states(left, right);
 	}
 
diff --git a/validation/sm_implied19.c b/validation/sm_implied19.c
new file mode 100644
index 00000000..e65487bc
--- /dev/null
+++ b/validation/sm_implied19.c
@@ -0,0 +1,34 @@
+#include "check_debug.h"
+
+int xxx, yyy;
+int aaa, bbb;
+int id, vbus;
+void frob(void)
+{
+	if (xxx)
+		id = yyy;
+	else
+		id = 1;
+
+	if (aaa)
+		vbus = bbb;
+	else
+		vbus = id;
+
+	if (id)
+		;
+	if (!vbus)
+		;
+
+	if (!id)
+		__smatch_implied(vbus);
+}
+
+/*
+ * check-name: smatch implied #19
+ * check-command: smatch -I.. sm_implied19.c
+ *
+ * check-output-start
+sm_implied19.c:24 frob() implied: vbus = 's32min-s32max'
+ * check-output-end
+ */
-- 
2.11.4.GIT