arm.mlw 2.9 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 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

(* experiments related to ARM program verification *)

module M

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

  parameter a : array int

  logic inv (a : t int int) = 
    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
        a[!j <- a[!j - 1]];
        a[!j - 1 <- temp];
        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)
  parameter mem_ldr : a:int -> {} int reads mem { result = mem[a] }
  parameter mem_str : a:int -> v:int -> 
    {} int writes mem { mem = (old mem)[a <- v] }

  (* 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 : 
    r:ref int -> a:int -> {} unit reads mem writes r { r = mem[a] }
  parameter str : 
    r:ref int -> a:int -> {} unit reads r writes mem { mem = (old mem)[a <- r] }

  (* condition flags *)
  parameter le : ref bool

  parameter cmp : r:ref int -> v:int -> 
    {} 
    unit reads r writes le 
    { le=True <-> r <= v }

end

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: 
*)