Add basic memory tests and introspection external functions

src/cmd/cmd_sym.ml

@@ -17,8 +17,12 @@ let link_state =
        Link.extern_module' Link.empty_state ~name:"symbolic" ~func_typ
          Symbolic_wasm_ffi.symbolic_extern_module
      in
-     Link.extern_module' link_state ~name:"summaries" ~func_typ
-       Symbolic_wasm_ffi.summaries_extern_module )
+     let link_state =
+       Link.extern_module' link_state ~name:"summaries" ~func_typ
+         Symbolic_wasm_ffi.summaries_extern_module
+     in
+     Link.extern_module' link_state ~name:"introspection" ~func_typ
+       Symbolic_wasm_ffi.introspection_extern_module )
 
 let run_file ~unsafe ~optimize pc filename =
   let*/ m = Compile.File.until_typecheck ~unsafe filename in

src/concolic/concolic_wasm_ffi.ml

@@ -169,3 +169,7 @@ let summaries_extern_module =
     ]
   in
   { Link.functions }
+
+let introspection_extern_module =
+  let functions = [] in
+  { Link.functions }

src/intf/symbolic_memory_intf.ml

@@ -27,6 +27,8 @@ module type M = sig
     -> Smtml.Expr.t Symbolic_choice_without_memory.t
 
   val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
+
+  val pp : Fmt.formatter -> t -> unit
 end
 
 module type S = sig
@@ -118,6 +120,8 @@ module type S = sig
 
   val get_limit_max : t -> Smtml.Expr.t option
 
+  val pp : Fmt.formatter -> t -> unit
+
   module ITbl : sig
     type 'a t
 

src/intf/wasm_ffi_intf.ml

@@ -48,4 +48,6 @@ module type S = sig
   val symbolic_extern_module : extern_func Link.extern_module
 
   val summaries_extern_module : extern_func Link.extern_module
+
+  val introspection_extern_module : extern_func Link.extern_module
 end

src/symbolic/symbolic_memory.ml

@@ -199,6 +199,18 @@ let free m base =
 
 let realloc m base size = Hashtbl.replace m.chunks base size
 
+let pp fmt m =
+  let pp_parent v =
+    Fmt.option
+      ~none:(fun fmt () -> Fmt.string fmt "None")
+      (fun fmt _v -> Fmt.string fmt "Some")
+      v
+  in
+  let pp_v fmt (a, b) = Fmt.pf fmt "0x%08ld %a" a Expr.pp b in
+  Fmt.pf fmt "size: %a@;" Expr.pp m.size;
+  Fmt.pf fmt "parent: %a@;" pp_parent m.parent;
+  Fmt.pf fmt "data:@;  @[<v>%a@]" (Fmt.hashtbl pp_v) m.data
+
 module ITbl = Hashtbl.Make (struct
   include Int
 

src/symbolic/symbolic_memory.mli

@@ -60,6 +60,8 @@ val size_in_pages : t -> Smtml.Expr.t
 
 val get_limit_max : t -> Smtml.Expr.t option
 
+val pp : Fmt.formatter -> t -> unit
+
 module ITbl : sig
   type 'a t
 

src/symbolic/symbolic_memory_concretizing.ml

@@ -145,6 +145,14 @@ module Backend = struct
     let+ base = address ptr in
     Hashtbl.replace m.chunks base size;
     Expr.ptr base (Symbolic_value.const_i32 0l)
+
+  let rec pp fmt m =
+    let pp_parent =
+      Fmt.option ~none:(fun fmt () -> Fmt.string fmt "None (root mem)") pp
+    in
+    let pp_v fmt (a, b) = Fmt.pf fmt "0x%08lx %a" a Expr.pp b in
+    Fmt.pf fmt "@[<v>parent:@;@[<v 1> %a@]@;data:@;@[<v 1> %a@]@]" pp_parent
+      m.parent (Fmt.hashtbl pp_v) m.data
 end
 
 include Symbolic_memory_make.Make (Backend)

src/symbolic/symbolic_memory_make.ml

@@ -134,6 +134,10 @@ module Make (Backend : M) = struct
 
   let realloc m ~ptr ~size = Backend.realloc m.data ~ptr ~size
 
+  let pp fmt m =
+    Fmt.pf fmt "@[<v 1>Memory:@;size: %a@;backend:@;@[<v 1> %a@]@]"
+      Smtml.Expr.pp m.size Backend.pp m.data
+
   (* TODO: Move this into a separate module? *)
   module ITbl = Hashtbl.Make (struct
     include Int

src/symbolic/symbolic_wasm_ffi.ml

@@ -98,3 +98,23 @@ let summaries_extern_module =
     ]
   in
   { Link.functions }
+
+let introspection_extern_module =
+  let dump_memory m : unit Choice.t =
+    Fmt.epr "%a@." Memory.pp m;
+    Choice.return ()
+  in
+
+  let print_i32 i32 : Symbolic_value.int32 Choice.t =
+    Fmt.pr "Print: %a@." Smtml.Expr.pp i32;
+    Choice.return i32
+  in
+  let functions =
+    [ ( "dump_memory"
+      , Symbolic.P.Extern_func.Extern_func (Func (Mem Res, R0), dump_memory) )
+    ; ( "print_i32"
+      , Symbolic.P.Extern_func.Extern_func
+          (Func (Arg (I32, Res), R1 I32), print_i32) )
+    ]
+  in
+  { Link.functions }

test/sym/memory/alloc_dynamic_dealloc_reuse_07.wat

@@ -0,0 +1,35 @@
+;; Reuse memory address chunk with different size
+(module
+  (import "summaries" "alloc" (func $malloc (param i32 i32) (result i32)))
+  (import "summaries" "dealloc" (func $free (param i32)))
+  (import "symbolic" "assert" (func $assert (param i32)))
+  (memory $m 1)
+  (global $__heap_base (mut i32) (i32.const 0x00000000))
+  (func $start (local i32)
+    global.get $__heap_base
+    i32.const 0x00000004
+    call $malloc
+    local.tee 0
+    i32.const 0x0000002a
+    i32.store
+    local.get 0
+    i32.load
+    i32.const 0x0000002a
+    i32.eq
+    call $assert
+    local.get 0
+    call $free
+    global.get $__heap_base
+    i32.const 0x00000008
+    call $malloc
+    local.tee 0
+    i32.const 0x00000054
+    i32.store
+    local.get 0
+    i32.load
+    i32.const 0x00000054
+    i32.eq
+    call $assert
+    local.get 0
+    call $free)
+  (start $start))

test/sym/memory/alloc_dynamic_multiple_blocks_06.wat

@@ -0,0 +1,37 @@
+;; Allocate multiple chunks and check that they don't overlap
+(module
+  (import "summaries" "alloc" (func $malloc (param i32 i32) (result i32)))
+  (import "summaries" "dealloc" (func $free (param i32)))
+  (import "symbolic" "assert" (func $assert (param i32)))
+  (memory $m 1)
+  (global $__heap_base (mut i32) (i32.const 0x00000000))
+  (func $start (local i32 i32)
+    global.get $__heap_base
+    i32.const 0x00000004
+    call $malloc
+    local.tee 0
+    global.get $__heap_base
+    i32.const 0x00000004
+    i32.add
+    i32.const 0x00000008
+    call $malloc
+    local.tee 1
+    i32.const 0x0000000a
+    i32.store
+    i32.const 0x0000000b
+    i32.store
+    local.get 0
+    i32.load
+    i32.const 0x0000000b
+    i32.eq
+    call $assert
+    local.get 1
+    i32.load
+    i32.const 0x0000000a
+    i32.eq
+    call $assert
+    local.get 1
+    call $free
+    local.get 0
+    call $free)
+  (start $start))

test/sym/memory/alloc_dynamic_single_block_05.wat

@@ -0,0 +1,22 @@
+;; Allocate a memory chunk, store and load same address
+(module
+  (import "summaries" "alloc" (func $malloc (param i32 i32) (result i32)))
+  (import "summaries" "dealloc" (func $free (param i32)))
+  (import "symbolic" "assert" (func $assert (param i32)))
+  (memory $m 1)
+  (global $__heap_base (mut i32) (i32.const 0x00000000))
+  (func $start (local i32)
+    global.get $__heap_base
+    i32.const 0x00000004
+    call $malloc
+    local.tee 0
+    i32.const 0xdeadbeef
+    i32.store
+    local.get 0
+    i32.load
+    i32.const 0xdeadbeef
+    i32.eq
+    call $assert
+    local.get 0
+    call $free)
+  (start $start))

test/sym/memory/alloc_dynamic_use_after_free_08.wat

@@ -0,0 +1,22 @@
+;; Dereference of a free'd pointer should not be allowed
+(module
+  (import "summaries" "alloc" (func $malloc (param i32 i32) (result i32)))
+  (import "summaries" "dealloc" (func $free (param i32)))
+  (import "symbolic" "assert" (func $assert (param i32)))
+  (memory $m 1)
+  (global $__heap_base (mut i32) (i32.const 0x00000000))
+  (func $start (local i32)
+    global.get $__heap_base
+    i32.const 0x00000004
+    call $malloc
+    local.tee 0
+    i32.const 0x0000002a
+    i32.store
+    local.get 0
+    call $free
+    local.get 0
+    i32.load
+    i32.const 0x0000002a
+    i32.eq
+    call $assert)
+  (start $start))

test/sym/memory/basic_load_uninitialized_02.wat

@@ -0,0 +1,10 @@
+(module
+  (import "symbolic" "assert" (func $assert (param i32)))
+  (memory $m 1)
+  (func $start
+    i32.const 0x00000000
+    i32.load
+    i32.const 0x00000000
+    i32.eq
+    call $assert)
+  (start $start))

test/sym/memory/basic_store_last_address_03.wat

@@ -0,0 +1,7 @@
+(module
+  (memory $m 1)
+  (func $start
+    i32.const 0x0000fffc
+    i32.const 0xbeefbabe
+    i32.store)
+  (start $start))

test/sym/memory/basic_store_load_single_address_01.wat

@@ -0,0 +1,17 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "assume" (func $assume (param i32)))
+  (import "symbolic" "assert" (func $assert (param i32)))
+  (import "introspection" "dump_memory" (func $dump_memory))
+  (import "introspection" "print_i32" (func $print_i32 (param i32) (result i32)))
+  (memory $m 1)
+  (func $start
+    i32.const 0x00000000
+    i32.const 0x50ffc001
+    i32.store
+    i32.const 0x00000000
+    i32.load
+    i32.const 0x50ffc001
+    i32.eq
+    call $assert)
+  (start $start))

test/sym/memory/basic_store_overflow_04.wat

@@ -0,0 +1,7 @@
+(module
+  (memory $m 1)
+  (func $start
+    i32.const 0x00010000
+    i32.const 0xbaaaaaad
+    i32.store)
+  (start $start))