From b8d94d9a31753b5097dc6ce93117e9c8a5ac25c4 Mon Sep 17 00:00:00 2001 From: isubasinghe Date: Thu, 29 Feb 2024 10:15:49 +1100 Subject: [PATCH] wip --- copy_spec.py | 504 ++++++++++++++++++++++++++++++++++++++++++ examples/copy.c | 103 +++++++++ examples/out_copy.c | 245 ++++++++++++++++++++ examples/out_copy.txt | 300 +++++++++++++++++++++++++ ghost_data.py | 4 +- ghost_data_helpers.py | 15 ++ out-model.smt2 | 374 +++++++++++++++++++++++++++++++ out.smt2 | 260 ++++++++++++++++++++++ out2.smt2 | 252 +++++++++++++++++++++ prog_globals.py | 247 +++++++++++++++++++++ smt.py | 12 +- source.py | 50 ++++- validate_dsa.py | 2 + 13 files changed, 2357 insertions(+), 11 deletions(-) create mode 100644 copy_spec.py create mode 100644 examples/copy.c create mode 100644 examples/out_copy.c create mode 100644 examples/out_copy.txt create mode 100644 out-model.smt2 create mode 100644 out.smt2 create mode 100644 out2.smt2 create mode 100644 prog_globals.py diff --git a/copy_spec.py b/copy_spec.py new file mode 100644 index 0000000..f3f605d --- /dev/null +++ b/copy_spec.py @@ -0,0 +1,504 @@ +from typing import Callable, Any, Optional +import source +import nip +from ghost_data_helpers import * + + +Mem = source.ExprVar(source.type_mem, source.ProgVarName('Mem')) + +def htd_assigned() -> source.ExprVarT[nip.GuardVarName]: + return g(source.ExprVar(source.type_bool, source.ProgVarName('HTD'))) + + +def mem_assigned() -> source.ExprVarT[nip.GuardVarName]: + return g(source.ExprVar(source.type_bool, source.ProgVarName('Mem'))) + + +def pms_assigned() -> source.ExprVarT[nip.GuardVarName]: + return g(source.ExprVar(source.type_bool, source.ProgVarName('PMS'))) + + +def ghost_asserts_assigned() -> source.ExprVarT[nip.GuardVarName]: + return g(source.ExprVar(source.type_bool, source.ProgVarName('GhostAssertions'))) + + +def retchar() -> source.ExprVarT[source.ProgVarName]: + return source.ExprVar(source.type_word8,source.ProgVarName('ret__unsigned_char#v')) + +def ret_unsigned() -> source.ExprVarT[source.ProgVarName]: + return source.ExprVar(source.type_word32, source.ProgVarName('ret__unsigned#v')) + +def ring_handle() -> source.ExprVarT[source.ProgVarName]: + return source.ExprVar(source.type_word64, source.ProgVarName("ring___ptr_to_struct_ring_handle_C#v")) + +def ring_handle_free_ring_offset(base: source.ExprVarT[source.ProgVarName]): + return plus(base, u64(0)) + +def ring_handle_used_ring_offset(base: source.ExprVarT[source.ProgVarName]): + return plus(base, u64(8)) + + +def free_ring(base_name: Optional[str] = None) -> source.ExprVarT[source.ProgVarName]: + default = "free_ring" if base_name is None else base_name + return source.ProgVar(source.type_word64, source.ProgVarName(f"{default}___ptr_to_struct_ring_buffer_C#v")) + +def ring(base_name: Optional[str] = None) -> source.ExprVarT[source.ProgVarName]: + default = "ring" if base_name is None else base_name + return source.ProgVar(source.type_word64, source.ProgVarName(f"{default}___ptr_to_struct_ring_buffer_C#v")) + +def ring_head_offset(base: source.ExprT[source.ProgVarName]) -> source.ExprT[source.ProgVarName]: + return plus(base, u64(0)) + +def ring_tail_offset(base: source.ExprT[source.ProgVarName]) -> source.ExprT[source.ProgVarName]: + return plus(base, u64(4)) + +def ring_buffers_offset(base: source.ExprT[source.ProgVarName]) -> source.ExprT[source.ProgVarName]: + return plus(base, u64(8)) + +def ring_sz_offset(base: source.ExprT[source.ProgVarName]) -> source.ExprT[source.ProgVarName]: + return plus(base, u64(12296)) + +def ring_consumer_signalled_offset(base: source.ExprT[source.ProgVarName]) -> source.ExprT[source.ProgVarName]: + return plus(base, u64(12300)) + +def buff_desc_phys_or_offset() -> source.ExprVarT[source.ProgVarName]: + return source.ExprVar(source.type_word64, source.ProgVarName("buffer___struct_buff_desc_C#v.phys_or_offset_C")) + +def buff_desc_phys_or_offset_offset(base: source.ExprT[source.ProgVarName]): + return plus(base, u64(0)) + +def buff_desc_len() -> source.ExprVarT[source.ProgVarName]: + return source.ExprVar(source.type_word16, source.ProgVarName("buffer___struct_buff_desc_C#v.len_C")) + +def buff_desc_len_offset(base: source.ExprT[source.ProgVarName]): + return plus(base, u64(8)) + +def buff_desc_cookie() -> source.ExprVarT[source.ProgVarName]: + return source.ExprVar(source.type_word64, source.ProgVarName("buffer___struct_buff_desc_C#v.cookie_C")) + + +def buff_desc_cookie_offset(base: source.ExprT[source.ProgVarName]): + return plus(base, u64(16)) + + +functions_spec = { + "tmp.init": source.Ghost( + precondition=conjs(), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.assert": source.Ghost( + precondition=conjs(), + postcondition=conjs(eq(arg(Mem), Mem)), + loop_invariants={}, + loop_iterations={} + ), + "tmp.memcpy": source.Ghost( + precondition=conjs(), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.dequeue": source.Ghost( + precondition=conjs( + neq(mem_acc(source.type_word32, ring_sz_offset(arg(ring())) , arg(Mem)), u32(0)), + ult(mem_acc(source.type_word32, ring_tail_offset(arg(ring())), arg(Mem)), u32(512)) + ), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.enqueue": source.Ghost( + precondition=conjs( + neq(mem_acc(source.type_word32, ring_sz_offset(arg(ring())) , arg(Mem)), u32(0)), + ult(mem_acc(source.type_word32, ring_head_offset(arg(ring())), arg(Mem)), u32(512)) + ), + postcondition=conjs( + eq( + ring(), + arg(ring()) + ), + eq( + mem_acc( + source.type_word32, + ring_head_offset(ring()), + Mem + ), + mod( + plus( + mem_acc( + source.type_word32, + ring_head_offset(arg(ring())), + arg(Mem) + ), + u32(1) + ), + mem_acc( + source.type_word32, + ring_sz_offset(arg(ring())), + arg(Mem) + ) + ) + ) + ), + loop_invariants={}, + loop_iterations={} + ), + "tmp.enqueue_free": source.Ghost( + precondition=conjs( + neq( + mem_acc( + source.type_word32, + ring_sz_offset( + mem_acc( + source.type_word64, + ring_handle_free_ring_offset( + arg(ring_handle()) + ), + arg(Mem) + ) + ), + arg(Mem) + ), + u32(0) + ), + ult( + mem_acc( + source.type_word32, + ring_head_offset( + mem_acc( + source.type_word64, + ring_handle_free_ring_offset( + arg(ring_handle()) + ), + arg(Mem) + ) + ), + arg(Mem) + ), + u32(512) + ) + + ), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.notified": source.Ghost( + precondition=conjs(), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.ring_full": source.Ghost( + precondition=conjs( + neq(mem_acc(source.type_word32, ring_sz_offset(arg(ring())) , arg(Mem)), u32(0)) + ), + postcondition=conjs( + eq(retchar(), + bv8eq( + mod( + plus( + mem_acc(source.type_word32, ring_head_offset(arg(ring())), arg(Mem)), + u32(1) + ), + mem_acc(source.type_word32, ring_sz_offset(arg(ring())), arg(Mem)), + ), + mem_acc(source.type_word32, ring_tail_offset(arg(ring())), arg(Mem)) + ) + ), + eq(arg(Mem), Mem) + ), + loop_invariants={}, + loop_iterations={} + ), + "tmp.ring_init": source.Ghost( + precondition=conjs(), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.ring_size": source.Ghost( + precondition=conjs( + + neq(mem_acc(source.type_word32, ring_sz_offset(arg(ring())) , arg(Mem)), u32(0)) + ), + postcondition=conjs( + eq(ret_unsigned(), + mod( + sub( + plus( + mem_acc( + source.type_word32, + ring_head_offset(arg(ring())), + arg(Mem)), + mem_acc( + source.type_word32, + ring_sz_offset(arg(ring())), + arg(Mem)) + ), + mem_acc( + source.type_word32, + ring_tail_offset(arg(ring())), + arg(Mem) + ) + ), + mem_acc(source.type_word32, ring_sz_offset(arg(ring())), arg(Mem)) + ) + ), + ), + loop_invariants={}, + loop_iterations={} + ), + "tmp.ring_empty": source.Ghost( + precondition=conjs(), + postcondition=conjs(eq(arg(Mem), Mem)), + loop_invariants={}, + loop_iterations={} + ), + "tmp.buffers_init": source.Ghost( + precondition=conjs( + neq(mem_acc(source.type_word32, ring_sz_offset(arg(free_ring())) , arg(Mem)), u32(0)), + ult(mem_acc(source.type_word32, ring_head_offset(arg(free_ring())), arg(Mem)), u32(512)), + ult(arg(u32v('ring_size')), u32(1024)) + ), + postcondition=conjs(), + loop_invariants={ + lh('3'): conjs( + g(i32v('i')), + g(u32v('ring_size')), + mem_assigned(), + htd_assigned(), + pms_assigned(), + ghost_asserts_assigned(), + conjs( + neq(mem_acc(source.type_word32, ring_sz_offset(free_ring()) , Mem), u32(0)), + ult(mem_acc(source.type_word32, ring_head_offset(free_ring()), Mem), u32(512)), + ), + ult(i32v('i'), u32(1024)) + ) + }, + loop_iterations={ + lh('3'): source.LoopIterationGhost( + pre_iter=source.expr_true, + post_iter=source.expr_true + ) + + } + ), + "tmp.dequeue_free": source.Ghost( + precondition=conjs( + neq( + mem_acc( + source.type_word32, + ring_sz_offset( + mem_acc( + source.type_word64, + ring_handle_free_ring_offset( + arg(ring_handle()) + ), + arg(Mem) + ) + ), + arg(Mem) + ), + u32(0) + ), + ult( + mem_acc( + source.type_word32, + ring_tail_offset( + mem_acc( + source.type_word64, + ring_handle_free_ring_offset( + arg(ring_handle()) + ), + arg(Mem) + ) + ), + arg(Mem) + ), + u32(512) + ) + ), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.dequeue_used": source.Ghost( + precondition=conjs( + neq( + mem_acc( + source.type_word32, + ring_sz_offset( + mem_acc( + source.type_word64, + ring_handle_used_ring_offset( + arg(ring_handle()) + ), + arg(Mem) + ) + ), + arg(Mem) + ), + u32(0) + ), + ult( + mem_acc( + source.type_word32, + ring_tail_offset( + mem_acc( + source.type_word64, + ring_handle_used_ring_offset( + arg(ring_handle()) + ), + arg(Mem) + ) + ), + arg(Mem) + ), + u32(512) + ) + ), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.enqueue_used": source.Ghost( + precondition=conjs( + neq( + mem_acc( + source.type_word32, + ring_sz_offset( + mem_acc( + source.type_word64, + ring_handle_used_ring_offset( + arg(ring_handle()) + ), + arg(Mem) + ) + ), + arg(Mem) + ), + u32(0) + ), + ult( + mem_acc( + source.type_word32, + ring_head_offset( + mem_acc( + source.type_word64, + ring_handle_used_ring_offset( + arg(ring_handle()) + ), + arg(Mem) + ) + ), + arg(Mem) + ), + u32(512) + ) + ), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.cancel_signal": source.Ghost( + precondition=conjs(), + postcondition=conjs( + eq(Mem, + mem_upd( + source.type_word8, + ring_consumer_signalled_offset(arg(ring('ring_buffer'))), + char(1), + arg(Mem) + ) + ) + ), + loop_invariants={}, + loop_iterations={} + ), + "tmp.require_signal": source.Ghost( + precondition=conjs(), + postcondition=conjs(), + loop_iterations={}, + loop_invariants={} + ), + "tmp.sel4cp_notify": source.Ghost( + precondition=conjs(), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.sel4cp_notify_delayed": source.Ghost( + precondition=conjs(), + postcondition=conjs(), + loop_invariants={}, + loop_iterations={} + ), + "tmp.request_signal": source.Ghost( + precondition=conjs( + ), + postcondition=conjs( + eq(Mem, + mem_upd( + source.type_word8, + ring_consumer_signalled_offset(arg(ring('ring_buffer'))), + char(0), + arg(Mem) + ) + ) + ), + loop_invariants={}, + loop_iterations={} + ) +} + +# mem_upd( +# source.type_word64, +# buff_desc_cookie_offset(plus( +# ring_buffers_offset(arg(ring())), +# mul( +# u64(24), +# ucast(source.type_word64, mem_acc( +# source.type_word32, +# arg(ring()), +# arg(Mem), +# )) +# ), +# )), +# arg(buff_desc_cookie()), +# mem_upd( +# source.type_word16, +# buff_desc_len_offset(plus( +# ring_buffers_offset(arg(ring())), +# mul( +# u64(24), +# ucast(source.type_word64, mem_acc( +# source.type_word32, +# arg(ring()), +# arg(Mem), +# )) +# ), +# )), +# arg(buff_desc_len()), +# mem_upd( +# source.type_word64, +# buff_desc_phys_or_offset_offset(plus( +# ring_buffers_offset(arg(ring())), +# mul( +# u64(24), +# ucast(source.type_word64, mem_acc( +# source.type_word32, +# arg(ring()), +# arg(Mem), +# )) +# ), +# )), +# arg(buff_desc_phys_or_offset()), +# arg(Mem) +# ), +# ), + +# ) diff --git a/examples/copy.c b/examples/copy.c new file mode 100644 index 0000000..aa976ad --- /dev/null +++ b/examples/copy.c @@ -0,0 +1,103 @@ +#include +#include + +#include "shared_ringbuffer.h" +#include "util.h" + +/* Notification and PPC channels - ensure these align with .system file! */ +#define MUX_RX_CH 0 +#define CLIENT_CH 1 + +/* Ring handles */ +ring_handle_t rx_ring_mux; +ring_handle_t rx_ring_cli; + +/* Ring buffer regions */ +uintptr_t rx_free_mux; +uintptr_t rx_used_mux; +uintptr_t rx_free_cli; +uintptr_t rx_used_cli; + +/* Buffer data regions */ +uintptr_t mux_buffer_data_region; +uintptr_t cli_buffer_data_region; + +uintptr_t uart_base; + +void rx_return(void) +{ + bool enqueued = false; + bool reprocess = true; + + while (reprocess) { + while (!ring_empty(rx_ring_mux.used_ring) && !ring_empty(rx_ring_cli.free_ring) && + !ring_full(rx_ring_mux.free_ring) && !ring_full(rx_ring_cli.used_ring)) { + buff_desc_t cli_buffer, mux_buffer; + int err __attribute__((unused)) = dequeue_free(&rx_ring_cli, &cli_buffer); + assert(!err); + + if (cli_buffer.offset % BUF_SIZE || cli_buffer.offset >= BUF_SIZE * NUM_BUFFERS) { + printf("COPY|LOG: Client provided offset %X which is not buffer aligned or outside of buffer region\n", cli_buffer.offset); + err = enqueue_free(&rx_ring_cli, cli_buffer); + assert(!err); + continue; + } + + err = dequeue_used(&rx_ring_mux, &mux_buffer); + assert(!err); + + uintptr_t cli_addr = cli_buffer_data_region + cli_buffer.offset; + uintptr_t mux_addr = mux_buffer_data_region + mux_buffer.offset; + + memcpy((void *)cli_addr, (void *)mux_addr, mux_buffer.len); + cli_buffer.len = mux_buffer.len; + mux_buffer.len = 0; + + err = enqueue_used(&rx_ring_cli, cli_buffer); + assert(!err); + + err = enqueue_free(&rx_ring_mux, mux_buffer); + assert(!err); + + enqueued = true; + } + + request_signal(rx_ring_mux.used_ring); + + /* Only request signal from client if incoming packets from multiplexer are awaiting free buffers */ + if (!ring_empty(rx_ring_mux.used_ring)) request_signal(rx_ring_cli.free_ring); + else cancel_signal(rx_ring_cli.free_ring); + + reprocess = false; + + if (!ring_empty(rx_ring_mux.used_ring) && !ring_empty(rx_ring_cli.free_ring) && + !ring_full(rx_ring_mux.free_ring) && !ring_full(rx_ring_cli.used_ring)) { + cancel_signal(rx_ring_mux.used_ring); + cancel_signal(rx_ring_cli.free_ring); + reprocess = true; + } + } + + if (enqueued && require_signal(rx_ring_cli.used_ring)) { + cancel_signal(rx_ring_cli.used_ring); + sel4cp_notify(CLIENT_CH); + } + + if (enqueued && require_signal(rx_ring_mux.free_ring)) { + cancel_signal(rx_ring_mux.free_ring); + sel4cp_notify_delayed(MUX_RX_CH); + } +} + +void notified(sel4cp_channel ch) +{ + rx_return(); +} + +void init(void) +{ + ring_init(&rx_ring_mux, (ring_buffer_t *)rx_free_mux, (ring_buffer_t *)rx_used_mux, NUM_BUFFERS, NUM_BUFFERS); + ring_init(&rx_ring_cli, (ring_buffer_t *)rx_free_cli, (ring_buffer_t *)rx_used_cli, NUM_BUFFERS, NUM_BUFFERS); + + buffers_init(rx_ring_cli.free_ring, 0, NUM_BUFFERS, BUF_SIZE); +} \ No newline at end of file diff --git a/examples/out_copy.c b/examples/out_copy.c new file mode 100644 index 0000000..9969c88 --- /dev/null +++ b/examples/out_copy.c @@ -0,0 +1,245 @@ +# 0 "out_copy.c" +# 0 "" +# 0 "" +# 1 "/usr/include/stdc-predef.h" 1 3 4 +# 0 "" 2 +# 1 "out_copy.c" + + +typedef unsigned long uint64_t; +typedef unsigned short uint16_t; +typedef unsigned int uint32_t; +typedef uint64_t size_t; +typedef uint64_t uintptr_t; + + +typedef unsigned char bool; +# 19 "out_copy.c" +void assert(bool b); + + + +void *memcpy(void *dest, const void *src, size_t n); + + +typedef unsigned int sel4cp_channel; +void sel4cp_notify(sel4cp_channel ch); +void sel4cp_notify_delayed(sel4cp_channel ch); +# 51 "out_copy.c" +typedef struct buff_desc { + uintptr_t phys_or_offset; + uint16_t len; + void *cookie; +} buff_desc_t; + + +typedef struct ring_buffer { + uint32_t head; + uint32_t tail; + buff_desc_t buffers[512]; + uint32_t size; + bool consumer_signalled; +} ring_buffer_t; + + +typedef struct ring_handle { + ring_buffer_t *free_ring; + ring_buffer_t *used_ring; +} ring_handle_t; +# 79 "out_copy.c" +static inline bool ring_empty(ring_buffer_t *ring) +{ + return (ring->head == ring->tail); +} +# 91 "out_copy.c" +static inline bool ring_full(ring_buffer_t *ring) + // requires ring->size >= 1 + // ensures return == {retbody} +{ + return (((ring->head + 1) % ring->size) == ring->tail); +} +# 103 "out_copy.c" +static inline uint32_t ring_size(ring_buffer_t *ring) +{ + return (((ring->head + ring->size) - ring->tail) % ring->size); +} +# 116 "out_copy.c" +static inline int enqueue(ring_buffer_t *ring, buff_desc_t buffer) +{ + if (ring_full(ring)) return -1; + + ring->buffers[ring->head].phys_or_offset = buffer.phys_or_offset; + ring->buffers[ring->head].len = buffer.len; + ring->buffers[ring->head].cookie = buffer.cookie; + if (0) ; + ring->head = (ring->head + 1) % ring->size; + + return 0; +} +# 135 "out_copy.c" +static inline buff_desc_t dequeue(ring_buffer_t *ring) +{ + if (ring_empty(ring)) assert(0); + + buff_desc_t buffer; + buffer = ring->buffers[ring->tail]; + if (0) ; + ring->tail = (ring->tail + 1) % ring->size; + + return buffer; +} +# 155 "out_copy.c" +static inline int enqueue_free(ring_handle_t *ring, buff_desc_t buffer) +{ + return enqueue(ring->free_ring, buffer); +} +# 168 "out_copy.c" +static inline int enqueue_used(ring_handle_t *ring, buff_desc_t buffer) +{ + return enqueue(ring->used_ring, buffer); +} +# 181 "out_copy.c" +static inline buff_desc_t dequeue_free(ring_handle_t *ring) +{ + return dequeue(ring->free_ring); +} +# 194 "out_copy.c" +static inline buff_desc_t dequeue_used(ring_handle_t *ring) +{ + return dequeue(ring->used_ring); +} +# 208 "out_copy.c" +void ring_init(ring_handle_t *ring, ring_buffer_t *free, ring_buffer_t *used, uint32_t free_size, uint32_t used_size); +# 218 "out_copy.c" +static inline void buffers_init(ring_buffer_t *free_ring, uintptr_t base_addr, uint32_t ring_size, uint32_t buffer_size) +{ + for (int i = 0; i < ring_size - 1; i++) { + buff_desc_t buffer = {(buffer_size * i) + base_addr, 0, ((void *) 0)}; + int err __attribute__((unused)) = enqueue(free_ring, buffer); + assert(!err); + } +} + + + + + + +static inline void request_signal(ring_buffer_t *ring_buffer) +{ + ring_buffer->consumer_signalled = 0; + if (0) ; +} + + + + + + +static inline void cancel_signal(ring_buffer_t *ring_buffer) +{ + ring_buffer->consumer_signalled = 1; + if (0) ; +} + + + + + + +static inline bool require_signal(ring_buffer_t *ring_buffer) +{ + return !ring_buffer->consumer_signalled; +} +# 269 "out_copy.c" +ring_handle_t rx_ring_mux; +ring_handle_t rx_ring_cli; + + +uintptr_t rx_free_mux; +uintptr_t rx_used_mux; +uintptr_t rx_free_cli; +uintptr_t rx_used_cli; + + +uintptr_t mux_buffer_data_region; +uintptr_t cli_buffer_data_region; + +uintptr_t uart_base; + +void rx_return(void) +{ + bool enqueued = 0; + bool reprocess = 1; + + while (reprocess) { + while (!ring_empty(rx_ring_mux.used_ring) && !ring_empty(rx_ring_cli.free_ring) && + !ring_full(rx_ring_mux.free_ring) && !ring_full(rx_ring_cli.used_ring)) { + buff_desc_t cli_buffer, mux_buffer; + int err; + cli_buffer = dequeue_free(&rx_ring_cli); + + if (cli_buffer.phys_or_offset % 2048 || cli_buffer.phys_or_offset >= 2048 * 512) { + ((void) 0); + err = enqueue_free(&rx_ring_cli, cli_buffer); + assert(!err); + } else { + mux_buffer = dequeue_used(&rx_ring_mux); + + uintptr_t cli_addr = cli_buffer_data_region + cli_buffer.phys_or_offset; + uintptr_t mux_addr = mux_buffer_data_region + mux_buffer.phys_or_offset; + + memcpy((void *)cli_addr, (void *)mux_addr, mux_buffer.len); + cli_buffer.len = mux_buffer.len; + mux_buffer.len = 0; + + err = enqueue_used(&rx_ring_cli, cli_buffer); + assert(!err); + + err = enqueue_free(&rx_ring_mux, mux_buffer); + assert(!err); + + enqueued = 1; + } + + } + + request_signal(rx_ring_mux.used_ring); + + + if (!ring_empty(rx_ring_mux.used_ring)) request_signal(rx_ring_cli.free_ring); + else cancel_signal(rx_ring_cli.free_ring); + + reprocess = 0; + + if (!ring_empty(rx_ring_mux.used_ring) && !ring_empty(rx_ring_cli.free_ring) && + !ring_full(rx_ring_mux.free_ring) && !ring_full(rx_ring_cli.used_ring)) { + cancel_signal(rx_ring_mux.used_ring); + cancel_signal(rx_ring_cli.free_ring); + reprocess = 1; + } + } + + if (enqueued && require_signal(rx_ring_cli.used_ring)) { + cancel_signal(rx_ring_cli.used_ring); + sel4cp_notify(1); + } + + if (enqueued && require_signal(rx_ring_mux.free_ring)) { + cancel_signal(rx_ring_mux.free_ring); + sel4cp_notify_delayed(0); + } +} + +void notified(sel4cp_channel ch) +{ + rx_return(); +} + +void init(void) +{ + ring_init(&rx_ring_mux, (ring_buffer_t *)rx_free_mux, (ring_buffer_t *)rx_used_mux, 512, 512); + ring_init(&rx_ring_cli, (ring_buffer_t *)rx_free_cli, (ring_buffer_t *)rx_used_cli, 512, 512); + + buffers_init(rx_ring_cli.free_ring, 0, 512, 2048); +} diff --git a/examples/out_copy.txt b/examples/out_copy.txt new file mode 100644 index 0000000..5aadb5a --- /dev/null +++ b/examples/out_copy.txt @@ -0,0 +1,300 @@ +Struct tmp.ring_handle_C 16 8 +StructField free_ring_C Word 64 0 +StructField used_ring_C Word 64 8 +Struct tmp.ring_buffer_C 12304 8 +StructField head_C Word 32 0 +StructField tail_C Word 32 4 +StructField buffers_C Array Struct tmp.buff_desc_C 512 8 +StructField size_C Word 32 12296 +StructField consumer_signalled_C Word 8 12300 +Struct tmp.buff_desc_C 24 8 +StructField phys_or_offset_C Word 64 0 +StructField len_C Word 16 8 +StructField cookie_C Word 64 16 + +Function tmp.init 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Call 1 tmp.buffers_init 8 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_cli Word 64 Op WordCastSigned Word 64 1 Num 0 Word 32 Op WordCastSigned Word 32 1 Num 512 Word 32 Op WordCastSigned Word 32 1 Num 2048 Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +3 Cond 2 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +4 Call 3 tmp.ring_init 9 Symbol rx_ring_cli Word 64 Num 0 Word 64 Num 0 Word 64 Op WordCastSigned Word 32 1 Num 512 Word 32 Op WordCastSigned Word 32 1 Num 512 Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +5 Cond 4 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +6 Call 5 tmp.ring_init 9 Symbol rx_ring_mux Word 64 Num 0 Word 64 Num 0 Word 64 Op WordCastSigned Word 32 1 Num 512 Word 32 Op WordCastSigned Word 32 1 Num 512 Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +7 Cond 6 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +EntryPoint 7 + +Function tmp.assert 5 b___unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 + +Function tmp.memcpy 7 dest___ptr_to_void#v Word 64 src___ptr_to_void#v Word 64 n___unsigned_long#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 5 ret__ptr_to_void#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 + +Function tmp.dequeue 5 ring___ptr_to_struct_ring_buffer_C#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 7 ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 ret__struct_buff_desc_C#v.len_C Word 16 ret__struct_buff_desc_C#v.cookie_C Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 Err Op False Bool 0 +3 Basic 1 3 ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 Var buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 ret__struct_buff_desc_C#v.len_C Word 16 Var buffer___struct_buff_desc_C#v.len_C Word 16 ret__struct_buff_desc_C#v.cookie_C Word 64 Var buffer___struct_buff_desc_C#v.cookie_C Word 64 +4 Basic 3 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 4 Word 64 Op Modulus Word 32 2 Op Plus Word 32 2 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 4 Word 64 Op WordCastSigned Word 32 1 Num 1 Word 32 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 12296 Word 64 +5 Cond 4 Err Op And Bool 2 Op And Bool 2 Op And Bool 2 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op Not Bool 1 Op Equals Bool 2 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 12296 Word 64 Num 0 Word 32 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 +6 Cond 5 5 Op Not Bool 1 Op Equals Bool 2 Num 0 Word 32 Num 0 Word 32 +7 Basic 6 3 buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 8 Word 64 Op Plus Word 64 2 Op Times Word 64 2 Num 24 Word 64 Op WordCast Word 64 1 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 4 Word 64 Num 0 Word 64 buffer___struct_buff_desc_C#v.len_C Word 16 Op MemAcc Word 16 2 Var Mem Mem Op Plus Word 64 2 Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 8 Word 64 Op Plus Word 64 2 Op Times Word 64 2 Num 24 Word 64 Op WordCast Word 64 1 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 4 Word 64 Num 8 Word 64 buffer___struct_buff_desc_C#v.cookie_C Word 64 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 8 Word 64 Op Plus Word 64 2 Op Times Word 64 2 Num 24 Word 64 Op WordCast Word 64 1 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 4 Word 64 Num 16 Word 64 +8 Cond 7 Err Op And Bool 2 Op And Bool 2 Op Less Bool 2 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 4 Word 64 Op WordCastSigned Word 32 1 Num 512 Word 32 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 +9 Call 8 tmp.assert 5 Op WordCastSigned Word 8 1 Num 0 Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +10 Cond 9 8 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 +11 Basic 10 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +12 Call 11 tmp.ring_empty 5 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +EntryPoint 12 + +Function tmp.enqueue 8 ring___ptr_to_struct_ring_buffer_C#v Word 64 buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 buffer___struct_buff_desc_C#v.len_C Word 16 buffer___struct_buff_desc_C#v.cookie_C Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 5 ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 Err Op False Bool 0 +3 Basic 1 1 ret__int#v Word 32 Num 0 Word 32 +4 Basic 3 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op Modulus Word 32 2 Op Plus Word 32 2 Op MemAcc Word 32 2 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op WordCastSigned Word 32 1 Num 1 Word 32 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 12296 Word 64 +5 Cond 4 Err Op And Bool 2 Op And Bool 2 Op And Bool 2 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op Not Bool 1 Op Equals Bool 2 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 12296 Word 64 Num 0 Word 32 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 +6 Cond 5 5 Op Not Bool 1 Op Equals Bool 2 Num 0 Word 32 Num 0 Word 32 +7 Basic 6 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Op Plus Word 64 2 Op Plus Word 64 2 Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 8 Word 64 Op Times Word 64 2 Op WordCast Word 64 1 Op MemAcc Word 32 2 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 24 Word 64 Num 16 Word 64 Var buffer___struct_buff_desc_C#v.cookie_C Word 64 +8 Cond 7 Err Op And Bool 2 Op And Bool 2 Op Less Bool 2 Op MemAcc Word 32 2 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op WordCastSigned Word 32 1 Num 512 Word 32 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 +9 Basic 8 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Op Plus Word 64 2 Op Plus Word 64 2 Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 8 Word 64 Op Times Word 64 2 Op WordCast Word 64 1 Op MemAcc Word 32 2 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 24 Word 64 Num 8 Word 64 Var buffer___struct_buff_desc_C#v.len_C Word 16 +10 Cond 9 Err Op And Bool 2 Op And Bool 2 Op Less Bool 2 Op MemAcc Word 32 2 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op WordCastSigned Word 32 1 Num 512 Word 32 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 +11 Basic 10 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Op Plus Word 64 2 Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 8 Word 64 Op Times Word 64 2 Op WordCast Word 64 1 Op MemAcc Word 32 2 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 24 Word 64 Var buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 +12 Cond 11 Err Op And Bool 2 Op And Bool 2 Op Less Bool 2 Op MemAcc Word 32 2 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op WordCastSigned Word 32 1 Num 512 Word 32 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 +13 Basic 1 1 ret__int#v Word 32 Op Minus Word 32 2 Num 0 Word 32 Num 1 Word 32 +14 Cond 13 Err Op Equals Bool 2 Op SignedLessEquals Bool 2 Num 0 Word 32 Op Minus Word 32 2 Num 0 Word 32 Num 1 Word 32 Op SignedLessEquals Bool 2 Num 1 Word 32 Num 0 Word 32 +15 Cond 14 12 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 +16 Basic 15 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +17 Call 16 tmp.ring_full 5 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +EntryPoint 17 + +Function tmp.notified 5 ch___unsigned#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Call 1 tmp.rx_return 4 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +EntryPoint 2 + +Function tmp.ring_full 5 ring___ptr_to_struct_ring_buffer_C#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 5 ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 Err Op False Bool 0 +3 Basic 1 1 ret__unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Op IfThenElse Word 32 3 Op Equals Bool 2 Op Modulus Word 32 2 Op Plus Word 32 2 Op MemAcc Word 32 2 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op WordCastSigned Word 32 1 Num 1 Word 32 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 12296 Word 64 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 4 Word 64 Num 1 Word 32 Num 0 Word 32 +4 Cond 3 Err Op And Bool 2 Op And Bool 2 Op And Bool 2 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op Not Bool 1 Op Equals Bool 2 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 12296 Word 64 Num 0 Word 32 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 +EntryPoint 4 + +Function tmp.ring_init 9 ring___ptr_to_struct_ring_handle_C#v Word 64 free___ptr_to_struct_ring_buffer_C#v Word 64 used___ptr_to_struct_ring_buffer_C#v Word 64 free_size___unsigned#v Word 32 used_size___unsigned#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 + +Function tmp.ring_size 5 ring___ptr_to_struct_ring_buffer_C#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 5 ret__unsigned#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 Err Op False Bool 0 +3 Basic 1 1 ret__unsigned#v Word 32 Op Modulus Word 32 2 Op Minus Word 32 2 Op Plus Word 32 2 Op MemAcc Word 32 2 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 12296 Word 64 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 4 Word 64 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 12296 Word 64 +4 Cond 3 Err Op And Bool 2 Op And Bool 2 Op And Bool 2 Op And Bool 2 Op Not Bool 1 Op Equals Bool 2 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 12296 Word 64 Num 0 Word 32 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 +EntryPoint 4 + +Function tmp.rx_return 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Call 1 tmp.sel4cp_notify_delayed 5 Op WordCastSigned Word 32 1 Num 0 Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +3 Call 2 tmp.cancel_signal 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_mux Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +4 Cond 3 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +5 Cond 4 1 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +6 Basic 5 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +7 Basic 6 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +8 Call 7 tmp.require_signal 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_mux Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +9 Cond 8 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +10 Cond 9 5 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +11 Basic 10 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Equals Bool 2 Var enqueued___unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +12 Call 11 tmp.sel4cp_notify 5 Op WordCastSigned Word 32 1 Num 1 Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +13 Call 12 tmp.cancel_signal 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_cli Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +14 Cond 13 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +15 Cond 14 11 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +16 Basic 15 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +17 Basic 16 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +18 Call 17 tmp.require_signal 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_cli Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +19 Cond 18 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +20 Cond 19 15 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +21 Basic 20 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Equals Bool 2 Var enqueued___unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +26 Basic 22 1 reprocess___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 1 Word 32 +27 Call 26 tmp.cancel_signal 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_cli Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +28 Cond 27 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +29 Call 28 tmp.cancel_signal 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_mux Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +30 Cond 29 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +31 Cond 30 22 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +32 Basic 31 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +33 Basic 32 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +34 Call 33 tmp.ring_full 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_cli Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +35 Cond 34 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +36 Cond 35 31 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +37 Basic 36 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +38 Basic 37 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +39 Call 38 tmp.ring_full 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_mux Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +40 Cond 39 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +41 Cond 40 36 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +42 Basic 41 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +43 Basic 42 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +44 Call 43 tmp.ring_empty 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_cli Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +45 Cond 44 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +46 Cond 45 41 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +47 Basic 46 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +48 Basic 47 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +49 Call 48 tmp.ring_empty 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_mux Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +50 Cond 49 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +51 Basic 50 1 reprocess___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 0 Word 32 +52 Call 51 tmp.request_signal 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_cli Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +53 Cond 52 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +54 Call 51 tmp.cancel_signal 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_cli Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +55 Cond 54 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +56 Cond 53 55 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 +57 Basic 56 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +58 Call 57 tmp.ring_empty 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_mux Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +59 Cond 58 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +60 Call 59 tmp.request_signal 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_mux Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +61 Cond 60 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +66 Basic 62 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +67 Basic 66 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +68 Call 67 tmp.ring_full 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_cli Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +69 Cond 68 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +70 Cond 69 62 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +71 Basic 70 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +72 Basic 71 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +73 Call 72 tmp.ring_full 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_mux Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +74 Cond 73 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +75 Cond 74 70 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +76 Basic 75 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +77 Basic 76 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +78 Call 77 tmp.ring_empty 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_cli Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +79 Cond 78 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +80 Cond 79 75 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +81 Basic 80 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +82 Basic 81 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +83 Call 82 tmp.ring_empty 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_mux Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +84 Cond 83 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +85 Call 84 tmp.assert 5 Op WordCastSigned Word 8 1 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var err___int#v Word 32 Num 0 Word 32 Num 1 Word 32 Num 0 Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +86 Basic 85 1 err___int#v Word 32 Var rv#space#ret__int#v Word 32 +87 Call 86 tmp.enqueue_free 8 Symbol rx_ring_cli Word 64 Var cli_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Var cli_buffer___struct_buff_desc_C#v.len_C Word 16 Var cli_buffer___struct_buff_desc_C#v.cookie_C Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +88 Cond 87 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +89 Basic 84 1 enqueued___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 1 Word 32 +90 Call 89 tmp.assert 5 Op WordCastSigned Word 8 1 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var err___int#v Word 32 Num 0 Word 32 Num 1 Word 32 Num 0 Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +91 Basic 90 1 err___int#v Word 32 Var rv#space#ret__int#v Word 32 +92 Call 91 tmp.enqueue_free 8 Symbol rx_ring_mux Word 64 Var mux_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Var mux_buffer___struct_buff_desc_C#v.len_C Word 16 Var mux_buffer___struct_buff_desc_C#v.cookie_C Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +93 Cond 92 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +94 Call 93 tmp.assert 5 Op WordCastSigned Word 8 1 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var err___int#v Word 32 Num 0 Word 32 Num 1 Word 32 Num 0 Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +95 Basic 94 1 err___int#v Word 32 Var rv#space#ret__int#v Word 32 +96 Call 95 tmp.enqueue_used 8 Symbol rx_ring_cli Word 64 Var cli_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Var cli_buffer___struct_buff_desc_C#v.len_C Word 16 Var cli_buffer___struct_buff_desc_C#v.cookie_C Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +97 Cond 96 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +98 Basic 97 1 mux_buffer___struct_buff_desc_C#v.len_C Word 16 Op WordCastSigned Word 16 1 Num 0 Word 32 +99 Basic 98 1 cli_buffer___struct_buff_desc_C#v.len_C Word 16 Var mux_buffer___struct_buff_desc_C#v.len_C Word 16 +100 Call 99 tmp.memcpy 7 Var cli_addr___unsigned_long#v Word 64 Var mux_addr___unsigned_long#v Word 64 Op WordCast Word 64 1 Var mux_buffer___struct_buff_desc_C#v.len_C Word 16 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__ptr_to_void#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +101 Basic 100 1 mux_addr___unsigned_long#v Word 64 Op Plus Word 64 2 Num 0 Word 64 Var mux_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 +102 Basic 101 1 cli_addr___unsigned_long#v Word 64 Op Plus Word 64 2 Num 0 Word 64 Var cli_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 +103 Basic 102 3 mux_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Var rv#space#ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 mux_buffer___struct_buff_desc_C#v.len_C Word 16 Var rv#space#ret__struct_buff_desc_C#v.len_C Word 16 mux_buffer___struct_buff_desc_C#v.cookie_C Word 64 Var rv#space#ret__struct_buff_desc_C#v.cookie_C Word 64 +104 Call 103 tmp.dequeue_used 5 Symbol rx_ring_mux Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 7 rv#space#ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 rv#space#ret__struct_buff_desc_C#v.len_C Word 16 rv#space#ret__struct_buff_desc_C#v.cookie_C Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +105 Cond 104 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +106 Cond 88 105 Op Or Bool 2 Op Not Bool 1 Op Equals Bool 2 Op Modulus Word 64 2 Var cli_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Op WordCastSigned Word 64 1 Num 2048 Word 32 Num 0 Word 64 Op LessEquals Bool 2 Op WordCastSigned Word 64 1 Op Times Word 32 2 Num 2048 Word 32 Num 512 Word 32 Var cli_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 +107 Cond 106 Err Op And Bool 2 Op Equals Bool 2 Op Times Word 64 2 Op WordCastSigned Word 64 1 Num 2048 Word 32 Op WordCastSigned Word 64 1 Num 512 Word 32 Op WordCastSigned Word 64 1 Op Times Word 32 2 Num 2048 Word 32 Num 512 Word 32 Op Not Bool 1 Op Equals Bool 2 Num 2048 Word 32 Num 0 Word 32 +108 Basic 107 3 cli_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Var rv#space#ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 cli_buffer___struct_buff_desc_C#v.len_C Word 16 Var rv#space#ret__struct_buff_desc_C#v.len_C Word 16 cli_buffer___struct_buff_desc_C#v.cookie_C Word 64 Var rv#space#ret__struct_buff_desc_C#v.cookie_C Word 64 +109 Call 108 tmp.dequeue_free 5 Symbol rx_ring_cli Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 7 rv#space#ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 rv#space#ret__struct_buff_desc_C#v.len_C Word 16 rv#space#ret__struct_buff_desc_C#v.cookie_C Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +110 Cond 109 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +62 Basic 63 1 loop#62#count Word 64 Op Plus Word 64 2 Var loop#62#count Word 64 Num 1 Word 64 +63 Cond 64 Err Op True Bool 0 +64 Cond 110 61 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +65 Basic 63 1 loop#62#count Word 64 Num 0 Word 64 +111 Basic 65 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +112 Basic 111 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +113 Call 112 tmp.ring_full 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_cli Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +114 Cond 113 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +115 Cond 114 65 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +116 Basic 115 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +117 Basic 116 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +118 Call 117 tmp.ring_full 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_mux Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +119 Cond 118 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +120 Cond 119 115 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +121 Basic 120 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +122 Basic 121 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +123 Call 122 tmp.ring_empty 5 Op MemAcc Word 64 2 Var Mem Mem Symbol rx_ring_cli Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +124 Cond 123 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 +125 Cond 124 120 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 +126 Basic 125 1 ret__int#v Word 32 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +127 Basic 126 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +128 Call 127 tmp.ring_empty 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Symbol rx_ring_mux Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +129 Cond 128 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 +22 Basic 23 1 loop#22#count Word 64 Op Plus Word 64 2 Var loop#22#count Word 64 Num 1 Word 64 +23 Cond 24 Err Op True Bool 0 +24 Cond 129 21 Op Not Bool 1 Op Equals Bool 2 Var reprocess___unsigned_char#v Word 8 Num 0 Word 8 +25 Basic 23 1 loop#22#count Word 64 Num 0 Word 64 +130 Basic 25 1 reprocess___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 1 Word 32 +131 Basic 130 1 enqueued___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 0 Word 32 +EntryPoint 131 + +Function tmp.ring_empty 5 ring___ptr_to_struct_ring_buffer_C#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 5 ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 Err Op False Bool 0 +3 Basic 1 1 ret__unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Op IfThenElse Word 32 3 Op Equals Bool 2 Op MemAcc Word 32 2 Var Mem Mem Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op MemAcc Word 32 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Num 4 Word 64 Num 1 Word 32 Num 0 Word 32 +4 Cond 3 Err Op And Bool 2 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring___ptr_to_struct_ring_buffer_C#v Word 64 +EntryPoint 4 + +Function tmp.buffers_init 8 free_ring___ptr_to_struct_ring_buffer_C#v Word 64 base_addr___unsigned_long#v Word 64 ring_size___unsigned#v Word 32 buffer_size___unsigned#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +6 Basic 2 1 i___int#v Word 32 Op Plus Word 32 2 Var i___int#v Word 32 Num 1 Word 32 +7 Cond 6 Err Op Equals Bool 2 Op SignedLessEquals Bool 2 Var i___int#v Word 32 Op Plus Word 32 2 Var i___int#v Word 32 Num 1 Word 32 Op SignedLessEquals Bool 2 Num 0 Word 32 Num 1 Word 32 +8 Call 7 tmp.assert 5 Op WordCastSigned Word 8 1 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var err___int#v Word 32 Num 0 Word 32 Num 1 Word 32 Num 0 Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +9 Basic 8 1 err___int#v Word 32 Var rv#space#ret__int#v Word 32 +10 Call 9 tmp.enqueue 8 Var free_ring___ptr_to_struct_ring_buffer_C#v Word 64 Var buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Var buffer___struct_buff_desc_C#v.len_C Word 16 Var buffer___struct_buff_desc_C#v.cookie_C Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +11 Basic 10 3 buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Op Plus Word 64 2 Op WordCast Word 64 1 Op Times Word 32 2 Var buffer_size___unsigned#v Word 32 Op WordCastSigned Word 32 1 Var i___int#v Word 32 Var base_addr___unsigned_long#v Word 64 buffer___struct_buff_desc_C#v.len_C Word 16 Op WordCastSigned Word 16 1 Num 0 Word 32 buffer___struct_buff_desc_C#v.cookie_C Word 64 Op WordCastSigned Word 64 1 Num 0 Word 32 +2 Basic 3 1 loop#2#count Word 64 Op Plus Word 64 2 Var loop#2#count Word 64 Num 1 Word 64 +3 Cond 4 Err Op True Bool 0 +4 Cond 11 1 Op Less Bool 2 Op WordCastSigned Word 32 1 Var i___int#v Word 32 Op Minus Word 32 2 Var ring_size___unsigned#v Word 32 Op WordCastSigned Word 32 1 Num 1 Word 32 +5 Basic 3 1 loop#2#count Word 64 Num 0 Word 64 +12 Basic 5 1 i___int#v Word 32 Num 0 Word 32 +EntryPoint 12 + +Function tmp.dequeue_free 5 ring___ptr_to_struct_ring_handle_C#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 7 ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 ret__struct_buff_desc_C#v.len_C Word 16 ret__struct_buff_desc_C#v.cookie_C Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 Err Op False Bool 0 +3 Basic 1 0 +4 Basic 3 3 ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 Var rv#space#ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 ret__struct_buff_desc_C#v.len_C Word 16 Var rv#space#ret__struct_buff_desc_C#v.len_C Word 16 ret__struct_buff_desc_C#v.cookie_C Word 64 Var rv#space#ret__struct_buff_desc_C#v.cookie_C Word 64 +5 Call 4 tmp.dequeue 5 Op MemAcc Word 64 2 Var Mem Mem Var ring___ptr_to_struct_ring_handle_C#v Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 7 rv#space#ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 rv#space#ret__struct_buff_desc_C#v.len_C Word 16 rv#space#ret__struct_buff_desc_C#v.cookie_C Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +6 Cond 5 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Var ring___ptr_to_struct_ring_handle_C#v Word 64 +EntryPoint 6 + +Function tmp.dequeue_used 5 ring___ptr_to_struct_ring_handle_C#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 7 ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 ret__struct_buff_desc_C#v.len_C Word 16 ret__struct_buff_desc_C#v.cookie_C Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 Err Op False Bool 0 +3 Basic 1 0 +4 Basic 3 3 ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 Var rv#space#ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 ret__struct_buff_desc_C#v.len_C Word 16 Var rv#space#ret__struct_buff_desc_C#v.len_C Word 16 ret__struct_buff_desc_C#v.cookie_C Word 64 Var rv#space#ret__struct_buff_desc_C#v.cookie_C Word 64 +5 Call 4 tmp.dequeue 5 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_handle_C#v Word 64 Num 8 Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 7 rv#space#ret__struct_buff_desc_C#v.phys_or_offset_C Word 64 rv#space#ret__struct_buff_desc_C#v.len_C Word 16 rv#space#ret__struct_buff_desc_C#v.cookie_C Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +6 Cond 5 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Var ring___ptr_to_struct_ring_handle_C#v Word 64 +EntryPoint 6 + +Function tmp.enqueue_free 8 ring___ptr_to_struct_ring_handle_C#v Word 64 buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 buffer___struct_buff_desc_C#v.len_C Word 16 buffer___struct_buff_desc_C#v.cookie_C Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 5 ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 Err Op False Bool 0 +3 Basic 1 0 +4 Basic 3 1 ret__int#v Word 32 Var rv#space#ret__int#v Word 32 +5 Call 4 tmp.enqueue 8 Op MemAcc Word 64 2 Var Mem Mem Var ring___ptr_to_struct_ring_handle_C#v Word 64 Var buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Var buffer___struct_buff_desc_C#v.len_C Word 16 Var buffer___struct_buff_desc_C#v.cookie_C Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +6 Cond 5 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Var ring___ptr_to_struct_ring_handle_C#v Word 64 +EntryPoint 6 + +Function tmp.enqueue_used 8 ring___ptr_to_struct_ring_handle_C#v Word 64 buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 buffer___struct_buff_desc_C#v.len_C Word 16 buffer___struct_buff_desc_C#v.cookie_C Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 5 ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 Err Op False Bool 0 +3 Basic 1 0 +4 Basic 3 1 ret__int#v Word 32 Var rv#space#ret__int#v Word 32 +5 Call 4 tmp.enqueue 8 Op MemAcc Word 64 2 Var Mem Mem Op Plus Word 64 2 Var ring___ptr_to_struct_ring_handle_C#v Word 64 Num 8 Word 64 Var buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 Var buffer___struct_buff_desc_C#v.len_C Word 16 Var buffer___struct_buff_desc_C#v.cookie_C Word 64 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 50 64 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +6 Cond 5 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Var ring___ptr_to_struct_ring_handle_C#v Word 64 +EntryPoint 6 + +Function tmp.cancel_signal 5 ring_buffer___ptr_to_struct_ring_buffer_C#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 1 Op Not Bool 1 Op Equals Bool 2 Num 0 Word 32 Num 0 Word 32 +3 Basic 2 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Op Plus Word 64 2 Var ring_buffer___ptr_to_struct_ring_buffer_C#v Word 64 Num 12300 Word 64 Op WordCastSigned Word 8 1 Num 1 Word 32 +4 Cond 3 Err Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring_buffer___ptr_to_struct_ring_buffer_C#v Word 64 +EntryPoint 4 + +Function tmp.sel4cp_notify 5 ch___unsigned#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 + +Function tmp.request_signal 5 ring_buffer___ptr_to_struct_ring_buffer_C#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 1 Op Not Bool 1 Op Equals Bool 2 Num 0 Word 32 Num 0 Word 32 +3 Basic 2 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Op Plus Word 64 2 Var ring_buffer___ptr_to_struct_ring_buffer_C#v Word 64 Num 12300 Word 64 Op WordCastSigned Word 8 1 Num 0 Word 32 +4 Cond 3 Err Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring_buffer___ptr_to_struct_ring_buffer_C#v Word 64 +EntryPoint 4 + +Function tmp.require_signal 5 ring_buffer___ptr_to_struct_ring_buffer_C#v Word 64 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 5 ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 +1 Basic Ret 0 +2 Cond 1 Err Op False Bool 0 +3 Basic 1 1 ret__unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Op IfThenElse Word 32 3 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Op MemAcc Word 8 2 Var Mem Mem Op Plus Word 64 2 Var ring_buffer___ptr_to_struct_ring_buffer_C#v Word 64 Num 12300 Word 64 Num 0 Word 8 Num 1 Word 32 Num 0 Word 32 +4 Cond 3 Err Op PAlignValid Bool 2 Type Struct tmp.ring_buffer_C Var ring_buffer___ptr_to_struct_ring_buffer_C#v Word 64 +EntryPoint 4 + +Function tmp.sel4cp_notify_delayed 5 ch___unsigned#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 64 diff --git a/ghost_data.py b/ghost_data.py index e802d8b..e1f235b 100644 --- a/ghost_data.py +++ b/ghost_data.py @@ -5,6 +5,7 @@ import monitor_spec import microkit_spec from ghost_data_helpers import * +import copy_spec def get(file_name: str, func_name: str) -> source.Ghost[source.ProgVarName | nip.GuardVarName] | None: @@ -254,5 +255,6 @@ def get(file_name: str, func_name: str) -> source.Ghost[source.ProgVarName | nip loop_iterations={}, loop_invariants={} ) - } + }, + "examples/out_copy.txt": copy_spec.functions_spec } diff --git a/ghost_data_helpers.py b/ghost_data_helpers.py index f81faa3..ea9a1d8 100644 --- a/ghost_data_helpers.py +++ b/ghost_data_helpers.py @@ -9,10 +9,12 @@ mul = source.expr_mul plus = source.expr_plus sub = source.expr_sub +mod = source.expr_mod slt = source.expr_slt sle = source.expr_sle ule = source.expr_ule +ult = source.expr_ult eq = source.expr_eq neq = source.expr_neq neg = source.expr_negate @@ -22,6 +24,8 @@ ite = source.expr_ite +bv8eq = source.bv8_expr_eq + i32ret = source.ExprVar(source.type_word32, source.CRetSpecialVar("c_ret.0")) i32ret.name.field_num = 0 @@ -118,3 +122,14 @@ def mem_acc(ty: source.Type, v: source.ExprT[source.ProgVarName], mem: source.Ex assert mem.typ == source.type_mem, "Mem typ is wrong" return source.ExprOp(ty, source.Operator.MEM_ACC, (mem, v, )) + +def mem_upd(ty: source.Type, loc: source.ExprT[source.ProgVarName],val: source.ExprT[source.ProgVarName], mem: source.ExprT[source.ProgVarName]) -> source.ExprT[source.ProgVarName]: + assert mem.typ == source.type_mem, "Mem typ is wrong" + if ty != val.typ: + print(ty, " != ", val.typ) + print(val) + assert ty == val.typ + return source.ExprOp(source.type_mem, source.Operator.MEM_UPDATE, (mem, loc, val, )) + +def ucast(ty: source.Type, e: source.ExprT[source.ProgVarName]): + return source.ExprOp(ty, source.Operator.WORD_CAST, (e, )) diff --git a/out-model.smt2 b/out-model.smt2 new file mode 100644 index 0000000..d5490b3 --- /dev/null +++ b/out-model.smt2 @@ -0,0 +1,374 @@ +sat +sat +( + ;; universe for HTD: + ;; HTD!val!0 + ;; ----------- + ;; definitions for universe elements: + (declare-fun HTD!val!0 () HTD) + ;; cardinality constraint: + (forall ((x HTD)) (= x HTD!val!0)) + ;; ----------- + ;; universe for PMS: + ;; PMS!val!0 + ;; ----------- + ;; definitions for universe elements: + (declare-fun PMS!val!0 () PMS) + ;; cardinality constraint: + (forall ((x PMS)) (= x PMS!val!0)) + ;; ----------- + (define-fun node_upd_n7_ok () Bool + true) + (define-fun node_guard_n15_ok () Bool + false) + (define-fun Mem@assigned~2 () Bool + true) + (define-fun node_upd_n17_ok () Bool + false) + (define-fun HTD~1 () HTD + HTD!val!0) + (define-fun Mem~5 () (Array (_ BitVec 64) (_ BitVec 8)) + (_ as-array k!54)) + (define-fun ret__unsigned_char@v@assigned~1 () Bool + false) + (define-fun node_upd_n13_ok () Bool + false) + (define-fun ret__int@v@assigned~1 () Bool + false) + (define-fun PMS/subject-arg~1 () PMS + PMS!val!0) + (define-fun node_15_ok () Bool + false) + (define-fun rv@space@ret__unsigned_char@v@assigned~1 () Bool + false) + (define-fun buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1 () Bool + true) + (define-fun Mem/call-arg~1 () (Array (_ BitVec 64) (_ BitVec 8)) + (let ((a!1 (store (store (store ((as const (Array (_ BitVec 64) (_ BitVec 8))) + #x00) + #xfefffffec0003007 + #xae) + #xfefffffebffffffe + #x1b) + #xfefffffec0003009 + #x4d))) + (store (store (store (store a!1 #xfefffffec0003006 #xcd) + #x0000000000000000 + #x44) + #xfefffffec0000002 + #x1c) + #xfefffffec0003008 + #x5f))) + (define-fun PMS@assigned~1 () Bool + true) + (define-fun Mem@assigned~6 () Bool + false) + (define-fun node_guard_n11_ok () Bool + true) + (define-fun node_10_ok () Bool + true) + (define-fun node_Ret_ok () Bool + true) + (define-fun node_9_ok () Bool + true) + (define-fun PMS/call-arg~1 () PMS + PMS!val!0) + (define-fun node_17_ok () Bool + false) + (define-fun node_upd_n4_ok () Bool + true) + (define-fun node_16_ok () Bool + false) + (define-fun node_Err_ok () Bool + false) + (define-fun node_upd_n3_ok () Bool + true) + (define-fun Mem@assigned~1 () Bool + true) + (define-fun node_6_ok () Bool + true) + (define-fun node_5_ok () Bool + true) + (define-fun node_upd_n9_ok () Bool + false) + (define-fun node_guard_n17_ok () Bool + false) + (define-fun node_guard_n7_ok () Bool + true) + (define-fun node_1_ok () Bool + false) + (define-fun node_guard_n16_ok () Bool + false) + (define-fun node_j2_ok () Bool + false) + (define-fun node_guard_n12_ok () Bool + true) + (define-fun node_guard_n4_ok () Bool + true) + (define-fun node_3_ok () Bool + true) + (define-fun Mem@assigned~4 () Bool + true) + (define-fun buffer___struct_buff_desc_C@v.len_C/subject-arg~1 () (_ BitVec 16) + #x0000) + (define-fun Mem~1 () (Array (_ BitVec 64) (_ BitVec 8)) + (let ((a!1 (store (store (store ((as const (Array (_ BitVec 64) (_ BitVec 8))) + #x00) + #xfefffffec0003007 + #xae) + #xfefffffebffffffe + #x1b) + #xfefffffec0003009 + #x4d))) + (store (store (store (store a!1 #xfefffffec0003006 #xcd) + #x0000000000000000 + #x44) + #xfefffffec0000002 + #x1c) + #xfefffffec0003008 + #x5f))) + (define-fun node_call_pre_17_pred_1_ok () Bool + false) + (define-fun Mem@assigned~5 () Bool + true) + (define-fun rv@space@ret__unsigned_char@v@assigned~2 () Bool + true) + (define-fun node_14_ok () Bool + false) + (define-fun node_j1_ok () Bool + true) + (define-fun ret__int@v~1 () (_ BitVec 32) + #xffffffff) + (define-fun Mem~4 () (Array (_ BitVec 64) (_ BitVec 8)) + (let ((a!1 (store (store (store ((as const (Array (_ BitVec 64) (_ BitVec 8))) + #x01) + #xfefffffec0000001 + #xca) + #xfefffffebfffffff + #x0b) + #x0000010000000000 + #x20))) + (store (store (store a!1 #xfefffffebffffffe #x19) #x0000000000000000 #xc6) + #xfefffffec0000000 + #xac))) + (define-fun eval_val4 () (_ BitVec 32) + #x4d5faecd) + (define-fun rv@space@ret__unsigned_char@v~1 () (_ BitVec 8) + #x01) + (define-fun GhostAssertions~1 () (Array (_ BitVec 50) (_ BitVec 64)) + ((as const (Array (_ BitVec 50) (_ BitVec 64))) #x0000000000000000)) + (define-fun buffer___struct_buff_desc_C@v.cookie_C@assigned~1 () Bool + true) + (define-fun node_11_ok () Bool + true) + (define-fun node_12_ok () Bool + true) + (define-fun buffer___struct_buff_desc_C@v.cookie_C~1 () (_ BitVec 64) + #x0000000000000000) + (define-fun HTD/call-arg~1 () HTD + HTD!val!0) + (define-fun node_call_post_17_ok () Bool + false) + (define-fun eval_val1 () (_ BitVec 32) + #x0000001b) + (define-fun node_upd_n11_ok () Bool + true) + (define-fun node_upd_n16_ok () Bool + false) + (define-fun ring___ptr_to_struct_ring_buffer_C@v@assigned~1 () Bool + true) + (define-fun node_guard_n5_ok () Bool + true) + (define-fun Mem~2 () (Array (_ BitVec 64) (_ BitVec 8)) + (let ((a!1 (store (store (store ((as const (Array (_ BitVec 64) (_ BitVec 8))) + #x00) + #xfefffffec0003007 + #xae) + #xfefffffebffffffe + #x1b) + #xfefffffec0003009 + #x4d))) + (store (store (store (store a!1 #xfefffffec0003006 #xcd) + #x0000000000000000 + #x44) + #xfefffffec0000002 + #x1c) + #xfefffffec0003008 + #x5f))) + (define-fun node_8_ok () Bool + false) + (define-fun Mem~6 () (Array (_ BitVec 64) (_ BitVec 8)) + (let ((a!1 (store (store (store ((as const (Array (_ BitVec 64) (_ BitVec 8))) + #x00) + #xfefffffec0003007 + #x08) + #x0000010000000000 + #xdb) + #xfefffffec0000001 + #x08))) +(let ((a!2 (store (store (store (store a!1 #xfefffffebfffffff #x0a) + #xfefffffec0003009 + #x24) + #xfefffffec0003008 + #x40) + #xfefffffec0003006 + #x9c))) + (store a!2 #x0000000000000000 #x09)))) + (define-fun node_13_ok () Bool + false) + (define-fun node_guard_n9_ok () Bool + true) + (define-fun GhostAssertions@assigned~1 () Bool + true) + (define-fun HTD@assigned~2 () Bool + true) + (define-fun buffer___struct_buff_desc_C@v.cookie_C/subject-arg~1 () (_ BitVec 64) + #x0000000000000000) + (define-fun GhostAssertions/call-arg~1 () (Array (_ BitVec 50) (_ BitVec 64)) + ((as const (Array (_ BitVec 50) (_ BitVec 64))) #x0000000000000000)) + (define-fun ret__unsigned_char@v~1 () (_ BitVec 8) + #x01) + (define-fun Mem/subject-arg~1 () (Array (_ BitVec 64) (_ BitVec 8)) + (let ((a!1 (store (store (store ((as const (Array (_ BitVec 64) (_ BitVec 8))) + #x00) + #xfefffffec0003007 + #xae) + #xfefffffebffffffe + #x1b) + #xfefffffec0003009 + #x4d))) + (store (store (store (store a!1 #xfefffffec0003006 #xcd) + #x0000000000000000 + #x44) + #xfefffffec0000002 + #x1c) + #xfefffffec0003008 + #x5f))) + (define-fun Mem@assigned~3 () Bool + true) + (define-fun node_33_ok () Bool + false) + (define-fun HTD/subject-arg~1 () HTD + HTD!val!0) + (define-fun node_call_stash_17_pred_1_ok () Bool + false) + (define-fun node_upd_n33_ok () Bool + false) + (define-fun ring___ptr_to_struct_ring_buffer_C@v~1 () (_ BitVec 64) + #xfefffffebffffffe) + (define-fun buffer___struct_buff_desc_C@v.phys_or_offset_C~1 () (_ BitVec 64) + #x0000000000000000) + (define-fun HTD@assigned~1 () Bool + true) + (define-fun Mem~7 () (Array (_ BitVec 64) (_ BitVec 8)) + (let ((a!1 (store (store (store ((as const (Array (_ BitVec 64) (_ BitVec 8))) + #x00) + #xfefffffec0003007 + #xae) + #xfefffffebffffffe + #x1b) + #xfefffffec0003009 + #x4d))) + (store (store (store (store a!1 #xfefffffec0003006 #xcd) + #x0000000000000000 + #x44) + #xfefffffec0000002 + #x1c) + #xfefffffec0003008 + #x5f))) + (define-fun ret__unsigned_char@v@assigned~2 () Bool + true) + (define-fun node_guard_n8_ok () Bool + false) + (define-fun node_7_ok () Bool + true) + (define-fun node_4_ok () Bool + true) + (define-fun PMS@assigned~2 () Bool + true) + (define-fun node_guard_n10_ok () Bool + true) + (define-fun ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 () (_ BitVec 64) + #xfefffffebffffffe) + (define-fun buffer___struct_buff_desc_C@v.phys_or_offset_C/subject-arg~1 () (_ BitVec 64) + #x0000000000000000) + (define-fun node_pre_condition_ok () Bool + false) + (define-fun GhostAssertions@assigned~2 () Bool + true) + (define-fun ret__int@v@assigned~2 () Bool + true) + (define-fun Mem@assigned~7 () Bool + true) + (define-fun eval_val3 () (_ BitVec 32) + #x0000001b) + (define-fun node_stash_initial_args_ok () Bool + false) + (define-fun node_post_condition_ok () Bool + false) + (define-fun GhostAssertions/subject-arg~1 () (Array (_ BitVec 50) (_ BitVec 64)) + ((as const (Array (_ BitVec 50) (_ BitVec 64))) #x0000000000000000)) + (define-fun ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 () (_ BitVec 64) + #xfefffffebffffffe) + (define-fun Mem~3 () (Array (_ BitVec 64) (_ BitVec 8)) + (let ((a!1 (store (store (store ((as const (Array (_ BitVec 64) (_ BitVec 8))) + #x01) + #xfefffffec0000001 + #x00) + #xfefffffebfffffff + #x00) + #x0000000000400000 + #x06))) + (store (store a!1 #xfefffffebffffffe #x00) #xfefffffec0000000 #x00))) + (define-fun buffer___struct_buff_desc_C@v.len_C@assigned~1 () Bool + true) + (define-fun buffer___struct_buff_desc_C@v.len_C~1 () (_ BitVec 16) + #x0000) + (define-fun eval_val2 () (_ BitVec 32) + #x4d5faecd) + (define-fun PMS~1 () PMS + PMS!val!0) + (define-fun k!42 ((x!0 (_ BitVec 64))) (_ BitVec 8) + (ite (= x!0 #xfefffffec0000001) #x00 + (ite (= x!0 #xfefffffebfffffff) #x00 + (ite (= x!0 #x0000000000400000) #x06 + (ite (= x!0 #xfefffffebffffffe) #x00 + (ite (= x!0 #xfefffffec0000000) #x00 + #x01)))))) + (define-fun k!50 ((x!0 (_ BitVec 64))) (_ BitVec 8) + (ite (= x!0 #xfefffffec0003007) #xae + (ite (= x!0 #xfefffffec0003009) #x4d + (ite (= x!0 #xfefffffebffffffe) #x1b + (ite (= x!0 #xfefffffec0003006) #xcd + (ite (= x!0 #x0000000000000000) #x44 + (ite (= x!0 #xfefffffec0000002) #x1c + (ite (= x!0 #xfefffffec0003008) #x5f + #x00)))))))) + (define-fun k!54 ((x!0 (_ BitVec 64))) (_ BitVec 8) + (ite (= x!0 #xfefffffec0003007) #x08 + (ite (= x!0 #xfefffffec0003009) #x24 + (ite (= x!0 #xfefffffebffffffe) #xff + (ite (= x!0 #xfefffffec0000001) #x08 + (ite (= x!0 #xfefffffebfffffff) #x09 + (ite (= x!0 #x0000010000000000) #xdb + (ite (= x!0 #xfefffffec0003008) #x40 + (ite (= x!0 #xfefffffec0003006) #x9c + (ite (= x!0 #x0000000000000000) #x09 + #x00)))))))))) + (define-fun k!62 ((x!0 (_ BitVec 64))) (_ BitVec 8) + (ite (= x!0 #xff000011c0210a6e) #x00 + (ite (= x!0 #xfefffffebffffffe) #x19 + (ite (= x!0 #xff000011c0210a75) #x00 + (ite (= x!0 #xff000011c0210a70) #x00 + (ite (= x!0 #xff000011c0210a6f) #x00 + (ite (= x!0 #x0000000000000000) #xc6 + (ite (= x!0 #xff000011c0210a73) #x00 + (ite (= x!0 #xff000011c0210a71) #x00 + (ite (= x!0 #xff000011c0210a74) #x00 + (ite (= x!0 #x0000010000000000) #x20 + (ite (= x!0 #xfefffffec0000000) #xac + (ite (= x!0 #xfefffffec0000001) #xca + (ite (= x!0 #xff000011c0210a72) #x00 + (ite (= x!0 #xfefffffebfffffff) #x0b + #x01))))))))))))))) +) diff --git a/out.smt2 b/out.smt2 new file mode 100644 index 0000000..2d4e81a --- /dev/null +++ b/out.smt2 @@ -0,0 +1,260 @@ +(set-logic QF_ABV) +(define-fun load-word8 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64))) + (_ BitVec 8) + (select m p) +) + + +(define-fun load-word16 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64))) + (_ BitVec 16) + (concat (select m (bvadd p #x0000000000000001)) + (select m p) + ) +) + + +(define-fun load-word32 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64))) + (_ BitVec 32) + (concat + (concat (select m (bvadd p #x0000000000000003)) + (select m (bvadd p #x0000000000000002))) + (concat (select m (bvadd p #x0000000000000001)) + (select m p)) + ) +) + + +(define-fun load-word64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64))) + (_ BitVec 64) + (concat (load-word32 m (bvadd p #x0000000000000004)) + (load-word32 m p) + ) +) + + +(define-fun store-word8 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64)) (v (_ BitVec 8))) + (Array (_ BitVec 64) (_ BitVec 8)) + (store m p v) +) + + +(define-fun store-word16 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64)) (v (_ BitVec 16))) + (Array (_ BitVec 64) (_ BitVec 8)) + (store-word8 + (store-word8 m p ((_ extract 7 0) v)) + (bvadd p #x0000000000000001) + ((_ extract 15 8) v) + ) +) + + +(define-fun store-word32 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64)) (v (_ BitVec 32))) + (Array (_ BitVec 64) (_ BitVec 8)) + (store-word16 + (store-word16 m p ((_ extract 15 0) v)) + (bvadd p #x0000000000000002) + ((_ extract 31 16) v) + ) +) + + +(define-fun store-word64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64)) (v (_ BitVec 64))) + (Array (_ BitVec 64) (_ BitVec 8)) + (store-word32 + (store-word32 m p ((_ extract 31 0) v)) + (bvadd p #x0000000000000004) + ((_ extract 63 32) v) + ) +) +(declare-sort PMS 0) +(declare-sort HTD 0) +(declare-fun node_Err_ok () Bool) +(declare-fun node_Ret_ok () Bool) +(declare-fun node_17_ok () Bool) +(declare-fun node_stash_initial_args_ok () Bool) +(declare-fun node_pre_condition_ok () Bool) +(declare-fun node_upd_n17_ok () Bool) +(declare-fun node_guard_n13_ok () Bool) +(declare-fun node_call_stash_13_pred_1_ok () Bool) +(declare-fun node_call_pre_13_pred_1_ok () Bool) +(declare-fun node_13_ok () Bool) +(declare-fun node_call_post_13_ok () Bool) +(declare-fun node_upd_n13_ok () Bool) +(declare-fun node_guard_n12_ok () Bool) +(declare-fun node_12_ok () Bool) +(declare-fun node_upd_n12_ok () Bool) +(declare-fun node_guard_n11_ok () Bool) +(declare-fun node_11_ok () Bool) +(declare-fun node_guard_n8_ok () Bool) +(declare-fun node_8_ok () Bool) +(declare-fun node_guard_n7_ok () Bool) +(declare-fun node_7_ok () Bool) +(declare-fun node_upd_n7_ok () Bool) +(declare-fun node_6_ok () Bool) +(declare-fun node_guard_n5_ok () Bool) +(declare-fun node_5_ok () Bool) +(declare-fun node_guard_n4_ok () Bool) +(declare-fun node_4_ok () Bool) +(declare-fun node_upd_n4_ok () Bool) +(declare-fun node_3_ok () Bool) +(declare-fun node_upd_n3_ok () Bool) +(declare-fun node_j1_ok () Bool) +(declare-fun node_10_ok () Bool) +(declare-fun node_9_ok () Bool) +(declare-fun node_upd_n9_ok () Bool) +(declare-fun node_j2_ok () Bool) +(declare-fun node_1_ok () Bool) +(declare-fun node_post_condition_ok () Bool) + +(declare-fun ring___ptr_to_struct_ring_buffer_C@v~1 () (_ BitVec 64)) +(declare-fun buffer___struct_buff_desc_C@v.phys_or_offset_C~1 () (_ BitVec 64)) +(declare-fun buffer___struct_buff_desc_C@v.len_C~1 () (_ BitVec 16)) +(declare-fun buffer___struct_buff_desc_C@v.cookie_C~1 () (_ BitVec 64)) +(declare-fun Mem~1 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun HTD~1 () HTD) +(declare-fun PMS~1 () PMS) +(declare-fun GhostAssertions~1 () (Array (_ BitVec 50) (_ BitVec 64))) +(declare-fun ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 () (_ BitVec 64)) +(declare-fun buffer___struct_buff_desc_C@v.phys_or_offset_C/subject-arg~1 () (_ BitVec 64)) +(declare-fun buffer___struct_buff_desc_C@v.len_C/subject-arg~1 () (_ BitVec 16)) +(declare-fun buffer___struct_buff_desc_C@v.cookie_C/subject-arg~1 () (_ BitVec 64)) +(declare-fun Mem/subject-arg~1 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun HTD/subject-arg~1 () HTD) +(declare-fun PMS/subject-arg~1 () PMS) +(declare-fun GhostAssertions/subject-arg~1 () (Array (_ BitVec 50) (_ BitVec 64))) +(declare-fun ring___ptr_to_struct_ring_buffer_C@v@assigned~1 () Bool) +(declare-fun buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1 () Bool) +(declare-fun buffer___struct_buff_desc_C@v.len_C@assigned~1 () Bool) +(declare-fun buffer___struct_buff_desc_C@v.cookie_C@assigned~1 () Bool) +(declare-fun Mem@assigned~1 () Bool) +(declare-fun HTD@assigned~1 () Bool) +(declare-fun PMS@assigned~1 () Bool) +(declare-fun GhostAssertions@assigned~1 () Bool) +(declare-fun ret__int@v@assigned~1 () Bool) +(declare-fun rv@space@ret__unsigned_char@v@assigned~1 () Bool) +(declare-fun ret__unsigned_char@v@assigned~1 () Bool) +(declare-fun ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 () (_ BitVec 64)) +(declare-fun Mem/call-arg~1 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun HTD/call-arg~1 () HTD) +(declare-fun PMS/call-arg~1 () PMS) +(declare-fun GhostAssertions/call-arg~1 () (Array (_ BitVec 50) (_ BitVec 64))) +(declare-fun Mem~2 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun ret__unsigned_char@v~1 () (_ BitVec 8)) +(declare-fun rv@space@ret__unsigned_char@v@assigned~2 () Bool) +(declare-fun Mem@assigned~2 () Bool) +(declare-fun HTD@assigned~2 () Bool) +(declare-fun PMS@assigned~2 () Bool) +(declare-fun GhostAssertions@assigned~2 () Bool) +(declare-fun rv@space@ret__unsigned_char@v~1 () (_ BitVec 8)) +(declare-fun ret__unsigned_char@v@assigned~2 () Bool) +(declare-fun Mem~3 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun Mem@assigned~3 () Bool) +(declare-fun Mem~4 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun Mem@assigned~4 () Bool) +(declare-fun ret__int@v~1 () (_ BitVec 32)) +(declare-fun ret__int@v@assigned~2 () Bool) +(declare-fun Mem~5 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun Mem@assigned~5 () Bool) + +(assert (= node_Err_ok false)) +(assert (= node_Ret_ok true)) +(assert (= node_17_ok node_stash_initial_args_ok)) +(assert (= node_stash_initial_args_ok (=> (= ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 ring___ptr_to_struct_ring_buffer_C@v~1) (=> (= buffer___struct_buff_desc_C@v.phys_or_offset_C/subject-arg~1 buffer___struct_buff_desc_C@v.phys_or_offset_C~1) (=> (= buffer___struct_buff_desc_C@v.len_C/subject-arg~1 buffer___struct_buff_desc_C@v.len_C~1) (=> (= buffer___struct_buff_desc_C@v.cookie_C/subject-arg~1 buffer___struct_buff_desc_C@v.cookie_C~1) (=> (= Mem/subject-arg~1 Mem~1) (=> (= HTD/subject-arg~1 HTD~1) (=> (= PMS/subject-arg~1 PMS~1) (=> (= GhostAssertions/subject-arg~1 GhostAssertions~1) node_pre_condition_ok)))))))))) +(assert (= node_pre_condition_ok (=> (and (not (= (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv12296 64))) (_ bv0 32))) (bvult (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv0 64))) (_ bv512 32))) node_upd_n17_ok))) +(assert (= node_upd_n17_ok (=> (= ring___ptr_to_struct_ring_buffer_C@v@assigned~1 true) (=> (= buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1 true) (=> (= buffer___struct_buff_desc_C@v.len_C@assigned~1 true) (=> (= buffer___struct_buff_desc_C@v.cookie_C@assigned~1 true) (=> (= Mem@assigned~1 true) (=> (= HTD@assigned~1 true) (=> (= PMS@assigned~1 true) (=> (= GhostAssertions@assigned~1 true) (=> (= ret__int@v@assigned~1 false) (=> (= rv@space@ret__unsigned_char@v@assigned~1 false) (=> (= ret__unsigned_char@v@assigned~1 false) node_guard_n13_ok))))))))))))) +(assert (= node_guard_n13_ok (and (=> (and (and (and (and PMS@assigned~1 HTD@assigned~1) GhostAssertions@assigned~1) Mem@assigned~1) ring___ptr_to_struct_ring_buffer_C@v@assigned~1) node_call_stash_13_pred_1_ok) (=> (not (and (and (and (and PMS@assigned~1 HTD@assigned~1) GhostAssertions@assigned~1) Mem@assigned~1) ring___ptr_to_struct_ring_buffer_C@v@assigned~1)) node_Err_ok)))) +(assert (= node_call_stash_13_pred_1_ok (=> (= ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 ring___ptr_to_struct_ring_buffer_C@v~1) (=> (= Mem/call-arg~1 Mem~1) (=> (= HTD/call-arg~1 HTD~1) (=> (= PMS/call-arg~1 PMS~1) (=> (= GhostAssertions/call-arg~1 GhostAssertions~1) node_call_pre_13_pred_1_ok))))))) +(assert (= node_call_pre_13_pred_1_ok (and (and (not (= (load-word32 Mem/call-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 (_ bv12296 64))) (_ bv0 32)))) node_13_ok))) +(assert (= node_13_ok node_call_post_13_ok)) +(assert (= node_call_post_13_ok (=> (and (= ret__unsigned_char@v~1 (ite (= (bvurem (bvadd (load-word32 Mem/call-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 (_ bv0 64))) (_ bv1 32)) (load-word32 Mem/call-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 (_ bv12296 64)))) (load-word32 Mem/call-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 (_ bv4 64)))) (_ bv1 8) (_ bv0 8))) (= Mem/call-arg~1 Mem~2)) node_upd_n13_ok))) +(assert (= node_upd_n13_ok (=> (= rv@space@ret__unsigned_char@v@assigned~2 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~1) HTD@assigned~1) PMS@assigned~1) GhostAssertions@assigned~1)) (=> (= Mem@assigned~2 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~1) HTD@assigned~1) PMS@assigned~1) GhostAssertions@assigned~1)) (=> (= HTD@assigned~2 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~1) HTD@assigned~1) PMS@assigned~1) GhostAssertions@assigned~1)) (=> (= PMS@assigned~2 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~1) HTD@assigned~1) PMS@assigned~1) GhostAssertions@assigned~1)) (=> (= GhostAssertions@assigned~2 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~1) HTD@assigned~1) PMS@assigned~1) GhostAssertions@assigned~1)) node_guard_n12_ok))))))) +(assert (= node_guard_n12_ok (and (=> rv@space@ret__unsigned_char@v@assigned~2 node_12_ok) (=> (not rv@space@ret__unsigned_char@v@assigned~2) node_Err_ok)))) +(assert (= node_12_ok (=> (= ret__unsigned_char@v~1 rv@space@ret__unsigned_char@v~1) node_upd_n12_ok))) +(assert (= node_upd_n12_ok (=> (= ret__unsigned_char@v@assigned~2 rv@space@ret__unsigned_char@v@assigned~2) node_guard_n11_ok))) +(assert (= node_guard_n11_ok (and (=> ret__unsigned_char@v@assigned~2 node_11_ok) (=> (not ret__unsigned_char@v@assigned~2) node_Err_ok)))) +(assert (= node_11_ok (and (=> (not (= ret__unsigned_char@v~1 (_ bv0 8))) node_10_ok) (=> (= ret__unsigned_char@v~1 (_ bv0 8)) node_guard_n8_ok)))) +(assert (= node_guard_n8_ok (and (=> (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~2) node_8_ok) (=> (not (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~2)) node_Err_ok)))) +(assert (= node_8_ok (and (=> (and (and (bvult (load-word32 Mem~2 ring___ptr_to_struct_ring_buffer_C@v~1) (_ bv512 32)) true) true) node_guard_n7_ok) (=> (not (and (and (bvult (load-word32 Mem~2 ring___ptr_to_struct_ring_buffer_C@v~1) (_ bv512 32)) true) true)) node_Err_ok)))) +(assert (= node_guard_n7_ok (and (=> (and (and (and (and Mem@assigned~2 ring___ptr_to_struct_ring_buffer_C@v@assigned~1) buffer___struct_buff_desc_C@v.len_C@assigned~1) buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1) buffer___struct_buff_desc_C@v.cookie_C@assigned~1) node_7_ok) (=> (not (and (and (and (and Mem@assigned~2 ring___ptr_to_struct_ring_buffer_C@v@assigned~1) buffer___struct_buff_desc_C@v.len_C@assigned~1) buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1) buffer___struct_buff_desc_C@v.cookie_C@assigned~1)) node_Err_ok)))) +(assert (= node_7_ok (=> (= Mem~3 (store-word64 (store-word16 (store-word64 Mem~2 (bvadd (bvadd (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv8 64)) (bvmul (_ bv24 64) ((_ zero_extend 32) (load-word32 Mem~2 ring___ptr_to_struct_ring_buffer_C@v~1)))) (_ bv0 64)) buffer___struct_buff_desc_C@v.phys_or_offset_C~1) (bvadd (bvadd (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv8 64)) (bvmul (_ bv24 64) ((_ zero_extend 32) (load-word32 Mem~2 ring___ptr_to_struct_ring_buffer_C@v~1)))) (_ bv8 64)) buffer___struct_buff_desc_C@v.len_C~1) (bvadd (bvadd (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv8 64)) (bvmul (_ bv24 64) ((_ zero_extend 32) (load-word32 Mem~2 ring___ptr_to_struct_ring_buffer_C@v~1)))) (_ bv16 64)) buffer___struct_buff_desc_C@v.cookie_C~1)) node_upd_n7_ok))) +(assert (= node_upd_n7_ok (=> (= Mem@assigned~3 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~2) buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1) buffer___struct_buff_desc_C@v.len_C@assigned~1) buffer___struct_buff_desc_C@v.cookie_C@assigned~1)) node_6_ok))) +(assert (= node_6_ok (and (=> (not (= (_ bv0 32) (_ bv0 32))) node_guard_n5_ok) (=> (= (_ bv0 32) (_ bv0 32)) node_guard_n5_ok)))) +(assert (= node_guard_n5_ok (and (=> (and Mem@assigned~3 ring___ptr_to_struct_ring_buffer_C@v@assigned~1) node_5_ok) (=> (not (and Mem@assigned~3 ring___ptr_to_struct_ring_buffer_C@v@assigned~1)) node_Err_ok)))) +(assert (= node_5_ok (and (=> (and (and (and true (not (= (load-word32 Mem~3 (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv12296 64))) (_ bv0 32)))) true) true) node_guard_n4_ok) (=> (not (and (and (and true (not (= (load-word32 Mem~3 (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv12296 64))) (_ bv0 32)))) true) true)) node_Err_ok)))) +(assert (= node_guard_n4_ok (and (=> (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~3) node_4_ok) (=> (not (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~3)) node_Err_ok)))) +(assert (= node_4_ok (=> (= Mem~4 (store-word32 Mem~3 ring___ptr_to_struct_ring_buffer_C@v~1 (bvurem (bvadd (load-word32 Mem~3 ring___ptr_to_struct_ring_buffer_C@v~1) (_ bv1 32)) (load-word32 Mem~3 (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv12296 64)))))) node_upd_n4_ok))) +(assert (= node_upd_n4_ok (=> (= Mem@assigned~4 (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~3)) node_3_ok))) +(assert (= node_3_ok (=> (= ret__int@v~1 (_ bv0 32)) node_upd_n3_ok))) +(assert (= node_upd_n3_ok (=> (= ret__int@v@assigned~2 true) node_j1_ok))) +(assert (= node_j1_ok (=> (= Mem~5 Mem~4) (=> (= Mem@assigned~5 Mem@assigned~4) node_1_ok)))) +(assert (= node_10_ok (and (=> (= (bvsle (_ bv0 32) (bvsub (_ bv0 32) (_ bv1 32))) (bvsle (_ bv1 32) (_ bv0 32))) node_9_ok) (=> (not (= (bvsle (_ bv0 32) (bvsub (_ bv0 32) (_ bv1 32))) (bvsle (_ bv1 32) (_ bv0 32)))) node_Err_ok)))) +(assert (= node_9_ok (=> (= ret__int@v~1 (bvsub (_ bv0 32) (_ bv1 32))) node_upd_n9_ok))) +(assert (= node_upd_n9_ok (=> (= ret__int@v@assigned~2 true) node_j2_ok))) +(assert (= node_j2_ok (=> (= Mem~5 Mem~2) (=> (= Mem@assigned~5 Mem@assigned~2) node_1_ok)))) +(assert (= node_1_ok node_post_condition_ok)) +(assert (= node_post_condition_ok (and (=> (and (= ring___ptr_to_struct_ring_buffer_C@v~1 ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1) (= (load-word32 Mem~5 (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv0 64))) (bvurem (bvadd (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv0 64))) (_ bv1 32)) (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv12296 64)))))) node_Ret_ok) (=> (not (and (= ring___ptr_to_struct_ring_buffer_C@v~1 ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1) (= (load-word32 Mem~5 (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv0 64))) (bvurem (bvadd (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv0 64))) (_ bv1 32)) (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv12296 64))))))) node_Err_ok)))) + +(declare-fun eval_val1 () (_ BitVec 32)) +(declare-fun eval_val2 () (_ BitVec 32)) +(declare-fun eval_val3 () (_ BitVec 32)) +(declare-fun eval_val4 () (_ BitVec 32)) + +(declare-fun eval_val5 () (_ BitVec 32)) +(declare-fun eval_val6 () (_ BitVec 32)) +(declare-fun eval_val7 () (_ BitVec 32)) +(declare-fun eval_val8 () (_ BitVec 32)) + +(assert (= (load-word32 Mem/subject-arg~1 ring___ptr_to_struct_ring_buffer_C@v~1) eval_val1)) +(assert (= + (load-word32 Mem/subject-arg~1 + (bvadd + ring___ptr_to_struct_ring_buffer_C@v~1 + (_ bv12296 64) + ) + ) + eval_val2 + ) +) + +(assert (= (load-word32 Mem~2 ring___ptr_to_struct_ring_buffer_C@v~1) eval_val3)) +(assert (= + (load-word32 Mem~2 + (bvadd + ring___ptr_to_struct_ring_buffer_C@v~1 + (_ bv12296 64) + ) + ) + eval_val4 + ) +) + +(assert (= (load-word32 Mem~3 ring___ptr_to_struct_ring_buffer_C@v~1) eval_val5)) +(assert (= + (load-word32 Mem~3 + (bvadd + ring___ptr_to_struct_ring_buffer_C@v~1 + (_ bv12296 64) + ) + ) + eval_val6 + ) +) + +(assert (= (load-word32 Mem~4 ring___ptr_to_struct_ring_buffer_C@v~1) eval_val7)) +(assert (= + (load-word32 Mem~4 + (bvadd + ring___ptr_to_struct_ring_buffer_C@v~1 + (_ bv12296 64) + ) + ) + eval_val8 + ) +) + +(check-sat) +(assert (not node_17_ok)) +(check-sat) +(get-model) + + diff --git a/out2.smt2 b/out2.smt2 new file mode 100644 index 0000000..637609b --- /dev/null +++ b/out2.smt2 @@ -0,0 +1,252 @@ +(set-logic QF_ABV) +(define-fun load-word8 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64))) + (_ BitVec 8) + (select m p) +) + + +(define-fun load-word16 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64))) + (_ BitVec 16) + (concat (select m (bvadd p #x0000000000000001)) + (select m p) + ) +) + + +(define-fun load-word32 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64))) + (_ BitVec 32) + (concat + (concat (select m (bvadd p #x0000000000000003)) + (select m (bvadd p #x0000000000000002))) + (concat (select m (bvadd p #x0000000000000001)) + (select m p)) + ) +) + + +(define-fun load-word64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64))) + (_ BitVec 64) + (concat (load-word32 m (bvadd p #x0000000000000004)) + (load-word32 m p) + ) +) + + +(define-fun store-word8 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64)) (v (_ BitVec 8))) + (Array (_ BitVec 64) (_ BitVec 8)) + (store m p v) +) + + +(define-fun store-word16 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64)) (v (_ BitVec 16))) + (Array (_ BitVec 64) (_ BitVec 8)) + (store-word8 + (store-word8 m p ((_ extract 7 0) v)) + (bvadd p #x0000000000000001) + ((_ extract 15 8) v) + ) +) + + +(define-fun store-word32 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64)) (v (_ BitVec 32))) + (Array (_ BitVec 64) (_ BitVec 8)) + (store-word16 + (store-word16 m p ((_ extract 15 0) v)) + (bvadd p #x0000000000000002) + ((_ extract 31 16) v) + ) +) + + +(define-fun store-word64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (p (_ BitVec 64)) (v (_ BitVec 64))) + (Array (_ BitVec 64) (_ BitVec 8)) + (store-word32 + (store-word32 m p ((_ extract 31 0) v)) + (bvadd p #x0000000000000004) + ((_ extract 63 32) v) + ) +) +(declare-sort PMS 0) +(declare-sort HTD 0) +(declare-fun node_Err_ok () Bool) +(declare-fun node_Ret_ok () Bool) +(declare-fun node_33_ok () Bool) +(declare-fun node_stash_initial_args_ok () Bool) +(declare-fun node_pre_condition_ok () Bool) +(declare-fun node_upd_n33_ok () Bool) +(declare-fun node_guard_n17_ok () Bool) +(declare-fun node_call_stash_17_pred_1_ok () Bool) +(declare-fun node_call_pre_17_pred_1_ok () Bool) +(declare-fun node_17_ok () Bool) +(declare-fun node_call_post_17_ok () Bool) +(declare-fun node_upd_n17_ok () Bool) +(declare-fun node_guard_n16_ok () Bool) +(declare-fun node_16_ok () Bool) +(declare-fun node_upd_n16_ok () Bool) +(declare-fun node_guard_n15_ok () Bool) +(declare-fun node_15_ok () Bool) +(declare-fun node_guard_n12_ok () Bool) +(declare-fun node_12_ok () Bool) +(declare-fun node_guard_n11_ok () Bool) +(declare-fun node_11_ok () Bool) +(declare-fun node_upd_n11_ok () Bool) +(declare-fun node_guard_n10_ok () Bool) +(declare-fun node_10_ok () Bool) +(declare-fun node_guard_n9_ok () Bool) +(declare-fun node_9_ok () Bool) +(declare-fun node_upd_n9_ok () Bool) +(declare-fun node_guard_n8_ok () Bool) +(declare-fun node_8_ok () Bool) +(declare-fun node_guard_n7_ok () Bool) +(declare-fun node_7_ok () Bool) +(declare-fun node_upd_n7_ok () Bool) +(declare-fun node_6_ok () Bool) +(declare-fun node_guard_n5_ok () Bool) +(declare-fun node_5_ok () Bool) +(declare-fun node_guard_n4_ok () Bool) +(declare-fun node_4_ok () Bool) +(declare-fun node_upd_n4_ok () Bool) +(declare-fun node_3_ok () Bool) +(declare-fun node_upd_n3_ok () Bool) +(declare-fun node_j1_ok () Bool) +(declare-fun node_14_ok () Bool) +(declare-fun node_13_ok () Bool) +(declare-fun node_upd_n13_ok () Bool) +(declare-fun node_j2_ok () Bool) +(declare-fun node_1_ok () Bool) +(declare-fun node_post_condition_ok () Bool) + +(declare-fun ring___ptr_to_struct_ring_buffer_C@v~1 () (_ BitVec 64)) +(declare-fun buffer___struct_buff_desc_C@v.phys_or_offset_C~1 () (_ BitVec 64)) +(declare-fun buffer___struct_buff_desc_C@v.len_C~1 () (_ BitVec 16)) +(declare-fun buffer___struct_buff_desc_C@v.cookie_C~1 () (_ BitVec 64)) +(declare-fun Mem~1 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun HTD~1 () HTD) +(declare-fun PMS~1 () PMS) +(declare-fun GhostAssertions~1 () (Array (_ BitVec 50) (_ BitVec 64))) +(declare-fun ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 () (_ BitVec 64)) +(declare-fun buffer___struct_buff_desc_C@v.phys_or_offset_C/subject-arg~1 () (_ BitVec 64)) +(declare-fun buffer___struct_buff_desc_C@v.len_C/subject-arg~1 () (_ BitVec 16)) +(declare-fun buffer___struct_buff_desc_C@v.cookie_C/subject-arg~1 () (_ BitVec 64)) +(declare-fun Mem/subject-arg~1 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun HTD/subject-arg~1 () HTD) +(declare-fun PMS/subject-arg~1 () PMS) +(declare-fun GhostAssertions/subject-arg~1 () (Array (_ BitVec 50) (_ BitVec 64))) +(declare-fun ring___ptr_to_struct_ring_buffer_C@v@assigned~1 () Bool) +(declare-fun buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1 () Bool) +(declare-fun buffer___struct_buff_desc_C@v.len_C@assigned~1 () Bool) +(declare-fun buffer___struct_buff_desc_C@v.cookie_C@assigned~1 () Bool) +(declare-fun Mem@assigned~1 () Bool) +(declare-fun HTD@assigned~1 () Bool) +(declare-fun PMS@assigned~1 () Bool) +(declare-fun GhostAssertions@assigned~1 () Bool) +(declare-fun ret__int@v@assigned~1 () Bool) +(declare-fun rv@space@ret__unsigned_char@v@assigned~1 () Bool) +(declare-fun ret__unsigned_char@v@assigned~1 () Bool) +(declare-fun ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 () (_ BitVec 64)) +(declare-fun Mem/call-arg~1 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun HTD/call-arg~1 () HTD) +(declare-fun PMS/call-arg~1 () PMS) +(declare-fun GhostAssertions/call-arg~1 () (Array (_ BitVec 50) (_ BitVec 64))) +(declare-fun Mem~2 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun ret__unsigned_char@v~1 () (_ BitVec 8)) +(declare-fun rv@space@ret__unsigned_char@v@assigned~2 () Bool) +(declare-fun Mem@assigned~2 () Bool) +(declare-fun HTD@assigned~2 () Bool) +(declare-fun PMS@assigned~2 () Bool) +(declare-fun GhostAssertions@assigned~2 () Bool) +(declare-fun rv@space@ret__unsigned_char@v~1 () (_ BitVec 8)) +(declare-fun ret__unsigned_char@v@assigned~2 () Bool) +(declare-fun Mem~3 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun Mem@assigned~3 () Bool) +(declare-fun Mem~4 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun Mem@assigned~4 () Bool) +(declare-fun Mem~5 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun Mem@assigned~5 () Bool) +(declare-fun Mem~6 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun Mem@assigned~6 () Bool) +(declare-fun ret__int@v~1 () (_ BitVec 32)) +(declare-fun ret__int@v@assigned~2 () Bool) +(declare-fun Mem~7 () (Array (_ BitVec 64) (_ BitVec 8))) +(declare-fun Mem@assigned~7 () Bool) + +(assert (= node_Err_ok false)) +(assert (= node_Ret_ok true)) +(assert (= node_33_ok node_stash_initial_args_ok)) +(assert (= node_stash_initial_args_ok (=> (= ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 ring___ptr_to_struct_ring_buffer_C@v~1) (=> (= buffer___struct_buff_desc_C@v.phys_or_offset_C/subject-arg~1 buffer___struct_buff_desc_C@v.phys_or_offset_C~1) (=> (= buffer___struct_buff_desc_C@v.len_C/subject-arg~1 buffer___struct_buff_desc_C@v.len_C~1) (=> (= buffer___struct_buff_desc_C@v.cookie_C/subject-arg~1 buffer___struct_buff_desc_C@v.cookie_C~1) (=> (= Mem/subject-arg~1 Mem~1) (=> (= HTD/subject-arg~1 HTD~1) (=> (= PMS/subject-arg~1 PMS~1) (=> (= GhostAssertions/subject-arg~1 GhostAssertions~1) node_pre_condition_ok)))))))))) +(assert (= node_pre_condition_ok (=> (and (not (= (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv12296 64))) (_ bv0 32))) (bvult (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv0 64))) (_ bv512 32))) node_upd_n33_ok))) +(assert (= node_upd_n33_ok (=> (= ring___ptr_to_struct_ring_buffer_C@v@assigned~1 true) (=> (= buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1 true) (=> (= buffer___struct_buff_desc_C@v.len_C@assigned~1 true) (=> (= buffer___struct_buff_desc_C@v.cookie_C@assigned~1 true) (=> (= Mem@assigned~1 true) (=> (= HTD@assigned~1 true) (=> (= PMS@assigned~1 true) (=> (= GhostAssertions@assigned~1 true) (=> (= ret__int@v@assigned~1 false) (=> (= rv@space@ret__unsigned_char@v@assigned~1 false) (=> (= ret__unsigned_char@v@assigned~1 false) node_guard_n17_ok))))))))))))) +(assert (= node_guard_n17_ok (and (=> (and (and (and (and PMS@assigned~1 HTD@assigned~1) GhostAssertions@assigned~1) Mem@assigned~1) ring___ptr_to_struct_ring_buffer_C@v@assigned~1) node_call_stash_17_pred_1_ok) (=> (not (and (and (and (and PMS@assigned~1 HTD@assigned~1) GhostAssertions@assigned~1) Mem@assigned~1) ring___ptr_to_struct_ring_buffer_C@v@assigned~1)) node_Err_ok)))) +(assert (= node_call_stash_17_pred_1_ok (=> (= ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 ring___ptr_to_struct_ring_buffer_C@v~1) (=> (= Mem/call-arg~1 Mem~1) (=> (= HTD/call-arg~1 HTD~1) (=> (= PMS/call-arg~1 PMS~1) (=> (= GhostAssertions/call-arg~1 GhostAssertions~1) node_call_pre_17_pred_1_ok))))))) +(assert (= node_call_pre_17_pred_1_ok (and (and (not (= (load-word32 Mem/call-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 (_ bv12296 64))) (_ bv0 32)))) node_17_ok))) +(assert (= node_17_ok node_call_post_17_ok)) +(assert (= node_call_post_17_ok (=> (and (= ret__unsigned_char@v~1 (ite (= (bvurem (bvadd (load-word32 Mem/call-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 (_ bv0 64))) (_ bv1 32)) (load-word32 Mem/call-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 (_ bv12296 64)))) (load-word32 Mem/call-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/call-arg~1 (_ bv4 64)))) (_ bv1 8) (_ bv0 8))) (= Mem/call-arg~1 Mem~2)) node_upd_n17_ok))) +(assert (= node_upd_n17_ok (=> (= rv@space@ret__unsigned_char@v@assigned~2 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~1) HTD@assigned~1) PMS@assigned~1) GhostAssertions@assigned~1)) (=> (= Mem@assigned~2 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~1) HTD@assigned~1) PMS@assigned~1) GhostAssertions@assigned~1)) (=> (= HTD@assigned~2 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~1) HTD@assigned~1) PMS@assigned~1) GhostAssertions@assigned~1)) (=> (= PMS@assigned~2 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~1) HTD@assigned~1) PMS@assigned~1) GhostAssertions@assigned~1)) (=> (= GhostAssertions@assigned~2 (and (and (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~1) HTD@assigned~1) PMS@assigned~1) GhostAssertions@assigned~1)) node_guard_n16_ok))))))) +(assert (= node_guard_n16_ok (and (=> rv@space@ret__unsigned_char@v@assigned~2 node_16_ok) (=> (not rv@space@ret__unsigned_char@v@assigned~2) node_Err_ok)))) +(assert (= node_16_ok (=> (= ret__unsigned_char@v~1 rv@space@ret__unsigned_char@v~1) node_upd_n16_ok))) +(assert (= node_upd_n16_ok (=> (= ret__unsigned_char@v@assigned~2 rv@space@ret__unsigned_char@v@assigned~2) node_guard_n15_ok))) +(assert (= node_guard_n15_ok (and (=> ret__unsigned_char@v@assigned~2 node_15_ok) (=> (not ret__unsigned_char@v@assigned~2) node_Err_ok)))) +(assert (= node_15_ok (and (=> (not (= ret__unsigned_char@v~1 (_ bv0 8))) node_14_ok) (=> (= ret__unsigned_char@v~1 (_ bv0 8)) node_guard_n12_ok)))) +(assert (= node_guard_n12_ok (and (=> (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~2) node_12_ok) (=> (not (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~2)) node_Err_ok)))) +(assert (= node_12_ok (and (=> (and (and (bvult (load-word32 Mem~2 ring___ptr_to_struct_ring_buffer_C@v~1) (_ bv512 32)) true) true) node_guard_n11_ok) (=> (not (and (and (bvult (load-word32 Mem~2 ring___ptr_to_struct_ring_buffer_C@v~1) (_ bv512 32)) true) true)) node_Err_ok)))) +(assert (= node_guard_n11_ok (and (=> (and (and buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1 ring___ptr_to_struct_ring_buffer_C@v@assigned~1) Mem@assigned~2) node_11_ok) (=> (not (and (and buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1 ring___ptr_to_struct_ring_buffer_C@v@assigned~1) Mem@assigned~2)) node_Err_ok)))) +(assert (= node_11_ok (=> (= Mem~3 (store-word64 Mem~2 (bvadd (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv8 64)) (bvmul ((_ zero_extend 32) (load-word32 Mem~2 ring___ptr_to_struct_ring_buffer_C@v~1)) (_ bv24 64))) buffer___struct_buff_desc_C@v.phys_or_offset_C~1)) node_upd_n11_ok))) +(assert (= node_upd_n11_ok (=> (= Mem@assigned~3 (and (and buffer___struct_buff_desc_C@v.phys_or_offset_C@assigned~1 ring___ptr_to_struct_ring_buffer_C@v@assigned~1) Mem@assigned~2)) node_guard_n10_ok))) +(assert (= node_guard_n10_ok (and (=> (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~3) node_10_ok) (=> (not (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~3)) node_Err_ok)))) +(assert (= node_10_ok (and (=> (and (and (bvult (load-word32 Mem~3 ring___ptr_to_struct_ring_buffer_C@v~1) (_ bv512 32)) true) true) node_guard_n9_ok) (=> (not (and (and (bvult (load-word32 Mem~3 ring___ptr_to_struct_ring_buffer_C@v~1) (_ bv512 32)) true) true)) node_Err_ok)))) +(assert (= node_guard_n9_ok (and (=> (and (and buffer___struct_buff_desc_C@v.len_C@assigned~1 ring___ptr_to_struct_ring_buffer_C@v@assigned~1) Mem@assigned~3) node_9_ok) (=> (not (and (and buffer___struct_buff_desc_C@v.len_C@assigned~1 ring___ptr_to_struct_ring_buffer_C@v@assigned~1) Mem@assigned~3)) node_Err_ok)))) +(assert (= node_9_ok (=> (= Mem~4 (store-word16 Mem~3 (bvadd (bvadd (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv8 64)) (bvmul ((_ zero_extend 32) (load-word32 Mem~3 ring___ptr_to_struct_ring_buffer_C@v~1)) (_ bv24 64))) (_ bv8 64)) buffer___struct_buff_desc_C@v.len_C~1)) node_upd_n9_ok))) +(assert (= node_upd_n9_ok (=> (= Mem@assigned~4 (and (and buffer___struct_buff_desc_C@v.len_C@assigned~1 ring___ptr_to_struct_ring_buffer_C@v@assigned~1) Mem@assigned~3)) node_guard_n8_ok))) +(assert (= node_guard_n8_ok (and (=> (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~4) node_8_ok) (=> (not (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~4)) node_Err_ok)))) +(assert (= node_8_ok (and (=> (and (and (bvult (load-word32 Mem~4 ring___ptr_to_struct_ring_buffer_C@v~1) (_ bv512 32)) true) true) node_guard_n7_ok) (=> (not (and (and (bvult (load-word32 Mem~4 ring___ptr_to_struct_ring_buffer_C@v~1) (_ bv512 32)) true) true)) node_Err_ok)))) +(assert (= node_guard_n7_ok (and (=> (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 buffer___struct_buff_desc_C@v.cookie_C@assigned~1) Mem@assigned~4) node_7_ok) (=> (not (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 buffer___struct_buff_desc_C@v.cookie_C@assigned~1) Mem@assigned~4)) node_Err_ok)))) +(assert (= node_7_ok (=> (= Mem~5 (store-word64 Mem~4 (bvadd (bvadd (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv8 64)) (bvmul ((_ zero_extend 32) (load-word32 Mem~4 ring___ptr_to_struct_ring_buffer_C@v~1)) (_ bv24 64))) (_ bv16 64)) buffer___struct_buff_desc_C@v.cookie_C~1)) node_upd_n7_ok))) +(assert (= node_upd_n7_ok (=> (= Mem@assigned~5 (and (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 buffer___struct_buff_desc_C@v.cookie_C@assigned~1) Mem@assigned~4)) node_6_ok))) +(assert (= node_6_ok (and (=> (not (= (_ bv0 32) (_ bv0 32))) node_guard_n5_ok) (=> (= (_ bv0 32) (_ bv0 32)) node_guard_n5_ok)))) +(assert (= node_guard_n5_ok (and (=> (and Mem@assigned~5 ring___ptr_to_struct_ring_buffer_C@v@assigned~1) node_5_ok) (=> (not (and Mem@assigned~5 ring___ptr_to_struct_ring_buffer_C@v@assigned~1)) node_Err_ok)))) +(assert (= node_5_ok (and (=> (and (and (and true (not (= (load-word32 Mem~5 (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv12296 64))) (_ bv0 32)))) true) true) node_guard_n4_ok) (=> (not (and (and (and true (not (= (load-word32 Mem~5 (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv12296 64))) (_ bv0 32)))) true) true)) node_Err_ok)))) +(assert (= node_guard_n4_ok (and (=> (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~5) node_4_ok) (=> (not (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~5)) node_Err_ok)))) +(assert (= node_4_ok (=> (= Mem~6 (store-word32 Mem~5 ring___ptr_to_struct_ring_buffer_C@v~1 (bvurem (bvadd (load-word32 Mem~5 ring___ptr_to_struct_ring_buffer_C@v~1) (_ bv1 32)) (load-word32 Mem~5 (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv12296 64)))))) node_upd_n4_ok))) +(assert (= node_upd_n4_ok (=> (= Mem@assigned~6 (and ring___ptr_to_struct_ring_buffer_C@v@assigned~1 Mem@assigned~5)) node_3_ok))) +(assert (= node_3_ok (=> (= ret__int@v~1 (_ bv0 32)) node_upd_n3_ok))) +(assert (= node_upd_n3_ok (=> (= ret__int@v@assigned~2 true) node_j1_ok))) +(assert (= node_j1_ok (=> (= Mem~7 Mem~6) (=> (= Mem@assigned~7 Mem@assigned~6) node_1_ok)))) +(assert (= node_14_ok (and (=> (= (bvsle (_ bv0 32) (bvsub (_ bv0 32) (_ bv1 32))) (bvsle (_ bv1 32) (_ bv0 32))) node_13_ok) (=> (not (= (bvsle (_ bv0 32) (bvsub (_ bv0 32) (_ bv1 32))) (bvsle (_ bv1 32) (_ bv0 32)))) node_Err_ok)))) +(assert (= node_13_ok (=> (= ret__int@v~1 (bvsub (_ bv0 32) (_ bv1 32))) node_upd_n13_ok))) +(assert (= node_upd_n13_ok (=> (= ret__int@v@assigned~2 true) node_j2_ok))) +(assert (= node_j2_ok (=> (= Mem~7 Mem~2) (=> (= Mem@assigned~7 Mem@assigned~2) node_1_ok)))) +(assert (= node_1_ok node_post_condition_ok)) +(assert (= node_post_condition_ok (and (=> (and (= ring___ptr_to_struct_ring_buffer_C@v~1 ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1) (= (load-word32 Mem~7 (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv0 64))) (bvurem (bvadd (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv0 64))) (_ bv1 32)) (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv12296 64)))))) node_Ret_ok) (=> (not (and (= ring___ptr_to_struct_ring_buffer_C@v~1 ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1) (= (load-word32 Mem~7 (bvadd ring___ptr_to_struct_ring_buffer_C@v~1 (_ bv0 64))) (bvurem (bvadd (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv0 64))) (_ bv1 32)) (load-word32 Mem/subject-arg~1 (bvadd ring___ptr_to_struct_ring_buffer_C@v/subject-arg~1 (_ bv12296 64))))))) node_Err_ok)))) + +(declare-fun eval_val1 () (_ BitVec 32)) +(declare-fun eval_val2 () (_ BitVec 32)) +(declare-fun eval_val3 () (_ BitVec 32)) +(declare-fun eval_val4 () (_ BitVec 32)) + +(assert (= (load-word32 Mem~1 ring___ptr_to_struct_ring_buffer_C@v~1) eval_val1)) +(assert (= + (load-word32 Mem~1 + (bvadd + ring___ptr_to_struct_ring_buffer_C@v~1 + (_ bv12296 64) + ) + ) + eval_val2 + ) +) +(assert (= (load-word32 Mem~2 ring___ptr_to_struct_ring_buffer_C@v~1) eval_val3)) +(assert (= + (load-word32 Mem~2 + (bvadd + ring___ptr_to_struct_ring_buffer_C@v~1 + (_ bv12296 64) + ) + ) + eval_val4 + ) +) + +(check-sat) +(assert (not node_33_ok)) +(check-sat) +(get-model) diff --git a/prog_globals.py b/prog_globals.py new file mode 100644 index 0000000..ac15886 --- /dev/null +++ b/prog_globals.py @@ -0,0 +1,247 @@ +from __future__ import annotations +from typing import Mapping, NamedTuple, TYPE_CHECKING, Sequence +from typing_extensions import assert_never +from collections import OrderedDict +from source import TypeArray, TypeBitVec, TypeBuiltin, TypeFloatingPoint, TypePtr, TypeSpecGhost, TypeWordArray, convert_type, TypeStruct, Type, ExprSymbolT, ExprT +import source +import assume_prove as ap + +ADDR_SIZE_BITS = 64 +ADDR_SIZE_BYTES = int(ADDR_SIZE_BITS / 8) + +if TYPE_CHECKING: + import assume_prove + import syntax + + +class StructField(NamedTuple): + name: str + offset: int + typ: Type + + +class Struct(NamedTuple): + """ + """ + name: str + size: int + align: int + fields: Mapping[str, StructField] + typ: Type + + +safe_globals: Mapping[ExprSymbolT, Type] = { + +} + +safe_structs: Mapping[TypeStruct, Struct] = { + +} + + +# These turns into asserts later +global_asserts: Sequence[ExprT[assume_prove.VarName]] = [] + +ring_handle_t = TypeStruct("Kernel_C.ring_handle_C") + +# declare your global variables here +__loose_globals: Mapping[str, Type] = { + "rx_ring_mux": ring_handle_t, + "rx_ring_cli": ring_handle_t, + "cookie": source.type_word64, + "m_len": source.type_word64, + "m_addr": source.type_word64, + "c_len": source.type_word64, + "c_addr": source.type_word64, + "cookie2": source.type_word64, +} + + +def sz(ty: Type) -> int: + """ + Returns the number of bits needed + to store a certain type + """ + size: int = 0 + + if isinstance(ty, TypeStruct): + struct = safe_structs[ty] + return struct.size + elif isinstance(ty, TypeBitVec): + assert ty.size % 8 == 0 + size += int(ty.size / 8) + elif isinstance(ty, TypePtr): + size += 8 + elif isinstance(ty, TypeArray): + inner_typ_sz = sz(ty.element_typ) + size += inner_typ_sz * ty.size + elif isinstance(ty, TypeFloatingPoint): + assert False, "TypeFloatingPoint not implemented" + elif isinstance(ty, TypeBuiltin): + assert False, "TypeBuiltin not implemented" + elif isinstance(ty, TypeWordArray): + assert False, "TypeWordArray not implemented" + elif isinstance(ty, TypeSpecGhost): + assert False, "TypeSpecGhost not implemented" + else: + assert_never(ty) + + return size + + +class InitMem(): + addr_bits: int + offset: int # we layout variables one by one + + sym_conds: Mapping[source.ExprSymbolT, list[source.ExprT[ap.VarName]]] + + def __init__(self, addr_bits: int): + self.addr_bits = addr_bits + self.offset = 0 + self.sym_conds = {} + + def init_mem(self, var: ExprSymbolT, ty: Type) -> None: + if isinstance(ty, TypeStruct): + assert safe_globals[var] == ty + assert ty in safe_structs + struct = safe_structs[ty] + self.init_struct(var, struct) + elif isinstance(ty, TypeBitVec): + self.init_bitvec(var) + elif isinstance(ty, TypeArray): + assert False, "not yet implemented" + elif isinstance(ty, TypeWordArray): + assert False, "not yet implemented" + elif isinstance(ty, TypePtr): + assert False, "not yet implemented" + elif isinstance(ty, TypeFloatingPoint): + assert False, "not yet implemented" + elif isinstance(ty, TypeSpecGhost): + assert False, "not yet implemented" + elif isinstance(ty, TypeBuiltin): + assert False, "not yet implemented" + else: + assert_never(ty) + + def init_struct(self, var: ExprSymbolT, struct: Struct) -> None: + assert var not in self.sym_conds + local_sym_conds: dict[source.ExprSymbolT, list[source.ExprT[ap.VarName]]] = { + k: v for k, v in self.sym_conds.items()} + + # alignment is given by default through this + starting_point = self.offset + (self.offset % struct.align) + + offset = starting_point + local_offset = 0 + + # finding our next offset is simple, + # we just want to sanity check though + + assert len(struct.fields) >= 1, "structs should have at least one field" + for _, (_, field) in enumerate(struct.fields.items()): + size = sz(field.typ) + + if field.offset != local_offset: + assert field.offset > local_offset, "padding is the only case where this makes any sense" + local_offset += (field.offset - local_offset) + local_offset += size + + offset = offset + local_offset + expected_offset = starting_point + struct.size + + assert offset == expected_offset + self.offset = offset + + cond: source.ExprT[ap.VarName] = source.expr_eq( + var, source.ExprNum(num=starting_point, typ=source.type_word64)) + # kinda hacky but safe, we know HTD~1 appears in every function + var_htd = source.ExprVar(source.type_htd, ap.VarName("HTD~1")) + # validity = source.expr_valid(var_htd, var.typ, var) + # local_sym_conds[var] = [cond, validity] + # self.sym_conds = local_sym_conds + + def init_bitvec(self, var: ExprSymbolT) -> None: + assert isinstance(var.typ, source.TypeBitVec) + assert var not in self.sym_conds + local_sym_conds: dict[source.ExprSymbolT, list[source.ExprT[ap.VarName]]] = { + k: v for k, v in self.sym_conds.items()} + + alignment = 0 + if var.typ.size == 8: + alignment = 0 + elif var.typ.size == 16: + alignment = 2 + elif var.typ.size == 32: + alignment = 4 + elif var.typ.size == 64: + alignment = 8 + else: + assert False, f"{var.typ.size} size is not supported" + + myoffset = self.offset + (self.offset % alignment) + end = myoffset + int(var.typ.size / 8) + + + # kinda hacky but safe, we know HTD~1 appears in every function + var_htd = source.ExprVar(source.type_htd, ap.VarName("HTD~1")) + # validity = source.expr_valid(var_htd, var.typ, var) + + # cond: source.ExprT[ap.VarName] = source.expr_eq( + # var, source.ExprNum(num=myoffset, typ=source.type_word64)) + + + # local_sym_conds[var] = [cond, validity] + # self.sym_conds = local_sym_conds + self.offset = end + + +def to_safe_struct(struct: syntax.Struct) -> Struct: + fields: OrderedDict[str, StructField] = OrderedDict() + + for field_name, (typ, offset, _) in struct.fields.items(): + assert field_name not in fields + fields[field_name] = StructField(field_name, offset, convert_type(typ)) + return Struct(struct.name, struct.size, struct.align, fields, convert_type(struct.typ)) + + +def populate_safe_structs(structs: Mapping[str, syntax.Struct]) -> None: + safe_structs_local: dict[TypeStruct, Struct] = {} + global safe_structs + for struct_name, struct in structs.items(): + safe_struct = to_safe_struct(struct) + key = TypeStruct(struct_name) + assert key not in safe_structs + safe_structs_local[key] = safe_struct + safe_structs = safe_structs_local + + +def populate_safe_globals() -> None: + """ + All we do is check if the structs referred in the __loose_globals + have actually been populated in safe_structs. + It then moves these variables to safe_globals. + We can then assume that every variable in safe_globals has an + associated type + """ + global safe_globals + safe_globals_local: dict[ExprSymbolT, Type] = {} + for variable, typ in __loose_globals.items(): + if isinstance(typ, TypeStruct): + assert typ in safe_structs + safe_globals_local[ExprSymbolT( + name=variable, typ=source.type_word64)] = typ + + safe_globals = safe_globals_local + + +mem = InitMem(ADDR_SIZE_BITS) + + +def initialise_memory() -> None: + """ + We need to initialise the array used to represent memory, + because our globals are by definition already valid. + """ + + for var, ty in safe_globals.items(): + mem.init_mem(var, ty) diff --git a/smt.py b/smt.py index 6e6b2bd..95fddac 100644 --- a/smt.py +++ b/smt.py @@ -42,7 +42,8 @@ source.Operator.WORD_ARRAY_ACCESS: SMTLIB("select"), source.Operator.WORD_ARRAY_UPDATE: SMTLIB("store"), source.Operator.MEM_DOM: SMTLIB("mem-dom"), - source.Operator.MEM_ACC: SMTLIB("mem-acc") + source.Operator.MEM_ACC: SMTLIB("mem-acc"), + source.Operator.MEM_UPDATE: SMTLIB("mem-update") } MEM_SORT = SMTLIB('(Array (_ BitVec 64) (_ BitVec 8))') @@ -279,6 +280,7 @@ def emit_expr(expr: source.ExprT[assume_prove.VarName]) -> SMTLIB: assert isinstance(typ, source.ExprType), typ if isinstance(val, source.ExprSymbol): return statically_infered_must_be_true + return statically_infered_must_be_true raise NotImplementedError( "PAlignValid for non symbols isn't supported") @@ -575,19 +577,19 @@ def send_smtlib(smtlib: SMTLIB, solver: Solver) -> Iterator[CheckSatResult]: """ with open_temp_file(suffix='.smt2') as (f, fullpath): + print("FILE: ", fullpath) f.write(smtlib) f.close() p = subprocess.Popen(get_subprocess_file( solver, fullpath), stderr=subprocess.PIPE, stdout=subprocess.PIPE) + output, error = p.communicate() p.wait() - assert p.stderr is not None - assert p.stdout is not None if p.returncode != 0: print("stderr:") - print(textwrap.indent(p.stdout.read().decode('utf-8'), ' ')) + print(textwrap.indent(error.decode('utf-8'), ' ')) return - lines = p.stdout.read().splitlines() + lines = output.splitlines() for ln in lines: yield CheckSatResult(ln.decode('utf-8')) diff --git a/source.py b/source.py index 0ab5c39..f629127 100644 --- a/source.py +++ b/source.py @@ -12,6 +12,8 @@ if typing.TYPE_CHECKING: import nip +import sys +sys.setrecursionlimit(10000) class ProgVarName(str): """ for example foo___int#v """ @@ -580,6 +582,7 @@ def f(lhs: ExprT[VarNameKind], rhs: ExprT[VarNameKind]) -> ExprT[VarNameKind]: expr_udiv = mk_binary_bitvec_operation(Operator.DIVIDED_BY) expr_shift_left = mk_binary_bitvec_operation(Operator.SHIFT_LEFT) expr_shift_right = mk_binary_bitvec_operation(Operator.SHIFT_RIGHT) +expr_mod = mk_binary_bitvec_operation(Operator.MODULUS) # don't implement expr_sdiv (cparser will never generate signed division) @@ -589,6 +592,10 @@ def expr_ite(cond: ExprT[VarNameKind], yes: ExprT[VarNameKind], no: ExprT[VarNam return ExprOp(yes.typ, Operator.IF_THEN_ELSE, (cond, yes, no)) +def bv8_expr_eq(lhs: ExprT[VarNameKind], rhs: ExprT[VarNameKind]) -> ExprT[VarNameKind]: + assert lhs.typ == rhs.typ + return expr_ite(expr_eq(lhs, rhs), ExprNum(type_word8, 1), ExprNum(type_word8, 0)) + def expr_negate(expr: ExprT[VarNameKind]) -> ExprT[VarNameKind]: assert expr.typ == type_bool @@ -959,6 +966,8 @@ def with_ghost(self, ghost: Ghost[ProgVarName | nip.GuardVarName] | None) -> Gen loop_iterations={ lh: empty_loop_ghost for lh in self.loops}, ) + if self.loops.keys() != ghost.loop_invariants.keys(): + print(self.loops.keys()) assert self.loops.keys() == ghost.loop_invariants.keys(), "loop invariants don't match" return GenericFunction(name=self.name, variables=self.variables, nodes=self.nodes, loops=self.loops, signature=self.signature, cfg=self.cfg, ghost=ghost) @@ -1075,7 +1084,7 @@ class SpecGhost: This should be loaded from a specification description (ie. a prelude and list of spec ghosts). This will be done in the stage mentionned above. """ -spec_ghosts: tuple[SpecGhost, ...] = (SpecGhost(name="test", bit_size=32), ) +spec_ghosts: tuple[SpecGhost, ...] = () # (SpecGhost(name="local_context", bit_size=408), ) @@ -1146,6 +1155,34 @@ def get_function_variables(func: GhostlessFunction[ProgVarName, Any], nodes: Map func, node_name, with_loop_targets=True)) return s +def can_reach(fn: GhostlessFunction[ProgVarName, Any], frm: NodeName, to: NodeName) -> bool: + if frm == to: + return True + for pred in fn.cfg.all_preds[frm]: + if (pred, frm) in fn.cfg.back_edges: + continue + if can_reach(fn, pred, to): + return True + return False + +def remove_unreachable(fn: GhostlessFunction[ProgVarName, Any]) -> GhostlessFunction[ProgVarName, Any]: + to_remove = set() + for node in fn.nodes.keys(): + if not can_reach(fn, node, fn.cfg.entry): + to_remove.add(node) + print(to_remove) + + new_nodes = {} + for name, node in fn.nodes.items(): + if name not in to_remove: + new_nodes[name] = node + + all_succs = abc_cfg.compute_all_successors_from_nodes(new_nodes) + cfg = abc_cfg.compute_cfg_from_all_succs(all_succs, NodeName(str(fn.cfg.entry))) + loops = abc_cfg.compute_loops(new_nodes, cfg) + tmpfn: GhostlessFunction[ProgVarName, Any] = GhostlessFunction(cfg=cfg, variables=set( + []), nodes=new_nodes, loops=loops, signature=fn.signature, name=fn.name) + return tmpfn def convert_function(func: syntax.Function) -> GhostlessFunction[ProgVarName, Any]: safe_nodes = convert_function_nodes(func.nodes) @@ -1159,11 +1196,14 @@ def convert_function(func: syntax.Function) -> GhostlessFunction[ProgVarName, An metadata = convert_function_metadata(func) # fn without any variables obtained - tmpfn: GhostlessFunction[ProgVarName, Any] = GhostlessFunction(cfg=cfg, variables=set( - []), nodes=safe_nodes, loops=loops, signature=metadata, name=func.name) + tmpfn: GhostlessFunction[ProgVarName, Any] = remove_unreachable(GhostlessFunction(cfg=cfg, variables=set( + []), nodes=safe_nodes, loops=loops, signature=metadata, name=func.name)) + + + del safe_nodes # Insert all variables here - variables = get_function_variables(tmpfn, safe_nodes) + variables = get_function_variables(tmpfn, tmpfn.nodes) variables.add(ExprVar(type_mem, ProgVarName('Mem'))) variables.add(ExprVar(type_htd, ProgVarName('HTD'))) variables.add(ExprVar(type_pms, ProgVarName('PMS'))) @@ -1177,4 +1217,4 @@ def convert_function(func: syntax.Function) -> GhostlessFunction[ProgVarName, An spec_var = mk_spec_ghost_var(spec_gh_var) variables.add(spec_var) - return GhostlessFunction(cfg=cfg, variables=variables, nodes=safe_nodes, loops=loops, signature=metadata, name=func.name) + return GhostlessFunction(cfg=tmpfn.cfg, variables=variables, nodes=tmpfn.nodes, loops=tmpfn.loops, signature=tmpfn.signature, name=func.name) diff --git a/validate_dsa.py b/validate_dsa.py index 5624b16..40652a1 100644 --- a/validate_dsa.py +++ b/validate_dsa.py @@ -6,6 +6,8 @@ import ghost_code import dsa +from rich.console import Console +console = Console() def compute_all_path(cfg: abc_cfg.CFG) -> Sequence[Sequence[source.NodeName]]: # binary number, 1 means go left 0 means go right