examples/arm.mlw

   1 (* experiments related to ARM program verification *)
   2
   3 module M
   4
   5   use int.Int
   6   use ref.Refint
   7   use array.Array
   8
   9   val a : array int
  10
  11   predicate inv (a : array int) =
  12     a[0] = 0 /\ length a = 11 /\ forall k:int. 1 <= k <= 10 -> 0 < a[k]
  13
  14   val ghost loop1 : ref int
  15   val ghost loop2 : ref int
  16
  17   let insertion_sort ()
  18     requires { inv a /\ !loop1 = 0 /\ !loop2 = 0 }
  19     ensures  { !loop1 = 9 /\ !loop2 <= 45 }
  20   = let i = ref 2 in
  21     while !i <= 10 do
  22       invariant { 2 <= !i <= 11 /\ inv a /\
  23                   !loop1 = !i - 2 /\ 2 * !loop2 <= (!i-2) * (!i-1) }
  24       variant { 10 - !i }
  25       ghost incr loop1;
  26       let j = ref !i in
  27       while a[!j] < a[!j - 1] do
  28         invariant { 1 <= !j <= !i /\ inv a /\
  29                     2 * !loop2 <= (!i-2) * (!i-1) + 2*(!i - !j) }
  30         variant { !j }
  31         ghost incr loop2;
  32         let temp = a[!j] in
  33         a[!j] <- a[!j - 1];
  34         a[!j - 1] <- temp;
  35         decr j
  36       done;
  37       incr i
  38     done
  39
  40 end
  41
  42 module ARM
  43
  44   use export int.Int
  45   use export map.Map
  46   use export ref.Ref
  47
  48   (* memory *)
  49   val mem : ref (map int int)
  50   val mem_ldr (a:int) : int ensures { result = !mem[a] }
  51   val mem_str (a:int) (v:int) : (_r: int) writes { mem }
  52     ensures { !mem = (old !mem)[a <- v] }
  53
  54   (* data segment *)
  55   (*
  56   val data : ref (t int int)
  57   val data_ldr (a:int) : int ensures { result = data[a] }
  58   val data_str (a:int) (v:int) : int writes { data }
  59     ensures { data = (old data)[a <- v] }
  60   *)
  61
  62   (* registers *)
  63   val r0 : ref int
  64   val r1 : ref int
  65   val r2 : ref int
  66   val r3 : ref int
  67   (* ... *)
  68   val fp : ref int
  69   val pc : ref int (* pc *)
  70
  71   val ldr (r : ref int) (a : int) : unit writes {r}
  72     ensures { !r = !mem[a] }
  73
  74   val str (r : ref int) (a : int) : unit writes {mem}
  75     ensures { !mem = (old !mem)[a <- !r] }
  76
  77   (* condition flags *)
  78   val le : ref bool
  79
  80   val cmp (r : ref int) (v : int) : unit writes {le}
  81     ensures { !le=True <-> !r <= v }
  82
  83 end
  84
  85 (*
  86 @@ logic separation (fp : int) = a+10 < fp-24
  87
  88 main:
  89     @@ assume separation fp
  90
  91 .L2:@@ invariant ...
  92
  93 .L3:
  94
  95 .L4:@@ invariant ...
  96
  97 *)
  98
  99 module InsertionSortExample
 100
 101   use ARM
 102
 103   (* i = fp-16
 104      j = fp-20
 105      temp = fp-24 *)
 106
 107   val l4 : ref int
 108   val l7 : ref int
 109
 110   function a : int
 111
 112   (* stack and data segment do not overlap *)
 113   predicate separation (fp : int) = a+10 < fp-24
 114
 115   predicate inv (mem: map int int) =
 116     mem[a] = 0 /\ forall k:int. 1 <= k <= 10 -> 0 < mem[a + k]
 117
 118   predicate inv_l2 (mem: map int int) (fp : int) (l4 : int) =
 119     2 <= mem[fp - 16] <= 11 /\ l4 = mem[fp-16] - 2 /\ inv mem
 120
 121   let path_init_l2 ()
 122     requires { separation !fp /\ inv !mem }
 123     ensures  { inv_l2 !mem !fp !l4 }
 124   = l4 := 0; l7 := 0;
 125     r3 := 2;
 126     str r3 (!fp - 16)
 127
 128   let path_l2_exit ()
 129     requires { separation !fp /\ inv_l2 !mem !fp !l4 }
 130     ensures  { !l4 = 9 }
 131   = ldr r3 (!fp - 16);
 132     cmp r3 10;
 133     assume { !le = False }
 134
 135 end