move-stackless-bytecode 0.3.2

Move stackless bytecode
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

============ initial translation from Move ================

[variant baseline]
fun Generics::remove<#0>($t0|a: address): Generics::R<#0> {
     var $t1: address
     var $t2: Generics::R<#0>
  0: $t1 := move($t0)
  1: $t2 := move_from<Generics::R<#0>>($t1)
  2: return $t2
}


[variant baseline]
fun Generics::remove_u64($t0|a: address): Generics::R<u64> {
     var $t1: address
     var $t2: Generics::R<u64>
  0: $t1 := move($t0)
  1: $t2 := Generics::remove<u64>($t1)
  2: return $t2
}

============ after pipeline `spec_instrumentation` ================

[variant verification]
fun Generics::remove<#0>($t0|a: address): Generics::R<#0> {
     var $t1: Generics::R<#0>
     var $t2: num
  0: assume CanModify<Generics::R<#0>>($t0)
     # VC: caller does not have permission to modify `Generics::R<#0>` at given address at tests/spec_instrumentation/generics.move:11:9+9
  1: assert CanModify<Generics::R<#0>>($t0)
  2: $t1 := move_from<Generics::R<#0>>($t0) on_abort goto 6 with $t2
  3: label L1
     # VC: post-condition does not hold at tests/spec_instrumentation/generics.move:20:9+25
  4: assert Not(exists<Generics::R<#0>>($t0))
  5: return $t1
  6: label L2
  7: abort($t2)
}


[variant verification]
fun Generics::remove_u64($t0|a: address): Generics::R<u64> {
     var $t1: Generics::R<u64>
     var $t2: bool
     var $t3: num
  0: assume CanModify<Generics::R<u64>>($t0)
     # VC: caller does not have permission to modify `Generics::R<u64>` at given address at tests/spec_instrumentation/generics.move:24:9+14
  1: assert CanModify<Generics::R<u64>>($t0)
  2: $t1 := opaque begin: Generics::remove<u64>($t0)
  3: havoc[val]($t2)
  4: if ($t2) goto 5 else goto 8
  5: label L4
  6: trace_abort($t3)
  7: goto 16
  8: label L3
  9: modifies global<Generics::R<u64>>($t0)
 10: assume WellFormed($t1)
 11: assume Not(exists<Generics::R<u64>>($t0))
 12: $t1 := opaque end: Generics::remove<u64>($t0)
 13: label L1
     # VC: post-condition does not hold at tests/spec_instrumentation/generics.move:20:9+25
 14: assert Not(exists<Generics::R<u64>>($t0))
 15: return $t1
 16: label L2
 17: abort($t3)
}



==== spec-instrumenter input specs ====

fun Generics::remove[baseline]
spec {
  modifies global<Generics::R<#0>>($t0);
  ensures Not(exists<Generics::R<#0>>($t0));
}

fun Generics::remove[verification]
spec {
  modifies global<Generics::R<#0>>($t0);
  ensures Not(exists<Generics::R<#0>>($t0));
}

fun Generics::remove_u64[baseline]
spec {
  modifies global<Generics::R<u64>>($t0);
  ensures Not(exists<Generics::R<u64>>($t0));
}

fun Generics::remove_u64[verification]
spec {
  modifies global<Generics::R<u64>>($t0);
  ensures Not(exists<Generics::R<u64>>($t0));
}