arm.mlw 3.12 KB
Newer Older
1 2 3 4 5

(* experiments related to ARM program verification *)

module M

6 7
  use import module ref.Refint
  use import module array.Array
8 9 10

  parameter a : array int

11
  logic inv (a : array int) =
12 13 14 15 16 17
    a[0] = 0 and length a = 11 and forall k:int. 1 <= k <= 10 -> 0 < a[k]

  parameter loop1 : ref int
  parameter loop2 : ref int

  let insertion_sort () =
18
    { inv a and
19
      (* ghost *) !loop1 = 0 and !loop2 = 0 }
20
    let i = ref 2 in
21
    while !i <= 10 do
22 23 24
      invariant { 2 <= !i <= 11 and inv a and
		  (* ghost *) !loop1 = !i - 2 and 2 * !loop2 <= (!i-2) * (!i-1) }
      variant { 10 - !i }
25 26 27
      (* ghost *) incr loop1;
      let j = ref !i in
      while a[!j] < a[!j - 1] do
28 29 30
        invariant { 1 <= !j <= !i and inv a and
		    (* ghost *) 2 * !loop2 <= (!i-2) * (!i-1) + 2*(!i - !j) }
	variant { !j }
31 32
        (* ghost *) incr loop2;
        let temp = a[!j] in
33 34
        a[!j] <- a[!j - 1];
        a[!j - 1] <- temp;
35 36 37 38
        decr j
      done;
      incr i
    done
39
    { !loop1 = 9 and !loop2 <= 45 }
40 41

end
42

43 44 45
module ARM

  use export int.Int
46
  use export map.Map
47
  use export module ref.Ref
48 49

  (* memory *)
50
  parameter mem : ref (map int int)
51
  parameter mem_ldr : a:int -> {} int reads mem.contents { result = !mem[a] }
52
  parameter mem_str : a:int -> v:int ->
53
    {} int writes mem.contents { !mem = (old !mem)[a <- v] }
54 55 56 57 58

  (* data segment *)
  (*
  parameter data : ref (t int int)
  parameter data_ldr : a:int -> {} int reads data { result = data[a] }
59
  parameter data_str :
60 61 62 63 64 65 66 67 68 69 70 71
    a:int -> v:int -> {} int writes data { data = (old data)[a <- v] }
  *)

  (* registers *)
  parameter r0 : ref int
  parameter r1 : ref int
  parameter r2 : ref int
  parameter r3 : ref int
  (* ... *)
  parameter fp : ref int
  parameter pc : ref int (* pc *)

72
  parameter ldr :
73
    r:ref int -> a:int -> {} unit reads mem.contents writes r.contents { !r = !mem[a] }
74
  parameter str :
75
    r:ref int -> a:int -> {} unit reads r.contents writes mem.contents { !mem = (old !mem)[a <- !r] }
76 77 78 79

  (* condition flags *)
  parameter le : ref bool

80 81 82
  parameter cmp : r:ref int -> v:int ->
    {}
    unit reads r.contents writes le.contents
83
    { !le=True <-> !r <= v }
84 85 86

end

87 88 89 90 91 92 93 94 95 96 97 98 99 100
(*
@@ logic separation (fp : int) = a+10 < fp-24

main:
    @@ assume separation fp

.L2:@@ invariant ...

.L3:

.L4:@@ invariant ...

*)

101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116
module InsertionSortExample

  use import module ARM

  (* i = fp-16
     j = fp-20
     temp = fp-24 *)

  parameter l4 : ref int
  parameter l7 : ref int

  logic a : int

  (* stack and data segment do not overlap *)
  logic separation (fp : int) = a+10 < fp-24

117
  logic inv (mem: map int int) =
118 119
    mem[a] = 0 and forall k:int. 1 <= k <= 10 -> 0 < mem[a + k]

120
  logic inv_l2 (mem: map int int) (fp : int) (l4 : int) =
121
    2 <= mem[fp - 16] <= 11 and l4 = mem[fp-16] - 2 and inv mem
122 123

  let path_init_l2 () =
124
    { separation !fp and inv !mem }
125 126 127
    (* ghost *) l4 := 0; l7 := 0;
    r3 := 2;
    str r3 (!fp - 16)
128
    { inv_l2 !mem !fp !l4 }
129 130

  let path_l2_exit () =
131
    { separation !fp and inv_l2 !mem !fp !l4 }
132 133
    ldr r3 (!fp - 16);
    cmp r3 10;
134 135
    assume { !le = False }
    { !l4 = 9 }
136 137 138 139

end

(*
140
Local Variables:
141
compile-command: "unset LANG; make -C ../.. examples/programs/arm.gui"
142
End:
143
*)