blob: 547b3b2dab845556ed3892dffc6dc1007144b362 (
plain)
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))))
|
