CFuns-annotated.txt

#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
#


# void
# f (int *p, int x) {
#   int i;
#
#   for (i = x; i < 100; i ++) {
#     p[i] = g (i);
#   }
# }
Function Loop.f 6 p#v Word 32 x#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
# i = x
12 Basic 5 1 i#v Word 32 Var x#v Word 32

# loop-count = 0    -- invented variable for loop analysis
5 Basic 3 1 loop#2#count Word 32 Num 0 Word 32

# ? i < 100
3 Cond 4 Err Op True Bool 0
4 Cond 11 1 Op SignedLess Bool 2 Var i#v Word 32 Num 100 Word 32

# tmpvar = g (i)    -- function result is saved to temporaries called rv#space#ret__int#v and ret__int#v
11 Call 10 Loop.g 5 Var i#v Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 64 32 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
10 Basic 9 1 ret__int#v Word 32 Var rv#space#ret__int#v Word 32

# p[i] = tmpvar     -- check p[i] is a valid pointer then save temporary there
9 Cond 8 Err Op PAlignValid Bool 2 Type Word 32 Op Plus Word 32 2 Var p#v Word 32 Op Times Word 32 2 Op WordCastSigned Word 32 1 Var i#v Word 32 Num 4 Word 32
8 Basic 7 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Op Plus Word 32 2 Var p#v Word 32 Op Times Word 32 2 Op WordCastSigned Word 32 1 Var i#v Word 32 Num 4 Word 32 Var ret__int#v Word 32

# i ++              -- first check i++ does not overflow
7 Cond 6 Err Op Equals Bool 2 Op SignedLessEquals Bool 2 Var i#v Word 32 Op Plus Word 32 2 Var i#v Word 32 Num 1 Word 32 Op SignedLessEquals Bool 2 Num 0 Word 32 Num 1 Word 32
6 Basic 2 1 i#v Word 32 Op Plus Word 32 2 Var i#v Word 32 Num 1 Word 32

# loop-count ++
2 Basic 3 1 loop#2#count Word 32 Op Plus Word 32 2 Var loop#2#count Word 32 Num 1 Word 32

# if loop finished proceed to Ret
1 Basic Ret 0
EntryPoint 12

# int g (int i) {
#   return i * 8 + (i & 15);
# }
Function Loop.g 5 i#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32 5 ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
# tmpv = i * 8 + (i & 15)     -- first check for overflow
4 Cond 3 Err Op And Bool 2 Op Equals Bool 2 Op SignedLessEquals Bool 2 Op Times Word 32 2 Var i#v Word 32 Num 8 Word 32 Op Plus Word 32 2 Op Times Word 32 2 Var i#v Word 32 Num 8 Word 32 Op BWAnd Word 32 2 Var i#v Word 32 Num 15 Word 32 Op SignedLessEquals Bool 2 Num 0 Word 32 Op BWAnd Word 32 2 Var i#v Word 32 Num 15 Word 32 Op Equals Bool 2 Op Times Word 64 2 Op WordCastSigned Word 64 1 Var i#v Word 32 Op WordCastSigned Word 64 1 Num 8 Word 32 Op WordCastSigned Word 64 1 Op Times Word 32 2 Var i#v Word 32 Num 8 Word 32

3 Basic 1 1 ret__int#v Word 32 Op Plus Word 32 2 Op Times Word 32 2 Var i#v Word 32 Num 8 Word 32 Op BWAnd Word 32 2 Var i#v Word 32 Num 15 Word 32
# proceed to Ret
1 Basic Ret 0
# unreachable check that end of non-void function is indeed unreachable
2 Cond 1 Err Op False Bool 0
EntryPoint 4


# other functions from loop.c, not fully annotated and produced in exporter's
# default (back-to-front) order.

Function Loop.check_one 5 result#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32 5 ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
1 Basic Ret 0
2 Cond 1 Err Op False Bool 0
3 Basic 1 1 ret__int#v Word 32 Num 1 Word 32
4 Basic 3 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Symbol global_x Word 32 Op Plus Word 32 2 Op MemAcc Word 32 2 Var Mem Mem Symbol global_x Word 32 Op WordCastSigned Word 32 1 Num 1 Word 32
5 Cond 4 Err Op PGlobalValid Bool 3 Var HTD HTD Type Word 32 Symbol global_x Word 32
EntryPoint 5

Function Loop.create_one 5 identifier#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32 5 ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
1 Basic Ret 0
2 Cond 1 Err Op False Bool 0
3 Basic 1 1 ret__int#v Word 32 Num 1 Word 32
4 Basic 3 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Symbol global_x Word 32 Op Plus Word 32 2 Op MemAcc Word 32 2 Var Mem Mem Symbol global_x Word 32 Op WordCastSigned Word 32 1 Num 1 Word 32
5 Cond 4 Err Op PGlobalValid Bool 3 Var HTD HTD Type Word 32 Symbol global_x Word 32
EntryPoint 5

Function Loop.create_loop 6 start#v Word 32 end#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32 5 ret__unsigned#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
1 Basic Ret 0
2 Cond 1 Err Op False Bool 0
3 Basic 1 1 ret__unsigned#v Word 32 Var end#v Word 32
8 Basic 4 1 f#v Word 32 Op Plus Word 32 2 Var f#v Word 32 Num 1024 Word 32
9 Cond 8 Err Op Equals Bool 2 Op SignedLessEquals Bool 2 Var f#v Word 32 Op Plus Word 32 2 Var f#v Word 32 Num 1024 Word 32 Op SignedLessEquals Bool 2 Num 0 Word 32 Num 1024 Word 32
10 Basic 1 1 ret__unsigned#v Word 32 Op WordCastSigned Word 32 1 Num 21 Word 32
11 Cond 10 9 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32
12 Basic 11 1 ret__int#v Word 32 Var rv#space#ret__int#v Word 32
13 Call 12 Loop.check_one 5 Var r#v Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 64 32 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
14 Basic 13 1 r#v Word 32 Var rv#space#ret__int#v Word 32
15 Call 14 Loop.create_one 5 Op WordCastSigned Word 32 1 Var f#v Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 64 32 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
4 Basic 5 1 loop#4#count Word 32 Op Plus Word 32 2 Var loop#4#count Word 32 Num 1 Word 32
5 Cond 6 Err Op True Bool 0
6 Cond 15 3 Op Less Bool 2 Op WordCastSigned Word 32 1 Var f#v Word 32 Var end#v Word 32
7 Basic 5 1 loop#4#count Word 32 Num 0 Word 32
16 Basic 7 1 f#v Word 32 Op WordCast Word 32 1 Var start#v Word 32
EntryPoint 16