arm.mlw 3.11 KB
Newer Older
1 2 3 4 5 6 7 8 9 10

(* experiments related to ARM program verification *)

module M

  use import module stdlib.Refint
  use import module stdlib.Array

  parameter a : array int

11
  logic inv (a : array int) = 
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
    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
33 34
        set a !j a[!j - 1];
        set a (!j - 1) temp;
35 36 37 38 39 40 41 42 43 44 45
        decr j
      done;
      incr i
    done
    { loop1 = 9 and loop2 <= 45 }

end
  
module ARM

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

  (* 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 59 60 61 62 63 64 65 66 67 68 69 70 71 72

  (* 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 : 
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 80 81

  (* condition flags *)
  parameter le : ref bool

  parameter cmp : r:ref int -> v:int -> 
    {} 
82
    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 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
    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: 
*)