From 5d6487136c91b793ea29b8a16e87a56825b41974 Mon Sep 17 00:00:00 2001 From: emersion Date: Tue, 24 Apr 2018 14:03:40 +0100 Subject: [PATCH] Fix Error.mapM returning reversed list This is (hopefully) the last episode of the long list of patches trying to fix the reversed lists issues. I originally started to try to fix in [1], but I realized that the fix is incorrect. My previous patch changed how `read_elf{32,64}_section_header_table'` returned its output: instead of putting the newly parsed element at the head of the list, it appends it at the end. However this is wrong: the function first parses a header, and then parses the remaining headers recursively. This means the parsed element must become the head of the returned list. I then tried to pin down the real issue from where I noticed it, in `elf_memory_image_of_elf64_file`. In this function the sections are reversed, in `read_elf{32,64}_section_header_table'` the order is correct, the issue is between those two functions. I ran into some issues with `List.mapi`: the standard OCaml version calls the iterator in the normal order meaning side effects (such as printing a debug line) are correctly triggered. However the Lem version calls the iterator in the reverse order, which is confusing. I'll definitely investigate this later. The problem lies in `obtain_elf64_interpreted_sections`: the section header list it eats is in the correct order, but the list of sections it returns is reversed. After some more debugging I realized `Error.mapM` reverses the lists it gets called with. This patch fixes this issue and removes the previous workarounds. [1]: https://github.com/rems-project/linksem/pull/1 --- src/elf_section_header_table.lem | 4 ++-- src/error.lem | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/elf_section_header_table.lem b/src/elf_section_header_table.lem index bf808c1..6661d16 100644 --- a/src/elf_section_header_table.lem +++ b/src/elf_section_header_table.lem @@ -638,7 +638,7 @@ let rec read_elf32_section_header_table' endian bs0 = else read_elf32_section_header_table_entry endian bs0 >>= fun (entry, bs1) -> read_elf32_section_header_table' endian bs1 >>= fun sht -> - return (sht ++ [entry]) + return (entry :: sht) (** [read_elf64_section_header_table' ed bs0] parses an ELF64 section header table * from byte sequence [bs0] assuming endianness [ed]. Assumes [bs0] is of the @@ -653,7 +653,7 @@ let rec read_elf64_section_header_table' endian bs0 = else read_elf64_section_header_table_entry endian bs0 >>= fun (entry, bs1) -> read_elf64_section_header_table' endian bs1 >>= fun sht -> - return (sht ++ [entry]) + return (entry :: sht) (** [read_elf32_section_header_table sz ed bs0] parses an ELF32 section header * table from a [sz] sized prefix of byte sequence [bs0] assuming endianness diff --git a/src/error.lem b/src/error.lem index 90f946b..b75df28 100644 --- a/src/error.lem +++ b/src/error.lem @@ -86,14 +86,14 @@ let rec repeatM' count seed action = action seed >>= fun (head, seed) -> repeatM' (count - 1) seed action >>= fun (tail, seed) -> return (head::tail, seed) - + (** [mapM f xs] maps [f] across [xs], failing if [f] fails on any element of [xs]. *) val mapM' : forall 'a 'b. ('a -> error 'b) -> list 'a -> error (list 'b) -> error (list 'b) -let rec mapM' f xs acc = +let rec mapM' f xs rev_acc = match xs with - | [] -> acc - | x::xs -> mapM' f xs (acc >>= fun tl -> f x >>= fun hd -> return (hd::tl)) + | [] -> rev_acc >>= fun rev_acc -> return (List.reverse rev_acc) + | x::xs -> mapM' f xs (rev_acc >>= fun tl -> f x >>= fun hd -> return (hd::tl)) end val mapM : forall 'a 'b. ('a -> error 'b) -> list 'a -> error (list 'b)