Add ocaml run-time and updates to sail for ocaml backend

8 files changed, 1686 insertions, 0 deletions

diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_abi.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_abi.ml
new file mode 100644
index 00000000..7371547f
--- /dev/null
+++ b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_abi.ml
@@ -0,0 +1,131 @@
+(*Generated by Lem from gnu_extensions/gnu_ext_abi.lem.*)
+open Lem_basic_classes
+open Lem_function
+open Lem_string
+open Lem_tuple
+open Lem_bool
+open Lem_list
+open Lem_sorting
+open Lem_num
+open Lem_maybe
+open Lem_assert_extra
+open Show
+open Missing_pervasives
+
+open Byte_sequence
+
+(* open import Abis *)
+
+open Elf_file
+open Elf_header
+open Elf_interpreted_segment
+open Elf_interpreted_section
+open Elf_program_header_table
+open Elf_section_header_table
+open Elf_symbol_table
+open Elf_types_native_uint
+open Elf_relocation
+open Elf_types_native_uint
+open Memory_image
+
+(** Optional, like [stt_func] but always points to a function or piece of
+  * executable code that takes no arguments and returns a function pointer.
+  *)
+let stt_gnu_ifunc : Nat_big_num.num= (Nat_big_num.of_int 10)
+
+(*val gnu_extend: forall 'abifeature. abi 'abifeature -> abi 'abifeature*)
+let gnu_extend a:'abifeature abi=   
+  ({ is_valid_elf_header = (a.is_valid_elf_header)
+    ; make_elf_header     =            
+( (*  t -> entry -> shoff -> phoff -> phnum -> shnum -> shstrndx -> hdr *)fun t -> fun entry -> fun shoff -> fun phoff -> fun phnum -> fun shnum -> fun shstrndx ->
+            let unmod = (a.make_elf_header t entry shoff phoff phnum shnum shstrndx)
+            in
+              { elf64_ident    = ((match unmod.elf64_ident with 
+                i0 :: i1 :: i2 :: i3  :: i4  :: i5  :: i6  :: 
+                _  :: _  :: i9 :: i10 :: i11 :: i12 :: i13 :: i14 :: i15 :: []
+                    -> [i0; i1; i2; i3; i4; i5; i6;
+                        Uint32.of_string (Nat_big_num.to_string elf_osabi_gnu);
+                        Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1));
+                        i9; i10; i11; i12; i13; i14; i15]
+                ))
+               ; elf64_type     = (Uint32.of_string (Nat_big_num.to_string t))
+               ; elf64_machine  = (unmod.elf64_machine)
+               ; elf64_version  = (unmod.elf64_version)
+               ; elf64_entry    = (unmod.elf64_entry)
+               ; elf64_phoff    = (Uint64.of_string (Nat_big_num.to_string phoff))
+               ; elf64_shoff    = (Uint64.of_string (Nat_big_num.to_string shoff))
+               ; elf64_flags    = (unmod.elf64_flags)
+               ; elf64_ehsize   = (unmod.elf64_ehsize)
+               ; elf64_phentsize= (unmod.elf64_phentsize)
+               ; elf64_phnum    = (Uint32.of_string (Nat_big_num.to_string phnum))
+               ; elf64_shentsize= (unmod.elf64_shentsize)
+               ; elf64_shnum    = (Uint32.of_string (Nat_big_num.to_string shnum))
+               ; elf64_shstrndx = (Uint32.of_string (Nat_big_num.to_string shstrndx))
+               })
+    ; reloc               = (a.reloc)
+    ; section_is_special  = (fun isec1 -> (fun img2 -> (
+                                a.section_is_special isec1 img2
+                                || (                                 
+(Lem.option_equal (=)(Ml_bindings.string_prefix (Nat_big_num.of_int (String.length ".gnu.warning")) isec1.elf64_section_name_as_string) (Some(".gnu.warning"))))
+        (* FIXME: This is a slight abuse. The GNU linker's treatment of 
+         * ".gnu.warning.*" section is not really a function of the output
+         * ABI -- it's a function of the input ABI, or arguably perhaps just
+         * of the linker itself. We have to do something to make sure these
+         * sections get silently processed separately from the usual linker
+         * control script, because otherwise our link map output doesn't match
+         * the GNU linker's. By declaring these sections "special" we achieve
+         * this by saying they don't participate in linking proper, just like 
+         * ".symtab" and similar sections don't. HMM. I suppose this is 
+         * okay, in that although a non-GNU linker might happily link these
+         * sections, arguably that is a failure to understand the input files. 
+         * But the issue about it being a per-input-file property remains.
+         * Q. What does the GNU linker do if a reloc input file whose OSABI
+         * is *not* GNU contains a .gnu.warning.* section? That would be a fair
+         * test about whether looking at the input ABI is worth doing. *)
+                            )))
+    ; section_is_large    = (a.section_is_large)
+    ; maxpagesize         = (a.maxpagesize)
+    ; minpagesize         = (a.minpagesize)
+    ; commonpagesize      = (a.commonpagesize)
+    ; symbol_is_generated_by_linker = (a.symbol_is_generated_by_linker)
+    ; make_phdrs          = (a.make_phdrs) (* FIXME: also make the GNU phdrs! *)
+    ; max_phnum           = (Nat_big_num.add(Nat_big_num.of_int 1) a.max_phnum) (* FIXME: GNU_RELRO, GNU_STACK; what else? *)
+    ; guess_entry_point   = (a.guess_entry_point)
+    ; pad_data            = (a.pad_data)
+    ; pad_code            = (a.pad_code)
+    ; generate_support    = (fun input_fnames_and_imgs -> 
+        let vanilla_support_img = (a.generate_support input_fnames_and_imgs) in
+        (* also generate .note.gnu.build-id *)
+        let new_by_range = (Pset.add (Some(".note.gnu.build-id", (Nat_big_num.of_int 0,Nat_big_num.of_int 24)), FileFeature(ElfSection(Nat_big_num.of_int 4 (* HACK: calculate this *), 
+          { elf64_section_name =(Nat_big_num.of_int 0) (* ignored *)
+           ; elf64_section_type = sht_note
+           ; elf64_section_flags = shf_alloc
+           ; elf64_section_addr =(Nat_big_num.of_int 0) (* ignored -- covered by element *)
+           ; elf64_section_offset =(Nat_big_num.of_int 0) (* ignored -- will be replaced when file offsets are assigned *)
+           ; elf64_section_size =(Nat_big_num.of_int 24) (* ignored? NO, we use it in linker_script to avoid plumbing through the element record *)
+           ; elf64_section_link =(Nat_big_num.of_int 0)
+           ; elf64_section_info =(Nat_big_num.of_int 0)
+           ; elf64_section_align =(Nat_big_num.of_int 4)
+           ; elf64_section_entsize =(Nat_big_num.of_int 0)
+           ; elf64_section_body = Byte_sequence.empty (* ignored *)
+           ; elf64_section_name_as_string = ".note.gnu.build-id"
+           }
+        ))) vanilla_support_img.by_range)
+        in
+        {  elements = (Pmap.add ".note.gnu.build-id" {
+                startpos = None
+           ;    length1 = (Some(Nat_big_num.of_int 24))
+           ;    contents = ([])
+           } (vanilla_support_img.elements))
+         ;   by_tag = (by_tag_from_by_range 
+  (instance_Basic_classes_SetType_Maybe_maybe_dict
+     (instance_Basic_classes_SetType_tup2_dict
+        instance_Basic_classes_SetType_var_dict
+        (instance_Basic_classes_SetType_tup2_dict
+           instance_Basic_classes_SetType_Num_natural_dict
+           instance_Basic_classes_SetType_Num_natural_dict))) instance_Basic_classes_SetType_var_dict new_by_range)
+         ;   by_range = new_by_range
+         })
+    ; concretise_support  = (a.concretise_support)
+    ; get_reloc_symaddr   = (a.get_reloc_symaddr)
+    })
diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_dynamic.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_dynamic.ml
new file mode 100644
index 00000000..e2957380
--- /dev/null
+++ b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_dynamic.ml
@@ -0,0 +1,531 @@
+(*Generated by Lem from gnu_extensions/gnu_ext_dynamic.lem.*)
+(** [gnu_ext_dynamic] contains GNU extension specific definitions related to the
+  * .dynamic section of an ELF file.
+  *)
+
+open Lem_basic_classes
+open Lem_bool
+open Lem_num
+open Lem_string
+
+open Error
+open Show
+open String_table
+
+open Elf_dynamic
+open Elf_types_native_uint
+
+(** Additional dynamic entries, see LSB section 11.3.2.2.
+  * All values taken from elf.c from binutils and GLIBC as the LSB does not
+  * specify them.
+  *
+  *  98 #define OLD_DT_LOOS     0x60000000
+  *  99 #define DT_LOOS         0x6000000d
+  * 100 #define DT_HIOS         0x6ffff000
+  * 101 #define DT_VALRNGLO     0x6ffffd00
+  * 102 #define DT_VALRNGHI     0x6ffffdff
+  * 103 #define DT_ADDRRNGLO    0x6ffffe00
+  * 104 #define DT_ADDRRNGHI    0x6ffffeff
+  * 105 #define DT_VERSYM       0x6ffffff0
+  * 106 #define DT_RELACOUNT    0x6ffffff9
+  * 107 #define DT_RELCOUNT     0x6ffffffa
+  * 108 #define DT_FLAGS_1      0x6ffffffb
+  * 109 #define DT_VERDEF       0x6ffffffc
+  * 110 #define DT_VERDEFNUM    0x6ffffffd
+  * 111 #define DT_VERNEED      0x6ffffffe
+  * 112 #define DT_VERNEEDNUM   0x6fffffff
+  * 113 #define OLD_DT_HIOS     0x6fffffff
+  * 114 #define DT_LOPROC       0x70000000
+  * 115 #define DT_HIPROC       0x7fffffff
+  *)
+
+let elf_dt_gnu_addrrnghi  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523967)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1))  (*0x6ffffeff*)
+let elf_dt_gnu_addrrnglo  : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 939523840)(Nat_big_num.of_int 2))        (*0x6ffffe00*)
+let elf_dt_gnu_auxiliary  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 1073741822)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x7ffffffd*)
+let elf_dt_gnu_filter     : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 1073741823)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x7fffffff*)
+(** The following is "specified" in the LSB document but is not present in the
+  * elf.c file so taken from elf.h from GLIBC:
+  *)
+let elf_dt_gnu_num        : Nat_big_num.num= (Nat_big_num.of_int 32) (** ??? This should match something *)
+let elf_dt_gnu_posflag_1  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523838)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffdfd*)
+let elf_dt_gnu_relcount   : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 939524093)(Nat_big_num.of_int 2))       (*0x6ffffffa*)
+let elf_dt_gnu_relacount  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939524092)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6FFFFFF9*)
+let elf_dt_gnu_syminent   : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523839)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffdff*)
+let elf_dt_gnu_syminfo    : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523967)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffeff*)
+let elf_dt_gnu_syminsz    : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 939523839)(Nat_big_num.of_int 2))       (*0x6ffffdfe*)
+let elf_dt_gnu_valrnghi   : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523839)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffdff*)
+let elf_dt_gnu_valrnglo   : Nat_big_num.num=  ( Nat_big_num.mul(Nat_big_num.of_int 939523712)(Nat_big_num.of_int 2))     (*0x6ffffd00*)
+let elf_dt_gnu_verdef     : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 939524094)(Nat_big_num.of_int 2))       (*0x6ffffffc*)
+let elf_dt_gnu_verdefnum  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939524094)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffffd*)
+let elf_dt_gnu_verneed    : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 939524095)(Nat_big_num.of_int 2))       (*0x6ffffffe*)
+let elf_dt_gnu_verneednum : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939524095)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6fffffff*)
+let elf_dt_gnu_versym     : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 939524088)(Nat_big_num.of_int 2))       (*0x6ffffff0*)
+
+(** Not present in the LSB but turns up in "real" ELF files... *)
+
+let elf_dt_gnu_hash      : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523962)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffef5*)
+let elf_dt_gnu_flags_1   : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939524093)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffffb*)
+let elf_dt_gnu_checksum  : Nat_big_num.num=  ( Nat_big_num.mul(Nat_big_num.of_int 939523836)(Nat_big_num.of_int 2))     (* 0x6FFFFDF8 *)
+let elf_dt_gnu_prelinked : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939523834))(Nat_big_num.of_int 1)) (* 0x6FFFFDF5 *)
+
+(** Extended DT flags for FLAGS_1 dynamic section types.  Taken from GLibC source
+  * as they appear to be completely unspecified!
+  *)
+  
+let gnu_df_1_now        : Nat_big_num.num= (Nat_big_num.of_int 1)     (*0x00000001*)
+let gnu_df_1_global     : Nat_big_num.num= (Nat_big_num.of_int 2)     (*0x00000002*)
+let gnu_df_1_group      : Nat_big_num.num= (Nat_big_num.of_int 4)     (*0x00000004*)
+let gnu_df_1_nodelete   : Nat_big_num.num= (Nat_big_num.of_int 8)     (*0x00000008*)
+let gnu_df_1_loadfltr   : Nat_big_num.num= (Nat_big_num.of_int 16)    (*0x00000010*)
+let gnu_df_1_initfirst  : Nat_big_num.num= (Nat_big_num.of_int 32)    (*0x00000020*)
+let gnu_df_1_noopen     : Nat_big_num.num= (Nat_big_num.of_int 64)    (*0x00000040*)
+let gnu_df_1_origin     : Nat_big_num.num= (Nat_big_num.of_int 128)   (*0x00000080*)
+let gnu_df_1_direct     : Nat_big_num.num= (Nat_big_num.of_int 256)   (*0x00000100*)
+let gnu_df_1_trans      : Nat_big_num.num= (Nat_big_num.of_int 512)   (*0x00000200*)
+let gnu_df_1_interpose  : Nat_big_num.num= (Nat_big_num.of_int 1024)  (*0x00000400*)
+let gnu_df_1_nodeflib   : Nat_big_num.num= (Nat_big_num.of_int 2048)  (*0x00000800*)
+let gnu_df_1_nodump     : Nat_big_num.num= (Nat_big_num.of_int 4096)  (*0x00001000*)
+let gnu_df_1_confalt    : Nat_big_num.num= (Nat_big_num.of_int 8192)  (*0x00002000*)
+let gnu_df_1_endfiltee  : Nat_big_num.num= (Nat_big_num.of_int 16384) (*0x00004000*)
+let gnu_df_1_dispreldne : Nat_big_num.num= (Nat_big_num.of_int 32768) (*0x00008000*)
+let gnu_df_1_disprelpnd : Nat_big_num.num= (Nat_big_num.of_int 65536) (*0x00010000*)
+
+(** [gnu_string_of_dt_flag1 m] produces a string based representation of GNU
+  * extensions flag_1 value [m].
+  *)
+(*val gnu_string_of_dt_flag_1 : natural -> string*)
+let gnu_string_of_dt_flag_1 flag:string=  
+ (if check_flag flag(Nat_big_num.of_int 0) then
+    "None"
+  else if check_flag flag gnu_df_1_now then
+    "NOW"
+  else if check_flag flag gnu_df_1_global then
+    "GLOBAL"
+  else if check_flag flag gnu_df_1_group then
+    "GROUP"
+  else if check_flag flag gnu_df_1_nodelete then
+    "NODELETE"
+  else if check_flag flag gnu_df_1_loadfltr then
+    "LOADFLTR"
+  else if check_flag flag gnu_df_1_initfirst then
+    "INITFIRST"
+  else if check_flag flag gnu_df_1_noopen then
+    "NOOPEN"
+  else if check_flag flag gnu_df_1_origin then
+    "ORIGIN"
+  else if check_flag flag gnu_df_1_direct then
+    "DIRECT"
+  else if check_flag flag gnu_df_1_trans then
+    "TRANS"
+  else if check_flag flag gnu_df_1_interpose then
+    "INTERPOSE"
+  else if check_flag flag gnu_df_1_nodeflib then
+    "NODEFLIB"
+  else if check_flag flag gnu_df_1_nodump then
+    "NODUMP"
+  else if check_flag flag gnu_df_1_confalt then
+    "CONFALT"
+  else if check_flag flag gnu_df_1_endfiltee then
+    "ENDFILTEE"
+  else if check_flag flag gnu_df_1_dispreldne then
+    "DISPRELDNE"
+  else if check_flag flag gnu_df_1_disprelpnd then
+    "DISPRELPND"
+  else if check_flag flag ( Nat_big_num.add gnu_df_1_nodelete gnu_df_1_now) then
+    "NOW NODELETE"
+  else if check_flag flag ( Nat_big_num.add gnu_df_1_nodelete gnu_df_1_initfirst) then
+    "NODELETE INITFIRST"
+  else (* XXX: add more as necessary *)
+    "Invalid GNU dynamic flag")
+
+(** [gnu_ext_os_additional_ranges m] checks whether dynamic section type [m]
+  * lies within the ranges set aside for GNU specific functionality.
+  * NB: quite ad hoc as this is not properly specified anywhere.
+  *)
+(*val gnu_ext_os_additional_ranges : natural -> bool*)
+let gnu_ext_os_additional_ranges m:bool=  
+ (if Nat_big_num.greater_equal m elf_dt_gnu_addrrnglo && Nat_big_num.less_equal m elf_dt_gnu_addrrnghi then
+    true
+  else Nat_big_num.equal (* ad hoc extensions go here... *)
+    m elf_dt_gnu_verneed || (Nat_big_num.equal
+    m elf_dt_gnu_verneednum || (Nat_big_num.equal
+    m elf_dt_gnu_versym || (Nat_big_num.equal
+    m elf_dt_gnu_verdef || (Nat_big_num.equal
+    m elf_dt_gnu_verdefnum || (Nat_big_num.equal
+    m elf_dt_gnu_flags_1 || (Nat_big_num.equal
+    m elf_dt_gnu_relcount || (Nat_big_num.equal
+    m elf_dt_gnu_relacount || (Nat_big_num.equal
+    m elf_dt_gnu_checksum || Nat_big_num.equal
+    m elf_dt_gnu_prelinked)))))))))
+
+(** [gnu_ext_tag_correspondence_of_tag0 m] produces a tag correspondence for the
+  * extended GNU-specific dynamic section types [m].  Used to provide the ABI
+  * specific functionality expected of the corresponding function in the elf_dynamic
+  * module.
+  *)
+(*val gnu_ext_tag_correspondence_of_tag0 : natural -> error tag_correspondence*)
+let gnu_ext_tag_correspondence_of_tag0 m:(tag_correspondence)error=  
+ (if Nat_big_num.equal m elf_dt_gnu_hash then
+    return C_Ptr
+  else if Nat_big_num.equal m elf_dt_gnu_flags_1 then
+    return C_Val
+  else if Nat_big_num.equal m elf_dt_gnu_versym then
+    return C_Ptr
+  else if Nat_big_num.equal m elf_dt_gnu_verneednum then
+    return C_Val
+  else if Nat_big_num.equal m elf_dt_gnu_verneed then
+    return C_Ptr
+  else if Nat_big_num.equal m elf_dt_gnu_verdef then
+    return C_Ptr
+  else if Nat_big_num.equal m elf_dt_gnu_verdefnum then
+    return C_Val
+  else if Nat_big_num.equal m elf_dt_gnu_relcount then
+    return C_Val
+  else if Nat_big_num.equal m elf_dt_gnu_relacount then
+    return C_Val
+  else if Nat_big_num.equal m elf_dt_gnu_checksum then
+    return C_Val
+  else if Nat_big_num.equal m elf_dt_gnu_prelinked then
+    return C_Val
+  else
+    fail "gnu_ext_tag_correspondence_of_tag0: invalid dynamic tag")
+
+(** [gnu_ext_tag_correspondence_of_tag m] produces a tag correspondence for the
+  * extended GNU-specific dynamic section types [m].  Used to provide the ABI
+  * specific functionality expected of the corresponding function in the elf_dynamic
+  * module.
+  * TODO: examine whether this and the function above really need separating into
+  * two functions.
+  *)
+(*val gnu_ext_tag_correspondence_of_tag : natural -> error tag_correspondence*)
+let gnu_ext_tag_correspondence_of_tag m:(tag_correspondence)error=  
+ (if Nat_big_num.greater_equal m elf_dt_gnu_addrrnglo && Nat_big_num.less_equal m elf_dt_gnu_addrrnghi then
+    return C_Ptr
+  else if Nat_big_num.greater_equal m elf_dt_gnu_valrnglo && Nat_big_num.less_equal m elf_dt_gnu_valrnghi then
+    return C_Val
+  else if gnu_ext_os_additional_ranges m then
+    gnu_ext_tag_correspondence_of_tag0 m
+  else if Nat_big_num.equal m elf_dt_gnu_syminsz then
+    return C_Val (** unsure *)
+  else if Nat_big_num.equal m elf_dt_gnu_syminfo then
+    return C_Ptr (** unsure *)
+  else if Nat_big_num.equal m elf_dt_gnu_syminent then
+    return C_Val (** unsure *)
+  else if Nat_big_num.equal m elf_dt_gnu_posflag_1 then
+    return C_Val (** unsure *)
+  else if Nat_big_num.equal m elf_dt_gnu_num then
+    return C_Ignored
+  else if Nat_big_num.equal m elf_dt_gnu_filter then
+    return C_Val (** unsure *)
+  else if Nat_big_num.equal m elf_dt_gnu_auxiliary then
+    return C_Val (** unsure *)
+  else
+    fail ("gnu_ext_tag_correspondence_of_tag: unrecognised GNU dynamic tag"))
+    
+(** [gnu_ext_elf32_value_of_elf32_dyn0 dyn] extracts a dynamic value from the
+  * dynamic section entry [dyn] under the assumption that its type is a GNU
+  * extended dynamic section type.  Fails otherwise.  Used to provide the
+  * ABI-specific functionality expected of the corresponding functions in
+  * elf_dynamic.lem.
+  *)
+(*val gnu_ext_elf32_value_of_elf32_dyn0 : elf32_dyn -> string_table -> error elf32_dyn_value*)
+let gnu_ext_elf32_value_of_elf32_dyn0 dyn stbl:(((Uint32.uint32),(Uint32.uint32))dyn_value)error=  
+ (let tag = (Nat_big_num.abs (Nat_big_num.of_int32 dyn.elf32_dyn_tag)) in
+    if Nat_big_num.equal tag elf_dt_gnu_hash then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_HASH must be a PTR"
+        | D_Ptr     p -> return p
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_HASH must be a PTR"
+      ) >>= (fun addr ->
+      return (Address addr))
+    else if Nat_big_num.equal tag elf_dt_gnu_flags_1 then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: FLAGS_1 must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: FlAGS_1 must be a Val"
+      ) >>= (fun f ->
+      return (Flags1 (Nat_big_num.of_string (Uint32.to_string f))))
+    else if Nat_big_num.equal tag elf_dt_gnu_versym then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERSYM must be a PTR"
+        | D_Ptr     p -> return p
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERSYM must be a PTR"
+      ) >>= (fun addr ->
+      return (Address addr))
+    else if Nat_big_num.equal tag elf_dt_gnu_verdef then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEF must be a PTR"
+        | D_Ptr     p -> return p
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEF must be a PTR"
+      ) >>= (fun addr ->
+      return (Address addr))
+    else if Nat_big_num.equal tag elf_dt_gnu_verdefnum then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEFNUM must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEFNUM must be a Val"
+      ) >>= (fun sz ->
+      return (Numeric (Nat_big_num.of_string (Uint32.to_string sz))))
+    else if Nat_big_num.equal tag elf_dt_gnu_verneednum then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEEDNUM must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEEDNUM must be a Val"
+      ) >>= (fun sz ->
+      return (Numeric (Nat_big_num.of_string (Uint32.to_string sz))))
+    else if Nat_big_num.equal tag elf_dt_gnu_verneed then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEED must be a PTR"
+        | D_Ptr     p -> return p
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEED must be a PTR"
+      ) >>= (fun addr ->
+      return (Address addr))
+    else if Nat_big_num.equal tag elf_dt_gnu_relcount then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELCOUNT must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELCOUNT must be a Val"
+      ) >>= (fun sz ->
+      return (Numeric (Nat_big_num.of_string (Uint32.to_string sz))))
+    else if Nat_big_num.equal tag elf_dt_gnu_relacount then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELACOUNT must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELACOUNT must be a Val"
+      ) >>= (fun sz ->
+      return (Numeric (Nat_big_num.of_string (Uint32.to_string sz))))
+    else if Nat_big_num.equal tag elf_dt_gnu_checksum then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: CHECKSUM must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: CHECKSUM must be a Val"
+      ) >>= (fun sz ->
+      return (Checksum (Nat_big_num.of_string (Uint32.to_string sz))))
+    else if Nat_big_num.equal tag elf_dt_gnu_prelinked then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_PRELINKED must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_PRELINKED must be a Val"
+      ) >>= (fun off ->
+      return (Timestamp (Nat_big_num.of_string (Uint32.to_string off))))
+    else
+      fail "gnu_ext_elf32_value_of_elf32_dyn0: unrecognised GNU dynamic tag")
+      
+(** [gnu_ext_elf64_value_of_elf64_dyn0 dyn] extracts a dynamic value from the
+  * dynamic section entry [dyn] under the assumption that its type is a GNU
+  * extended dynamic section type.  Fails otherwise.  Used to provide the
+  * ABI-specific functionality expected of the corresponding functions in
+  * elf_dynamic.lem.
+  *)
+(*val gnu_ext_elf64_value_of_elf64_dyn0 : elf64_dyn -> string_table -> error elf64_dyn_value*)
+let gnu_ext_elf64_value_of_elf64_dyn0 dyn stbl:(((Uint64.uint64),(Uint64.uint64))dyn_value)error=  
+ (let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in
+    if Nat_big_num.equal tag elf_dt_gnu_hash then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_HASH must be a PTR"
+        | D_Ptr     p -> return p
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_HASH must be a PTR"
+      ) >>= (fun addr ->
+      return (Address addr))
+    else if Nat_big_num.equal tag elf_dt_gnu_flags_1 then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: FLAGS_1 must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: FlAGS_1 must be a Val"
+      ) >>= (fun f ->
+      return (Flags1 (Ml_bindings.nat_big_num_of_uint64 f)))
+    else if Nat_big_num.equal tag elf_dt_gnu_versym then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERSYM must be a PTR"
+        | D_Ptr     p -> return p
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERSYM must be a PTR"
+      ) >>= (fun addr ->
+      return (Address addr))
+    else if Nat_big_num.equal tag elf_dt_gnu_verdef then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERDEF must be a PTR"
+        | D_Ptr     p -> return p
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERDEF must be a PTR"
+      ) >>= (fun addr ->
+      return (Address addr))
+    else if Nat_big_num.equal tag elf_dt_gnu_verdefnum then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf64_dyn: VERDEFNUM must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf64_dyn: VERDEFNUM must be a Val"
+      ) >>= (fun sz ->
+      return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz)))
+    else if Nat_big_num.equal tag elf_dt_gnu_verneednum then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEEDNUM must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEEDNUM must be a Val"
+      ) >>= (fun sz ->
+      return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz)))
+    else if Nat_big_num.equal tag elf_dt_gnu_verneed then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEED must be a PTR"
+        | D_Ptr     p -> return p
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEED must be a PTR"
+      ) >>= (fun addr ->
+      return (Address addr))
+    else if Nat_big_num.equal tag elf_dt_gnu_relcount then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELCOUNT must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELCOUNT must be a Val"
+      ) >>= (fun sz ->
+      return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz)))
+    else if Nat_big_num.equal tag elf_dt_gnu_relacount then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELACOUNT must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELACOUNT must be a Val"
+      ) >>= (fun sz ->
+      return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz)))
+    else if Nat_big_num.equal tag elf_dt_gnu_checksum then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: CHECKSUM must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: CHECKSUM must be a Val"
+      ) >>= (fun sz ->
+      return (Checksum (Ml_bindings.nat_big_num_of_uint64 sz)))
+    else if Nat_big_num.equal tag elf_dt_gnu_prelinked then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_PRELINKED must be a Val"
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_PRELINKED must be a Val"
+      ) >>= (fun off ->
+      return (Timestamp (Ml_bindings.nat_big_num_of_uint64 off)))
+    else
+      fail "gnu_ext_elf64_value_of_elf64_dyn0: unrecognised GNU dynamic tag")
+      
+(** [gnu_ext_elf32_value_of_elf32_dyn dyn] extracts a dynamic value from the
+  * dynamic section entry [dyn] under the assumption that its type is a GNU
+  * extended dynamic section type.  Fails otherwise.  Used to provide the
+  * ABI-specific functionality expected of the corresponding functions in
+  * elf_dynamic.lem.
+  * TODO: some of these cases are missing as they have never come up in "real"
+  * ELF files that have been processed as part of validation.  Try and find some
+  * files that do actually exhibit these.
+  *)
+(*val gnu_ext_elf32_value_of_elf32_dyn : elf32_dyn -> string_table -> error elf32_dyn_value*)
+let gnu_ext_elf32_value_of_elf32_dyn dyn stbl:(elf32_dyn_value)error=  
+ (let tag = (Nat_big_num.abs (Nat_big_num.of_int32 dyn.elf32_dyn_tag)) in
+    if gnu_ext_os_additional_ranges tag then (* this should cover valrngs and addrrngs *)
+      gnu_ext_elf32_value_of_elf32_dyn0 dyn stbl
+    else if Nat_big_num.equal tag elf_dt_gnu_syminsz then
+      (match dyn.elf32_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: SYMINSZ must be a VAL"
+        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: SYMINSZ must be a VAL"
+      ) >>= (fun sz ->
+      return (Size sz))
+    else if Nat_big_num.equal tag elf_dt_gnu_syminfo then
+      fail "SYMINFO" (* XXX: never seen in 32-bit ELF *)
+    else if Nat_big_num.equal tag elf_dt_gnu_syminent then
+      fail "SYMINENT" (* XXX: never seen in 32-bit ELF *)
+    else if Nat_big_num.equal tag elf_dt_gnu_posflag_1 then
+      fail "POSFLAG_1" (* XXX: never seen in 32-bit ELF *)
+    else if Nat_big_num.equal tag elf_dt_gnu_num then
+      fail "NUM" (* XXX: never seen in 32-bit ELF *)
+    else if Nat_big_num.equal tag elf_dt_gnu_filter then
+      fail "FILTER" (* XXX: never seen in 32-bit ELF *)
+    else if Nat_big_num.equal tag elf_dt_gnu_auxiliary then
+      fail "AUXILIARY" (* XXX: never seen in 32-bit ELF *)
+    else
+      fail "gnu_ext_elf32_value_of_elf32_dyn: unrecognised GNU dynamic tag")
+      
+(** [gnu_ext_elf64_value_of_elf64_dyn dyn] extracts a dynamic value from the
+  * dynamic section entry [dyn] under the assumption that its type is a GNU
+  * extended dynamic section type.  Fails otherwise.  Used to provide the
+  * ABI-specific functionality expected of the corresponding functions in
+  * elf_dynamic.lem.
+  * TODO: some of these cases are missing as they have never come up in "real"
+  * ELF files that have been processed as part of validation.  Try and find some
+  * files that do actually exhibit these.
+  *)
+(*val gnu_ext_elf64_value_of_elf64_dyn : elf64_dyn -> string_table -> error elf64_dyn_value*)
+let gnu_ext_elf64_value_of_elf64_dyn dyn stbl:(elf64_dyn_value)error=  
+ (let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in
+    if gnu_ext_os_additional_ranges tag then (* this should cover valrngs and addrrngs *)
+      gnu_ext_elf64_value_of_elf64_dyn0 dyn stbl
+    else if Nat_big_num.equal tag elf_dt_gnu_syminsz then
+      (match dyn.elf64_dyn_d_un with
+        | D_Val     v -> return v
+        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: SYMINSZ must be a VAL"
+        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: SYMINSZ must be a VAL"
+      ) >>= (fun sz ->
+      return (Size sz))
+    else if Nat_big_num.equal tag elf_dt_gnu_syminfo then
+      fail "SYMINFO" (* XXX: fill in as seen *)
+    else if Nat_big_num.equal tag elf_dt_gnu_syminent then
+      fail "SYMINENT" (* XXX: fill in as seen *)
+    else if Nat_big_num.equal tag elf_dt_gnu_posflag_1 then
+      fail "POSFLAG_1" (* XXX: fill in as seen *)
+    else if Nat_big_num.equal tag elf_dt_gnu_num then
+      fail "NUM" (* XXX: fill in as seen *)
+    else if Nat_big_num.equal tag elf_dt_gnu_filter then
+      fail "FILTER" (* XXX: fill in as seen *)
+    else if Nat_big_num.equal tag elf_dt_gnu_auxiliary then
+      fail "AUXILIARY" (* XXX: fill in as seen *)
+    else
+      fail "gnu_ext_elf64_value_of_elf64_dyn: unrecognised GNU dynamic tag")
+    
+(** [string_of_gnu_ext_dynamic_tag0 m] produces a string based representation of
+  * GNU extensions dynamic tag value [m].
+  *)
+(*val string_of_gnu_ext_dynamic_tag0 : natural -> string*)
+let string_of_gnu_ext_dynamic_tag0 m:string=  
+ (if Nat_big_num.equal m elf_dt_gnu_hash then
+    "GNU_HASH"
+  else if Nat_big_num.equal m elf_dt_gnu_flags_1 then
+    "FLAGS_1"
+  else if Nat_big_num.equal m elf_dt_gnu_versym then
+    "VERSYM"
+  else if Nat_big_num.equal m elf_dt_gnu_verneednum then
+    "VERNEEDNUM"
+  else if Nat_big_num.equal m elf_dt_gnu_verneed then
+    "VERNEED"
+  else if Nat_big_num.equal m elf_dt_gnu_relcount then
+    "RELCOUNT"
+  else if Nat_big_num.equal m elf_dt_gnu_relacount then
+    "RELACOUNT"
+  else if Nat_big_num.equal m elf_dt_gnu_verdefnum then
+    "VERDEFNUM"
+  else if Nat_big_num.equal m elf_dt_gnu_verdef then
+    "VERDEF"
+  else if Nat_big_num.equal m elf_dt_gnu_checksum then
+    "CHECKSUM"
+  else if Nat_big_num.equal m elf_dt_gnu_prelinked then
+    "GNU_PRELINKED"
+  else
+    "Invalid dynamic tag")
+    
+(** [string_of_gnu_ext_dynamic_tag m] produces a string based representation of
+  * GNU extensions dynamic tag value [m].
+  *)
+(*val string_of_gnu_ext_dynamic_tag : natural -> string*)
+let string_of_gnu_ext_dynamic_tag m:string=  
+ (if Nat_big_num.greater_equal m elf_dt_gnu_addrrnglo && Nat_big_num.less_equal m elf_dt_gnu_addrrnghi then
+    string_of_gnu_ext_dynamic_tag0 m
+  else if Nat_big_num.greater_equal m elf_dt_gnu_valrnglo && Nat_big_num.less_equal m elf_dt_gnu_valrnghi then
+    string_of_gnu_ext_dynamic_tag0 m
+  else if gnu_ext_os_additional_ranges m then
+    string_of_gnu_ext_dynamic_tag0 m
+  else if Nat_big_num.equal m elf_dt_gnu_syminsz then
+    "SYMINSZ"
+  else if Nat_big_num.equal m elf_dt_gnu_syminfo then
+    "SYMINFO"
+  else if Nat_big_num.equal m elf_dt_gnu_syminent then
+    "SYMINENT"
+  else if Nat_big_num.equal m elf_dt_gnu_posflag_1 then
+    "POSFLAG_1"
+  else if Nat_big_num.equal m elf_dt_gnu_num then
+    "NUM"
+  else if Nat_big_num.equal m elf_dt_gnu_filter then
+    "FILTER"
+  else if Nat_big_num.equal m elf_dt_gnu_auxiliary then
+    "AUXILIARY"
+  else
+    "Invalid dynamic tag")
diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_note.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_note.ml
new file mode 100644
index 00000000..f8f4328f
--- /dev/null
+++ b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_note.ml
@@ -0,0 +1,268 @@
+(*Generated by Lem from gnu_extensions/gnu_ext_note.lem.*)
+(** [gnu_ext_note] contains GNU extension specific definitions relating to the
+  * .note section/segment of an ELF file.
+  *)
+
+open Lem_basic_classes
+open Lem_bool
+open Lem_list
+open Lem_maybe
+open Lem_string
+
+open Byte_sequence
+open Endianness
+open Error
+open Missing_pervasives
+open String_table
+
+open Elf_note
+open Elf_section_header_table
+open Elf_types_native_uint
+
+open Gnu_ext_section_header_table
+
+(** The following two functions are utility functions to convert a list of bytes
+  * into words, ready for further processing into strings.
+  *)
+  
+(*val group_elf32_words : endianness -> list byte -> error (list elf32_word)*)
+let rec group_elf32_words endian xs:((Uint32.uint32)list)error=  
+ ((match xs with
+    | []                 -> return []
+    | x1::x2::x3::x4::xs ->
+      let bs0 = (Byte_sequence.from_byte_lists [[x1;x2;x3;x4]]) in
+      read_elf32_word   endian bs0 >>= (fun (w, _) ->
+      group_elf32_words endian xs  >>= (fun ws ->
+      return (w::ws)))
+    | xs                 -> fail "group_elf32_words: the impossible happened"
+  ))
+  
+(*val group_elf64_words : endianness -> list byte -> error (list elf64_word)*)
+let rec group_elf64_words endian xs:((Uint32.uint32)list)error=  
+ ((match xs with
+    | []                 -> return []
+    | x1::x2::x3::x4::xs ->
+      let bs0 = (Byte_sequence.from_byte_lists [[x1;x2;x3;x4]]) in
+      read_elf64_word   endian bs0 >>= (fun (w, _) ->
+      group_elf64_words endian xs  >>= (fun ws ->
+      return (w::ws)))
+    | xs                 -> fail "group_elf64_words: the impossible happened"
+  ))
+
+(** [gnu_ext_check_elf32_abi_note_tag_section endain sht stbl bs0] checks the
+  * .note.ABI-tag section of an ELF file to ensure conformance with the GNU
+  * extensions.  The string in this note should contain the string "GNU".
+  *)
+(*val gnu_ext_check_elf32_abi_note_tag_section : endianness -> elf32_section_header_table ->
+  string_table -> byte_sequence -> bool*)
+let gnu_ext_check_elf32_abi_note_tag_section endian sht sect_hdr_tbl bs0:bool=  
+ (let abi_note_sects =    
+(List.filter (fun x ->
+      if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_type)) sht_note then
+        let nm = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_name)) in
+          (match String_table.get_string_at nm sect_hdr_tbl with
+            | Success name1 -> name1 = ".note.ABI-tag"
+            | Fail _       -> false
+          )
+      else
+        false
+    ) sht)
+  in
+    (match abi_note_sects with
+      | [note] ->
+        let off = (Nat_big_num.of_string (Uint32.to_string note.elf32_sh_offset)) in
+        let siz = (Nat_big_num.of_string (Uint32.to_string note.elf32_sh_size)) in
+        let abi_tag =          
+(Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel ->
+          Elf_note.read_elf32_note endian rel >>= (fun (abi_tag, _) ->
+          return abi_tag)))
+        in
+          (match abi_tag with
+            | Fail _          -> false
+            | Success abi_tag ->
+              let str = (name_string_of_elf32_note abi_tag) in
+                if str = "GNU\000" then
+                  if Nat_big_num.greater_equal (Nat_big_num.of_string (Uint32.to_string abi_tag.elf32_note_descsz))(Nat_big_num.of_int 16) then
+                    let take2 = (Lem_list.take( 16) abi_tag.elf32_note_desc) in
+                      if List.length take2 < 16 then
+                        false
+                      else
+                        true
+                  else
+                    false
+                else
+                  false
+          )
+      | _      ->
+          false
+    ))
+
+(** [gnu_ext_check_elf64_abi_note_tag_section endain sht stbl bs0] checks the
+  * .note.ABI-tag section of an ELF file to ensure conformance with the GNU
+  * extensions.  The string in this note should contain the string "GNU".
+  *)
+(*val gnu_ext_check_elf64_abi_note_tag_section : endianness -> elf64_section_header_table ->
+  string_table -> byte_sequence -> bool*)
+let gnu_ext_check_elf64_abi_note_tag_section endian sht sect_hdr_tbl bs0:bool=  
+ (let abi_note_sects =    
+(List.filter (fun x ->
+      if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf64_sh_type)) sht_note then
+        let nm = (Nat_big_num.of_string (Uint32.to_string x.elf64_sh_name)) in
+          (match String_table.get_string_at nm sect_hdr_tbl with
+            | Success name1 -> name1 = ".note.ABI-tag"
+            | Fail _       -> false
+          )
+      else
+        false
+    ) sht)
+  in
+    (match abi_note_sects with
+      | [note] ->
+        let off = (Nat_big_num.of_string (Uint64.to_string note.elf64_sh_offset)) in
+        let siz = (Ml_bindings.nat_big_num_of_uint64 note.elf64_sh_size) in
+        let abi_tag =          
+(Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel ->
+          Elf_note.read_elf64_note endian rel >>= (fun (abi_tag, _) ->
+          return abi_tag)))
+        in
+          (match abi_tag with
+            | Fail _          -> false
+            | Success abi_tag ->
+              let str = (name_string_of_elf64_note abi_tag) in
+                if str = "GNU\000" then
+                  if Nat_big_num.greater_equal (Ml_bindings.nat_big_num_of_uint64 abi_tag.elf64_note_descsz)(Nat_big_num.of_int 16) then
+                    let take2 = (Lem_list.take( 16) abi_tag.elf64_note_desc) in
+                      if List.length take2 < 16 then
+                        false
+                      else
+                        true
+                  else
+                    false
+                else
+                  false
+          )
+      | _      ->
+          false
+    ))
+    
+(** [gnu_ext_extract_elf32_earliest_compatible_kernel end sht stab bs0] extracts
+  * the earliest compatible Linux kernel with the given ELF file from its section
+  * header table [sht], and string table [stbl], assuming endianness [endian].
+  * NB: marked as OCaml only as need to extract a string from integers.
+  * TODO: implement some string parsing functions in Isabelle/HOL so things like
+  * this can be extracted.
+  *)
+(*val gnu_ext_extract_elf32_earliest_compatible_kernel : endianness -> elf32_section_header_table ->
+  string_table -> byte_sequence -> error string*)
+let gnu_ext_extract_elf32_earliest_compatible_kernel endian sht sect_hdr_tbl bs0:(string)error=  
+ (let abi_note_sects =    
+(List.filter (fun x ->
+      if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_type)) sht_note then
+        let nm = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_name)) in
+          (match String_table.get_string_at nm sect_hdr_tbl with
+            | Success name1 -> name1 = ".note.ABI-tag"
+            | Fail _       -> false
+          )
+      else
+        false
+    ) sht)
+  in
+    (match abi_note_sects with
+      | [note] ->
+        let off = (Nat_big_num.of_string (Uint32.to_string note.elf32_sh_offset)) in
+        let siz = (Nat_big_num.of_string (Uint32.to_string note.elf32_sh_size)) in
+        let abi_tag =          
+(Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel ->
+          Elf_note.read_elf32_note endian rel >>= (fun (abi_tag, _) ->
+          return abi_tag)))
+        in
+          (match abi_tag with
+            | Fail _          -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: parsing of NOTE section failed"
+            | Success abi_tag ->
+              let str = (name_string_of_elf32_note abi_tag) in
+                if str = "GNU\000" then
+                  if Nat_big_num.greater_equal (Nat_big_num.of_string (Uint32.to_string abi_tag.elf32_note_descsz))(Nat_big_num.of_int 16) then
+                    let take2 = (Lem_list.take( 16) abi_tag.elf32_note_desc) in
+                      if List.length take2 < 16 then
+                        fail "gnu_ext_extract_elf32_earliest_compatible_kernel: the impossible happened"
+                      else
+                        (match group_elf32_words endian take2 with
+                          | Fail err   -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: word grouping failed"
+                          | Success ss ->
+                            (match ss with
+                              | c1::c2::c3::cs ->
+                                let c1 = (Uint32.to_string c1) in
+                                let c2 = (Uint32.to_string c2) in
+                                let c3 = (Uint32.to_string c3) in
+                                  return (List.fold_right (^) (intercalate "." [c1;c2;c3]) "")
+                              | _              -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: kernel version must have three components"
+                            )
+                        )
+                  else
+                    fail "gnu_ext_extract_elf32_earliest_compatible_kernel: .note.ABI-tag description size not required length"
+                else
+                  fail "gnu_ext_extract_elf32_earliest_compatible_kernel: required GNU string not present"
+          )
+      | _      -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: more than one .note.ABI-tag section present"
+    ))
+    
+(** [gnu_ext_extract_elf64_earliest_compatible_kernel end sht stab bs0] extracts
+  * the earliest compatible Linux kernel with the given ELF file from its section
+  * header table [sht], and string table [stbl], assuming endianness [endian].
+  * NB: marked as OCaml only as need to extract a string from integers.
+  * TODO: implement some string parsing functions in Isabelle/HOL so things like
+  * this can be extracted.
+  *)
+(*val gnu_ext_extract_elf64_earliest_compatible_kernel : endianness -> elf64_section_header_table ->
+  string_table -> byte_sequence -> error string*)
+let gnu_ext_extract_elf64_earliest_compatible_kernel endian sht sect_hdr_tbl bs0:(string)error=  
+ (let abi_note_sects =    
+(List.filter (fun x ->
+      if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf64_sh_type)) sht_note then
+        let nm = (Nat_big_num.of_string (Uint32.to_string x.elf64_sh_name)) in
+          (match String_table.get_string_at nm sect_hdr_tbl with
+            | Success name1 -> name1 = ".note.ABI-tag"
+            | Fail _       -> false
+          )
+      else
+        false
+    ) sht)
+  in
+    (match abi_note_sects with
+      | [note] ->
+        let off = (Nat_big_num.of_string (Uint64.to_string note.elf64_sh_offset)) in
+        let siz = (Ml_bindings.nat_big_num_of_uint64 note.elf64_sh_size) in
+        let abi_tag =          
+(Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel ->
+          Elf_note.read_elf64_note endian rel >>= (fun (abi_tag, _) ->
+          return abi_tag)))
+        in
+          (match abi_tag with
+            | Fail _          -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: parsing of NOTE section failed"
+            | Success abi_tag ->
+              let str = (name_string_of_elf64_note abi_tag) in
+                if str = "GNU\000" then
+                  if Nat_big_num.greater_equal (Ml_bindings.nat_big_num_of_uint64 abi_tag.elf64_note_descsz)(Nat_big_num.of_int 16) then
+                    let take2 = (Lem_list.take( 16) abi_tag.elf64_note_desc) in
+                      if List.length take2 < 16 then
+                        fail "gnu_ext_extract_elf64_earliest_compatible_kernel: the impossible happened"
+                      else
+                        (match group_elf64_words endian take2 with
+                          | Fail err   -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: word grouping failed"
+                          | Success ss ->
+                            (match ss with
+                              | c1::c2::c3::cs ->
+                                let c1 = (Uint32.to_string c1) in
+                                let c2 = (Uint32.to_string c2) in
+                                let c3 = (Uint32.to_string c3) in
+                                  return (List.fold_right (^) (intercalate "." [c1;c2;c3]) "")
+                              | _              -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: kernel version must have three components"
+                            )
+                        )
+                  else
+                    fail "gnu_ext_extract_elf64_earliest_compatible_kernel: .note.ABI-tag description size not required length"
+                else
+                  fail "gnu_ext_extract_elf64_earliest_compatible_kernel: required GNU string not present"
+          )
+      | _      -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: more than one .note.ABI-tag section present"
+    ))
diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_program_header_table.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_program_header_table.ml
new file mode 100644
index 00000000..4c5b78c1
--- /dev/null
+++ b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_program_header_table.ml
@@ -0,0 +1,34 @@
+(*Generated by Lem from gnu_extensions/gnu_ext_program_header_table.lem.*)
+(** [gnu_ext_program_header_table] contains GNU extension specific functionality
+  * related to the program header table.
+  *)
+
+open Lem_basic_classes
+open Lem_num
+
+(** GNU extensions, as defined in the LSB, see section 11.2. *)
+
+(** The element specifies the location and size of a segment that may be made
+  * read-only after relocations have been processed.
+  *)
+let elf_pt_gnu_relro : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 421345620))(Nat_big_num.of_int 2)) (* 0x6474e552 *)
+(** The [p_flags] member specifies the permissions of the segment containing the
+  * stack and is used to indicate whether the stack should be executable.
+  *)
+let elf_pt_gnu_stack : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 421345620))(Nat_big_num.of_int 1)) (* 0x6474e551 *)
+(** Element specifies the location and size of exception handling information. *)
+let elf_pt_gnu_eh_frame : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 421345620))    (* 0x6474e550 *)
+
+(** [string_of_gnu_ext_segment_type m] produces a string representation of
+  * GNU extension segment type [m].
+  *)
+(*val string_of_gnu_ext_segment_type : natural -> string*)
+let string_of_gnu_ext_segment_type pt:string=  
+ (if Nat_big_num.equal pt elf_pt_gnu_relro then
+    "GNU_RELRO"
+  else if Nat_big_num.equal pt elf_pt_gnu_stack then
+    "GNU_STACK"
+  else if Nat_big_num.equal pt elf_pt_gnu_eh_frame then
+    "GNU_EH_FRAME"
+  else
+    "Invalid GNU EXT segment type")
diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_header_table.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_header_table.ml
new file mode 100644
index 00000000..98faa8e4
--- /dev/null
+++ b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_header_table.ml
@@ -0,0 +1,151 @@
+(*Generated by Lem from gnu_extensions/gnu_ext_section_header_table.lem.*)
+(** The module [gnu_ext_section_header_table] implements function, definitions
+  * and types relating to the GNU extensions to the standard ELF section header
+  * table.
+  *)
+
+open Lem_basic_classes
+open Lem_bool
+open Lem_map
+open Lem_maybe
+open Lem_num
+open Lem_string
+
+open Hex_printing
+
+open Error
+open String_table
+open Show
+
+open Elf_section_header_table
+open Elf_interpreted_section
+
+(** GNU extended section types *)
+
+(** [GNU_HASH] does not appear to be defined in the LSB but is present in
+  * several ELF binaries collected in the wild...
+  *
+  * TODO: find out where this comes from?
+  * ANSW: a mailing list apparently!  See here:
+  *   https://sourceware.org/ml/binutils/2006-10/msg00377.html
+  *)
+let sht_gnu_hash    : Nat_big_num.num=  ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524091))     (* 0x6FFFFFF6 *)
+
+(** The following are all defined in Section 10.2.2.2 of the LSB as additional
+  * section types over the ones defined in the SCO ELF spec.
+  *)
+
+(** [sht_gnu_verdef] contains the symbol versions that are provided.
+  *)
+let sht_gnu_verdef  : Nat_big_num.num=  (Nat_big_num.sub_nat ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524095))(Nat_big_num.of_int 1)) (* 0x6ffffffd *)
+(** [sht_gnu_verneed] contains the symbol versions that are required.
+  *)
+let sht_gnu_verneed : Nat_big_num.num=  ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524095))     (* 0x6ffffffe *)
+(** [sht_gnu_versym] contains the symbol version table.
+  *)
+let sht_gnu_versym  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524095))(Nat_big_num.of_int 1)) (* 0x6fffffff *)
+(** [sht_gnu_liblist] appears to be undocumented but appears in PowerPC 64 ELF
+  * binaries in "the wild".
+  *)
+let sht_gnu_liblist : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524091))(Nat_big_num.of_int 1)) (* 0x6FFFFFF7 *)
+
+(** [string_of_gnu_ext_section_type m] produces a string based representation of
+  * GNU extension section type [m].
+  *)
+(*val string_of_gnu_ext_section_type : natural -> string*)
+let string_of_gnu_ext_section_type i:string=  
+ (if Nat_big_num.equal i sht_gnu_hash then
+    "GNU_HASH"
+  else if Nat_big_num.equal i sht_gnu_verdef then
+    "VERDEF"
+  else if Nat_big_num.equal i sht_gnu_verneed then
+    "VERNEED"
+  else if Nat_big_num.equal i sht_gnu_versym then
+    "VERSYM"
+  else if Nat_big_num.equal i sht_gnu_liblist then
+    "GNU_LIBLIST"
+  else if Nat_big_num.greater_equal i sht_loos && Nat_big_num.less_equal i sht_hios then
+    let diff = (Nat_big_num.sub_nat i sht_loos) in
+    let suff = (unsafe_hex_string_of_natural( 0) diff) in
+      "LOOS+" ^ suff
+  else
+    "Invalid GNU EXT section type: " ^ Nat_big_num.to_string i)
+    
+(** [gnu_ext_additionall_special_sections] records additional section names that
+  * map appear in GNU ELF binaries and their required associated types and
+  * attributes.  See Section 10.3.1.1 of the LSB and the related map
+  * [elf_special_sections] in [Elf_section_header_table] which records section
+  * names and their required types and attributes that all ELF binaries share.
+  *)
+(*val gnu_ext_additional_special_sections : Map.map string (natural * natural)*)
+let gnu_ext_additional_special_sections:((string),(Nat_big_num.num*Nat_big_num.num))Pmap.map=  
+ (Lem_map.fromList (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) [
+    (".ctors", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
+  ; (".data.rel.ro", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
+  ; (".dtors", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
+  ; (".eh_frame", (sht_progbits, shf_alloc))
+  ; (".eh_frame_hdr", (sht_progbits, shf_alloc))
+  ; (".gcc_execpt_table", (sht_progbits, shf_alloc))
+  ; (".gnu.version", (sht_gnu_versym, shf_alloc))
+  ; (".gnu.version_d", (sht_gnu_verdef, shf_alloc))
+  ; (".gnu.version_r", (sht_gnu_verneed, shf_alloc))
+  ; (".got.plt", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
+  ; (".jcr", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
+  ; (".note.ABI-tag", (sht_note, shf_alloc))
+  ; (".stab", (sht_progbits,Nat_big_num.of_int 0))
+  ; (".stabstr", (sht_strtab,Nat_big_num.of_int 0))
+  ])
+  
+(** [is_valid_gnu_ext_elf32_section_header_table_entry scts stbl] checks whether
+  * sections [scts] conforms with the contents of the special sections table.
+  * Fails otherwise.
+  *)
+(*val is_valid_gnu_ext_elf32_section_header_table_entry : elf32_interpreted_section ->
+  string_table -> bool*)
+let is_valid_gnu_ext_elf32_section_header_table_entry ent stbl:bool=  
+ ((match String_table.get_string_at ent.elf32_section_name stbl with
+    | Fail    f    -> false
+    | Success name1 ->
+      (match Pmap.lookup name1 gnu_ext_additional_special_sections with
+        | None           ->
+            is_valid_elf32_section_header_table_entry ent stbl
+        | Some (typ, flags) -> Nat_big_num.equal
+            typ ent.elf32_section_type && Nat_big_num.equal flags ent.elf32_section_flags
+      )
+  ))
+  
+(** [is_valid_gnu_ext_elf32_section_header_table sht stbl] checks whether every
+  * member of the section header table [sht] conforms with the special sections
+  * table.
+  *)
+(*val is_valid_gnu_ext_elf32_section_header_table : list elf32_interpreted_section ->
+  string_table -> bool*)
+let is_valid_gnu_ext_elf32_section_header_table ents stbl:bool=  
+ (List.for_all (fun x -> is_valid_gnu_ext_elf32_section_header_table_entry x stbl) ents)
+  
+(** [is_valid_gnu_ext_elf64_section_header_table_entry scts stbl] checks whether
+  * sections [scts] conforms with the contents of the special sections table.
+  * Fails otherwise.
+  *)
+(*val is_valid_gnu_ext_elf64_section_header_table_entry : elf64_interpreted_section ->
+  string_table -> bool*)
+let is_valid_gnu_ext_elf64_section_header_table_entry ent stbl:bool=  
+ ((match String_table.get_string_at ent.elf64_section_name stbl with
+    | Fail    f    -> false
+    | Success name1 ->
+      (match Pmap.lookup name1 gnu_ext_additional_special_sections with
+        | None           ->
+            is_valid_elf64_section_header_table_entry ent stbl
+        | Some (typ, flags) -> Nat_big_num.equal
+            typ ent.elf64_section_type && Nat_big_num.equal flags ent.elf64_section_flags
+      )
+  ))
+  
+(** [is_valid_gnu_ext_elf64_section_header_table sht stbl] checks whether every
+  * member of the section header table [sht] conforms with the special sections
+  * table.
+  *)
+(*val is_valid_gnu_ext_elf64_section_header_table : list elf64_interpreted_section ->
+  string_table -> bool*)
+let is_valid_gnu_ext_elf64_section_header_table ents stbl:bool=  
+ (List.for_all (fun x -> is_valid_gnu_ext_elf64_section_header_table_entry x stbl) ents)
diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_to_segment_mapping.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_to_segment_mapping.ml
new file mode 100644
index 00000000..86a5c5ed
--- /dev/null
+++ b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_to_segment_mapping.ml
@@ -0,0 +1,265 @@
+(*Generated by Lem from gnu_extensions/gnu_ext_section_to_segment_mapping.lem.*)
+(** [gnu_ext_section_to_segment_mapping] contains (GNU specific) functionality
+  * relating to calculating the section to segment mapping for an ELF file.  In
+  * particular, the test over whether a section is inside a segment is ABI
+  * specific.  This module provides that test.
+  *)
+
+open Lem_basic_classes
+open Lem_bool
+open Lem_num
+
+open Elf_header
+open Elf_program_header_table
+open Elf_section_header_table
+open Elf_types_native_uint
+
+open Lem_string
+open Show
+
+open Gnu_ext_program_header_table
+
+(** [elf32_section_in_segment sec_hdr segment] implements the
+  * ELF_SECTION_IN_SEGMENT1 macro from readelf.  Note the macro is always used
+  * with [check_vma] and [strict] set to 1.
+  *
+  #define ELF_SECTION_IN_SEGMENT_1(sec_hdr, segment, check_vma, strict)	\
+  ((/* Only PT_LOAD, PT_GNU_RELRO and PT_TLS segments can contain	\
+       SHF_TLS sections.  */						\
+    ((((sec_hdr)->sh_flags & SHF_TLS) != 0)				\
+     && ((segment)->p_type == PT_TLS					\
+	 || (segment)->p_type == PT_GNU_RELRO				\
+	 || (segment)->p_type == PT_LOAD))				\
+    /* PT_TLS segment contains only SHF_TLS sections, PT_PHDR no	\
+       sections at all.  */						\
+    || (((sec_hdr)->sh_flags & SHF_TLS) == 0				\
+	&& (segment)->p_type != PT_TLS					\
+	&& (segment)->p_type != PT_PHDR))				\
+   /* PT_LOAD and similar segments only have SHF_ALLOC sections.  */	\
+   && !(((sec_hdr)->sh_flags & SHF_ALLOC) == 0				\
+	&& ((segment)->p_type == PT_LOAD				\
+	    || (segment)->p_type == PT_DYNAMIC				\
+	    || (segment)->p_type == PT_GNU_EH_FRAME			\
+	    || (segment)->p_type == PT_GNU_RELRO			\
+	    || (segment)->p_type == PT_GNU_STACK))			\
+   /* Any section besides one of type SHT_NOBITS must have file		\
+      offsets within the segment.  */					\
+   && ((sec_hdr)->sh_type == SHT_NOBITS					\
+       || ((bfd_vma) (sec_hdr)->sh_offset >= (segment)->p_offset	\
+	   && (!(strict)						\
+	       || ((sec_hdr)->sh_offset - (segment)->p_offset		\
+		   <= (segment)->p_filesz - 1))				\
+	   && (((sec_hdr)->sh_offset - (segment)->p_offset		\
+		+ ELF_SECTION_SIZE(sec_hdr, segment))			\
+	       <= (segment)->p_filesz)))				\
+   /* SHF_ALLOC sections must have VMAs within the segment.  */		\
+   && (!(check_vma)							\
+       || ((sec_hdr)->sh_flags & SHF_ALLOC) == 0			\
+       || ((sec_hdr)->sh_addr >= (segment)->p_vaddr			\
+	   && (!(strict)						\
+	       || ((sec_hdr)->sh_addr - (segment)->p_vaddr		\
+		   <= (segment)->p_memsz - 1))				\
+	   && (((sec_hdr)->sh_addr - (segment)->p_vaddr			\
+		+ ELF_SECTION_SIZE(sec_hdr, segment))			\
+	       <= (segment)->p_memsz)))					\
+   /* No zero size sections at start or end of PT_DYNAMIC.  */		\
+   && ((segment)->p_type != PT_DYNAMIC					\
+       || (sec_hdr)->sh_size != 0					\
+       || (segment)->p_memsz == 0					\
+       || (((sec_hdr)->sh_type == SHT_NOBITS				\
+	    || ((bfd_vma) (sec_hdr)->sh_offset > (segment)->p_offset	\
+	        && ((sec_hdr)->sh_offset - (segment)->p_offset		\
+		    < (segment)->p_filesz)))				\
+	   && (((sec_hdr)->sh_flags & SHF_ALLOC) == 0			\
+	       || ((sec_hdr)->sh_addr > (segment)->p_vaddr		\
+		   && ((sec_hdr)->sh_addr - (segment)->p_vaddr		\
+		       < (segment)->p_memsz))))))
+  *
+  * From [internal.h] of readelf's source code.
+  *)
+  
+(*val elf32_section_flags : elf32_section_header_table_entry -> natural -> bool*)
+let elf32_section_flags0 sec_hdr typ:bool=  (not ((Uint32.logand sec_hdr.elf32_sh_flags (Uint32.of_string (Nat_big_num.to_string typ))) = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))))
+    
+(*val elf64_section_flags : elf64_section_header_table_entry -> natural -> bool*)
+let elf64_section_flags0 sec_hdr typ:bool=  (not ((Uint64.logand sec_hdr.elf64_sh_flags (Uint64.of_string (Nat_big_num.to_string typ))) = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))))
+    
+(*val elf32_section_of_type : elf32_section_header_table_entry -> natural -> bool*)
+let elf32_section_of_type sec_hdr typ:bool=  
+ (sec_hdr.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string typ))
+  
+(*val elf64_section_of_type : elf64_section_header_table_entry -> natural -> bool*)
+let elf64_section_of_type sec_hdr typ:bool=  
+ (sec_hdr.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string typ))
+  
+(*val elf32_segment_of_type : elf32_program_header_table_entry -> natural -> bool*)
+let elf32_segment_of_type segment typ:bool=  
+ (segment.elf32_p_type = Uint32.of_string (Nat_big_num.to_string typ))
+  
+(*val elf64_segment_of_type : elf64_program_header_table_entry -> natural -> bool*)
+let elf64_segment_of_type segment typ:bool=  
+ (segment.elf64_p_type = Uint32.of_string (Nat_big_num.to_string typ))
+
+(** Only PT_LOAD, PT_GNU_RELRO and PT_TLS segments can contain SHF_TLS sections
+  * and PT_TLS segment contains only SHF_TLS sections, PT_PHDR no	sections at all
+  *)
+(*val elf32_section_in_segment1 : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*)
+let elf32_section_in_segment1 sec_hdr segment:bool=  
+ ((elf32_section_flags0 sec_hdr shf_tls &&
+  (elf32_segment_of_type segment elf_pt_tls ||    
+(elf32_segment_of_type segment elf_pt_gnu_relro ||
+    elf32_segment_of_type segment elf_pt_load))) ||
+  (not (elf32_section_flags0 sec_hdr shf_tls)
+  && (not (elf32_segment_of_type segment elf_pt_tls)
+  && not (elf32_segment_of_type segment elf_pt_phdr))))
+  
+(*val elf64_section_in_segment1 : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*)
+let elf64_section_in_segment1 sec_hdr segment:bool=  
+ ((elf64_section_flags0 sec_hdr shf_tls &&
+  (elf64_segment_of_type segment elf_pt_tls ||    
+(elf64_segment_of_type segment elf_pt_gnu_relro ||
+    elf64_segment_of_type segment elf_pt_load))) ||
+  (not (elf64_section_flags0 sec_hdr shf_tls)
+  && (not (elf64_segment_of_type segment elf_pt_tls)
+  && not (elf64_segment_of_type segment elf_pt_phdr))))
+
+(** PT_LOAD and similar segments only have SHF_ALLOC sections *)
+
+(*val elf32_section_in_segment2 : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*)
+let elf32_section_in_segment2 sec_hdr segment:bool=  
+ (not ((not (elf32_section_flags0 sec_hdr shf_alloc)) &&
+       (elf32_segment_of_type segment elf_pt_load ||        
+(elf32_segment_of_type segment elf_pt_dynamic ||        
+(elf32_segment_of_type segment elf_pt_gnu_eh_frame ||        
+(elf32_segment_of_type segment elf_pt_gnu_relro ||
+        elf32_segment_of_type segment elf_pt_gnu_stack))))))
+
+(*val elf64_section_in_segment2 : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*)
+let elf64_section_in_segment2 sec_hdr segment:bool=  
+ (not ((not (elf64_section_flags0 sec_hdr shf_alloc)) &&
+       (elf64_segment_of_type segment elf_pt_load ||        
+(elf64_segment_of_type segment elf_pt_dynamic ||        
+(elf64_segment_of_type segment elf_pt_gnu_eh_frame ||        
+(elf64_segment_of_type segment elf_pt_gnu_relro ||
+        elf64_segment_of_type segment elf_pt_gnu_stack))))))
+ 
+    
+(** Any section besides one of type SHT_NOBITS must have file offsets within
+  * the segment.
+  *)
+
+(*val elf32_sect_size : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> natural*)
+let elf32_sect_size hdr sec_hdr segment:Nat_big_num.num=  
+ (if is_elf32_tbss_special sec_hdr segment then Nat_big_num.of_int 0
+  else
+    Nat_big_num.of_string (Uint32.to_string (hdr.elf32_shentsize)))
+  
+(*val elf64_sect_size : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> natural*)
+let elf64_sect_size hdr sec_hdr segment:Nat_big_num.num=  
+ (if is_elf64_tbss_special sec_hdr segment then Nat_big_num.of_int 0
+  else
+    Nat_big_num.of_string (Uint32.to_string (hdr.elf64_shentsize)))
+    
+(*val elf32_section_in_segment3 : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*)
+let elf32_section_in_segment3 hdr sec_hdr segment:bool=  
+ (let sec_off = ((Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_offset))) in
+  let seg_off = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_offset))) in
+  let seg_fsz = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_filesz))) in
+  let sec_siz = ((elf32_sect_size hdr sec_hdr segment)) in
+    elf32_section_of_type sec_hdr sht_nobits ||
+    ( Nat_big_num.greater_equal sec_off seg_off &&    
+(( Nat_big_num.less_equal( Nat_big_num.sub sec_off seg_off) ( Nat_big_num.sub seg_fsz(Nat_big_num.of_int 1))) &&
+    ( Nat_big_num.less_equal (Nat_big_num.sub sec_off ( Nat_big_num.add seg_off sec_siz)) seg_fsz))))
+  
+(*val elf64_section_in_segment3 : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*)
+let elf64_section_in_segment3 hdr sec_hdr segment:bool=  
+ (let sec_off = ((Nat_big_num.of_string (Uint64.to_string sec_hdr.elf64_sh_offset))) in
+  let seg_off = ((Nat_big_num.of_string (Uint64.to_string segment.elf64_p_offset))) in
+  let seg_fsz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_filesz)) in
+  let sec_siz = ((elf64_sect_size hdr sec_hdr segment)) in
+    elf64_section_of_type sec_hdr sht_nobits ||
+    ( Nat_big_num.greater_equal sec_off seg_off &&    
+(( Nat_big_num.less_equal( Nat_big_num.sub sec_off seg_off) ( Nat_big_num.sub seg_fsz(Nat_big_num.of_int 1))) &&
+    ( Nat_big_num.less_equal (Nat_big_num.sub sec_off ( Nat_big_num.add seg_off sec_siz)) seg_fsz))))
+      
+(** SHF_ALLOC sections must have VMAs within the segment
+  *)
+  
+(*val elf32_section_in_segment4 : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*)
+let elf32_section_in_segment4 hdr sec_hdr segment:bool=  
+ (let sec_addr = ((Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_addr))) in
+  let seg_vadr = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_vaddr))) in
+  let seg_mmsz = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_memsz))) in
+  let sec_size = ((elf32_sect_size hdr sec_hdr segment)) in
+    (not (elf32_section_flags0 sec_hdr shf_alloc) || Nat_big_num.greater_equal
+     sec_addr seg_vadr) && (Nat_big_num.less_equal (Nat_big_num.sub
+     sec_addr seg_vadr) (Nat_big_num.sub seg_mmsz(Nat_big_num.of_int 1)) && Nat_big_num.less_equal (Nat_big_num.sub
+     sec_addr ( Nat_big_num.add seg_vadr sec_size)) seg_mmsz))
+  
+(*val elf64_section_in_segment4 : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*)
+let elf64_section_in_segment4 hdr sec_hdr segment:bool=  
+ (let sec_addr = ((Ml_bindings.nat_big_num_of_uint64 sec_hdr.elf64_sh_addr)) in
+  let seg_vadr = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_vaddr)) in
+  let seg_mmsz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_memsz)) in
+  let sec_size = ((elf64_sect_size hdr sec_hdr segment)) in
+     (not (elf64_section_flags0 sec_hdr shf_alloc) || Nat_big_num.greater_equal
+     sec_addr seg_vadr) && (Nat_big_num.less_equal (Nat_big_num.sub
+     sec_addr seg_vadr) (Nat_big_num.sub seg_mmsz(Nat_big_num.of_int 1)) && Nat_big_num.less_equal (Nat_big_num.sub
+     sec_addr ( Nat_big_num.add seg_vadr sec_size)) seg_mmsz))
+    
+(** No zero size sections at start or end of PT_DYNAMIC *)
+
+(*val elf32_section_in_segment5 : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*)
+let elf32_section_in_segment5 sec_hdr segment:bool=  
+ (let sec_siz = ((Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_size))) in
+  let seg_msz = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_memsz))) in
+  let sec_off = ((Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_offset))) in
+  let seg_off = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_offset))) in
+  let seg_fsz = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_filesz))) in
+  let sec_adr = ((Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_addr))) in
+  let seg_vad = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_vaddr))) in
+    (not (elf32_segment_of_type segment elf_pt_dynamic)) || (not (Nat_big_num.equal sec_siz(Nat_big_num.of_int 0)) || (Nat_big_num.equal
+    seg_msz(Nat_big_num.of_int 0) ||
+    ((elf32_section_of_type sec_hdr sht_nobits ||
+      ( Nat_big_num.greater sec_off seg_off && Nat_big_num.less (Nat_big_num.sub
+       sec_off seg_off) seg_fsz)) &&
+       (not (elf32_section_flags0 sec_hdr shf_alloc) ||
+        ( Nat_big_num.greater sec_adr seg_vad && Nat_big_num.less (Nat_big_num.sub
+         sec_adr seg_vad) seg_msz))))))
+
+(*val elf64_section_in_segment5 : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*)
+let elf64_section_in_segment5 sec_hdr segment:bool=  
+ (let sec_siz = ((Ml_bindings.nat_big_num_of_uint64 sec_hdr.elf64_sh_size)) in
+  let seg_msz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_memsz)) in
+  let sec_off = ((Nat_big_num.of_string (Uint64.to_string sec_hdr.elf64_sh_offset))) in
+  let seg_off = ((Nat_big_num.of_string (Uint64.to_string segment.elf64_p_offset))) in
+  let seg_fsz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_filesz)) in
+  let sec_adr = ((Ml_bindings.nat_big_num_of_uint64 sec_hdr.elf64_sh_addr)) in
+  let seg_vad = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_vaddr)) in
+    (not (elf64_segment_of_type segment elf_pt_dynamic)) || (not (Nat_big_num.equal sec_siz(Nat_big_num.of_int 0)) || (Nat_big_num.equal
+    seg_msz(Nat_big_num.of_int 0) ||
+    ((elf64_section_of_type sec_hdr sht_nobits ||
+      ( Nat_big_num.greater sec_off seg_off && Nat_big_num.less (Nat_big_num.sub
+       sec_off seg_off) seg_fsz)) &&
+       (not (elf64_section_flags0 sec_hdr shf_alloc) ||
+        ( Nat_big_num.greater sec_adr seg_vad && Nat_big_num.less (Nat_big_num.sub
+         sec_adr seg_vad) seg_msz))))))
+
+(** The final section in segment tests, bringing all the above together.
+  *)
+
+(*val elf32_section_in_segment : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*)
+let elf32_section_in_segment hdr sec_hdr segment:bool=  
+ (elf32_section_in_segment1 sec_hdr segment &&  
+(elf32_section_in_segment2 sec_hdr segment &&  
+(elf32_section_in_segment3 hdr sec_hdr segment &&  
+(elf32_section_in_segment4 hdr sec_hdr segment &&
+  elf32_section_in_segment5 sec_hdr segment))))
+    
+(*val elf64_section_in_segment : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*)
+let elf64_section_in_segment hdr sec_hdr segment:bool=  
+ (elf64_section_in_segment1 sec_hdr segment &&  
+(elf64_section_in_segment2 sec_hdr segment &&  
+(elf64_section_in_segment3 hdr sec_hdr segment &&  
+(elf64_section_in_segment4 hdr sec_hdr segment &&
+  elf64_section_in_segment5 sec_hdr segment))))
diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_symbol_versioning.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_symbol_versioning.ml
new file mode 100644
index 00000000..fe9382b0
--- /dev/null
+++ b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_symbol_versioning.ml
@@ -0,0 +1,294 @@
+(*Generated by Lem from gnu_extensions/gnu_ext_symbol_versioning.lem.*)
+(** The [gnu_ext_symbol_versioning] defines constants, types and functions
+  * relating to the GNU symbol versioning extensions (i.e. contents of
+  * GNU_VERSYM sections).
+  *
+  * TODO: work out what is going on with symbol versioning.  The specification
+  * is completely opaque.
+  *)
+
+open Lem_basic_classes
+open Lem_bool
+open Lem_list
+open Lem_maybe
+open Lem_num
+open Lem_string
+
+open Byte_sequence
+open Endianness
+open Error
+
+open Elf_dynamic
+open Elf_file
+open Elf_header
+open Elf_section_header_table
+open Elf_symbol_table
+open Elf_types_native_uint
+
+open Missing_pervasives
+open Show
+
+open Gnu_ext_dynamic
+open Gnu_ext_section_header_table
+
+(** [gnu_ext_elf32_symbol_version_table] is an array (linked list, here) of
+  * [elf32_half] entries.
+  *)
+type gnu_ext_elf32_symbol_version_table = Uint32.uint32
+  list
+  
+type gnu_ext_elf64_symbol_version_table = Uint32.uint32
+  list
+
+(*val obtain_gnu_ext_elf32_symbol_version_table : elf32_file -> byte_sequence -> error gnu_ext_elf32_symbol_version_table*)
+let obtain_gnu_ext_elf32_symbol_version_table f1 bs0:((Uint32.uint32)list)error=  
+ (let sht = (f1.elf32_file_section_header_table) in
+  let endian = (get_elf32_header_endianness f1.elf32_file_header) in
+  let vers = (List.filter (fun ent ->
+    ent.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string sht_gnu_versym)
+  ) sht)
+  in
+    (match vers with
+      | []    -> return []
+      | [ver] ->
+        let off = (Nat_big_num.of_string (Uint32.to_string ver.elf32_sh_offset)) in
+        let siz = (Nat_big_num.of_string (Uint32.to_string ver.elf32_sh_size)) in
+        let lnk = (Nat_big_num.of_string (Uint32.to_string ver.elf32_sh_link)) in
+        get_elf32_symbol_table_by_index f1 lnk >>= (fun symtab ->
+        let dlen = (Nat_big_num.of_int (List.length symtab)) in
+        Byte_sequence.offset_and_cut off siz bs0         >>= (fun ver      ->
+        Error.repeatM' dlen bs0 (read_elf32_half endian) >>= (fun (ver, _) ->
+        return ver)))
+      | _     -> fail "obtain_gnu_ext_elf32_symbol_version_table: multiple sections of type .gnu_versym present in file"
+    ))
+ 
+(*val obtain_gnu_ext_elf64_symbol_version_table : endianness -> elf64_section_header_table -> elf64_symbol_table -> byte_sequence -> error gnu_ext_elf64_symbol_version_table*)
+let obtain_gnu_ext_elf64_symbol_version_table endian sht dynsym bs0:((Uint32.uint32)list)error=  
+ (let dlen = (Nat_big_num.of_int (List.length dynsym)) in
+    if Nat_big_num.equal dlen(Nat_big_num.of_int 0) then
+      return []
+    else
+      let vers = (List.filter (fun ent ->
+          ent.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string sht_gnu_versym)
+        ) sht)
+      in
+        (match vers with
+          | []    -> return []
+          | [ver] ->
+            let off = (Nat_big_num.of_string (Uint64.to_string ver.elf64_sh_offset)) in
+            let siz = (Ml_bindings.nat_big_num_of_uint64 ver.elf64_sh_size) in
+            Byte_sequence.offset_and_cut off siz bs0         >>= (fun ver      ->
+            Error.repeatM' dlen bs0 (read_elf64_half endian) >>= (fun (ver, _) ->
+            return ver))
+          | _     -> fail "obtain_gnu_ext_elf64_symbol_version_table: multiple sections of type .gnu_versym present in file"
+        ))
+  
+type gnu_ext_elf32_verdef =
+  { gnu_ext_elf32_vd_version : Uint32.uint32
+   ; gnu_ext_elf32_vd_flags   : Uint32.uint32
+   ; gnu_ext_elf32_vd_ndx     : Uint32.uint32
+   ; gnu_ext_elf32_vd_cnt     : Uint32.uint32
+   ; gnu_ext_elf32_vd_hash    : Uint32.uint32
+   ; gnu_ext_elf32_vd_aux     : Uint32.uint32
+   ; gnu_ext_elf32_vd_next    : Uint32.uint32
+   }
+   
+type gnu_ext_elf64_verdef =
+  { gnu_ext_elf64_vd_version : Uint32.uint32
+   ; gnu_ext_elf64_vd_flags   : Uint32.uint32
+   ; gnu_ext_elf64_vd_ndx     : Uint32.uint32
+   ; gnu_ext_elf64_vd_cnt     : Uint32.uint32
+   ; gnu_ext_elf64_vd_hash    : Uint32.uint32
+   ; gnu_ext_elf64_vd_aux     : Uint32.uint32
+   ; gnu_ext_elf64_vd_next    : Uint32.uint32
+   }
+   
+(*val string_of_gnu_ext_elf32_verdef : gnu_ext_elf32_verdef -> string*)
+let string_of_gnu_ext_elf32_verdef verdef:string=  
+ (unlines [    
+("Version: " ^ Uint32.to_string verdef.gnu_ext_elf32_vd_version)
+  ; ("Flags: " ^ Uint32.to_string verdef.gnu_ext_elf32_vd_flags)
+  ; ("Index: " ^ Uint32.to_string verdef.gnu_ext_elf32_vd_ndx)
+  ; ("Count: " ^ Uint32.to_string verdef.gnu_ext_elf32_vd_cnt)
+  ; ("Hash: " ^ Uint32.to_string verdef.gnu_ext_elf32_vd_hash)
+  ])
+  
+(*val string_of_gnu_ext_elf64_verdef : gnu_ext_elf64_verdef -> string*)
+let string_of_gnu_ext_elf64_verdef verdef:string=  
+ (unlines [    
+("Version: " ^ Uint32.to_string verdef.gnu_ext_elf64_vd_version)
+  ; ("Flags: " ^ Uint32.to_string verdef.gnu_ext_elf64_vd_flags)
+  ; ("Index: " ^ Uint32.to_string verdef.gnu_ext_elf64_vd_ndx)
+  ; ("Count: " ^ Uint32.to_string verdef.gnu_ext_elf64_vd_cnt)
+  ; ("Hash: " ^ Uint32.to_string verdef.gnu_ext_elf64_vd_hash)
+  ])
+   
+(*val read_gnu_ext_elf32_verdef : endianness -> byte_sequence -> error (gnu_ext_elf32_verdef * byte_sequence)*)
+let read_gnu_ext_elf32_verdef endian bs0:(gnu_ext_elf32_verdef*byte_sequence)error=  
+ (read_elf32_half endian bs0 >>= (fun (ver, bs0) ->
+  read_elf32_half endian bs0 >>= (fun (flg, bs0) ->
+  read_elf32_half endian bs0 >>= (fun (ndx, bs0) ->
+  read_elf32_half endian bs0 >>= (fun (cnt, bs0) ->
+  read_elf32_word endian bs0 >>= (fun (hsh, bs0) ->
+  read_elf32_word endian bs0 >>= (fun (aux, bs0) ->
+  read_elf32_word endian bs0 >>= (fun (nxt, bs0) ->
+    return ({ gnu_ext_elf32_vd_version = ver; gnu_ext_elf32_vd_flags = flg;
+      gnu_ext_elf32_vd_ndx = ndx; gnu_ext_elf32_vd_cnt = cnt;
+        gnu_ext_elf32_vd_hash = hsh; gnu_ext_elf32_vd_aux = aux;
+      gnu_ext_elf32_vd_next = nxt }, bs0)))))))))
+      
+(*val read_gnu_ext_elf64_verdef : endianness -> byte_sequence -> error (gnu_ext_elf64_verdef * byte_sequence)*)
+let read_gnu_ext_elf64_verdef endian bs0:(gnu_ext_elf64_verdef*byte_sequence)error=  
+ (read_elf64_half endian bs0 >>= (fun (ver, bs0) ->
+  read_elf64_half endian bs0 >>= (fun (flg, bs0) ->
+  read_elf64_half endian bs0 >>= (fun (ndx, bs0) ->
+  read_elf64_half endian bs0 >>= (fun (cnt, bs0) ->
+  read_elf64_word endian bs0 >>= (fun (hsh, bs0) ->
+  read_elf64_word endian bs0 >>= (fun (aux, bs0) ->
+  read_elf64_word endian bs0 >>= (fun (nxt, bs0) ->
+    return ({ gnu_ext_elf64_vd_version = ver; gnu_ext_elf64_vd_flags = flg;
+      gnu_ext_elf64_vd_ndx = ndx; gnu_ext_elf64_vd_cnt = cnt;
+        gnu_ext_elf64_vd_hash = hsh; gnu_ext_elf64_vd_aux = aux;
+      gnu_ext_elf64_vd_next = nxt }, bs0)))))))))
+      
+(*val gnu_ext_elf32_verdef_size : natural*)
+let gnu_ext_elf32_verdef_size:Nat_big_num.num= (Nat_big_num.of_int 160)
+  
+(*val gnu_ext_elf64_verdef_size : natural*)
+let gnu_ext_elf64_verdef_size:Nat_big_num.num= (Nat_big_num.of_int 256)
+   
+type gnu_ext_elf32_veraux =
+  { gnu_ext_elf32_vda_name : Uint32.uint32
+   ; gnu_ext_elf32_vda_next : Uint32.uint32
+   }
+   
+type gnu_ext_elf64_veraux =
+  { gnu_ext_elf64_vda_name : Uint32.uint32
+   ; gnu_ext_elf64_vda_next : Uint32.uint32
+   }
+   
+(*val gnu_ext_elf32_veraux_size : natural*)
+let gnu_ext_elf32_veraux_size:Nat_big_num.num= (Nat_big_num.of_int 64)
+
+(*val gnu_ext_elf64_veraux_size : natural*)
+let gnu_ext_elf64_veraux_size:Nat_big_num.num= (Nat_big_num.of_int 128)
+   
+(*val read_gnu_ext_elf32_veraux : endianness -> byte_sequence -> error (gnu_ext_elf32_veraux * byte_sequence)*)
+let read_gnu_ext_elf32_veraux endian bs0:(gnu_ext_elf32_veraux*byte_sequence)error=  
+ (read_elf32_word endian bs0 >>= (fun (nme, bs0) ->
+  read_elf32_word endian bs0 >>= (fun (nxt, bs0) ->
+    return ({ gnu_ext_elf32_vda_name = nme; gnu_ext_elf32_vda_next = nxt }, bs0))))
+    
+(*val read_gnu_ext_elf64_veraux : endianness -> byte_sequence -> error (gnu_ext_elf64_veraux * byte_sequence)*)
+let read_gnu_ext_elf64_veraux endian bs0:(gnu_ext_elf64_veraux*byte_sequence)error=  
+ (read_elf64_word endian bs0 >>= (fun (nme, bs0) ->
+  read_elf64_word endian bs0 >>= (fun (nxt, bs0) ->
+    return ({ gnu_ext_elf64_vda_name = nme; gnu_ext_elf64_vda_next = nxt }, bs0))))
+   
+type gnu_ext_elf32_verneed =
+  { gnu_ext_elf32_vn_version : Uint32.uint32
+   ; gnu_ext_elf32_vn_cnt     : Uint32.uint32
+   ; gnu_ext_elf32_vn_file    : Uint32.uint32
+   ; gnu_ext_elf32_vn_aux     : Uint32.uint32
+   ; gnu_ext_elf32_vn_next    : Uint32.uint32
+   }
+   
+type gnu_ext_elf64_verneed =
+  { gnu_ext_elf64_vn_version : Uint32.uint32
+   ; gnu_ext_elf64_vn_cnt     : Uint32.uint32
+   ; gnu_ext_elf64_vn_file    : Uint32.uint32
+   ; gnu_ext_elf64_vn_aux     : Uint32.uint32
+   ; gnu_ext_elf64_vn_next    : Uint32.uint32
+   }
+   
+(*val gnu_ext_elf32_verneed_size : natural*)
+let gnu_ext_elf32_verneed_size:Nat_big_num.num= (Nat_big_num.of_int 128)
+
+(*val gnu_ext_elf64_verneed_size : natural*)
+let gnu_ext_elf64_verneed_size:Nat_big_num.num= (Nat_big_num.of_int 224)
+   
+(*val read_gnu_ext_elf32_verneed : endianness -> byte_sequence -> error (gnu_ext_elf32_verneed * byte_sequence)*)
+let read_gnu_ext_elf32_verneed endian bs0:(gnu_ext_elf32_verneed*byte_sequence)error=  
+ (read_elf32_half endian bs0 >>= (fun (ver, bs0) ->
+  read_elf32_half endian bs0 >>= (fun (cnt, bs0) ->
+  read_elf32_word endian bs0 >>= (fun (fle, bs0) ->
+  read_elf32_word endian bs0 >>= (fun (aux, bs0) ->
+  read_elf32_word endian bs0 >>= (fun (nxt, bs0) ->
+    return ({ gnu_ext_elf32_vn_version = ver; gnu_ext_elf32_vn_cnt = cnt;
+      gnu_ext_elf32_vn_file = fle; gnu_ext_elf32_vn_aux = aux;
+        gnu_ext_elf32_vn_next = nxt }, bs0)))))))
+
+(*val read_gnu_ext_elf64_verneed : endianness -> byte_sequence -> error (gnu_ext_elf64_verneed * byte_sequence)*)
+let read_gnu_ext_elf64_verneed endian bs0:(gnu_ext_elf64_verneed*byte_sequence)error=  
+ (read_elf64_half endian bs0 >>= (fun (ver, bs0) ->
+  read_elf64_half endian bs0 >>= (fun (cnt, bs0) ->
+  read_elf64_word endian bs0 >>= (fun (fle, bs0) ->
+  read_elf64_word endian bs0 >>= (fun (aux, bs0) ->
+  read_elf64_word endian bs0 >>= (fun (nxt, bs0) ->
+    return ({ gnu_ext_elf64_vn_version = ver; gnu_ext_elf64_vn_cnt = cnt;
+      gnu_ext_elf64_vn_file = fle; gnu_ext_elf64_vn_aux = aux;
+        gnu_ext_elf64_vn_next = nxt }, bs0)))))))
+   
+type gnu_ext_elf32_vernaux =
+  { gnu_ext_elf32_vna_hash  : Uint32.uint32
+   ; gnu_ext_elf32_vna_flags : Uint32.uint32
+   ; gnu_ext_elf32_vna_other : Uint32.uint32
+   ; gnu_ext_elf32_vna_name  : Uint32.uint32
+   ; gnu_ext_elf32_vna_next  : Uint32.uint32
+   }
+   
+type gnu_ext_elf64_vernaux =
+  { gnu_ext_elf64_vna_hash  : Uint32.uint32
+   ; gnu_ext_elf64_vna_flags : Uint32.uint32
+   ; gnu_ext_elf64_vna_other : Uint32.uint32
+   ; gnu_ext_elf64_vna_name  : Uint32.uint32
+   ; gnu_ext_elf64_vna_next  : Uint32.uint32
+   }
+   
+(*val string_of_gnu_ext_elf32_vernaux : gnu_ext_elf32_vernaux -> string*)
+let string_of_gnu_ext_elf32_vernaux vernaux:string=  
+ (unlines [    
+("Hash: " ^ Uint32.to_string vernaux.gnu_ext_elf32_vna_hash)
+  ; ("Flags: " ^ Uint32.to_string vernaux.gnu_ext_elf32_vna_flags)
+  ; ("Other: " ^ Uint32.to_string vernaux.gnu_ext_elf32_vna_other)
+  ; ("Name: " ^ Uint32.to_string vernaux.gnu_ext_elf32_vna_name)
+  ; ("Next: " ^ Uint32.to_string vernaux.gnu_ext_elf32_vna_next)
+  ])
+  
+(*val string_of_gnu_ext_elf64_vernaux : gnu_ext_elf64_vernaux -> string*)
+let string_of_gnu_ext_elf64_vernaux vernaux:string=  
+ (unlines [    
+("Hash: " ^ Uint32.to_string vernaux.gnu_ext_elf64_vna_hash)
+  ; ("Flags: " ^ Uint32.to_string vernaux.gnu_ext_elf64_vna_flags)
+  ; ("Other: " ^ Uint32.to_string vernaux.gnu_ext_elf64_vna_other)
+  ; ("Name: " ^ Uint32.to_string vernaux.gnu_ext_elf64_vna_name)
+  ; ("Next: " ^ Uint32.to_string vernaux.gnu_ext_elf64_vna_next)
+  ])
+   
+(*val gnu_ext_elf32_vernaux_size : natural*)
+let gnu_ext_elf32_vernaux_size:Nat_big_num.num= (Nat_big_num.of_int 16)
+
+(*val gnu_ext_elf64_vernaux_size : natural*)
+let gnu_ext_elf64_vernaux_size:Nat_big_num.num= (Nat_big_num.of_int 224)
+   
+(*val read_gnu_ext_elf32_vernaux : endianness -> byte_sequence -> error (gnu_ext_elf32_vernaux * byte_sequence)*)
+let read_gnu_ext_elf32_vernaux endian bs0:(gnu_ext_elf32_vernaux*byte_sequence)error=  
+ (read_elf32_word endian bs0 >>= (fun (hsh, bs0) ->
+  read_elf32_half endian bs0 >>= (fun (flg, bs0) ->
+  read_elf32_half endian bs0 >>= (fun (otr, bs0) ->
+  read_elf32_word endian bs0 >>= (fun (nme, bs0) ->
+  read_elf32_word endian bs0 >>= (fun (nxt, bs0) ->
+    return ({ gnu_ext_elf32_vna_hash = hsh; gnu_ext_elf32_vna_flags = flg;
+      gnu_ext_elf32_vna_other = otr; gnu_ext_elf32_vna_name = nme;
+    gnu_ext_elf32_vna_next = nxt }, bs0)))))))
+
+(*val read_gnu_ext_elf64_vernaux : endianness -> byte_sequence -> error (gnu_ext_elf64_vernaux * byte_sequence)*)
+let read_gnu_ext_elf64_vernaux endian bs0:(gnu_ext_elf64_vernaux*byte_sequence)error=  
+ (read_elf64_word endian bs0 >>= (fun (hsh, bs0) ->
+  read_elf64_half endian bs0 >>= (fun (flg, bs0) ->
+  read_elf64_half endian bs0 >>= (fun (otr, bs0) ->
+  read_elf64_word endian bs0 >>= (fun (nme, bs0) ->
+  read_elf64_word endian bs0 >>= (fun (nxt, bs0) ->
+    return ({ gnu_ext_elf64_vna_hash = hsh; gnu_ext_elf64_vna_flags = flg;
+      gnu_ext_elf64_vna_other = otr; gnu_ext_elf64_vna_name = nme;
+    gnu_ext_elf64_vna_next = nxt }, bs0)))))))
diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_types_native_uint.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_types_native_uint.ml
new file mode 100644
index 00000000..ec4be185
--- /dev/null
+++ b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_types_native_uint.ml
@@ -0,0 +1,12 @@
+(*Generated by Lem from gnu_extensions/gnu_ext_types_native_uint.lem.*)
+(** [gnu_ext_types_native_uint] provides extended types defined by the GNU
+  * extensions over and above the based ELF types.
+  *)
+
+open Missing_pervasives
+open Elf_types_native_uint
+
+(** LSB section 9.2.1.1: in addition to SCO ELF spec types GNU defines an
+  * additional 1-byte integral type.
+  *)
+type gnu_ext_byte = char