address PR #128 review - 2

ECMA-SL/semantics/core/concrete/external.ml

@@ -48,7 +48,7 @@ module Impl = struct
     | List _ -> Str "list"
     | App (`Op "NullType", [])
     | App (`Op "IntType", [])
-    | App (`Op "RealType", [])
+    | App (`Op "FltType", [])
     | App (`Op "StrType", [])
     | App (`Op "BoolType", [])
     | App (`Op "SymbolType", [])

ECMA-SL/semantics/core/functorial/symbolic_extern.ml → ECMA-SL/semantics/core/functorial/symbolic_esl_ffi.ml

@@ -1,5 +1,4 @@
 open EslBase
-(* open EslSyntax *)
 module Env = Symbolic.P.Env
 module SMap = Link_env.SMap
 module PC = Choice_monad.PC
@@ -31,7 +30,7 @@ module Make () = struct
   let fresh_x = Base.make_name_generator "x"
   let fresh_func = Base.make_name_generator "eval_func_"
   let ok v = Choice.return (Ok v)
-  let ok_v v = ok (Smtml.Expr.(make @@ Val v))
+  let ok_v v = ok (E.value v)
   let err v = Choice.return (Error (`Failure v))
 
   let extern_cmds env =
@@ -464,21 +463,21 @@ module Make () = struct
     let is_exec_sat (e : value) =
       (* TODO: more fine-grained exploit analysis *)
       let i = Value.int_symbol_s (fresh_i ()) in
-      let len = E.(make @@ Val (Int 18)) in
+      let len = E.(value (Int 18)) in
       let sub = E.(triop Ty_str String_extract e i len) in
       let query =
-        E.(relop Ty_bool Eq sub (make @@ Val (V.Str "A; touch success #")))
+        E.(relop Ty_bool Eq sub (value (V.Str "A; touch success #")))
       in
       let/ b = Choice.check_add_true query in
       ok_v (if b then V.True else V.False)
     in
     let is_eval_sat (e : value) =
       (* TODO: more fine-grained exploit analysis *)
       let i = Value.int_symbol_s (fresh_i ()) in
-      let len = E.(make @@ Val (Int 25)) in
+      let len = E.(value (Int 25)) in
       let sub = E.(triop Ty_str String_extract e i len) in
       let query =
-        E.(relop Ty_bool Eq sub (make @@ Val (V.Str ";console.log('success')//")))
+        E.(relop Ty_bool Eq sub (value (V.Str ";console.log('success')//")))
       in
       let/ b = Choice.check_add_true query in
       ok_v (if b then V.True else V.False)
@@ -512,7 +511,7 @@ module Make () = struct
           let opt = Thread.optimizer thread in
           let v = optimize Optimizer.maximize opt e pc in
           match v with
-          | Some v -> Ok  (E.(make @@ Val v))
+          | Some v -> Ok  (E.(value v))
           | None ->
             (* TODO: Error here *)
             assert false )
@@ -523,7 +522,7 @@ module Make () = struct
           let opt = Thread.optimizer thread in
           let v = optimize Optimizer.minimize opt e pc in
           match v with
-          | Some v -> Ok  (E.(make @@ Val v))
+          | Some v -> Ok  (E.(value v))
           | None ->
             (* TODO: Error here *)
             assert false )

ECMA-SL/semantics/core/functorial/symbolic_memory.ml

@@ -20,7 +20,7 @@ module Make (O : Object_intf.S with type value = V.value) = struct
   let insert ({ data = memory; _ } : t) (o : object_) : value =
     let loc = Loc.create () in
     Loc.Tbl.replace memory loc o;
-    E.(make @@ Val (App (`Op "loc", [Int loc])))
+    E.(value (App (`Op "loc", [Int loc])))
 
   let remove (m : t) (l : Loc.t) : unit = Loc.Tbl.remove m.data l
 
@@ -100,13 +100,13 @@ module Make (O : Object_intf.S with type value = V.value) = struct
     match E.view e with
     | Val (App (`Op "loc", [Int l])) -> Ok [ (None, l) ]
     | Triop (_, Ty.Ite, c, a, v) -> (
-      match Expr.view a with
+      match E.view a with
       | Val (App (`Op "loc", [Int l])) ->
           Ok
             ((Some c, l)
-            :: unfold_ite ~accum:Expr.(unop Ty.Ty_bool Ty.Not c) v)
+            :: unfold_ite ~accum:E.(unop Ty.Ty_bool Ty.Not c) v)
       | _ ->
-          Error (Fmt.str "Value '%a' is not a loc expression" Expr.pp e))
+          Error (Fmt.str "Value '%a' is not a loc expression" E.pp e))
     | _ -> Error (Fmt.str "Value '%a' is not a loc expression" V.pp e)
 
   let pp_val (h : t) (e : value) : string =

ECMA-SL/semantics/core/functorial/symbolic_object.ml

@@ -5,7 +5,7 @@ module E = Symbolic_value.E
 
 let eq v1 v2 = E.(relop Ty_bool Ty.Eq v1 v2)
 let ne v1 v2 = E.(unop Ty.Ty_bool Ty.Not (eq v1 v2))
-let ite c v1 v2 = Expr.(Bool.ite c v1 v2)
+let ite c v1 v2 = E.(Bool.ite c v1 v2)
 let undef = V.mk_symbol "undefined"
 let is_val e = match E.view e with Val _ -> true | _ -> false
 
@@ -61,7 +61,7 @@ module M : Object_intf.S with type value = V.value = struct
       m
 
   let set o ~key ~data =
-    match Expr.view key with
+    match E.view key with
     | Val _ -> { o with fields = VMap.add key data o.fields }
     | _ ->
       { fields = map_ite o.fields ~key ~data
@@ -111,7 +111,7 @@ module M : Object_intf.S with type value = V.value = struct
           [ (v, []); (undef, neg_conds) ] ) )
 
   let delete o key =
-    match Expr.view key with
+    match E.view key with
     | Val _ -> { o with fields = VMap.remove key o.fields }
     | _ -> assert false
 

ECMA-SL/semantics/core/functorial/symbolic_value.ml

@@ -18,7 +18,7 @@ module M = struct
   let int_symbol_s (x : string) : value = E.mk_symbol (Symbol.make Ty_int x)
   [@@inline]
 
-  let mk_symbol (x : string) : value =  E.(make @@ Val (App (`Op "symbol", [Str x]))) [@@inline]
+  let mk_symbol (x : string) : value =  E.(value (App (`Op "symbol", [Str x]))) [@@inline]
 
   let mk_list (vs : value list) : value = E.(make (List vs))
   [@@inline]
@@ -35,8 +35,9 @@ module M = struct
 
   module Bool = struct
     include E.Bool
-    let const b = v b [@@inline]
-    let not_ e = not e [@@inline]
+
+    let const b = if b then true_ else false_
+    let not_ e = not_ e [@@inline]
   end
 
   module Store = struct
@@ -94,7 +95,7 @@ module M = struct
   | StringToInt -> E.(cvtop Ty_str String_to_int)
   | StringToFloat -> 
     (fun v -> match E.view v with 
-      | Val Str _ -> ( try E.(cvtop Ty_str Ty.String_to_float) v with _ -> E.(make @@ Val (Real nan )))
+      | Val Str _ -> ( try E.(cvtop Ty_str Ty.String_to_float) v with _ -> E.(value (Real nan )))
       | _ -> failwith "TODO:x StringToFloat" )
   | FromCharCode -> E.(cvtop Ty_str String_from_code)
   | ToCharCode -> E.(cvtop Ty_str String_to_code)
@@ -241,7 +242,7 @@ module M = struct
 
   let rec eval_expr (store : store) (e : Expr.t) : value =
     match e.it with
-    | Val v -> E.(make (Val v))
+    | Val v -> E.value v
     | Var x -> (
       match Store.find store x with
       | Some v -> v

ECMA-SL/semantics/core/parser/parser.mly

@@ -218,7 +218,7 @@ let val_target :=
 let dtype_target :=
   | DTYPE_NULL;          { "NullType" }
   | DTYPE_INT;           { "IntType" }
-  | DTYPE_FLT;           { "RealType" }
+  | DTYPE_FLT;           { "FltType" }
   | DTYPE_STR;           { "StrType" }
   | DTYPE_BOOL;          { "BoolType" }
   | DTYPE_SYMBOL;        { "SymbolType" }

ECMA-SL/semantics/dune

@@ -66,7 +66,7 @@
   memory_intf
   object_intf
   solver
-  symbolic_extern
+  symbolic_esl_ffi
   symbolic_interpreter
   symbolic_memory
   symbolic_object

ECMA-SL/semantics/extended/parser/eParser.mly

@@ -360,7 +360,7 @@ let val_target :=
 let dtype_target :=
   | DTYPE_NULL;          { "NullType" }
   | DTYPE_INT;           { "IntType" }
-  | DTYPE_FLT;           { "RealType" }
+  | DTYPE_FLT;           { "FltType" }
   | DTYPE_STR;           { "StrType" }
   | DTYPE_BOOL;          { "BoolType" }
   | DTYPE_SYMBOL;        { "SymbolType" }

ECMA-SL/syntax/extended/eExpr.ml

@@ -46,7 +46,7 @@ let pp_val_custom_inner (pp_inner_val : Fmt.t -> Smtml.Value.t -> unit) (ppf : F
   | List lst -> format ppf "[%a]" (pp_lst !>", " pp_inner_val) lst
   | App (`Op "NullType" , []) -> format ppf "__$Null" 
   | App (`Op "IntType" , []) -> format ppf "__$Int" 
-  | App (`Op "RealType" , []) -> format ppf "__$Flt" 
+  | App (`Op "FltType" , []) -> format ppf "__$Flt" 
   | App (`Op "StrType" , []) -> format ppf "__$Str" 
   | App (`Op "BoolType" , []) -> format ppf "__$Bool" 
   | App (`Op "SymbolType" , []) -> format ppf "__$Symbol" 

bin/commands/cmd_symbolic.ml

@@ -46,9 +46,9 @@ let dispatch_prog (lang : Enums.Lang.t) (fpath : Fpath.t) : Prog.t Result.t =
 
 let link_env (prog : Prog.t) : Extern_func.extern_func Symbolic.Env.t =
   let env0 = Env.Build.empty () |> Env.Build.add_functions prog in
-  Env.Build.add_extern_functions (Symbolic_extern.extern_cmds env0) env0
-  |> Env.Build.add_extern_functions Symbolic_extern.concrete_api
-  |> Env.Build.add_extern_functions Symbolic_extern.symbolic_api
+  Env.Build.add_extern_functions (Symbolic_esl_ffi.extern_cmds env0) env0
+  |> Env.Build.add_extern_functions Symbolic_esl_ffi.concrete_api
+  |> Env.Build.add_extern_functions Symbolic_esl_ffi.symbolic_api
 
 let pp_model (ppf : Fmt.t) (model : Smtml.Model.t) : unit =
   let open Fmt in

ecma-sl.opam

@@ -48,5 +48,5 @@ build: [
 dev-repo: "git+https://github.com/formalsec/ECMA-SL.git"
 
 pin-depends: [
-  [ "smtml.dev" "git+https://github.com/formalsec/smtml#extend_ops"]
+  [ "smtml.dev" "git+https://github.com/formalsec/smtml#ff3c34ad926f7b4329fe7412fe31d270c7b2220b"]
 ]

ecma-sl.opam.template

@@ -1,4 +1,4 @@
 
 pin-depends: [
-  [ "smtml.dev" "git+https://github.com/formalsec/smtml#extend_ops"]
+  [ "smtml.dev" "git+https://github.com/formalsec/smtml#ff3c34ad926f7b4329fe7412fe31d270c7b2220b"]
 ]