ocaml64.drv 4.11 KB
Newer Older
1 2 3 4 5

(* OCaml driver for 64-bit architecture *)

import "ocaml-gen.drv"

6 7 8 9
(* TODO bv.BV31 ? *)

(* TODO bv.BV32 -> int or int32 ? *)

10 11 12 13 14 15 16 17 18 19 20 21
module mach.int.Int32
  syntax val of_int "Why3__BigInt.to_int"
  syntax converter of_int "%1"

  syntax function to_int "(Why3__BigInt.of_int %1)"

  syntax type     int32     "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
22
  syntax val      ( % )     "(mod)"
23 24 25 26 27 28 29 30 31 32 33 34 35
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end

module mach.int.UInt32
  syntax val of_int "Why3__BigInt.to_int"
  syntax converter of_int "%1"

  syntax function to_int "(Why3__BigInt.of_int %1)"
36
  syntax constant zero_unsigned "0"
37 38 39 40 41 42 43

  syntax type     uint32    "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
44
  syntax val      ( % )     "(mod)"
45 46 47 48 49 50
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
51 52 53 54 55 56 57 58 59 60 61 62 63 64


  syntax val      add_with_carry "(fun x y c ->
    let r = x + y + c in
    (r land 0xFFFFFFFF,r lsr 32))"

  syntax val      add3 "(fun x y z ->
    let r = x + y + z in
    (r land 0xFFFFFFFF,r lsr 32))"

  syntax val      mul_double "(fun x y ->
    let r = Int64.mul (Int64.of_int x) (Int64.of_int y) in
    (Int64.to_int (Int64.logand r 0xFFFFFFFFL),Int64.to_int (Int64.shift_right_logical r 32)))"

65 66
end

67 68 69
theory bv.BV63
  syntax type      t      "int"
  syntax constant  zero   "0"
70
  syntax constant  ones    "-1"
71 72 73 74 75
  syntax function  bw_and "(%1 land %2)"
  syntax predicate eq     "(%1 = %2)"
  (* TODO ... *)
end

76 77 78 79 80 81 82 83 84 85 86 87
module mach.int.Int63
  syntax val of_int "Why3__BigInt.to_int"
  syntax converter of_int "%1"

  syntax function to_int "(Why3__BigInt.of_int %1)"

  syntax type     int63     "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
88
  syntax val      ( % )     "(mod)"
89 90 91 92 93 94
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
95 96 97

  syntax val      to_bv     "(fun x -> x)"
  syntax val      of_bv     "(fun x -> x)"
98 99
end

100 101
(* TODO bv.BV64 -> int64 *)

102 103 104 105 106 107 108 109 110 111 112 113
module mach.int.Int64
  syntax val of_int "Why3__BigInt.to_int64"
  syntax converter of_int "%1L"

  syntax function to_int "(Why3__BigInt.of_int64 %1)"

  syntax type     int64     "Int64.t"
  syntax val      (+)       "Int64.add"
  syntax val      (-)       "Int64.sub"
  syntax val      (-_)      "Int64.neg"
  syntax val      ( * )     "Int64.mul"
  syntax val      (/)       "Int64.div"
114
  syntax val      (%)       "Int64.mod"
115 116 117 118 119 120 121 122
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end

123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
(* arrays *)

module mach.array.Array32
  syntax type array  "(%1 array)"

  syntax val  make   "Array.make"
  syntax val  ([])   "Array.get"
  syntax val  ([]<-) "Array.set"
  syntax val  length "Array.length"
  syntax val  append "Array.append"
  syntax val  sub    "Array.sub"
  syntax val  copy   "Array.copy"
  syntax val  fill   "Array.fill"
  syntax val  blit   "Array.blit"
  syntax val  self_blit "Array.blit"
end

module mach.array.Array63
  syntax type array  "(%1 array)"

  syntax val  make   "Array.make"
  syntax val  ([])   "Array.get"
  syntax val  ([]<-) "Array.set"
  syntax val  length "Array.length"
  syntax val  append "Array.append"
  syntax val  sub    "Array.sub"
  syntax val  copy   "Array.copy"
  syntax val  fill   "Array.fill"
  syntax val  blit   "Array.blit"
  syntax val  self_blit "Array.blit"
end