arm.mlw 3.08 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 22
    while !i <= 10 do
      invariant { 2 <= i <= 11 and inv a and
23
		  (* ghost *) loop1 = i - 2 and 2 * loop2 <= (i-2) * (i-1) }
24 25 26 27
      variant { 10 - i }
      (* ghost *) incr loop1;
      let j = ref !i in
      while a[!j] < a[!j - 1] do
28 29
        invariant { 1 <= j <= i and inv a and
		    (* ghost *) 2 * loop2 <= (i-2) * (i-1) + 2*(i-j) }
30 31 32
	variant { j }
        (* ghost *) incr loop2;
        let temp = a[!j] in
33 34
        a[!j] <- a[!j - 1];
        a[!j - 1] <- temp;
35 36 37 38 39 40 41
        decr j
      done;
      incr i
    done
    { loop1 = 9 and loop2 <= 45 }

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 84 85 86
    { le=True <-> r <= v }

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 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
    { separation fp and inv mem }
    (* ghost *) l4 := 0; l7 := 0;
    r3 := 2;
    str r3 (!fp - 16)
    { inv_l2 mem fp l4 }

  let path_l2_exit () =
    { separation fp and inv_l2 mem fp l4 }
    ldr r3 (!fp - 16);
    cmp r3 10;
    assume { le = False }
    { l4 = 9 }

end

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