diff options
| -rw-r--r-- | .gitignore | 35 | ||||
| -rw-r--r-- | Documentation/TODO.md | 11 | ||||
| -rw-r--r-- | Makefile | 7 | ||||
| -rw-r--r-- | builtin.c | 65 | ||||
| -rw-r--r-- | builtin.h | 4 | ||||
| -rw-r--r-- | ident-list.h | 6 | ||||
| -rw-r--r-- | linearize.c | 3 | ||||
| -rw-r--r-- | parse.c | 2 | ||||
| -rw-r--r-- | scheck.c | 362 | ||||
| -rw-r--r-- | simplify.c | 98 | ||||
| -rw-r--r-- | validation/knr-attr-crash.c | 12 | ||||
| -rw-r--r-- | validation/optim/cmpe-and0.c | 10 | ||||
| -rw-r--r-- | validation/optim/cmpe-or0.c | 10 | ||||
| -rw-r--r-- | validation/optim/cmps-and0.c | 21 | ||||
| -rw-r--r-- | validation/optim/cmps-minmax.c | 8 | ||||
| -rw-r--r-- | validation/optim/cmps-or0.c | 21 | ||||
| -rw-r--r-- | validation/optim/cmps0-and0.c | 12 | ||||
| -rw-r--r-- | validation/optim/cmpu-and0.c | 17 | ||||
| -rw-r--r-- | validation/optim/cmpu-or0.c | 18 | ||||
| -rw-r--r-- | validation/scheck/ko.c | 10 | ||||
| -rw-r--r-- | validation/scheck/ok.c | 22 | ||||
| -rwxr-xr-x | validation/test-suite | 17 |
22 files changed, 747 insertions, 24 deletions
@@ -8,25 +8,26 @@ .*.swp # generated -version.h +/version.h # programs -c2xml -compile -ctags -example -graph -obfuscate -sparse -sparse-llvm -semind -test-dissect -test-inspect -test-lexing -test-linearize -test-parsing -test-show-type -test-unssa +/c2xml +/compile +/ctags +/example +/graph +/obfuscate +/scheck +/semind +/sparse +/sparse-llvm +/test-dissect +/test-inspect +/test-lexing +/test-linearize +/test-parsing +/test-show-type +/test-unssa # tags tags diff --git a/Documentation/TODO.md b/Documentation/TODO.md index 3f00bb11..a2763895 100644 --- a/Documentation/TODO.md +++ b/Documentation/TODO.md @@ -56,6 +56,17 @@ Optimization IR -- +* pseudos are untyped, it's usually OK but often it complicates things: + + - PSEUDO_REGs are defined by instructions and their type is normally + retrievable via this defining instruction but in some cases they're not: + for example, pseudos defined by ASM output. + - PSEUDO_ARGs are considered as defined by OP_ENTRY and are used like + this for liveness trackability but their type can't simply be + retrieved via this instruction like PSEUDO_REGs are (with ->def->type). + - PSEUDO_VALs are completely typeless. + + Maybe a few bits should be used to store some kind of low-level type. * OP_SET should return a bool, always * add IR instructions for va_arg() & friends * add a possibility to import of file in "IR assembly" @@ -226,6 +226,13 @@ else $(warning Your system does not have llvm, disabling sparse-llvm) endif +ifeq ($(HAVE_BOOLECTOR),yes) +PROGRAMS += scheck +scheck-cflags := -I${BOOLECTORDIR}/include/boolector +scheck-ldflags := -L${BOOLECTORDIR}/lib +scheck-ldlibs := -lboolector -llgl -lbtor2parser +endif + ######################################################################## LIBS := libsparse.a OBJS := $(LIB_OBJS) $(EXTRA_OBJS) $(PROGRAMS:%=%.o) @@ -390,6 +390,69 @@ static struct symbol_op overflow_p_op = { }; +/// +// Evaluate the arguments of 'generic' integer operators. +// +// Parameters with a complete type are used like in a normal prototype. +// The first parameter with a 'dynamic' type will be consider +// as polymorphic and for each calls will be instancied with the type +// of its effective argument. +// The next dynamic parameters will the use this polymorphic type. +// This allows to declare functions with some parameters having +// a type variably defined at call time: +// int foo(int, T, T); +static int evaluate_generic_int_op(struct expression *expr) +{ + struct symbol *fntype = expr->fn->ctype->ctype.base_type; + struct symbol_list *types = NULL; + struct symbol *ctype = NULL; + struct expression *arg; + struct symbol *t; + int n = 0; + + PREPARE_PTR_LIST(fntype->arguments, t); + FOR_EACH_PTR(expr->args, arg) { + n++; + + if (!is_dynamic_type(t)) { + ; + } else if (!ctype) { + // first 'dynamic' type, check that it's an integer + t = arg->ctype; + if (!t) + return 0; + if (t->type == SYM_NODE) + t = t->ctype.base_type; + if (!t) + return 0; + if (t->ctype.base_type != &int_type) + goto err; + + // next 'dynamic' arguments will use this type + ctype = t; + } else { + // use the previous 'dynamic' type + t = ctype; + } + add_ptr_list(&types, t); + NEXT_PTR_LIST(t); + } END_FOR_EACH_PTR(arg); + FINISH_PTR_LIST(t); + return evaluate_arguments(types, expr->args); + +err: + sparse_error(arg->pos, "non-integer type for argument %d:", n); + info(arg->pos, " %s", show_typename(arg->ctype)); + expr->ctype = &bad_ctype; + return 0; +} + +struct symbol_op generic_int_op = { + .args = args_prototype, + .evaluate = evaluate_generic_int_op, +}; + + static int eval_atomic_common(struct expression *expr) { struct symbol *fntype = expr->fn->ctype->ctype.base_type; @@ -559,7 +622,7 @@ static void declare_builtin(int stream, const struct builtin_fn *entry) } } -static void declare_builtins(int stream, const struct builtin_fn tbl[]) +void declare_builtins(int stream, const struct builtin_fn tbl[]) { if (!tbl) return; @@ -12,4 +12,8 @@ struct builtin_fn { struct symbol_op *op; }; +void declare_builtins(int stream, const struct builtin_fn tbl[]); + +extern struct symbol_op generic_int_op; + #endif diff --git a/ident-list.h b/ident-list.h index 8049b694..3c08e8ca 100644 --- a/ident-list.h +++ b/ident-list.h @@ -78,6 +78,12 @@ IDENT(memset); IDENT(memcpy); IDENT(copy_to_user); IDENT(copy_from_user); IDENT(main); +/* used by the symbolic checker */ +IDENT(__assume); +IDENT(__assert); +IDENT(__assert_eq); +IDENT(__assert_const); + #undef __IDENT #undef IDENT #undef IDENT_RESERVED diff --git a/linearize.c b/linearize.c index 7248fa56..cf87545c 100644 --- a/linearize.c +++ b/linearize.c @@ -1533,7 +1533,7 @@ static pseudo_t linearize_assignment(struct entrypoint *ep, struct expression *e static pseudo_t linearize_call_expression(struct entrypoint *ep, struct expression *expr) { struct expression *arg, *fn; - struct instruction *insn = alloc_typed_instruction(OP_CALL, expr->ctype); + struct instruction *insn; pseudo_t retval, call; struct ctype *ctype = NULL; struct symbol *fntype; @@ -1554,6 +1554,7 @@ static pseudo_t linearize_call_expression(struct entrypoint *ep, struct expressi ctype = &fntype->ctype; + insn = alloc_typed_instruction(OP_CALL, expr->ctype); add_symbol(&insn->fntypes, fntype); FOR_EACH_PTR(expr->args, arg) { pseudo_t new = linearize_expression(ep, arg); @@ -1653,7 +1653,7 @@ static bool match_attribute(struct token *token) if (token_type(token) != TOKEN_IDENT) return false; sym = lookup_keyword(token->ident, NS_TYPEDEF); - if (!sym) + if (!sym || !sym->op) return false; return sym->op->type & KW_ATTRIBUTE; } diff --git a/scheck.c b/scheck.c new file mode 100644 index 00000000..754fe76f --- /dev/null +++ b/scheck.c @@ -0,0 +1,362 @@ +// SPDX-License-Identifier: MIT +// Copyright (C) 2021 Luc Van Oostenryck + +/// +// Symbolic checker for Sparse's IR +// -------------------------------- +// +// This is an example client program with a dual purpose: +// # It shows how to translate Sparse's IR into the language +// of SMT solvers (only the part concerning integers, +// floating-point and memory is ignored). +// # It's used as a simple symbolic checker for the IR. +// The idea is to create a mini-language that allows to +// express some assertions with some pre-conditions. + +#include <stdarg.h> +#include <stdlib.h> +#include <stdio.h> +#include <string.h> +#include <ctype.h> +#include <unistd.h> +#include <fcntl.h> + +#include <boolector.h> +#include "lib.h" +#include "expression.h" +#include "linearize.h" +#include "symbol.h" +#include "builtin.h" + + +#define dyntype incomplete_ctype +static const struct builtin_fn builtins_scheck[] = { + { "__assume", &void_ctype, 0, { &dyntype }, .op = &generic_int_op }, + { "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op }, + { "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op }, + { "__assert_const", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op }, + {} +}; + + +static BoolectorSort get_sort(Btor *btor, struct symbol *type, struct position pos) +{ + if (!is_int_type(type)) { + sparse_error(pos, "invalid type"); + return NULL; + } + return boolector_bitvec_sort(btor, type->bit_size); +} + +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: + n = boolector_var(btor, s, show_pseudo(pseudo)); + break; + default: + fprintf(stderr, "invalid pseudo: %s\n", show_pseudo(pseudo)); + return NULL; + } + return pseudo->priv = n; +} + +static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx) +{ + pseudo_t arg = ptr_list_nth(insn->arguments, idx); + struct symbol *type = ptr_list_nth(insn->fntypes, idx + 1); + BoolectorSort s = get_sort(btor, type, insn->pos); + + return mkvar(btor, s, arg); +} + +static BoolectorNode *zext(Btor *btor, struct instruction *insn, BoolectorNode *s) +{ + int old = boolector_get_width(btor, s); + int new = insn->type->bit_size; + return boolector_uext(btor, s, new - old); +} + +static BoolectorNode *sext(Btor *btor, struct instruction *insn, BoolectorNode *s) +{ + int old = boolector_get_width(btor, s); + int new = insn->type->bit_size; + return boolector_sext(btor, s, new - old); +} + +static BoolectorNode *slice(Btor *btor, struct instruction *insn, BoolectorNode *s) +{ + int old = boolector_get_width(btor, s); + int new = insn->type->bit_size; + return boolector_slice(btor, s, old - new - 1, 0); +} + +static void binary(Btor *btor, BoolectorSort s, struct instruction *insn) +{ + BoolectorNode *t, *a, *b; + + a = mkvar(btor, s, insn->src1); + b = mkvar(btor, s, insn->src2); + if (!a || !b) + return; + switch (insn->opcode) { + case OP_ADD: t = boolector_add(btor, a, b); break; + case OP_SUB: t = boolector_sub(btor, a, b); break; + case OP_MUL: t = boolector_mul(btor, a, b); break; + case OP_AND: t = boolector_and(btor, a, b); break; + case OP_OR: t = boolector_or (btor, a, b); break; + case OP_XOR: t = boolector_xor(btor, a, b); break; + case OP_SHL: t = boolector_sll(btor, a, b); break; + case OP_LSR: t = boolector_srl(btor, a, b); break; + case OP_ASR: t = boolector_sra(btor, a, b); break; + case OP_DIVS: t = boolector_sdiv(btor, a, b); break; + case OP_DIVU: t = boolector_udiv(btor, a, b); break; + case OP_MODS: t = boolector_srem(btor, a, b); break; + case OP_MODU: t = boolector_urem(btor, a, b); break; + case OP_SET_EQ: t = zext(btor, insn, boolector_eq(btor, a, b)); break; + case OP_SET_NE: t = zext(btor, insn, boolector_ne(btor, a, b)); break; + case OP_SET_LT: t = zext(btor, insn, boolector_slt(btor, a, b)); break; + case OP_SET_LE: t = zext(btor, insn, boolector_slte(btor, a, b)); break; + case OP_SET_GE: t = zext(btor, insn, boolector_sgte(btor, a, b)); break; + case OP_SET_GT: t = zext(btor, insn, boolector_sgt(btor, a, b)); break; + case OP_SET_B: t = zext(btor, insn, boolector_ult(btor, a, b)); break; + case OP_SET_BE: t = zext(btor, insn, boolector_ulte(btor, a, b)); break; + 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"); + return; + } + insn->target->priv = t; +} + +static void binop(Btor *btor, struct instruction *insn) +{ + BoolectorSort s = get_sort(btor, insn->type, insn->pos); + binary(btor, s, insn); +} + +static void icmp(Btor *btor, struct instruction *insn) +{ + BoolectorSort s = get_sort(btor, insn->itype, insn->pos); + binary(btor, s, insn); +} + +static void unop(Btor *btor, struct instruction *insn) +{ + BoolectorSort s = get_sort(btor, insn->type, insn->pos); + BoolectorNode *t, *a; + + 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; + default: + fprintf(stderr, "unsupported insn\n"); + return; + } + insn->target->priv = t; +} + +static void ternop(Btor *btor, struct instruction *insn) +{ + BoolectorSort s = get_sort(btor, insn->type, insn->pos); + BoolectorNode *t, *a, *b, *c, *z, *d; + + a = mkvar(btor, s, insn->src1); + b = mkvar(btor, s, insn->src2); + c = mkvar(btor, s, insn->src3); + if (!a || !b || !c) + return; + switch (insn->opcode) { + case OP_SEL: + z = boolector_zero(btor, s); + d = boolector_ne(btor, a, z); + t = boolector_cond(btor, d, b, c); + break; + default: + fprintf(stderr, "unsupported insn\n"); + return; + } + insn->target->priv = t; +} + +static bool add_precondition(Btor *btor, BoolectorNode **pre, struct instruction *insn) +{ + BoolectorNode *a = get_arg(btor, insn, 0); + BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a)); + BoolectorNode *n = boolector_ne(btor, a, z); + BoolectorNode *p = boolector_and(btor, *pre, n); + *pre = p; + return true; +} + +static bool check_btor(Btor *btor, BoolectorNode *p, BoolectorNode *n, struct instruction *insn) +{ + char model_format[] = "btor"; + int res; + + n = boolector_implies(btor, p, n); + boolector_assert(btor, boolector_not(btor, n)); + res = boolector_sat(btor); + switch (res) { + case BOOLECTOR_UNSAT: + return 1; + case BOOLECTOR_SAT: + sparse_error(insn->pos, "assertion failed"); + show_entry(insn->bb->ep); + boolector_dump_btor(btor, stdout); + boolector_print_model(btor, model_format, stdout); + break; + default: + sparse_error(insn->pos, "SMT failure"); + break; + } + return 0; +} + +static bool check_assert(Btor *btor, BoolectorNode *pre, struct instruction *insn) +{ + BoolectorNode *a = get_arg(btor, insn, 0); + BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a)); + BoolectorNode *n = boolector_ne(btor, a, z); + return check_btor(btor, pre, n, insn); +} + +static bool check_equal(Btor *btor, BoolectorNode *pre, struct instruction *insn) +{ + BoolectorNode *a = get_arg(btor, insn, 0); + BoolectorNode *b = get_arg(btor, insn, 1); + BoolectorNode *n = boolector_eq(btor, a, b); + return check_btor(btor, pre, n, insn); +} + +static bool check_const(Btor *ctxt, struct instruction *insn) +{ + pseudo_t src1 = ptr_list_nth(insn->arguments, 0); + pseudo_t src2 = ptr_list_nth(insn->arguments, 1); + + if (src2->type != PSEUDO_VAL) + sparse_error(insn->pos, "should be a constant: %s", show_pseudo(src2)); + if (src1 == src2) + return 1; + if (src1->type != PSEUDO_VAL) + sparse_error(insn->pos, "not a constant: %s", show_pseudo(src1)); + else + sparse_error(insn->pos, "invalid value: %s != %s", show_pseudo(src1), show_pseudo(src2)); + return 0; +} + +static bool check_call(Btor *btor, BoolectorNode **pre, struct instruction *insn) +{ + pseudo_t func = insn->func; + struct ident *ident = func->ident; + + if (ident == &__assume_ident) + return add_precondition(btor, pre, insn); + if (ident == &__assert_ident) + return check_assert(btor, *pre, insn); + if (ident == &__assert_eq_ident) + return check_equal(btor, *pre, insn); + if (ident == &__assert_const_ident) + return check_const(btor, insn); + return 0; +} + +static bool check_function(struct entrypoint *ep) +{ + Btor *btor = boolector_new(); + BoolectorNode *pre = boolector_true(btor); + struct basic_block *bb; + int rc = 0; + + boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1); + boolector_set_opt(btor, BTOR_OPT_INCREMENTAL, 1); + + FOR_EACH_PTR(ep->bbs, bb) { + struct instruction *insn; + FOR_EACH_PTR(bb->insns, insn) { + if (!insn->bb) + continue; + switch (insn->opcode) { + case OP_ENTRY: + continue; + case OP_BINARY ... OP_BINARY_END: + binop(btor, insn); + break; + case OP_BINCMP ... OP_BINCMP_END: + icmp(btor, insn); + break; + case OP_UNOP ... OP_UNOP_END: + unop(btor, insn); + break; + case OP_SEL: + ternop(btor, insn); + break; + case OP_CALL: + rc &= check_call(btor, &pre, insn); + break; + case OP_RET: + goto out; + default: + fprintf(stderr, "unsupported insn\n"); + goto out; + } + } END_FOR_EACH_PTR(insn); + } END_FOR_EACH_PTR(bb); + fprintf(stderr, "unterminated function\n"); + +out: + boolector_release_all(btor); + boolector_delete(btor); + return rc; +} + +static void check_functions(struct symbol_list *list) +{ + struct symbol *sym; + + FOR_EACH_PTR(list, sym) { + struct entrypoint *ep; + + expand_symbol(sym); + ep = linearize_symbol(sym); + if (!ep || !ep->entry) + continue; + check_function(ep); + } END_FOR_EACH_PTR(sym); +} + +int main(int argc, char **argv) +{ + struct string_list *filelist = NULL; + char *file; + + Wdecl = 0; + + sparse_initialize(argc, argv, &filelist); + + declare_builtins(0, builtins_scheck); + predefine_strong("__SYMBOLIC_CHECKER__"); + + // Expand, linearize and check. + FOR_EACH_PTR(filelist, file) { + check_functions(sparse(file)); + } END_FOR_EACH_PTR(file); + return 0; +} @@ -1258,6 +1258,104 @@ static int simplify_compare_constant(struct instruction *insn, long long value) src2 = insn->src2; value = src2->value; switch (DEF_OPCODE(def, src1)) { + case OP_AND: + if (!constant(def->src2)) + break; + bits = def->src2->value; + switch (insn->opcode) { + case OP_SET_EQ: + if ((value & bits) != value) + return replace_with_value(insn, 0); + break; + case OP_SET_NE: + if ((value & bits) != value) + return replace_with_value(insn, 1); + break; + case OP_SET_LE: + value = sign_extend(value, def->size); + if (bits & sign_bit(def->size)) + break; + if (value < 0) + return replace_with_value(insn, 0); + if (value >= (long long)bits) + return replace_with_value(insn, 1); + if (value == 0) + return replace_opcode(insn, OP_SET_EQ); + break; + case OP_SET_GT: + value = sign_extend(value, def->size); + if (bits & sign_bit(def->size)) + break; + if (value < 0) + return replace_with_value(insn, 1); + if (value >= (long long)bits) + return replace_with_value(insn, 0); + if (value == 0) + return replace_opcode(insn, OP_SET_NE); + break; + case OP_SET_B: + if (value > bits) + return replace_with_value(insn, 1); + break; + case OP_SET_BE: + if (value >= bits) + return replace_with_value(insn, 1); + break; + case OP_SET_AE: + if (value > bits) + return replace_with_value(insn, 0); + break; + case OP_SET_A: + if (value >= bits) + return replace_with_value(insn, 0); + break; + } + break; + case OP_OR: + if (!constant(def->src2)) + break; + bits = def->src2->value; + switch (insn->opcode) { + case OP_SET_EQ: + if ((value & bits) != bits) + return replace_with_value(insn, 0); + break; + case OP_SET_NE: + if ((value & bits) != bits) + return replace_with_value(insn, 1); + break; + case OP_SET_B: + if (bits >= value) + return replace_with_value(insn, 0); + break; + case OP_SET_BE: + if (bits > value) + return replace_with_value(insn, 0); + break; + case OP_SET_AE: + if (bits > value) + return replace_with_value(insn, 1); + break; + case OP_SET_A: + if (bits >= value) + return replace_with_value(insn, 1); + break; + case OP_SET_LE: + value = sign_extend(value, def->size); + if (bits & sign_bit(def->size)) { + if (value >= -1) + return replace_with_value(insn, 1); + } + break; + case OP_SET_GT: + value = sign_extend(value, def->size); + if (bits & sign_bit(def->size)) { + if (value >= -1) + return replace_with_value(insn, 0); + } + break; + } + break; case OP_SEXT: // sext(x) cmp C --> x cmp trunc(C) osize = def->orig_type->bit_size; if (is_signed_constant(value, osize, size)) { diff --git a/validation/knr-attr-crash.c b/validation/knr-attr-crash.c new file mode 100644 index 00000000..176ff503 --- /dev/null +++ b/validation/knr-attr-crash.c @@ -0,0 +1,12 @@ +typedef int word; + +void foo(word x); + +void foo(x) + word x; +{ } + +/* + * check-name: knr-attr-crash + * check-command: sparse -Wno-old-style-definition $file + */ diff --git a/validation/optim/cmpe-and0.c b/validation/optim/cmpe-and0.c new file mode 100644 index 00000000..75af7752 --- /dev/null +++ b/validation/optim/cmpe-and0.c @@ -0,0 +1,10 @@ +int cmpe_and_eq(int a) { return ((a & 0xff00) == 0xff01) + 1; } +int cmpe_and_ne(int a) { return ((a & 0xff00) != 0xff01) + 0; } + +/* + * check-name: cmpe-and0 + * check-command: test-linearize -Wno-decl $file + * + * check-output-ignore + * check-output-returns: 1 + */ diff --git a/validation/optim/cmpe-or0.c b/validation/optim/cmpe-or0.c new file mode 100644 index 00000000..2e89d611 --- /dev/null +++ b/validation/optim/cmpe-or0.c @@ -0,0 +1,10 @@ +int cmp_eq(int a) { return ((a | 1) != 0) + 0; } +int cmp_ne(int a) { return ((a | 1) == 0) + 1; } + +/* + * check-name: cmpe-or0 + * check-command: test-linearize -Wno-decl $file + * + * check-output-ignore + * check-output-returns: 1 + */ diff --git a/validation/optim/cmps-and0.c b/validation/optim/cmps-and0.c new file mode 100644 index 00000000..962fbd2d --- /dev/null +++ b/validation/optim/cmps-and0.c @@ -0,0 +1,21 @@ +#define MINUS_ONE -1 +#define MASK 32 + + +int cmps_and_lt_lt0(int a) { return ((a & MASK) < MINUS_ONE) + 1; } +int cmps_and_lt_gtm(int a) { return ((a & MASK) < (MASK + 1)) + 0; } +int cmps_and_le_lt0(int a) { return ((a & MASK) <= MINUS_ONE) + 1; } +int cmps_and_le_gtm(int a) { return ((a & MASK) <= (MASK + 1)) + 0; } + +int cmps_and_gt_lt0(int a) { return ((a & MASK) > MINUS_ONE) + 0; } +int cmps_and_gt_gtm(int a) { return ((a & MASK) > (MASK + 1)) + 1; } +int cmps_and_ge_lt0(int a) { return ((a & MASK) >= MINUS_ONE) + 0; } +int cmps_and_ge_gtm(int a) { return ((a & MASK) >= (MASK + 1)) + 1; } + +/* + * check-name: cmps-and0 + * check-command: test-linearize -Wno-decl $file + * + * check-output-ignore + * check-output-returns: 1 + */ diff --git a/validation/optim/cmps-minmax.c b/validation/optim/cmps-minmax.c index 5802cdbc..0b1a0a09 100644 --- a/validation/optim/cmps-minmax.c +++ b/validation/optim/cmps-minmax.c @@ -1,11 +1,11 @@ #define SMAX __INT_MAX__ #define SMIN (-__INT_MAX__-1) -int lt_smin(int a) { return (a < SMIN) == 0; } -int le_smax(int a) { return (a <= SMAX) == 1; } +int lt_smin(int a) { return (a < SMIN) + 1; } +int le_smax(int a) { return (a <= SMAX) + 0; } -int ge_smin(int a) { return (a >= SMIN) == 1; } -int gt_smax(int a) { return (a > SMAX) == 0; } +int ge_smin(int a) { return (a >= SMIN) + 0; } +int gt_smax(int a) { return (a > SMAX) + 1; } /* * check-name: cmps-minmax diff --git a/validation/optim/cmps-or0.c b/validation/optim/cmps-or0.c new file mode 100644 index 00000000..70fcb024 --- /dev/null +++ b/validation/optim/cmps-or0.c @@ -0,0 +1,21 @@ +#define EQ(X) + (X == 0) +#define SIGN (1 << 31) +#define MASK (SIGN | 32) + + +int cmps_ior_lt_x(int a) { return ((a | MASK) < 4) EQ(1); } +int cmps_ior_lt_0(int a) { return ((a | MASK) < 0) EQ(1); } +int cmps_ior_le_x(int a) { return ((a | MASK) <= 4) EQ(1); } +int cmps_ior_le_0(int a) { return ((a | MASK) <= 0) EQ(1); } +int cmps_ior_ge_x(int a) { return ((a | MASK) >= 4) EQ(0); } +int cmps_ior_ge_0(int a) { return ((a | MASK) >= 0) EQ(0); } +int cmps_ior_gt_x(int a) { return ((a | MASK) > 4) EQ(0); } +int cmps_ior_gt_0(int a) { return ((a | MASK) > 0) EQ(0); } + +/* + * check-name: cmps-or0 + * check-command: test-linearize -Wno-decl $file + * + * check-output-ignore + * check-output-returns: 1 + */ diff --git a/validation/optim/cmps0-and0.c b/validation/optim/cmps0-and0.c new file mode 100644 index 00000000..8316916a --- /dev/null +++ b/validation/optim/cmps0-and0.c @@ -0,0 +1,12 @@ +#define M 32 + +int cmps_and_sle0(int a) { return ((a & M) <= 0) == ((a & M) == 0); } +int cmps_and_sgt0(int a) { return ((a & M) > 0) == ((a & M) != 0); } + +/* + * check-name: cmps0-and + * check-command: test-linearize -Wno-decl $file + * + * check-output-ignore + * check-output-returns: 1 + */ diff --git a/validation/optim/cmpu-and0.c b/validation/optim/cmpu-and0.c new file mode 100644 index 00000000..927b9fb6 --- /dev/null +++ b/validation/optim/cmpu-and0.c @@ -0,0 +1,17 @@ +#define MASK 32U + + +int cmps_and_ltu_gt(int a) { return ((a & MASK) < (MASK + 1)) + 0; } +int cmps_and_leu_gt(int a) { return ((a & MASK) <= (MASK + 1)) + 0; } +int cmps_and_leu_eq(int a) { return ((a & MASK) <= (MASK + 0)) + 0; } +int cmps_and_geu_gt(int a) { return ((a & MASK) >= (MASK + 1)) + 1; } +int cmps_and_gtu_gt(int a) { return ((a & MASK) > (MASK + 1)) + 1; } +int cmps_and_gtu_eq(int a) { return ((a & MASK) > (MASK + 0)) + 1; } + +/* + * check-name: cmpu-and0 + * check-command: test-linearize -Wno-decl $file + * + * check-output-ignore + * check-output-returns: 1 + */ diff --git a/validation/optim/cmpu-or0.c b/validation/optim/cmpu-or0.c new file mode 100644 index 00000000..e97e9180 --- /dev/null +++ b/validation/optim/cmpu-or0.c @@ -0,0 +1,18 @@ +#define EQ(X) + (X == 0) +#define MASK 32U + + +int cmpu_ior_lt_lt(int a) { return ((a | MASK) < (MASK - 1)) EQ(0); } +int cmpu_ior_lt_eq(int a) { return ((a | MASK) < (MASK )) EQ(0); } +int cmpu_ior_le_lt(int a) { return ((a | MASK) <= (MASK - 1)) EQ(0); } +int cmpu_ior_ge_lt(int a) { return ((a | MASK) >= (MASK - 1)) EQ(1); } +int cmpu_ior_ge_eq(int a) { return ((a | MASK) >= (MASK )) EQ(1); } +int cmpu_ior_gt_lt(int a) { return ((a | MASK) > (MASK - 1)) EQ(1); } + +/* + * check-name: cmpu-or0 + * check-command: test-linearize -Wno-decl $file + * + * check-output-ignore + * check-output-returns: 1 + */ diff --git a/validation/scheck/ko.c b/validation/scheck/ko.c new file mode 100644 index 00000000..dbd861ea --- /dev/null +++ b/validation/scheck/ko.c @@ -0,0 +1,10 @@ +static void ko(int x) +{ + __assert((~x) == (~0 + x)); +} + +/* + * check-name: scheck-ko + * check-command: scheck $file + * check-known-to-fail + */ diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c new file mode 100644 index 00000000..1e5314f2 --- /dev/null +++ b/validation/scheck/ok.c @@ -0,0 +1,22 @@ +static void ok(int x) +{ + __assert((~x) == (~0 - x)); // true but not simplified yet + __assert_eq(~x, ~0 - x); + __assert_const(x & 0, 0); +} + +static void always(int x) +{ + __assert((x - x) == 0); // true and simplified +} + +static void assumed(int x, int a, int b) +{ + __assume((a & ~b) == 0); + __assert_eq((x ^ a) | b, x | b); +} + +/* + * check-name: scheck-ok + * check-command: scheck $file + */ diff --git a/validation/test-suite b/validation/test-suite index 1b05c75e..305edd1f 100755 --- a/validation/test-suite +++ b/validation/test-suite @@ -13,6 +13,9 @@ prog_name=`basename $0` if [ ! -x "$default_path/sparse-llvm" ]; then disabled_cmds="sparsec sparsei sparse-llvm sparse-llvm-dis" fi +if [ ! -x "$default_path/scheck" ]; then + disabled_cmds="$disabled_cmds scheck" +fi # flags: # - some tests gave an unexpected result @@ -512,7 +515,9 @@ echo "options:" echo " -a append the created test to the input file" echo " -f write a test known to fail" echo " -l write a test for linearized code" +echo " -r write a test for linearized code returning 1" echo " -p write a test for pre-processing" +echo " -s write a test for symbolic checking" echo echo "argument(s):" echo " file file containing the test case(s)" @@ -528,6 +533,7 @@ do_format() append=0 linear=0 fail=0 + ret='' while [ $# -gt 0 ] ; do case "$1" in @@ -538,8 +544,13 @@ do_format() -l) def_cmd='test-linearize -Wno-decl $file' linear=1 ;; + -r) + def_cmd='test-linearize -Wno-decl $file' + ret=1 ;; -p) def_cmd='sparse -E $file' ;; + -s) + def_cmd='scheck $file' ;; help|-*) do_format_help @@ -582,6 +593,12 @@ _EOF if [ $fail != 0 ]; then echo " * check-known-to-fail" fi + if [ "$ret" != '' ]; then + echo ' *' + echo ' * check-output-ignore' + echo " * check-output-returns: $ret" + rm -f "$file.output.got" + fi if [ $linear != 0 ]; then echo ' *' echo ' * check-output-ignore' |