--- /dev/null	Fri Dec 21 15:00:16 2018
+++ new/usr/src/tools/smatch/src/smatch_constraints.c	Fri Dec 21 15:00:16 2018
@@ -0,0 +1,541 @@
+/*
+ * Copyright (C) 2017 Oracle.
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, see http://www.gnu.org/copyleft/gpl.txt
+ */
+
+/*
+ * Basically I see constraints as a way of saying "x <= some_limit".  The
+ * problem is that smatch_capped is not granullar enough.
+ *
+ * This is mostly for finding out of bounds errors.  So there are different
+ * types of constraints.  Quite often we have "foo->xxx[i] = 42;" and we want
+ * to verify that "i" is less than foo->size.
+ *
+ * My idea was that we could automatically figure out these constraints.  And we
+ * could load them in the DB so that they are the same every time.  As in a
+ * constraint could be "< (struct whatever)->size" and give that in ID that
+ * would be constant until you completely wiped the DB.  So when you do a normal
+ * DB rebuild then the first thing it will do is preserve all the constraints.
+ * I guess the reason to do it this way is to save space...  I sometimes suspect
+ * that worrying about saving space is premature optimization.
+ *
+ * The other thing that I want to do a little bit different here is how I merge
+ * constraints.  If a constraint is true on both sides, then that's normal.  If
+ * we merge constraint 23 and 67 then we get constraint 23|67.  If we merge 23
+ * with &undefined then we get &undefined.  We can also have two constraints
+ * that are both true so we could have (45&23)|12 which means either both 45 and
+ * 23 are true or 12 is true.
+ *
+ */
+
+
+#include "smatch.h"
+#include "smatch_extra.h"
+#include "smatch_slist.h"
+
+static int my_id;
+
+ALLOCATOR(constraint, "constraints");
+
+static void add_constraint(struct constraint_list **list, int op, int constraint)
+{
+	struct constraint *tmp, *new;
+
+	FOR_EACH_PTR(*list, tmp) {
+		if (tmp->id < constraint)
+			continue;
+		if (tmp->id == constraint) {
+			if (tmp->op == '<')
+				return;
+			if (op == SPECIAL_LTE)
+				return;
+
+			new = __alloc_constraint(0);
+			new->op = op;
+			new->id = constraint;
+			REPLACE_CURRENT_PTR(tmp, new);
+			return;
+		}
+
+		new = __alloc_constraint(0);
+		new->op = op;
+		new->id = constraint;
+		INSERT_CURRENT(new, tmp);
+		return;
+	} END_FOR_EACH_PTR(tmp);
+
+	new = __alloc_constraint(0);
+	new->op = op;
+	new->id = constraint;
+	add_ptr_list(list, new);
+}
+
+static struct constraint_list *merge_constraint_lists(struct constraint_list *one, struct constraint_list *two)
+{
+	struct constraint_list *ret = NULL;
+	struct constraint *tmp;
+
+	// FIXME: not || but &&
+	FOR_EACH_PTR(one, tmp) {
+		add_constraint(&ret, tmp->op, tmp->id);
+	} END_FOR_EACH_PTR(tmp);
+
+	FOR_EACH_PTR(two, tmp) {
+		add_constraint(&ret, tmp->op, tmp->id);
+	} END_FOR_EACH_PTR(tmp);
+
+	return ret;
+}
+
+static struct constraint_list *clone_constraint_list(struct constraint_list *list)
+{
+	struct constraint_list *ret = NULL;
+	struct constraint *tmp;
+
+	FOR_EACH_PTR(list, tmp) {
+		add_constraint(&ret, tmp->op, tmp->id);
+	} END_FOR_EACH_PTR(tmp);
+
+	return ret;
+}
+
+static struct smatch_state *alloc_constraint_state(struct constraint_list *list)
+{
+	struct smatch_state *state;
+	struct constraint *con;
+	static char buf[256];
+	int cnt = 0;
+
+	FOR_EACH_PTR(list, con) {
+		if (cnt != 0)
+			cnt += snprintf(buf + cnt, sizeof(buf) - cnt, ", ");
+		cnt += snprintf(buf + cnt, sizeof(buf) - cnt, "%s%d",
+				show_special(con->op), con->id);
+	} END_FOR_EACH_PTR(con);
+
+	state = __alloc_smatch_state(0);
+	state->name = alloc_string(buf);
+	state->data = list;
+	return state;
+}
+
+static struct smatch_state *merge_func(struct smatch_state *s1, struct smatch_state *s2)
+{
+	struct constraint_list *list;
+
+	// FIXME:  use the dead code below instead
+	if (strcmp(s1->name, s2->name) == 0)
+		return s1;
+	return &merged;
+
+	list = merge_constraint_lists(s1->data, s2->data);
+	return alloc_constraint_state(list);
+}
+
+static int negate_gt(int op)
+{
+	switch (op) {
+	case '>':
+	case SPECIAL_UNSIGNED_GT:
+	case SPECIAL_GTE:
+	case SPECIAL_UNSIGNED_GTE:
+		return negate_comparison(op);
+	}
+	return op;
+}
+
+static char *get_func_constraint(struct expression *expr)
+{
+	char buf[256];
+	char *name;
+
+	if (is_fake_call(expr))
+		return NULL;
+	name = expr_to_str(expr->fn);
+	if (!name)
+		return NULL;
+	snprintf(buf, sizeof(buf), "%s()", name);
+	free_string(name);
+	return alloc_string(buf);
+}
+
+static char *get_toplevel_name(struct expression *expr)
+{
+	struct symbol *sym;
+	char buf[256];
+
+	expr = strip_expr(expr);
+	if (expr->type != EXPR_SYMBOL || !expr->symbol || !expr->symbol->ident)
+		return NULL;
+
+	sym = expr->symbol;
+	if (!(sym->ctype.modifiers & MOD_TOPLEVEL))
+		return NULL;
+
+	if (sym->ctype.modifiers & MOD_STATIC)
+		snprintf(buf, sizeof(buf), "%s %s", get_base_file(), sym->ident->name);
+	else
+		snprintf(buf, sizeof(buf), "extern %s", sym->ident->name);
+
+	return alloc_string(buf);
+}
+
+char *get_constraint_str(struct expression *expr)
+{
+	char *name;
+
+	if (!expr)
+		return NULL;
+	if (expr->type == EXPR_CALL)
+		return get_func_constraint(expr);
+	if (expr->type == EXPR_BINOP)
+		return expr_to_str(expr);
+	name = get_toplevel_name(expr);
+	if (name)
+		return name;
+	return get_member_name(expr);
+}
+
+static int save_int_callback(void *_p, int argc, char **argv, char **azColName)
+{
+	int *p = _p;
+
+	*p = atoi(argv[0]);
+	return 0;
+}
+
+static int constraint_str_to_id(const char *str)
+{
+	int id = -1;
+
+	run_sql(save_int_callback, &id,
+		"select id from constraints where str = '%q'", str);
+
+	return id;
+}
+
+static int save_constraint_str(void *_str, int argc, char **argv, char **azColName)
+{
+	char **str = _str;
+
+	*str = alloc_string(argv[0]);
+	return 0;
+}
+
+static char *constraint_id_to_str(int id)
+{
+	char *str = NULL;
+
+	run_sql(save_constraint_str, &str,
+		"select str from constraints where id = '%d'", id);
+
+	return str;
+}
+
+static int save_op_callback(void *_p, int argc, char **argv, char **azColName)
+{
+	int *p = _p;
+
+	if (argv[0][0] == '<' && argv[0][1] == '=')
+		*p = SPECIAL_LTE;
+	else
+		*p = '<';
+	return 0;
+}
+
+static int save_str_callback(void *_p, int argc, char **argv, char **azColName)
+{
+	char **p = _p;
+
+	if (!*p) {
+		*p = alloc_string(argv[0]);
+	} else {
+		char buf[256];
+
+		snprintf(buf, sizeof(buf), "%s, %s", *p, argv[0]);
+		*p = alloc_string(buf);
+	}
+	return 0;
+}
+
+char *get_required_constraint(const char *data_str)
+{
+	char *required = NULL;
+
+	run_sql(save_str_callback, &required,
+		"select bound from constraints_required where data = '%q'", data_str);
+
+	return required;
+}
+
+static int get_required_op(char *data_str, char *con_str)
+{
+	int op = 0;
+
+	run_sql(save_op_callback, &op,
+		"select op from constraints_required where data = '%q' and bound = '%q'", data_str, con_str);
+
+	return op;
+}
+
+char *unmet_constraint(struct expression *data, struct expression *offset)
+{
+	struct smatch_state *state;
+	struct constraint_list *list;
+	struct constraint *con;
+	char *data_str;
+	char *required;
+	int req_op;
+
+	data_str = get_constraint_str(data);
+	if (!data_str)
+		return NULL;
+
+	required = get_required_constraint(data_str);
+	if (!required)
+		goto free_data;
+
+	state = get_state_expr(my_id, offset);
+	if (!state)
+		goto free_data;
+	list = state->data;
+
+	/* check the list of bounds on our index against the list that work */
+	FOR_EACH_PTR(list, con) {
+		char *con_str;
+
+		con_str = constraint_id_to_str(con->id);
+		if (!con_str) {
+			sm_msg("constraint %d not found", con->id);
+			continue;
+		}
+
+		req_op = get_required_op(data_str, con_str);
+		free_string(con_str);
+		if (!req_op)
+			continue;
+		if (con->op == '<' || con->op == req_op) {
+			free_string(required);
+			required = NULL;
+			goto free_data;
+		}
+	} END_FOR_EACH_PTR(con);
+
+free_data:
+	free_string(data_str);
+	return required;
+}
+
+struct string_list *saved_constraints;
+static void save_new_constraint(const char *con)
+{
+	if (list_has_string(saved_constraints, con))
+		return;
+	insert_string(&saved_constraints, con);
+	sql_save_constraint(con);
+}
+
+static void handle_comparison(struct expression *left, int op, struct expression *right)
+{
+	struct constraint_list *constraints;
+	struct smatch_state *state;
+	char *constraint;
+	int constraint_id;
+	int orig_op = op;
+	sval_t sval;
+
+	/* known values are handled in smatch extra */
+	if (get_value(left, &sval) || get_value(right, &sval))
+		return;
+
+	if (local_debug)
+		sm_msg("COMPARE: %s %s %s", expr_to_str(left), show_special(op), expr_to_str(right));
+
+	constraint = get_constraint_str(right);
+	if (!constraint)
+		return;
+	if (local_debug)
+		sm_msg("EXPR: %s CONSTRAINT %s", expr_to_str(right), constraint);
+	constraint_id = constraint_str_to_id(constraint);
+	if (local_debug)
+		sm_msg("CONSTRAINT ID %d", constraint_id);
+	if (constraint_id < 0)
+		save_new_constraint(constraint);
+	free_string(constraint);
+	if (constraint_id < 0)
+		return;
+
+	constraints = get_constraints(left);
+	constraints = clone_constraint_list(constraints);
+	op = negate_gt(orig_op);
+	add_constraint(&constraints, remove_unsigned_from_comparison(op), constraint_id);
+	state = alloc_constraint_state(constraints);
+
+	if (op == orig_op) {
+		if (local_debug)
+			sm_msg("SETTING %s true %s", expr_to_str(left), state->name);
+		set_true_false_states_expr(my_id, left,	state, NULL);
+	} else {
+		if (local_debug)
+			sm_msg("SETTING %s false %s", expr_to_str(left), state->name);
+
+		set_true_false_states_expr(my_id, left, NULL, state);
+	}
+}
+
+static void match_condition(struct expression *expr)
+{
+	if (expr->type != EXPR_COMPARE)
+		return;
+
+	if (expr->op == SPECIAL_EQUAL ||
+	    expr->op == SPECIAL_NOTEQUAL)
+		return;
+
+	handle_comparison(expr->left, expr->op, expr->right);
+	handle_comparison(expr->right, flip_comparison(expr->op), expr->left);
+}
+
+struct constraint_list *get_constraints(struct expression *expr)
+{
+	struct smatch_state *state;
+
+	state = get_state_expr(my_id, expr);
+	if (!state)
+		return NULL;
+	return state->data;
+}
+
+static void match_caller_info(struct expression *expr)
+{
+	struct expression *tmp;
+	struct smatch_state *state;
+	int i;
+
+	i = -1;
+	FOR_EACH_PTR(expr->args, tmp) {
+		i++;
+		state = get_state_expr(my_id, tmp);
+		if (!state || state == &merged || state == &undefined)
+			continue;
+		sql_insert_caller_info(expr, CONSTRAINT, i, "$", state->name);
+	} END_FOR_EACH_PTR(tmp);
+}
+
+static void struct_member_callback(struct expression *call, int param, char *printed_name, struct sm_state *sm)
+{
+	if (sm->state == &merged || sm->state == &undefined)
+		return;
+	sql_insert_caller_info(call, CONSTRAINT, param, printed_name, sm->state->name);
+}
+
+static struct smatch_state *constraint_str_to_state(char *value)
+{
+	struct constraint_list *list = NULL;
+	char *p = value;
+	int op;
+	long long id;
+
+	while (true) {
+		op = '<';
+		if (*p != '<')
+			return &undefined;
+		p++;
+		if (*p == '=') {
+			op = SPECIAL_LTE;
+			p++;
+		}
+		id = strtoll(p, &p, 10);
+		add_constraint(&list, op, id);
+		if (*p != ',')
+			break;
+		p++;
+		if (*p != ' ')
+			return &undefined;
+	}
+
+	return alloc_constraint_state(list);
+}
+
+static void set_param_constrained(const char *name, struct symbol *sym, char *key, char *value)
+{
+	char fullname[256];
+
+	if (strcmp(key, "*$") == 0)
+		snprintf(fullname, sizeof(fullname), "*%s", name);
+	else if (strncmp(key, "$", 1) == 0)
+		snprintf(fullname, 256, "%s%s", name, key + 1);
+	else
+		return;
+
+	set_state(my_id, name, sym, constraint_str_to_state(value));
+}
+
+static void print_return_implies_constrained(int return_id, char *return_ranges, struct expression *expr)
+{
+	struct smatch_state *orig;
+	struct sm_state *sm;
+	const char *param_name;
+	int param;
+
+	FOR_EACH_MY_SM(my_id, __get_cur_stree(), sm) {
+		if (sm->state == &merged || sm->state == &undefined)
+			continue;
+
+		param = get_param_num_from_sym(sm->sym);
+		if (param < 0)
+			continue;
+
+		orig = get_state_stree(get_start_states(), my_id, sm->name, sm->sym);
+		if (orig && strcmp(sm->state->name, orig->name) == 0)
+			continue;
+
+		param_name = get_param_name(sm);
+		if (!param_name)
+			continue;
+
+		sql_insert_return_states(return_id, return_ranges, CONSTRAINT,
+					 param, param_name, sm->state->name);
+	} END_FOR_EACH_SM(sm);
+}
+
+static void db_returns_constrained(struct expression *expr, int param, char *key, char *value)
+{
+	char *name;
+	struct symbol *sym;
+
+	name = return_state_to_var_sym(expr, param, key, &sym);
+	if (!name || !sym)
+		goto free;
+
+	set_state(my_id, name, sym, constraint_str_to_state(value));
+free:
+	free_string(name);
+}
+
+void register_constraints(int id)
+{
+	my_id = id;
+
+	add_merge_hook(my_id, &merge_func);
+	add_hook(&match_condition, CONDITION_HOOK);
+
+	add_hook(&match_caller_info, FUNCTION_CALL_HOOK);
+	add_member_info_callback(my_id, struct_member_callback);
+	select_caller_info_hook(&set_param_constrained, CONSTRAINT);
+
+	add_split_return_callback(print_return_implies_constrained);
+	select_return_states_hook(CONSTRAINT, &db_returns_constrained);
+}
