From 8fd2c0b489d3fe371081ceddb1637713a452eefd Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Fri, 9 Apr 2021 23:59:30 +0200 Subject: export declare_builtins() Make declare_builtins() extern so that it can be used from other files. Signed-off-by: Luc Van Oostenryck --- builtin.c | 2 +- builtin.h | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/builtin.c b/builtin.c index c7e7da3b..ff03dbab 100644 --- a/builtin.c +++ b/builtin.c @@ -559,7 +559,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; diff --git a/builtin.h b/builtin.h index d0d3fd2c..9cb67284 100644 --- a/builtin.h +++ b/builtin.h @@ -12,4 +12,6 @@ struct builtin_fn { struct symbol_op *op; }; +void declare_builtins(int stream, const struct builtin_fn tbl[]); + #endif -- cgit 1.2.3-korg From f7eb2ea83b2ba26032ad0f9d216dda8780165b95 Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Sat, 10 Apr 2021 00:00:18 +0200 Subject: builtin: define a symbol_op for a generic op acting on integer This can be used to define some generic (polymorphic) builtin with a signature like: (int) (T, T) (int, T) (int, T, long, T, ... T) where T is some integer type which will be instantiated at each call. Signed-off-by: Luc Van Oostenryck --- builtin.c | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ builtin.h | 2 ++ 2 files changed, 65 insertions(+) diff --git a/builtin.c b/builtin.c index ff03dbab..8e1d2d7e 100644 --- a/builtin.c +++ b/builtin.c @@ -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; diff --git a/builtin.h b/builtin.h index 9cb67284..5fe77c92 100644 --- a/builtin.h +++ b/builtin.h @@ -14,4 +14,6 @@ struct builtin_fn { void declare_builtins(int stream, const struct builtin_fn tbl[]); +extern struct symbol_op generic_int_op; + #endif -- cgit 1.2.3-korg From 4806f30a473ca70ffee3b10136f7ee8ea2b36f6f Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Sat, 10 Apr 2021 14:34:44 +0200 Subject: .gitignore is a bit too greedy The current .gitignore specifies that the generated programs must be ignored. Good. However, this is done by just specifying the name of the program which has the effect of having any files or directories with the same name to be ignored too. This is not intended. Fix this using the pattern '/' instead so that they match in the root folder. Signed-off-by: Luc Van Oostenryck --- .gitignore | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/.gitignore b/.gitignore index 63c74afd..6a28fa50 100644 --- a/.gitignore +++ b/.gitignore @@ -8,25 +8,25 @@ .*.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 +/semind +/sparse +/sparse-llvm +/test-dissect +/test-inspect +/test-lexing +/test-linearize +/test-parsing +/test-show-type +/test-unssa # tags tags -- cgit 1.2.3-korg From 7a9fab6984f7bce3fd52809ecf6e21b79f115be3 Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Fri, 9 Apr 2021 00:07:40 +0200 Subject: scheck: add a symbolic checker Some instruction simplifications can be quite tricky and thus easy to get wrong. Often, they also are hard to test (for example, you can test it with a few input values but of course not all combinations). I'm used to validate some of these with an independent tool (Alive cfr. [1], [2]) which is quite neat but has some issues: 1) This tool doesn't work with Sparse's IR or C source but it needs to have the tests written in its own language (very close to LLVM's IR). So it can be used to test if the logic of a simplification but not if implemented correctly. 2) This tool isn't maintained anymore (has some bugs too) and it's successor (Alive2 [3]) is not quite as handy to me (I miss the pre-conditions a lot). So, this patch implement the same idea but fully integrated with Sparse. This mean that you can write a test in C, let Sparse process and simplify it and then directly validate it and not only for a few values but symbolically, for all possible values. Note: Of course, this is not totally stand-alone and depends on an external library for the solver (Boolector, see [4], [5]). Note: Currently, it's just a proof of concept and, except the included tests, it's only very slightly tested (and untested with anything more complex than a few instructions). [1] https://blog.regehr.org/archives/1170 [2] https://www.cs.utah.edu/~regehr/papers/pldi15.pdf [3] https://blog.regehr.org/archives/1722 [4] https://boolector.github.io/ [5] https://boolector.github.io/papers/BrummayerBiere-TACAS09.pdf Signed-off-by: Luc Van Oostenryck --- .gitignore | 1 + Makefile | 7 ++ ident-list.h | 3 + scheck.c | 315 +++++++++++++++++++++++++++++++++++++++++++++++++ validation/scheck/ko.c | 10 ++ validation/scheck/ok.c | 14 +++ validation/test-suite | 6 + 7 files changed, 356 insertions(+) create mode 100644 scheck.c create mode 100644 validation/scheck/ko.c create mode 100644 validation/scheck/ok.c diff --git a/.gitignore b/.gitignore index 6a28fa50..b22f86b1 100644 --- a/.gitignore +++ b/.gitignore @@ -17,6 +17,7 @@ /example /graph /obfuscate +/scheck /semind /sparse /sparse-llvm diff --git a/Makefile b/Makefile index f9883da1..a0178a65 100644 --- a/Makefile +++ b/Makefile @@ -227,6 +227,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) diff --git a/ident-list.h b/ident-list.h index 8049b694..918f54d7 100644 --- a/ident-list.h +++ b/ident-list.h @@ -78,6 +78,9 @@ IDENT(memset); IDENT(memcpy); IDENT(copy_to_user); IDENT(copy_from_user); IDENT(main); +/* used by the symbolic checker */ +IDENT(__assert); + #undef __IDENT #undef IDENT #undef IDENT_RESERVED diff --git a/scheck.c b/scheck.c new file mode 100644 index 00000000..63cbfa2d --- /dev/null +++ b/scheck.c @@ -0,0 +1,315 @@ +// 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 +#include +#include +#include +#include +#include +#include + +#include +#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[] = { + { "__assert", &void_ctype, 0, { &bool_ctype }, .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 check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn) +{ + char model_format[] = "btor"; + int res; + + 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, 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, n, insn); +} + +static bool check_call(Btor *btor, struct instruction *insn) +{ + pseudo_t func = insn->func; + struct ident *ident = func->ident; + + if (ident == &__assert_ident) + return check_assert(btor, insn); + return 0; +} + +static bool check_function(struct entrypoint *ep) +{ + Btor *btor = boolector_new(); + struct basic_block *bb; + int rc = 0; + + boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 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, insn); + goto out; + 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); + + // Expand, linearize and check. + FOR_EACH_PTR(filelist, file) { + check_functions(sparse(file)); + } END_FOR_EACH_PTR(file); + return 0; +} 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..113912e0 --- /dev/null +++ b/validation/scheck/ok.c @@ -0,0 +1,14 @@ +static void ok(int x) +{ + __assert((~x) == (~0 - x)); // true but not simplified yet +} + +static void always(int x) +{ + __assert((x - x) == 0); // true and simplified +} + +/* + * check-name: scheck-ok + * check-command: scheck $file + */ diff --git a/validation/test-suite b/validation/test-suite index 1b05c75e..2f7950ef 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 @@ -513,6 +516,7 @@ 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 " -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)" @@ -540,6 +544,8 @@ do_format() linear=1 ;; -p) def_cmd='sparse -E $file' ;; + -s) + def_cmd='scheck $file' ;; help|-*) do_format_help -- cgit 1.2.3-korg From d1ab4c40982ffcfadebf3155f498469aeb1355b0 Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Fri, 9 Apr 2021 18:03:58 +0200 Subject: scheck: assert_eq() Testing the equivalence of two sub-expressions can be done with with a single assertion like __assert(A == B). However, in some cases, Sparse can use the equality to simplify the whole expression although it's unable to simplify one of the two sub-expressions into the other. So, add a new assertion, __assert_eq(), testing the equality of the two expressions given in argument independently of each other. Signed-off-by: Luc Van Oostenryck --- ident-list.h | 1 + scheck.c | 11 +++++++++++ validation/scheck/ok.c | 5 +++++ 3 files changed, 17 insertions(+) diff --git a/ident-list.h b/ident-list.h index 918f54d7..ab5bc5f5 100644 --- a/ident-list.h +++ b/ident-list.h @@ -80,6 +80,7 @@ IDENT(main); /* used by the symbolic checker */ IDENT(__assert); +IDENT(__assert_eq); #undef __IDENT #undef IDENT diff --git a/scheck.c b/scheck.c index 63cbfa2d..c64e8651 100644 --- a/scheck.c +++ b/scheck.c @@ -32,6 +32,7 @@ #define dyntype incomplete_ctype static const struct builtin_fn builtins_scheck[] = { { "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op }, + { "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op }, {} }; @@ -224,6 +225,14 @@ static bool check_assert(Btor *btor, struct instruction *insn) return check_btor(btor, n, insn); } +static bool check_equal(Btor *btor, 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, n, insn); +} + static bool check_call(Btor *btor, struct instruction *insn) { pseudo_t func = insn->func; @@ -231,6 +240,8 @@ static bool check_call(Btor *btor, struct instruction *insn) if (ident == &__assert_ident) return check_assert(btor, insn); + if (ident == &__assert_eq_ident) + return check_equal(btor, insn); return 0; } diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index 113912e0..76c04c4f 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -3,6 +3,11 @@ static void ok(int x) __assert((~x) == (~0 - x)); // true but not simplified yet } +static void also_ok(int x) +{ + __assert_eq(~x, ~0 - x); +} + static void always(int x) { __assert((x - x) == 0); // true and simplified -- cgit 1.2.3-korg From 75e72f82c8645db0f8cf6954ce3beb18a00dee37 Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Fri, 9 Apr 2021 18:08:33 +0200 Subject: scheck: allow multiple assertions With the SMT solver used here, by default, once an expression is checked it's kinda consumed by the process and can't be reused anymore for another check. So, enable the incremental mode: it allows to call boolecter_sat() several times. Note: Another would be, of course, to just AND together all assertions and just check this but then we would lost the finer grained diagnostic in case of failure. Signed-off-by: Luc Van Oostenryck --- scheck.c | 5 +++-- validation/scheck/ok.c | 4 ---- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/scheck.c b/scheck.c index c64e8651..efa5c1c3 100644 --- a/scheck.c +++ b/scheck.c @@ -252,6 +252,7 @@ static bool check_function(struct entrypoint *ep) 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; @@ -274,8 +275,8 @@ static bool check_function(struct entrypoint *ep) ternop(btor, insn); break; case OP_CALL: - rc = check_call(btor, insn); - goto out; + rc &= check_call(btor, insn); + break; case OP_RET: goto out; default: diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index 76c04c4f..f4a0daab 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -1,10 +1,6 @@ static void ok(int x) { __assert((~x) == (~0 - x)); // true but not simplified yet -} - -static void also_ok(int x) -{ __assert_eq(~x, ~0 - x); } -- cgit 1.2.3-korg From 0b0805cf17aeb6a6cd0a7ed3f47ad8f0b4a3407b Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Fri, 9 Apr 2021 18:10:44 +0200 Subject: scheck: assert_const() Since, the symbolic checker check expressions at the ... symbolic level, this can be used to check if two expressions are equivalent but not if this equivalence is effectively used. So, add a new assertion (this time not at the symbolic level) to check if an expression which is expected to simplify to a constant is effectively simplified to this constant. Signed-off-by: Luc Van Oostenryck --- ident-list.h | 1 + scheck.c | 19 +++++++++++++++++++ validation/scheck/ok.c | 1 + 3 files changed, 21 insertions(+) diff --git a/ident-list.h b/ident-list.h index ab5bc5f5..6264fd06 100644 --- a/ident-list.h +++ b/ident-list.h @@ -81,6 +81,7 @@ IDENT(main); /* used by the symbolic checker */ IDENT(__assert); IDENT(__assert_eq); +IDENT(__assert_const); #undef __IDENT #undef IDENT diff --git a/scheck.c b/scheck.c index efa5c1c3..f5ea4cf1 100644 --- a/scheck.c +++ b/scheck.c @@ -33,6 +33,7 @@ static const struct builtin_fn builtins_scheck[] = { { "__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 }, {} }; @@ -233,6 +234,22 @@ static bool check_equal(Btor *btor, struct instruction *insn) return check_btor(btor, 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, struct instruction *insn) { pseudo_t func = insn->func; @@ -242,6 +259,8 @@ static bool check_call(Btor *btor, struct instruction *insn) return check_assert(btor, insn); if (ident == &__assert_eq_ident) return check_equal(btor, insn); + if (ident == &__assert_const_ident) + return check_const(btor, insn); return 0; } diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index f4a0daab..8f65013e 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -2,6 +2,7 @@ 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) -- cgit 1.2.3-korg From 2e3c2464ca3522fe0a6dfc93ea36c88cbe7bf117 Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Fri, 9 Apr 2021 23:36:32 +0200 Subject: scheck: support pre-conditions via __assume() A lot of simplifications are only valid when their variables satisfy to some conditions (like "is within a given range" or "is a power of two"). So, allow to add such pre-conditions via new _assume() statements. Internally, all such preconditions are ANDed together and what is checked is they imply the assertions: AND(pre-condition) implies assertion 1 ... Note: IIUC, it seems that boolector has a native mechanism for such things but I'm not sure if t can be used here. Signed-off-by: Luc Van Oostenryck --- ident-list.h | 1 + scheck.c | 33 ++++++++++++++++++++++++--------- validation/scheck/ok.c | 6 ++++++ 3 files changed, 31 insertions(+), 9 deletions(-) diff --git a/ident-list.h b/ident-list.h index 6264fd06..3c08e8ca 100644 --- a/ident-list.h +++ b/ident-list.h @@ -79,6 +79,7 @@ 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); diff --git a/scheck.c b/scheck.c index f5ea4cf1..6752b9d9 100644 --- a/scheck.c +++ b/scheck.c @@ -31,6 +31,7 @@ #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 }, @@ -195,11 +196,22 @@ static void ternop(Btor *btor, struct instruction *insn) insn->target->priv = t; } -static bool check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn) +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) { @@ -218,20 +230,20 @@ static bool check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn) return 0; } -static bool check_assert(Btor *btor, struct instruction *insn) +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, n, insn); + return check_btor(btor, pre, n, insn); } -static bool check_equal(Btor *btor, struct instruction *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, n, insn); + return check_btor(btor, pre, n, insn); } static bool check_const(Btor *ctxt, struct instruction *insn) @@ -250,15 +262,17 @@ static bool check_const(Btor *ctxt, struct instruction *insn) return 0; } -static bool check_call(Btor *btor, struct instruction *insn) +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, insn); + return check_assert(btor, *pre, insn); if (ident == &__assert_eq_ident) - return check_equal(btor, insn); + return check_equal(btor, *pre, insn); if (ident == &__assert_const_ident) return check_const(btor, insn); return 0; @@ -267,6 +281,7 @@ static bool check_call(Btor *btor, struct instruction *insn) static bool check_function(struct entrypoint *ep) { Btor *btor = boolector_new(); + BoolectorNode *pre = boolector_true(btor); struct basic_block *bb; int rc = 0; @@ -294,7 +309,7 @@ static bool check_function(struct entrypoint *ep) ternop(btor, insn); break; case OP_CALL: - rc &= check_call(btor, insn); + rc &= check_call(btor, &pre, insn); break; case OP_RET: goto out; diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index 8f65013e..1e5314f2 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -10,6 +10,12 @@ 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 -- cgit 1.2.3-korg From 15806a1f68178a278c7a297b163d5692fe71cbf2 Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Sat, 17 Apr 2021 14:50:03 +0200 Subject: scheck: predefine __SYMBOLIC_CHECKER__ It can be useful to use the same testcase for the symbolic checker and normal sparse (or test-linearize) processing. So, there must be a mean to somehow ignore the assertions used for the symbolic checker when it's not used (since these are otherwise not known to sparse). Resolve this by adding a predefine, __SYMBOLIC_CHECKER__, to the symbolic checker. Signed-off-by: Luc Van Oostenryck --- scheck.c | 1 + 1 file changed, 1 insertion(+) diff --git a/scheck.c b/scheck.c index 6752b9d9..754fe76f 100644 --- a/scheck.c +++ b/scheck.c @@ -352,6 +352,7 @@ int main(int argc, char **argv) sparse_initialize(argc, argv, &filelist); declare_builtins(0, builtins_scheck); + predefine_strong("__SYMBOLIC_CHECKER__"); // Expand, linearize and check. FOR_EACH_PTR(filelist, file) { -- cgit 1.2.3-korg