From 6e41cab42230e2f3879f2e0ec586d86da09a8cf3 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 11 Mar 2019 09:11:48 -0700
Subject: [PATCH] [sledge] Change strlen from an instruction to an intrinsic

Summary:
Also minor change to make strlen implementation syntactically closer
to spec.

Reviewed By: ngorogiannis

Differential Revision: D14403647

fbshipit-source-id: 48c771329
---
 sledge/src/llair/frontend.ml |  7 -------
 sledge/src/llair/llair.ml    | 11 +----------
 sledge/src/llair/llair.mli   |  4 ----
 sledge/src/symbheap/exec.ml  |  9 ++++++---
 4 files changed, 7 insertions(+), 24 deletions(-)

diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml
index 76f4399a8..c24953af1 100644
--- a/sledge/src/llair/frontend.ml
+++ b/sledge/src/llair/frontend.ml
@@ -954,13 +954,6 @@ let xlate_instr :
       | ["__llair_throw"] ->
           let exc = xlate_value x (Llvm.operand instr 0) in
           terminal (pop loc) (Llair.Term.throw ~exc ~loc) []
-      | ["strlen"] ->
-          let ptr = xlate_value x (Llvm.operand instr 0) in
-          continue (fun (insts, term) ->
-              ( Llair.Inst.strlen ~reg:(Option.value_exn reg) ~ptr ~loc
-                :: insts
-              , term
-              , [] ) )
       | ["malloc"] ->
           let siz = xlate_value x (Llvm.operand instr 0) in
           continue (fun (insts, term) ->
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 025bab18e..b30d4dab4 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -16,7 +16,6 @@ type inst =
   | Alloc of {reg: Var.t; num: Exp.t; len: Exp.t; loc: Loc.t}
   | Free of {ptr: Exp.t; loc: Loc.t}
   | Malloc of {reg: Var.t; siz: Exp.t; loc: Loc.t}
-  | Strlen of {reg: Var.t; ptr: Exp.t; loc: Loc.t}
   | Nondet of {reg: Var.t option; msg: string; loc: Loc.t}
 [@@deriving sexp]
 
@@ -109,8 +108,6 @@ let pp_inst fs inst =
   | Free {ptr; loc} -> pf "@[<2>free %a;@]\t%a" Exp.pp ptr Loc.pp loc
   | Malloc {reg; siz; loc} ->
       pf "@[<2>malloc %a@ %a;@]\t%a" Var.pp reg Exp.pp siz Loc.pp loc
-  | Strlen {reg; ptr; loc} ->
-      pf "@[<2>strlen %a@ %a;@]\t%a" Var.pp reg Exp.pp ptr Loc.pp loc
   | Nondet {reg; msg; loc} ->
       pf "@[<2>nondet %a\"%s\";@]\t%a" (Option.pp "%a " Var.pp) reg msg
         Loc.pp loc
@@ -195,7 +192,6 @@ module Inst = struct
   let alloc ~reg ~num ~len ~loc = Alloc {reg; num; len; loc}
   let free ~ptr ~loc = Free {ptr; loc}
   let malloc ~reg ~siz ~loc = Malloc {reg; siz; loc}
-  let strlen ~reg ~ptr ~loc = Strlen {reg; ptr; loc}
   let nondet ~reg ~msg ~loc = Nondet {reg; msg; loc}
 
   let loc = function
@@ -207,17 +203,12 @@ module Inst = struct
      |Alloc {loc}
      |Free {loc}
      |Malloc {loc}
-     |Strlen {loc}
      |Nondet {loc} ->
         loc
 
   let union_locals inst vs =
     match inst with
-    | Load {reg}
-     |Alloc {reg}
-     |Malloc {reg}
-     |Strlen {reg}
-     |Nondet {reg= Some reg} ->
+    | Load {reg} | Alloc {reg} | Malloc {reg} | Nondet {reg= Some reg} ->
         Set.add vs reg
     | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _ | Nondet {reg= None}
       ->
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index b29eac273..57f132442 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -50,9 +50,6 @@ type inst = private
   | Malloc of {reg: Var.t; siz: Exp.t; loc: Loc.t}
       (** Maybe allocate a block of memory of size [siz] bytes and bind
           [reg] to the first address, otherwise bind [reg] to [null]. *)
-  | Strlen of {reg: Var.t; ptr: Exp.t; loc: Loc.t}
-      (** Bind [reg] to the length of the null-terminated string in memory
-          starting from [ptr]. *)
   | Nondet of {reg: Var.t option; msg: string; loc: Loc.t}
       (** Bind [reg] to an arbitrary value, representing non-deterministic
           approximation of behavior described by [msg]. *)
@@ -136,7 +133,6 @@ module Inst : sig
   val alloc : reg:Var.t -> num:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val free : ptr:Exp.t -> loc:Loc.t -> inst
   val malloc : reg:Var.t -> siz:Exp.t -> loc:Loc.t -> inst
-  val strlen : reg:Var.t -> ptr:Exp.t -> loc:Loc.t -> inst
   val nondet : reg:Var.t option -> msg:string -> loc:Loc.t -> inst
   val loc : inst -> Loc.t
   val locals : inst -> Var.Set.t
diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml
index 3f2cc8f23..29627ce5f 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/sledge/src/symbheap/exec.ml
@@ -248,7 +248,7 @@ let strlen_spec us reg ptr =
   let {Sh.loc= p; bas= b; len= m} = seg in
   let ret =
     Exp.sub Typ.siz
-      (Exp.add Typ.siz (Exp.sub Typ.siz b p) m)
+      (Exp.sub Typ.siz (Exp.add Typ.siz b m) p)
       (Exp.integer Z.one Typ.siz)
   in
   let post = Sh.and_ (Exp.eq (Exp.var reg) ret) foot in
@@ -300,7 +300,6 @@ let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result =
   | Alloc {reg; num; len} -> exec_spec pre (alloc_spec us reg num len)
   | Free {ptr} -> exec_spec pre (free_spec us ptr)
   | Malloc {reg; siz} -> exec_spec pre (malloc_spec us reg siz)
-  | Strlen {reg; ptr} -> exec_spec pre (strlen_spec us reg ptr)
   | Nondet _ -> Ok pre
 
 let intrinsic :
@@ -316,4 +315,8 @@ let intrinsic :
       result Var.pp intrinsic (List.pp ",@ " Exp.pp) (List.rev actuals)
       Sh.pp pre] ;
   let us = pre.us in
-  match (result, Var.name intrinsic, actuals) with _ -> None
+  match (result, Var.name intrinsic, actuals) with
+  (* size_t strlen (const char* ptr) *)
+  | Some reg, "strlen", [ptr] ->
+      Some (exec_spec pre (strlen_spec us reg ptr))
+  | _ -> None