diff --git a/copy_spec.py b/copy_spec.py index 134ec60..63f05f2 100644 --- a/copy_spec.py +++ b/copy_spec.py @@ -1042,6 +1042,12 @@ def truthy() -> source.ExprVarT[source.ProgVarName]: ), "tmp.rx_return_inner_inner": source.Ghost( precondition=conjs( + # eq( + # arg(copied_ghost), + # u64(0), + # ), + # eq(arg(mux_addr_ghost), u64(0)), + # eq(arg(cli_addr_ghost), u64(0)), common_mem_wf(arg(Mem)), neg(ring_empty_spec( mem_acc( @@ -1079,18 +1085,18 @@ def truthy() -> source.ExprVarT[source.ProgVarName]: ), postcondition=conjs( common_mem_wf(Mem), - eq( - copied_ghost, - u64(1) - ), - eq( - mux_addr_ghost, - u64(0) - ), - eq( - cli_addr_ghost, - u64(0) - ) + # eq( + # copied_ghost, + # u64(1) + # ), + # eq( + # mux_addr_ghost, + # u64(0) + # ), + # eq( + # cli_addr_ghost, + # u64(0) + # ) ), loop_invariants={ }, @@ -2187,10 +2193,10 @@ def truthy() -> source.ExprVarT[source.ProgVarName]: precondition=conjs(), postcondition=conjs(), loop_invariants={ - lh('43'): conjs() + lh('23'): conjs() }, loop_iterations={ - lh('43'): source.empty_loop_ghost + lh('23'): source.empty_loop_ghost } ), "tmp.rx_return": source.Ghost( diff --git a/examples/out_copy.txt b/examples/out_copy.txt index 7198417..cc00d33 100644 --- a/examples/out_copy.txt +++ b/examples/out_copy.txt @@ -85,7 +85,7 @@ 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 +2 Call 1 tmp.rx_return_outer 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 @@ -104,142 +104,6 @@ Function tmp.ring_size 5 ring___ptr_to_struct_ring_buffer_C#v Word 64 Mem Mem HT 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 Op MemAcc Word 64 2 Var Mem Mem Symbol mux_buffer_data_region Word 64 Var mux_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 -102 Cond 101 Err Op PGlobalValid Bool 3 Var HTD HTD Type Word 64 Symbol mux_buffer_data_region Word 64 -103 Basic 102 1 cli_addr___unsigned_long#v Word 64 Op Plus Word 64 2 Op MemAcc Word 64 2 Var Mem Mem Symbol cli_buffer_data_region Word 64 Var cli_buffer___struct_buff_desc_C#v.phys_or_offset_C Word 64 -104 Cond 103 Err Op PGlobalValid Bool 3 Var HTD HTD Type Word 64 Symbol cli_buffer_data_region Word 64 -105 Basic 104 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 -106 Call 105 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 -107 Cond 106 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 -108 Cond 88 107 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 -109 Cond 108 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 -110 Basic 109 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 -111 Call 110 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 -112 Cond 111 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 112 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 -113 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 -114 Basic 113 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 -115 Call 114 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 -116 Cond 115 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 -117 Cond 116 65 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 -118 Basic 117 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 -119 Basic 118 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 -120 Call 119 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 -121 Cond 120 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_mux Word 64 -122 Cond 121 117 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 -123 Basic 122 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 -124 Basic 123 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 -125 Call 124 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 -126 Cond 125 Err Op PAlignValid Bool 2 Type Struct tmp.ring_handle_C Symbol rx_ring_cli Word 64 -127 Cond 126 122 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32 -128 Basic 127 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 -129 Basic 128 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 -130 Call 129 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 -131 Cond 130 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 131 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 -132 Basic 25 1 reprocess___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 1 Word 32 -133 Basic 132 1 enqueued___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 0 Word 32 -EntryPoint 133 - 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 @@ -456,17 +320,18 @@ Function tmp.rx_return_outer 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 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.require_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 5 rv#space#ret__unsigned_char#v Word 8 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 50 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 -62 Basic 61 1 enqueued___unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 -63 Call 62 tmp.rx_return_inner 4 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 +62 Basic 61 1 enqueued___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Op IfThenElse Word 32 3 Op Or Bool 2 Op Not Bool 1 Op Equals Bool 2 Var ret__unsigned_char#v Word 8 Num 0 Word 8 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 +63 Basic 62 1 ret__unsigned_char#v Word 8 Var rv#space#ret__unsigned_char#v Word 8 +64 Call 63 tmp.rx_return_inner 4 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 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 63 21 Op Not Bool 1 Op Equals Bool 2 Var reprocess___unsigned_char#v Word 8 Num 0 Word 8 +24 Cond 64 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 -64 Basic 25 1 enqueued___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 0 Word 32 -65 Basic 64 1 reprocess___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 1 Word 32 -EntryPoint 65 +65 Basic 25 1 enqueued___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 0 Word 32 +66 Basic 65 1 reprocess___unsigned_char#v Word 8 Op WordCastSigned Word 8 1 Num 1 Word 32 +EntryPoint 66 Function tmp.assert_non_empty 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 diff --git a/source.py b/source.py index aeb3916..098bf9b 100644 --- a/source.py +++ b/source.py @@ -1089,8 +1089,10 @@ 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="cli_addr", bit_size=64), - SpecGhost("mux_addr", bit_size=64), SpecGhost("mux_size", bit_size=16), SpecGhost("copied", bit_size=64), ) +spec_ghosts: tuple[SpecGhost, ...] = () + +# (SpecGhost(name="cli_addr", bit_size=64), +# SpecGhost("mux_addr", bit_size=64), SpecGhost("mux_size", bit_size=16), SpecGhost("copied", bit_size=64), ) # (SpecGhost(name="local_context", bit_size=408), )