Add in elf model from Dominic/Stephen. Make run_power build again. Does not effectively use elf model yet

1 files changed, 87 insertions, 0 deletions

diff --git a/src/elf_model/bitstring.lem b/src/elf_model/bitstring.lem
new file mode 100644
index 00000000..ed9df857
--- /dev/null
+++ b/src/elf_model/bitstring.lem
@@ -0,0 +1,87 @@
+open import Basic_classes
+open import Bool
+open import Num
+open import Show
+
+open import Error
+
+declare {ocaml} rename module = bitstring_local
+
+type bitstring
+
+declare ocaml target_rep type bitstring = `Bitstring.bitstring`
+
+(** [empty] is the empty bitstring.
+  *)
+val empty : bitstring
+
+declare ocaml target_rep function empty = `Bitstring.empty`
+
+(** [zeros m] creates a bitstring of length [m] containing all zeros.
+  *)
+val zeros : nat -> bitstring
+
+declare ocaml target_rep function zeros = `Bitstring.create_bitstring`
+
+(** [create m c] creates a bitstring of length [m] containing all [c]
+  * characters.
+  *)
+val create : nat -> char -> bitstring
+
+declare ocaml target_rep function create = `Bitstring.make_bitstring`
+
+(** [concat xs] concatenates a list of bitstrings [xs] into a single bitstring.
+  *)
+val concat : list bitstring -> bitstring
+
+declare ocaml target_rep function concat = `Bitstring.concat`
+
+(** [acquire fname] acquires a bitstring from a binary file, located at [fname].
+  *)
+val acquire : string -> error bitstring
+
+declare ocaml target_rep function acquire = `Ml_bindings.acquire_bitstring`
+
+(** [length bs0] returns the length of bitstring [bs0].
+  *)
+val length : bitstring -> nat
+
+declare ocaml target_rep function length = `Bitstring.bitstring_length`
+
+(** [partition offset bs0] cuts [bs0] into two pieces at offset [offset].  Throws
+  * an exception if 
+  *)
+val partition : nat -> bitstring -> (bitstring * bitstring)
+
+declare ocaml target_rep function partition = `Ml_bindings.partition_bitstring`
+
+(** [offset_and_cut offset size bs0] cuts a [size]-lengthed bitstring out of [bs0]
+  * at offset [offset].
+  *)
+val offset_and_cut : nat -> nat -> bitstring -> bitstring
+let offset_and_cut offset size bs0 =
+  let (_, cut) = partition offset bs0 in
+  let (rel, _) = partition size cut in
+    rel
+
+(** [equal bs0 bs1] tests whether [bs0] and [bs1] are equal.
+  *)
+val equal : bitstring -> bitstring -> bool
+
+declare ocaml target_rep function equal = unsafe_structural_equality
+
+(** [string_of_bitstring bs0] produces a string-based representation of bitstring
+  * [bs0].
+  *)
+val string_of_bitstring : bitstring -> string
+
+declare ocaml target_rep function string_of_bitstring = `Bitstring.string_of_bitstring`
+
+instance (Eq bitstring)
+  let (=) = equal
+  let (<>) l r = not (equal l r)
+end
+
+instance (Show bitstring)
+  let show = string_of_bitstring
+end