Add literal test generation

src/dune

@@ -4,6 +4,7 @@
  (modules
   run
   syntax
+  value
   vuln
   vuln_intf
   vuln_parser

src/main.ml

@@ -1,14 +1,22 @@
 open I2
 open Cmdliner
 
-let main debug taint_summary file output =
+let symbolic debug taint_summary file output =
   if debug then Logs.set_level (Some Debug);
   match Run.run ?file ~config:taint_summary ~output () with
   | Ok _n -> 0
   | Error err ->
     Format.eprintf "unexpected error: %a@." Result.pp err;
     Result.to_code err
 
+let literal debug taint_summary file witness output =
+  if debug then Logs.set_level (Some Debug);
+  match Run.literal ?file taint_summary witness output with
+  | Ok _n -> 0
+  | Error err ->
+    Format.eprintf "unexpected error: %a@." Result.pp err;
+    Result.to_code err
+
 let debug =
   let doc = "debug mode" in
   Arg.(value & flag & info [ "debug" ] ~doc)
@@ -21,10 +29,23 @@ let file =
   let doc = "normalized file" in
   Arg.(value & pos 1 (some non_dir_file) None & info [] ~docv:"FILE" ~doc)
 
+let witness =
+  let doc = "witness file" in
+  Arg.(required & opt (some string) None & info [ "witness" ] ~doc)
+
 let output =
   let doc = "output file" in
   Arg.(value & opt string "symbolic_test" & info [ "output"; "o" ] ~doc)
 
+let cmd_symbolic =
+  let info = Cmd.info "symbolic" in
+  Cmd.v info Term.(const symbolic $ debug $ taint_summary $ file $ output)
+
+let cmd_literal =
+  let info = Cmd.info "literal" in
+  Cmd.v info
+    Term.(const literal $ debug $ taint_summary $ file $ witness $ output)
+
 let cmd =
   let doc = "Instrumentor2" in
   let man =
@@ -33,6 +54,6 @@ let cmd =
     ]
   in
   let info = Cmd.info "instrumentation2" ~version:"%%VERSION%%" ~doc ~man in
-  Cmd.v info Term.(const main $ debug $ taint_summary $ file  $ output)
+  Cmd.group info [ cmd_symbolic; cmd_literal ]
 
 let () = exit @@ Cmd.eval' cmd

src/run.ml

@@ -12,6 +12,10 @@ let write_test ~mode ~file module_data vuln =
   Format.eprintf "Genrating %a@." Fpath.pp file;
   OS.File.writef ~mode file "%s@\n%a@." module_data Vuln_symbolic.pp vuln
 
+let write_literal_test ~mode map file module_data vuln =
+  Format.eprintf "Genrating %a@." Fpath.pp file;
+  OS.File.writef ~mode file "%s@\n%a@." module_data (Vuln_literal.pp map) vuln
+
 (** [run file config output] creates symbolic tests [file] from [config] *)
 let run ?(mode = 0o644) ?file ~config ~output () =
   let+ vulns = Vuln_parser.from_file config in
@@ -42,3 +46,39 @@ let run ?(mode = 0o644) ?file ~config ~output () =
         confs )
     vulns
   |> List.concat
+
+let literal ?(mode = 0o644) ?file taint_summary witness output =
+  let* vulns = Vuln_parser.from_file taint_summary in
+  let+ witness_map = Value.Parser.from_file witness in
+  List.iteri
+    (fun i vuln ->
+      let confs = Vuln.unroll vuln in
+      List.iteri
+        (fun j conf ->
+          let st = Format.sprintf "symbolic_test_%d_%d" i j in
+          match Astring.String.find_sub ~sub:st witness with
+          | Some _ ->
+            let output_file = get_test_name output (i, j) in
+            let filename =
+              match file with
+              | Some f -> f
+              | None ->
+                let filename =
+                  match conf.Vuln_intf.filename with
+                  | Some f -> f
+                  | None -> assert false
+                in
+                Filename.(concat (dirname taint_summary) filename)
+            in
+            let module_data = In_channel.(with_open_text filename input_all) in
+            begin
+              match
+                write_literal_test ~mode witness_map output_file module_data
+                  conf
+              with
+              | Ok () -> ()
+              | Error (`Msg msg) -> failwith msg
+            end
+          | None -> () )
+        confs )
+    vulns

src/run.mli

@@ -4,4 +4,12 @@ val run :
   -> config:string
   -> output:string
   -> unit
-  -> (Fpath.t list, [> Result.err ]) Result.t
+  -> (Fpath.t list, [> Result.err ]) result
+
+val literal :
+     ?mode:int
+  -> ?file:string
+  -> string
+  -> string
+  -> string
+  -> (unit, [> Result.err ]) result

src/value.ml

@@ -0,0 +1,39 @@
+type t =
+  [ `Number of float
+  | `String of string
+  | `Bool of bool
+  | `Undefined
+  ]
+
+module Map = Map.Make (String)
+
+let pp fmt = function
+  | `Number x -> Format.pp_print_float fmt x
+  | `String x -> Format.fprintf fmt "%S" x
+  | `Bool x -> Format.pp_print_bool fmt x
+  | `Undefined -> Format.pp_print_string fmt "undefined"
+
+module Parser = struct
+  open Syntax.Result
+  module Json = Yojson.Basic
+  module Util = Yojson.Basic.Util
+
+  let from_json (json : Json.t) : t Map.t =
+    let add_binding map (name, json) =
+      match Util.member "value" json with
+      | `Null -> map
+      | `Float x -> Map.add name (`Number x) map
+      | `String x -> Map.add name (`String x) map
+      | `Bool x -> Map.add name (`Bool x) map
+      | _ -> assert false
+    in
+    let model = Util.member "model" json |> Util.to_assoc in
+    List.fold_left add_binding Map.empty model
+
+  let from_file (fname : string) : (t Map.t, [> Result.err ]) result =
+    let* json =
+      try Ok (Json.from_file ~fname fname)
+      with Yojson.Json_error msg -> Error (`Malformed_json msg)
+    in
+    Ok (from_json json)
+end

src/vuln_literal.ml

@@ -0,0 +1,104 @@
+open Format
+open Vuln_intf
+
+let template0 : ('a, Format.formatter, unit) format = "// Vuln: %a@\n%a"
+
+let template1 : ('a, Format.formatter, unit) format =
+  "// Vuln: %a@\n%a@\nconsole.log(({}).toString);"
+
+let get_template = function
+  | Some (Cmd_injection | Code_injection | Path_traversal) -> template0
+  | Some Proto_pollution | None -> template1
+
+let fresh_str =
+  let id = ref 0 in
+  fun () ->
+    incr id;
+    Format.sprintf "x_%d" !id
+
+let pp_vuln_type fmt = function
+  | Some Cmd_injection -> fprintf fmt "command-injection"
+  | Some Code_injection -> fprintf fmt "code-injection"
+  | Some Path_traversal -> fprintf fmt "path-traversal"
+  | Some Proto_pollution -> fprintf fmt "prototype-pollution"
+  | None -> ()
+
+let array_iter x f arr = List.iteri (fun i v -> f (x ^ string_of_int i, v)) arr
+
+let pp_iter ~pp_sep iter pp_v fmt v =
+  let is_first = ref true in
+  let pp_v v =
+    if !is_first then is_first := false else pp_sep fmt ();
+    pp_v fmt v
+  in
+  iter pp_v v
+
+let pp_array (iter : ('a -> unit) -> 'b -> unit) pp_v fmt v =
+  pp_iter ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") iter pp_v fmt v
+
+let get_value (map : Value.t Value.Map.t) (name : string) : Value.t =
+  match Value.Map.find_opt name map with Some v -> v | None -> `Undefined
+
+let rec pp_param map (box : ('a, formatter, unit) format) fmt
+  ((x, ty) : string * param_type) =
+  let rec pp_p fmt (x, ty) =
+    match ty with
+    | Any | Number | String | Boolean ->
+      let v = get_value map x in
+      Format.fprintf fmt "%a" Value.pp v
+    | Function -> fprintf fmt {|(_) => { return () => {}; };|}
+    | Object `Lazy -> fprintf fmt "{}"
+    | Object (`Polluted 2) ->
+      fprintf fmt {|{ ["__proto__"]: { "toString": "polluted" } }|}
+    | Object (`Polluted 3) ->
+      fprintf fmt
+        {|{ "constructor": { "prototype": { "toString": "polluted" } } }|}
+    | Object (`Normal props) ->
+      fprintf fmt "@[{ %a@ }@]" (pp_obj_props map) props
+    | Array arr -> fprintf fmt "[ %a ]" (pp_array (array_iter x) pp_p) arr
+    | Union _ | Object (`Polluted _) -> assert false
+  in
+  fprintf fmt box x pp_p (x, ty)
+
+and pp_obj_props map fmt props =
+  pp_print_list
+    ~pp_sep:(fun fmt () -> fprintf fmt "@\n, ")
+    (pp_param map "@[<hov 2>%s:@ %a@]")
+    fmt props
+
+and pp_params_as_decl map fmt (params : (string * param_type) list) =
+  pp_print_list
+    ~pp_sep:(fun fmt () -> fprintf fmt ";@\n")
+    (pp_param map "@[<hov 2>let %s =@ %a@]")
+    fmt params
+
+let pp_params_as_args fmt (args : (string * 'a) list) =
+  let args = List.map fst args in
+  pp_print_list
+    ~pp_sep:(fun fmt () -> pp_print_string fmt ", ")
+    pp_print_string fmt args
+
+let normalize = String.map (fun c -> match c with '.' | ' ' -> '_' | _ -> c)
+let ( let* ) v f = Option.bind v f
+
+let pp map fmt (v : vuln_conf) =
+  let rec pp_aux fmt { source; params; cont; _ } =
+    if List.length params > 0 then
+      fprintf fmt "%a;@\n" (pp_params_as_decl map) params;
+    match (cont, source) with
+    | None, Some source -> fprintf fmt "%s(%a);" source pp_params_as_args params
+    | Some (Return ret), Some source ->
+      let var_aux = "ret_" ^ normalize source in
+      fprintf fmt "var %s = %s(%a);@\n" var_aux source pp_params_as_args params;
+      let source =
+        let* ret_source = ret.source in
+        Some (var_aux ^ ret_source)
+      in
+      pp_aux fmt { ret with source }
+    | Some (Sequence cont), Some source ->
+      fprintf fmt "%s(%a);@\n" source pp_params_as_args params;
+      pp_aux fmt cont
+    | _, None -> assert false
+  in
+  let template = get_template v.ty in
+  fprintf fmt template pp_vuln_type v.ty pp_aux v

test/test_literal.t

@@ -0,0 +1,9 @@
+  $ instrumentation2 literal -o - unit/string.json unit/identity.js --witness unit/symbolic_test_0_0_witness.json
+  Genrating -
+  module.exports = function identity(some_arg) {
+    return some_arg
+  }
+
+  // Vuln: command-injection
+  let some_arg = "sou um valor concreto!";
+  module.exports(some_arg);

test/test_toy.t

@@ -1,5 +1,5 @@
 Test toy examples:
-  $ instrumentation2 toy/vfunexported.json toy/vfunexported.js -o -
+  $ instrumentation2 symbolic toy/vfunexported.json toy/vfunexported.js -o -
   Genrating -
   let exec = require('child_process').exec;
 
@@ -12,7 +12,7 @@ Test toy examples:
   // Vuln: command-injection
   let x = esl_symbolic.string("x");
   module.exports(x);
-  $ instrumentation2 toy/vfunretbyexport.json -o -
+  $ instrumentation2 symbolic toy/vfunretbyexport.json -o -
   Genrating -
   Genrating -
   function f1(a) {
@@ -45,7 +45,7 @@ Test toy examples:
   var ret_f1 = f1(a);
   let b = esl_symbolic.number("b");
   ret_f1(b);
-  $ instrumentation2 toy/vfunpropofexportedobj.json toy/vfunpropofexportedobj.js -o -
+  $ instrumentation2 symbolic toy/vfunpropofexportedobj.json toy/vfunpropofexportedobj.js -o -
   Genrating -
   let Obj = (function () {
     function Obj(source) { this.source = source; }
@@ -68,7 +68,7 @@ Test toy examples:
   var ret_module_exports_Obj = module.exports.Obj(source);
   let obj = { cond: esl_symbolic.number("cond") };
   ret_module_exports_Obj.f(obj);
-  $ instrumentation2 toy/example-20.json toy/example-20.js -o -
+  $ instrumentation2 symbolic toy/example-20.json toy/example-20.js -o -
   Genrating -
   var target = "";