/*
 * 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;

        expr = strip_expr(expr);
        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 (!insert_string(&saved_constraints, con))
                return;
        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;

        constraint = get_constraint_str(right);
        if (!constraint)
                return;
        constraint_id = constraint_str_to_id(constraint);
        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)
                set_true_false_states_expr(my_id, left, state, NULL);
        else
                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;

        set_dynamic_states(my_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);
}