package linksem

  1. Overview
  2. Docs
A formalisation of the core ELF and DWARF file formats written in Lem

Install

Dune Dependency

Authors

Maintainers

Sources

0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2

doc/src/linksem_zarith/dwarf_ctypes.ml.html

Source file dwarf_ctypes.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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
(*Generated by Lem from dwarf_ctypes.lem.*)
open Lem_basic_classes
open Lem_bool
open Lem_function
open Lem_maybe
open Lem_num
open Lem_string

open Lem_list (* TODO: check why this is not imported in ELF *)

(* these are Lem types of C source type names, based on Cerberus
frontend/model/ctype.lem (see the types "ctype_" and "tag_definition")
and pointer arithmetic, based on
frontend/model/defacto_memory_types.lem (see "shift_path_element").

They will need to be adapted significantly to exactly match the DWARF
notion of C source types, at least for those we use.  *)


(* (C) Justus Matthiesen
 *     Kayvan Memarian
 *     Victor Gomes
 *)



  
type sym = string (* in cerberus this is Symbol.sym; here we maight want a unique die tag *)  

type cabs_identifier = string (* in cerberus this is Cabs.cabs_identifier *)

type integer_value_base = int (* in cerberus this is more complex...*)

      
type (* name = "^\\(\\|\\([a-z A-Z]+_\\)\\)ibty[0-9]*'?$"*) integerBaseType =
 | Ichar
 | Short
 | Int_
 | Long
 | LongLong
   (* Things defined in the standard libraries *)
 | IntN_t of int
 | Int_leastN_t of int
 | Int_fastN_t of int
 | Intmax_t
 | Intptr_t

(* STD §6.2.5#17, sentence 1 *)
type integerType (* [name = "^\\(\\|\\([a-z A-Z]+_\\)\\)ity[0-9]*'?$"] *) =
 | Char
 | Bool
 | Signed of integerBaseType
 | Unsigned of integerBaseType
 | Enum of sym
   (* Things defined in the standard libraries *)
 | Wchar_t
 | Wint_t
 | Size_t
 | Ptrdiff_t

(* STD §6.2.5#10, sentence 1 *)
type realFloatingType =
  | Float
  | Double
  | LongDouble

(* STD §6.2.5#11, sentence 2 *)
type floatingType =
  | RealFloating of realFloatingType
(*  | Complex of floatingType (* STD §6.2.5#11, sentence 1 *) *)

(* STD §6.2.5#14, sentence 1 *)
type (* name = "^\\(\\|\\([a-z A-Z]+_\\)\\)bty[0-9]*'?$"*) basicType =
 | Integer of integerType
 | Floating of floatingType

(* STD §6.2.5#26, sentence 1-2 *)
type qualifiers (*[name = "^\\(\\|\\([a-z A-Z]+_\\)\\)qs[0-9]*'?$"]*) = {
  const    : bool;
  restrict : bool;
  volatile : bool;
  (* NOTE: the desugaring collapse _Atomic qualifiers and specifiers *)
}

type ctype_ (*[name = "^\\([a-z A-Z]*_\\)?ty[0-9]*'?$"]*) =
 | Void
 | Basic of basicType
   (* INVARIANT if the element ctype is an array, the qualifiers must be empty *)
   (* the qualifiers are that of the element type (§6.7.3#9) *)
   (* STD §6.2.5#20, bullet 1 *)
 | Array of ctype * ( Nat_big_num.num option)
   (* NOTE: the qualifiers associated to a ctype in the
            list of parameters is that of the parameter lvalue. For example if
            we have a parameter with type "restrict pointer to a const char",
            the qualifiers in the tuple will be:
              {no_qualifiers with restrict=true} *)
   (* STD §6.2.5#20, bullet 4 *)
 | Function of (* has_proto *)bool * (qualifiers * ctype)
             * (qualifiers * ctype * (* is_register *)bool) list
             * (* is_variadic *)bool
   (* STD §6.2.5#20, bullet 5 *)
   (* NOTE: the qualifiers are that of the referenced type *)
 | Pointer of qualifiers * ctype
   (* STD §6.2.5#20, bullet 6 *)
 | Atomic of ctype
 | Struct of sym
 | Union of sym
and ctype =
  Ctype of ctype_ list

type struct_tag = sym
type union_tag  = sym
type member_id  = sym


type tag_definition =
  | StructDef of (cabs_identifier * (qualifiers * ctype)) list
  | UnionDef of (cabs_identifier * (qualifiers * ctype)) list


type shift_path_element =
  | SPE_array of ctype * integer_value_base
  | SPE_member of sym (*struct/union tag*) * cabs_identifier (*member*) 
 
OCaml

Innovation. Community. Security.