arm.mlw 3.13 KB
Newer Older
1 2 3 4 5 6

(* experiments related to ARM program verification *)

module M

  use import module stdlib.Refint
7
  use import array.ArrayLength
8 9 10 11
  use import module stdlib.Array

  parameter a : array int

12
  logic inv (a : map int) = 
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
    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 () =
    { inv a and 
      (* ghost *) loop1 = 0 and loop2 = 0 }
    let i = ref 2 in 
    while !i <= 10 do
      invariant { 2 <= i <= 11 and inv a and
		  (* ghost *) loop1 = i - 2 and 2 * loop2 <= (i-2) * (i-1) } 
      variant { 10 - i }
      (* ghost *) incr loop1;
      let j = ref !i in
      while a[!j] < a[!j - 1] do
        invariant { 1 <= j <= i and inv a and 
		    (* ghost *) 2 * loop2 <= (i-2) * (i-1) + 2*(i-j) } 
	variant { j }
        (* ghost *) incr loop2;
        let temp = a[!j] in
34 35
        set a !j a[!j - 1];
        set a (!j - 1) temp;
36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
        decr j
      done;
      incr i
    done
    { loop1 = 9 and loop2 <= 45 }

end
  
module ARM

  use export int.Int
  use export array.Array
  use export module stdlib.Ref

  (* memory *)
  parameter mem : ref (t int int)
52
  parameter mem_ldr : a:int -> {} int reads mem.contents { result = mem[a] }
53
  parameter mem_str : a:int -> v:int -> 
54
    {} int writes mem.contents { mem = (old mem)[a <- v] }
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73

  (* data segment *)
  (*
  parameter data : ref (t int int)
  parameter data_ldr : a:int -> {} int reads data { result = data[a] }
  parameter data_str : 
    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 *)

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

  (* condition flags *)
  parameter le : ref bool

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

end

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

main:
    @@ assume separation fp

.L2:@@ invariant ...

.L3:

.L4:@@ invariant ...

*)

102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
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

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

  logic inv_l2 (mem : t int int) (fp : int) (l4 : int) =
    2 <= mem[fp - 16] <= 11 and l4 = mem[fp-16] - 2 and inv mem
  
  let path_init_l2 () = 
    { 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

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