1 files changed, 59 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/abstract_linker_script.ml b/lib/ocaml_rts/linksem/abstract_linker_script.ml
new file mode 100644
index 00000000..547b3b2d
--- /dev/null
+++ b/lib/ocaml_rts/linksem/abstract_linker_script.ml
@@ -0,0 +1,59 @@
+(*Generated by Lem from abstract_linker_script.lem.*)
+open Lem_basic_classes
+open Lem_list
+open Lem_num
+
+type binary_relation
+  = Eq0
+  | Lt0
+
+type binary_connective
+  = And0 (** Conjunction *)
+  | Or0  (** Disjunction *)
+
+(** The type [expression] denotes addresses, whether known or to be ascertained.
+  *)
+type expression
+  = Var0   of string   (** Ranges over memory addresses *)
+  | Const of Nat_big_num.num  (** Fixed memory address *)
+
+(* These are *one-place* predicates on unsigned integer solutions (usually representing 
+ * addresses). Implicitly, every binary relation is being applied to the solution. HMM: is 
+ * this sane? Taking my lead from KLEE / SMT solver formulae. What we're describing is a
+ * big SMT instance; it's sane if we can always factor the instances we want into this 
+ * form, i.e. into a big conjunction of per-variable formulae where each two-place relation
+ * has the variable in one of its places. 
+ * 
+ * Could try to claim it follows from taking CNF and assigning
+ * each conjunct to one of the variables it contains. But what if that conjunct is a big 
+ * disjunction including some other binary operators applied to two other variables?
+ * Might need to factor those out into a "global" extra conjunct. YES. *)
+type value_formula
+  = VFTrue
+  | VFFalse
+  | VFBinaryRelation of (binary_relation * expression)
+  | VFBinaryConnective of (binary_connective * value_formula * value_formula)
+  | VFNot of value_formula
+
+type memory_image_formula
+  = MIFTrue
+  | MIFFalse
+  | MIFExists of (string * memory_image_formula)
+  | MIFBinaryRelation of (binary_relation * expression * expression)
+  | MIFBinaryConnective of (binary_connective * memory_image_formula * memory_image_formula)
+  | MIFAssertValueFormula of (expression * value_formula)
+  | MIFNot of memory_image_formula
+
+type memory_image0
+  = MemoryImage of memory_image_formula
+
+(*val mk_range : natural -> natural -> value_formula*)
+let rec mk_range left right:value_formula=  
+ (if Nat_big_num.equal left right then
+    VFTrue
+  else if Nat_big_num.less right left then
+    VFFalse
+  else
+    let l = (Const left) in
+    let r = (Const right) in
+    VFBinaryConnective(And0, VFBinaryRelation(Lt0, r), VFNot(VFBinaryRelation(Lt0, l))))