Start concrete backend for symbolic engine

src/symbolic/symbolicUtility.ml

@@ -315,6 +315,23 @@ module MakeInterpreter (Filesystem: FILESYSTEM) = struct
   end
 end
 
+(* Concrete *)
+
+module ConcreteImplementation = struct
+  type filesystem = FilesystemSpec.t
+  type case_spec = filesystem -> filesystem option
+  let apply_spec fs spec = Option.to_list (spec fs)
+  let noop fs = Some fs
+end
+
+module Concrete = struct
+  include ConcreteImplementation
+  include MakeInterpreter (ConcreteImplementation)
+  include MakeSpecifications (ConcreteImplementation)
+
+  type config = unit
+
+  let filesystems () fs = [fs]
 end
 
 (* Constraints *)
@@ -392,19 +409,22 @@ end
 module MixedImplementation = struct
 
   type filesystem =
+    | Concrete of ConcreteImplementation.filesystem
     | Constraints of ConstraintsImplementation.filesystem
     | Transducers of TransducersImplementation.filesystem
 
   (* The case_specs are wrapped in a closure because they may raise Incomplete_case_spec *)
   type case_spec = {
+    concrete: unit -> ConcreteImplementation.case_spec;
     constraints: unit -> ConstraintsImplementation.case_spec;
     transducers: unit -> TransducersImplementation.case_spec;
   }
 
-  let case_spec ?transducers ?constraints () : case_spec =
+  let case_spec ?concrete ?transducers ?constraints () : case_spec =
     let case_spec_or_incomplete opt () =
       match opt with Some x -> x | None -> raise Incomplete_case_spec in
-    {constraints = case_spec_or_incomplete constraints;
+    {concrete = case_spec_or_incomplete concrete;
+     constraints = case_spec_or_incomplete constraints;
      transducers = case_spec_or_incomplete transducers}
 
   let noop : case_spec =
@@ -415,6 +435,9 @@ module MixedImplementation = struct
 
   let apply_spec fs spec =
     match fs with
+    | Concrete fs ->
+      ConcreteImplementation.apply_spec fs (spec.concrete ()) |>
+      List.map (fun fs -> Concrete fs)
     | Constraints fs ->
       ConstraintsImplementation.apply_spec fs (spec.constraints ()) |>
       List.map (fun fs -> Constraints fs)
@@ -434,6 +457,30 @@ module Mixed = struct
     args: string list;
   }
 
+  let state_from_concrete (s : Concrete.state) : state = {
+    filesystem=MixedImplementation.Concrete s.filesystem;
+    stdin=s.stdin;
+    stdout=s.stdout;
+    log=s.log;
+  }
+
+  let sym_state_from_concrete (s: Concrete.sym_state) : sym_state = {
+    state = state_from_concrete s.state;
+    context = s.context;
+  }
+
+  let state_to_concrete (s: state) : Concrete.state =
+    let filesystem =
+      match s.filesystem with
+      | Concrete fs -> fs
+      | _ -> invalid_arg "state_to_concrete" in
+    {filesystem; stdin=s.stdin; stdout=s.stdout; log=s.log}
+
+  let interp_program_concrete inp stas pro =
+    let stas' = List.map sym_state_from_concrete stas in
+    let normals, errors, failures = interp_program inp stas' pro in
+    List.map state_to_concrete normals, List.map state_to_concrete errors, List.map state_to_concrete failures
+
   let state_from_constraints (s : Constraints.state) : state = {
     filesystem=MixedImplementation.Constraints s.filesystem;
     stdin=s.stdin;
@@ -450,7 +497,7 @@ module Mixed = struct
     let filesystem =
       match s.filesystem with
       | Constraints fs -> fs
-      | Transducers _ -> invalid_arg "state_to_constraints" in
+      | _ -> invalid_arg "state_to_constraints" in
     {filesystem; stdin=s.stdin; stdout=s.stdout; log=s.log}
 
   let interp_program_constraints inp stas pro =
@@ -474,7 +521,7 @@ module Mixed = struct
     let filesystem =
       match s.filesystem with
       | Transducers fs -> fs
-      | Constraints _ -> invalid_arg "state_to_transducers" in
+      | _ -> invalid_arg "state_to_transducers" in
     {filesystem; stdin=s.stdin; stdout=s.stdout; log=s.log}
 
   let interp_program_transducers inp stas pro =

src/symbolic/symbolicUtility.mli

@@ -199,6 +199,24 @@ module MakeInterpreter (Filesystem: FILESYSTEM) : sig
   end
 end
 
+(** {1 Concrete backend} *)
+
+module ConcreteImplementation : sig
+  type filesystem = FilesystemSpec.t
+  type case_spec = filesystem -> filesystem option
+  val apply_spec : filesystem -> case_spec -> filesystem list
+  val noop : case_spec
+end
+
+(** Instantiation of the constraints-based backend with the interpreter and
+    specifications. *)
+module Concrete : sig
+  include module type of ConcreteImplementation
+    with type filesystem = ConcreteImplementation.filesystem
+  include module type of MakeInterpreter (ConcreteImplementation)
+  include module type of MakeSpecifications (ConcreteImplementation)
+  type config = unit
+  val filesystems : config -> FilesystemSpec.t -> filesystem list
 end
 
 (** {1 Constraints backend} *)
@@ -264,12 +282,16 @@ end
    backend. *)
 module MixedImplementation : sig
   type filesystem =
+    | Concrete of Concrete.filesystem
     | Constraints of Constraints.filesystem
     | Transducers of Transducers.filesystem
   type case_spec
   val noop : case_spec
-  val case_spec : ?transducers:TransducersImplementation.case_spec ->
-    ?constraints:ConstraintsImplementation.case_spec -> unit -> case_spec
+  val case_spec :
+    ?concrete:ConcreteImplementation.case_spec ->
+    ?transducers:TransducersImplementation.case_spec ->
+    ?constraints:ConstraintsImplementation.case_spec ->
+    unit -> case_spec
   val apply_spec : filesystem -> case_spec -> filesystem list
 end
 
@@ -288,6 +310,9 @@ module Mixed : sig
     args: string list;
   }
 
+  (** Symbolically interprete a program using the constraints backend *)
+  val interp_program_concrete : input -> Concrete.sym_state list -> program -> (Concrete.state list * Concrete.state list * Concrete.state list)
+
   (** Symbolically interprete a program using the constraints backend *)
   val interp_program_constraints : input -> Constraints.sym_state list -> program -> (Constraints.state list * Constraints.state list * Constraints.state list)
 

src/symbolic/utilities/mkdir.ml

@@ -21,6 +21,11 @@ let interp_mkdir1 cwd path_str =
       success_case
         ~descr:(asprintf "mkdir %a: create directory" Path.pp p)
         (case_spec
+           ~concrete:begin fun fs ->
+             let path = List.map Feat.to_string (cwd @ [f]) in
+             try Some (FilesystemSpec.add_dir path fs)
+             with Invalid_argument _ -> None
+           end
            ~transducers:()
            ~constraints:begin fun root root' ->
              exists3 @@ fun x x' y ->