Source file `abstract_linker_script.ml`

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