From 18f157b8442af2f8b47ba8b78809b3d778566bfe Mon Sep 17 00:00:00 2001 From: Benjamin Bott Date: Sun, 1 May 2022 21:16:00 +0200 Subject: [PATCH] Invalidate variables (potentially) modified by an asm statement --- src/analyses/base.ml | 18 ++++++++ src/util/options.schema.json | 32 +++++++++++++ tests/regression/56-asm/01-parsing.c | 14 ++++++ .../56-asm/02-basic-discard-local.c | 12 +++++ .../56-asm/03-basic-discard-global.c | 12 +++++ tests/regression/56-asm/04-memory-clobber.c | 12 +++++ .../56-asm/10-advanced-discard-local.c | 15 +++++++ .../56-asm/11-advanced-discard-global.c | 15 +++++++ .../56-asm/12-advanced-discard-mixed.c | 20 +++++++++ .../56-asm/13-advanced-discard-local-multi.c | 17 +++++++ .../56-asm/14-advanced-discard-global-multi.c | 17 +++++++ .../56-asm/15-advanced-discard-mixed-multi.c | 24 ++++++++++ .../56-asm/20-advanced-read-local.c | 16 +++++++ .../56-asm/21-advanced-read-global.c | 16 +++++++ .../56-asm/22-advanced-read-mixed.c | 21 +++++++++ .../56-asm/23-advanced-read-local-multi.c | 18 ++++++++ .../56-asm/24-advanced-read-global-multi.c | 18 ++++++++ .../56-asm/25-advanced-read-mixed-multi.c | 25 +++++++++++ tests/regression/56-asm/30-simple-branch.c | 17 +++++++ tests/regression/56-asm/31-struct-value.c | 19 ++++++++ .../56-asm/32-struct-value-branch.c | 22 +++++++++ tests/regression/56-asm/33-struct-ptr.c | 26 +++++++++++ tests/regression/56-asm/34-struct-pr-branch.c | 29 ++++++++++++ tests/regression/56-asm/60-goto-issue.c | 45 +++++++++++++++++++ 24 files changed, 480 insertions(+) create mode 100644 tests/regression/56-asm/01-parsing.c create mode 100644 tests/regression/56-asm/02-basic-discard-local.c create mode 100644 tests/regression/56-asm/03-basic-discard-global.c create mode 100644 tests/regression/56-asm/04-memory-clobber.c create mode 100644 tests/regression/56-asm/10-advanced-discard-local.c create mode 100644 tests/regression/56-asm/11-advanced-discard-global.c create mode 100644 tests/regression/56-asm/12-advanced-discard-mixed.c create mode 100644 tests/regression/56-asm/13-advanced-discard-local-multi.c create mode 100644 tests/regression/56-asm/14-advanced-discard-global-multi.c create mode 100644 tests/regression/56-asm/15-advanced-discard-mixed-multi.c create mode 100644 tests/regression/56-asm/20-advanced-read-local.c create mode 100644 tests/regression/56-asm/21-advanced-read-global.c create mode 100644 tests/regression/56-asm/22-advanced-read-mixed.c create mode 100644 tests/regression/56-asm/23-advanced-read-local-multi.c create mode 100644 tests/regression/56-asm/24-advanced-read-global-multi.c create mode 100644 tests/regression/56-asm/25-advanced-read-mixed-multi.c create mode 100644 tests/regression/56-asm/30-simple-branch.c create mode 100644 tests/regression/56-asm/31-struct-value.c create mode 100644 tests/regression/56-asm/32-struct-value-branch.c create mode 100644 tests/regression/56-asm/33-struct-ptr.c create mode 100644 tests/regression/56-asm/34-struct-pr-branch.c create mode 100644 tests/regression/56-asm/60-goto-issue.c diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 20f886b7e5..0a1e5852c4 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2401,6 +2401,24 @@ struct (* D.join ctx.local @@ *) ctx.local + let asm ctx _ an = + let inv_globs, inv_exps = match an with + | None -> + (* asm basic instruction *) + (not (get_bool "sem.asm.basic-preserve-globals"), []) + | Some (outs, ins, clobbers) -> + (* advanced asm instructions *) + ( + List.mem "memory" clobbers && not (get_bool "sem.asm.memory-preserve-globals"), + List.append (if get_bool "sem.asm.readonly-inputs" then [] else List.map (fun (_, _, exp) -> exp, InvalidateTransitive) ins) + (List.map (fun (_, c, lval) -> Lval lval, match String.find c "+" with + | _ -> InvalidateSelfAndTransitive + | exception Not_found -> InvalidateSelf) outs) + ) + in + (if get_bool "sem.asm.enabled" then invalidate_core ~ctx inv_globs inv_exps); + ctx.local + let event ctx e octx = let st: store = ctx.local in let ask = ask_of_ctx ctx in diff --git a/src/util/options.schema.json b/src/util/options.schema.json index e8b6cb1731..03ebf3e2ed 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1108,6 +1108,38 @@ } }, "additionalProperties": false + }, + "asm": { + "title": "sem.asm", + "description": "Inline Assembly Analysis options", + "type": "object", + "properties": { + "enabled": { + "title": "sem.asm.enabled", + "description": "", + "type": "boolean", + "default": true + }, + "basic-preserve-globals": { + "title": "sem.asm.basic-preserve-globals", + "description": "If enabled, do preserve globals across basic asm statements", + "type": "boolean", + "default": false + }, + "memory-preserve-globals": { + "title": "sem.asm.memory-preserve-globals", + "description": "If enabled, do preserve globals across advanced asm statements with memory clobber annotation", + "type": "boolean", + "default": false + }, + "readonly-inputs": { + "title": "sem.asm.readonly-inputs", + "description": "If enabled, do not consider changes through pointers given as inputs", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false } }, "additionalProperties": false diff --git a/tests/regression/56-asm/01-parsing.c b/tests/regression/56-asm/01-parsing.c new file mode 100644 index 0000000000..bb05546912 --- /dev/null +++ b/tests/regression/56-asm/01-parsing.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int x; + + asm("nop"); + + asm volatile(""); + + assert(1); + + return 0; +} diff --git a/tests/regression/56-asm/02-basic-discard-local.c b/tests/regression/56-asm/02-basic-discard-local.c new file mode 100644 index 0000000000..0914212512 --- /dev/null +++ b/tests/regression/56-asm/02-basic-discard-local.c @@ -0,0 +1,12 @@ +#include + +int main() +{ + int x = 0; + + asm("nop"); + + assert(x == 0); + + return 0; +} diff --git a/tests/regression/56-asm/03-basic-discard-global.c b/tests/regression/56-asm/03-basic-discard-global.c new file mode 100644 index 0000000000..454fd8956e --- /dev/null +++ b/tests/regression/56-asm/03-basic-discard-global.c @@ -0,0 +1,12 @@ +#include + +int x = 0; + +int main() +{ + asm("nop"); + + assert(x == 0); // UNKNOWN + + return 0; +} diff --git a/tests/regression/56-asm/04-memory-clobber.c b/tests/regression/56-asm/04-memory-clobber.c new file mode 100644 index 0000000000..59673cfbf3 --- /dev/null +++ b/tests/regression/56-asm/04-memory-clobber.c @@ -0,0 +1,12 @@ +#include + +int x = 0; + +int main() +{ + asm("movl $1, x" : : : "memory"); + + assert(x == 1); // UNKNOWN + + return 0; +} diff --git a/tests/regression/56-asm/10-advanced-discard-local.c b/tests/regression/56-asm/10-advanced-discard-local.c new file mode 100644 index 0000000000..fb6e4685fa --- /dev/null +++ b/tests/regression/56-asm/10-advanced-discard-local.c @@ -0,0 +1,15 @@ +#include + +int main() +{ + int x = 0; + int y = 0; + + asm("nop" + : "=r"(x)); + + assert(x == 0); // UNKNOWN + assert(y == 0); + + return 0; +} diff --git a/tests/regression/56-asm/11-advanced-discard-global.c b/tests/regression/56-asm/11-advanced-discard-global.c new file mode 100644 index 0000000000..f870974e7a --- /dev/null +++ b/tests/regression/56-asm/11-advanced-discard-global.c @@ -0,0 +1,15 @@ +#include + +int x = 0; +int y = 0; + +int main() +{ + asm("nop" + : "=r"(x)); + + assert(x == 0); // UNKNOWN + assert(y == 0); + + return 0; +} diff --git a/tests/regression/56-asm/12-advanced-discard-mixed.c b/tests/regression/56-asm/12-advanced-discard-mixed.c new file mode 100644 index 0000000000..fe8609a672 --- /dev/null +++ b/tests/regression/56-asm/12-advanced-discard-mixed.c @@ -0,0 +1,20 @@ +#include + +int gx = 0; +int gy = 0; + +int main() +{ + int x = 0; + int y = 0; + + asm("nop" + : "=r"(x), "=r"(gx)); + + assert(x == 0); // UNKNOWN + assert(y == 0); + assert(gx == 0); // UNKNOWN + assert(gy == 0); + + return 0; +} diff --git a/tests/regression/56-asm/13-advanced-discard-local-multi.c b/tests/regression/56-asm/13-advanced-discard-local-multi.c new file mode 100644 index 0000000000..82ab281ff4 --- /dev/null +++ b/tests/regression/56-asm/13-advanced-discard-local-multi.c @@ -0,0 +1,17 @@ +#include + +int main() +{ + int x = 0; + int y = 0; + int z = 0; + + asm("nop" + : "=r"(x), "=r"(y)); + + assert(x == 0); // UNKNOWN + assert(y == 0); // UNKNOWN + assert(z == 0); + + return 0; +} diff --git a/tests/regression/56-asm/14-advanced-discard-global-multi.c b/tests/regression/56-asm/14-advanced-discard-global-multi.c new file mode 100644 index 0000000000..b6c52cbb1f --- /dev/null +++ b/tests/regression/56-asm/14-advanced-discard-global-multi.c @@ -0,0 +1,17 @@ +#include + +int x = 0; +int y = 0; +int z = 0; + +int main() +{ + asm("nop" + : "=r"(x), "=r"(y)); + + assert(x == 0); // UNKNOWN + assert(y == 0); // UNKNOWN + assert(z == 0); + + return 0; +} diff --git a/tests/regression/56-asm/15-advanced-discard-mixed-multi.c b/tests/regression/56-asm/15-advanced-discard-mixed-multi.c new file mode 100644 index 0000000000..8ecd451d89 --- /dev/null +++ b/tests/regression/56-asm/15-advanced-discard-mixed-multi.c @@ -0,0 +1,24 @@ +#include + +int gx = 0; +int gy = 0; +int gz = 0; + +int main() +{ + int x = 0; + int y = 0; + int z = 0; + + asm("nop" + : "=r"(x), "=r"(y), "=r"(gx), "=r"(gy)); + + assert(x == 0); // UNKNOWN + assert(y == 0); // UNKNOWN + assert(z == 0); + assert(gx == 0); // UNKNOWN + assert(gy == 0); // UNKNOWN + assert(gz == 0); + + return 0; +} diff --git a/tests/regression/56-asm/20-advanced-read-local.c b/tests/regression/56-asm/20-advanced-read-local.c new file mode 100644 index 0000000000..d8b7b33a14 --- /dev/null +++ b/tests/regression/56-asm/20-advanced-read-local.c @@ -0,0 +1,16 @@ +#include + +int main() +{ + int x = 0; + int y = 0; + + asm("nop" + : + : "r"(x)); + + assert(x == 0); + assert(y == 0); + + return 0; +} diff --git a/tests/regression/56-asm/21-advanced-read-global.c b/tests/regression/56-asm/21-advanced-read-global.c new file mode 100644 index 0000000000..d5efabd86f --- /dev/null +++ b/tests/regression/56-asm/21-advanced-read-global.c @@ -0,0 +1,16 @@ +#include + +int x = 0; +int y = 0; + +int main() +{ + asm("nop" + : + : "r"(x)); + + assert(x == 0); + assert(y == 0); + + return 0; +} diff --git a/tests/regression/56-asm/22-advanced-read-mixed.c b/tests/regression/56-asm/22-advanced-read-mixed.c new file mode 100644 index 0000000000..684c1bc514 --- /dev/null +++ b/tests/regression/56-asm/22-advanced-read-mixed.c @@ -0,0 +1,21 @@ +#include + +int gx = 0; +int gy = 0; + +int main() +{ + int x = 0; + int y = 0; + + asm("nop" + : + : "r"(x), "r"(gx)); + + assert(x == 0); + assert(y == 0); + assert(gx == 0); + assert(gy == 0); + + return 0; +} diff --git a/tests/regression/56-asm/23-advanced-read-local-multi.c b/tests/regression/56-asm/23-advanced-read-local-multi.c new file mode 100644 index 0000000000..e3d4528bb0 --- /dev/null +++ b/tests/regression/56-asm/23-advanced-read-local-multi.c @@ -0,0 +1,18 @@ +#include + +int main() +{ + int x = 0; + int y = 0; + int z = 0; + + asm("nop" + : + : "r"(x), "r"(y)); + + assert(x == 0); + assert(y == 0); + assert(z == 0); + + return 0; +} diff --git a/tests/regression/56-asm/24-advanced-read-global-multi.c b/tests/regression/56-asm/24-advanced-read-global-multi.c new file mode 100644 index 0000000000..9cb433c005 --- /dev/null +++ b/tests/regression/56-asm/24-advanced-read-global-multi.c @@ -0,0 +1,18 @@ +#include + +int x = 0; +int y = 0; +int z = 0; + +int main() +{ + asm("nop" + : + : "r"(x), "r"(y)); + + assert(x == 0); + assert(y == 0); + assert(z == 0); + + return 0; +} diff --git a/tests/regression/56-asm/25-advanced-read-mixed-multi.c b/tests/regression/56-asm/25-advanced-read-mixed-multi.c new file mode 100644 index 0000000000..d174c59a3b --- /dev/null +++ b/tests/regression/56-asm/25-advanced-read-mixed-multi.c @@ -0,0 +1,25 @@ +#include + +int gx = 0; +int gy = 0; +int gz = 0; + +int main() +{ + int x = 0; + int y = 0; + int z = 0; + + asm("nop" + : + : "r"(x), "r"(y), "r"(gx), "r"(gy)); + + assert(x == 0); + assert(y == 0); + assert(z == 0); + assert(gx == 0); + assert(gy == 0); + assert(gz == 0); + + return 0; +} diff --git a/tests/regression/56-asm/30-simple-branch.c b/tests/regression/56-asm/30-simple-branch.c new file mode 100644 index 0000000000..60153fc7b1 --- /dev/null +++ b/tests/regression/56-asm/30-simple-branch.c @@ -0,0 +1,17 @@ +#include + +int main() +{ + int x = 0; + int y; + + if (!y) + { + asm("movl $1, %0" + : "=r"(x)); + } + + assert(x == 1); // UNKNOWN + + return 0; +} diff --git a/tests/regression/56-asm/31-struct-value.c b/tests/regression/56-asm/31-struct-value.c new file mode 100644 index 0000000000..16ddfc4966 --- /dev/null +++ b/tests/regression/56-asm/31-struct-value.c @@ -0,0 +1,19 @@ +#include + +int main() +{ + struct test + { + int a; + int b; + } x = {0, 0}; + int y; + + asm("movl $1, %0" + : "=r"(x.a)); + + assert(x.a == 1); // UNKNOWN + assert(x.b == 0); + + return 0; +} diff --git a/tests/regression/56-asm/32-struct-value-branch.c b/tests/regression/56-asm/32-struct-value-branch.c new file mode 100644 index 0000000000..56f6dc74f7 --- /dev/null +++ b/tests/regression/56-asm/32-struct-value-branch.c @@ -0,0 +1,22 @@ +#include + +int main() +{ + struct test + { + int a; + int b; + } x = {0, 0}; + int y; + + if (!y) + { + asm("movl $1, %0" + : "=r"(x.a)); + } + + assert(x.a == 1); // UNKNOWN + assert(x.b == 0); + + return 0; +} diff --git a/tests/regression/56-asm/33-struct-ptr.c b/tests/regression/56-asm/33-struct-ptr.c new file mode 100644 index 0000000000..bdd28174c4 --- /dev/null +++ b/tests/regression/56-asm/33-struct-ptr.c @@ -0,0 +1,26 @@ +#include + +int main() +{ + struct test + { + int a; + int b; + }; + + struct test v = {0, 0}; + struct test *x = &v; + int y; + + asm("nop" + : + : "r"(x)); + + assert(x->a == 0); // UNKNOWN + assert(x->b == 0); // UNKNOWN + + assert(v.a == 0); // UNKNOWN + assert(v.b == 0); // UNKNOWN + + return 0; +} diff --git a/tests/regression/56-asm/34-struct-pr-branch.c b/tests/regression/56-asm/34-struct-pr-branch.c new file mode 100644 index 0000000000..9bb0ba05f1 --- /dev/null +++ b/tests/regression/56-asm/34-struct-pr-branch.c @@ -0,0 +1,29 @@ +#include + +int main() +{ + struct test + { + int a; + int b; + }; + + struct test v = {0, 0}; + struct test *x = &v; + int y; + + if (!y) + { + asm("nop" + : + : "r"(x)); + } + + assert(x->a == 0); // UNKNOWN + assert(x->b == 0); // UNKNOWN + + assert(v.a == 0); // UNKNOWN + assert(v.b == 0); // UNKNOWN + + return 0; +} diff --git a/tests/regression/56-asm/60-goto-issue.c b/tests/regression/56-asm/60-goto-issue.c new file mode 100644 index 0000000000..b80b3563ec --- /dev/null +++ b/tests/regression/56-asm/60-goto-issue.c @@ -0,0 +1,45 @@ +// see https://github.com/goblint/cil/issues/81 + +#define __stringify_1(x...) #x +#define __stringify(x...) __stringify_1(x) + +#define __ASM_FORM(x, ...) " " __stringify(x, ##__VA_ARGS__) " " +#define __ASM_SEL(a, b) __ASM_FORM(b) + +#define _ASM_PTR __ASM_SEL(.long, .quad) +#define _ASM_ALIGN __ASM_SEL(.balign 4, .balign 8) + +#define JUMP_TABLE_ENTRY \ + ".pushsection __jump_table, \"aw\" \n\t" _ASM_ALIGN "\n\t" \ + ".long 1b - . \n\t" \ + ".long %l[l_yes] - . \n\t" _ASM_PTR "%c0 + %c1 - .\n\t" \ + ".popsection \n\t" + +#define __stringify_1(x...) #x +#define __stringify(x...) __stringify_1(x) + +#define asm_volatile_goto(x...) \ + do \ + { \ + asm goto(x); \ + asm(""); \ + } while (0) + +static int arch_static_branch(const int key, const int branch) +{ + asm_volatile_goto("1:" + ".byte " __stringify(BYTES_NOP5) "\n\t" JUMP_TABLE_ENTRY + : + : "i"(key), "i"(branch) + : + : l_yes); + + return 0; +l_yes: + return 1; +} + +int main() +{ + return 0; +} \ No newline at end of file