Functorize symbolic engine

src/colis.ml

@@ -14,11 +14,15 @@ end
 module Common = struct
   module Arguments = Semantics__Arguments
   module Behaviour = Semantics__Behaviour
-  module Env = Env
-  module Stdin = Semantics__Buffers.Stdin
-  module Stdout = Semantics__Buffers.Stdout
   module Config = Semantics__Config
+  module Context = Semantics__Context
+  module Env = Semantics__Env
   module Input = Semantics__Input
+  module InterpUtilitySpec = Semantics__InterpUtilitySpec
+  module Path = Semantics__Path
+  module Result = Semantics__Result
+  module Stdin = Semantics__Buffers.Stdin
+  module Stdout = Semantics__Buffers.Stdout
 end
 
 module Concrete = struct
@@ -29,16 +33,12 @@ module Concrete = struct
 end
 
 module Symbolic = struct
-  module Filesystem = SymbolicInterpreter__Filesystem
+  include SymbolicUtility.Symbolic
+
   module FilesystemSpec = FilesystemSpec
-  module Semantics = SymbolicInterpreter__Semantics
-  module SymState = SymbolicInterpreter__SymState
-  module Results = SymbolicInterpreter__Results
-  module Interpreter = SymbolicInterpreter__Interpreter
-  module Utility = SymbolicUtility
 
   let () =
-    List.iter SymbolicUtility.register [
+    List.iter register [
       (module Basics.True) ;
       (module Basics.Colon) ;
       (module Basics.False) ;
@@ -68,16 +68,16 @@ module Symbolic = struct
 
   let to_state ~prune_init_state ~root clause : Semantics.state =
     let root0 = if prune_init_state then None else Some root in
-    let filesystem = {Filesystem.root; clause; root0} in
+    let filesystem = {root; clause; root0} in
     {Semantics.filesystem; stdin=Common.Stdin.empty; stdout=Common.Stdout.empty; log=Common.Stdout.empty}
 
   let to_symbolic_state ~vars ~arguments state =
-    let open Semantics in
     let context =
-      let var_env = Semantics.add_var_bindings true vars Semantics.empty_var_env in
-      {Semantics.empty_context with arguments; var_env; cwd=[]}
+      let open Common.Context in
+      let var_env = add_var_bindings true vars empty_var_env in
+      {empty_context with arguments; var_env; cwd=[]}
     in
-    {SymState.state; context; data=()}
+    {state; context}
 
   let interp_program ~loop_limit ~stack_size ~argument0 stas' program =
     let open Common in
@@ -88,7 +88,7 @@ module Symbolic = struct
         let stack_size = Finite (Z.of_int stack_size) in
         { loop_limit; stack_size } in
       Input.({ argument0; config; under_condition=false }) in
-    let normals, errors, failures = Interpreter.interp_program inp stas' program in
+    let normals, errors, failures = interp_program inp stas' program in
     normals, errors, failures
 end
 
@@ -164,12 +164,13 @@ let colis_to_file filename colis =
 let run ~argument0 ?(arguments=[]) ?(vars=[]) colis =
   let open Common in
   let open Concrete in
+  let open Context in
   let input =
     let config = Config.({loop_limit = Infinite; stack_size = Infinite }) in
     Input.({ argument0; config; under_condition=false }) in
   let state = Interpreter.empty_state () in
   state.arguments := arguments;
-  state.var_env := Semantics.add_var_bindings true vars Semantics.empty_var_env;
+  state.var_env := add_var_bindings true vars empty_var_env;
   try
     Interpreter.interp_program input state colis;
     print_string (Stdout.all_lines !(state.stdout) |> List.rev |> String.concat "\n");
@@ -196,7 +197,7 @@ type symbolic_config = {
 
 let print_symbolic_filesystem fmt fs =
   let open Colis_constraints in
-  let open Symbolic.Filesystem in
+  let open Symbolic in
   fprintf fmt "root: %a@\n" Var.pp fs.root;
   fprintf fmt "clause: %a@\n" Clause.pp_sat_conj fs.clause
 

src/colis.mli

@@ -14,10 +14,15 @@ end
 module Common : sig
   module Arguments = Semantics__Arguments
   module Behaviour = Semantics__Behaviour
-  module Env = Env
+  module Config = Semantics__Config
+  module Context = Semantics__Context
+  module Env = Semantics__Env
+  module Input = Semantics__Input
+  module InterpUtilitySpec = Semantics__InterpUtilitySpec
+  module Path = Semantics__Path
+  module Result = Semantics__Result
   module Stdin = Semantics__Buffers.Stdin
   module Stdout = Semantics__Buffers.Stdout
-  module Input = Semantics__Input
 end
 
 module Concrete : sig
@@ -28,27 +33,23 @@ module Concrete : sig
 end
 
 module Symbolic : sig
-  module Filesystem = SymbolicInterpreter__Filesystem
+  include module type of SymbolicUtility.Symbolic
   module FilesystemSpec = FilesystemSpec
-  module Semantics = SymbolicInterpreter__Semantics
-  module SymState = SymbolicInterpreter__SymState
-  module Results = SymbolicInterpreter__Results
-  module Interpreter = SymbolicInterpreter__Interpreter
-  module Utility = SymbolicUtility
 
   open Colis_constraints
+  open Semantics
 
   (** [compile_fs_spec root conj fs_spec] creates a disjunction that represents the conjunction [conj] with constraints representing the filesystem specified by [fs_spec] *)
   val add_fs_spec_to_clause : Var.t -> Clause.sat_conj -> FilesystemSpec.t -> Clause.sat_conj list
 
   (* Create a state corresponding to a conjunction *)
-  val to_state : prune_init_state:bool -> root:Var.t -> Clause.sat_conj -> Semantics.state
+  val to_state : prune_init_state:bool -> root:Var.t -> Clause.sat_conj -> state
 
   (* Create a symbolic states by adding context to a stringe *)
-  val to_symbolic_state : vars:(string * string) list -> arguments:string list -> Semantics.state -> unit SymState.sym_state
+  val to_symbolic_state : vars:(string * string) list -> arguments:string list -> state -> sym_state
 
   (* Wrapper around [Symbolic.Interpreter.interp_program] *)
-  val interp_program : loop_limit:int -> stack_size:int -> argument0:string -> unit SymState.sym_state list -> Language.Syntax.program -> (Semantics.state list * Semantics.state list * Semantics.state list)
+  val interp_program : loop_limit:int -> stack_size:int -> argument0:string -> sym_state list -> Language.Syntax.program -> (state list * state list * state list)
 end
 
 module Constraints = Colis_constraints
@@ -119,13 +120,13 @@ type symbolic_config = {
   (** Maximum height of the call stack in symbolic execution *)
 }
 
-open Symbolic
+open Symbolic.Semantics
 
-val print_symbolic_state : Format.formatter -> ?id:string -> Semantics.state -> unit
+val print_symbolic_state : Format.formatter -> ?id:string -> state -> unit
 
-val print_symbolic_states : initials:Semantics.state list -> (Semantics.state list * Semantics.state list * Semantics.state list) -> unit
+val print_symbolic_states : initials:state list -> (state list * state list * state list) -> unit
 
-val exit_code : (Semantics.state list * Semantics.state list * Semantics.state list) -> int
+val exit_code : (state list * state list * state list) -> int
 
 val run_symbolic : symbolic_config -> Symbolic.FilesystemSpec.t -> argument0:string -> ?arguments:(string list) -> ?vars:((string * string) list) -> colis -> unit
 (** Symbolically executes a Colis program. *)

src/concrete/driver.drv

@@ -3,16 +3,26 @@ module semantics.Env
   syntax val empty_env "Env.empty %1"
   syntax val ([]) "Env.get %1 %2"
   syntax val ([<-]) "Env.set %1 %2 %3"
+  syntax type env0 "%1 Env.SMap.t"
 end
 
 module semantics.Buffers
   syntax val concat_lines "String.concat \"\n\" %1"
   syntax val split_on_default_ifs "Str.(split (regexp \"[ \t\n]+\") %1)"
 end
 
-module interpreter.Semantics
-  syntax val filter_var_env "Env.filter_var_env (fun v -> v.Interpreter__Semantics.exported) (fun v -> v.Interpreter__Semantics.value) %1"
-  syntax val interp_utility "Utilities.interp_utility %1 %2 %3"
-  syntax val normalized_path_to_string "String.concat \"/\" %1"
-  syntax val absolute_or_concat_relative "Utilities.absolute_or_concat_relative %1 %2"
+module semantics.Path
+  syntax type feature "Colis_constraints.Feat.t"
+  syntax type normalized_path "Colis_constraints.Path.normal"
+  syntax val default_cwd "[]"
+  syntax val normalized_path_to_string "Colis_constraints.Path.normal_to_string %1"
+  syntax val absolute_or_concat_relative "Colis_constraints.Path.(normalize ~cwd:%1 (from_string %2))"
+end
+
+module semantics.Context
+  syntax val filter_var_env "Semantics__Context.(Env.filter_var_env (fun v -> v.exported) (fun v -> v.value) %1)"
+end
+
+module interpreter.Interpreter
+  syntax val interp_utility "Utilities.interp_utility %1"
 end

src/concrete/env.ml

@@ -1,14 +1,19 @@
-module IdMap = Map.Make (String)
-type 'a env = {map: 'a IdMap.t; default: 'a}
-let empty default = {map=IdMap.empty; default}
-let get env id = try IdMap.find id env.map with Not_found -> env.default
-let set env id value = {env with map=IdMap.add id value env.map}
-let filter p env = {env with map=IdMap.filter p env.map}
-let map f default env = {map=IdMap.map f env.map; default}
-let elements env = IdMap.fold (fun k v t -> (k, v) :: t) env.map []
+module SMap = Map.Make (String)
+
+type 'a env = {map: 'a SMap.t; default: 'a}
+
+let empty default = {map=SMap.empty; default}
+let get env id = try SMap.find id env.map with Not_found -> env.default
+let set env id value = {env with map=SMap.add id value env.map}
+let filter p env = {env with map=SMap.filter p env.map}
+let map f default env = {map=SMap.map f env.map; default}
+let elements env = SMap.fold (fun k v t -> (k, v) :: t) env.map []
 let to_map env = env.map
 
-let filter_var_env (var_exported: 'a -> bool) (var_value: 'a -> string option) (env : 'a env) : string IdMap.t =
+let filter_var_env (var_exported: 'a -> bool) (var_value: 'a -> 'b option) (env : 'a env) : 'b SMap.t =
+  let open SMap in
   env.map |>
-  IdMap.filter (fun _ v -> var_exported v && var_value v <> None) |>
-  IdMap.map (fun v -> match var_value v with Some s -> s | _ -> assert false)
+  filter (fun _ -> var_exported) |>
+  map var_value |>
+  filter (fun _ -> (<>) None) |>
+  map (function Some x -> x | _ -> assert false)

src/concrete/env.mli

@@ -8,9 +8,9 @@ val filter : (string -> 'a -> bool) -> 'a env -> 'a env
 val map : ('a -> 'b) -> 'b -> 'a env -> 'b env
 val elements : 'a env -> (string * 'a) list
 
-module IdMap : Map.S with type key = string
+module SMap : Map.S with type key = string
 
 (** Conversion to a normal map without default value *)
-val to_map : 'a env -> 'a IdMap.t
+val to_map : 'a env -> 'a SMap.t
 
-val filter_var_env : ('a -> bool) -> ('a -> string option) -> 'a env -> string IdMap.t
+val filter_var_env : ('a -> bool) -> ('a -> 'b option) -> 'a env -> 'b SMap.t

src/concrete/interpreter.mlw

@@ -22,8 +22,12 @@ module State
   use ref.Ref
   use list.List
   use string.String
-  use Filesystem
+
   use semantics.Buffers
+  use semantics.Context
+  use semantics.Env
+  use semantics.Path
+  use Filesystem
   use import Semantics as S
 
   type sem_state = state
@@ -42,7 +46,7 @@ module State
     var_env : ref var_env;
     func_env : func_env;
     arguments: ref (list string);
-    cwd : ref (list string);
+    cwd : ref normalized_path;
     result : ref bool;
   }
 end
@@ -59,18 +63,21 @@ module Interpreter
   use map.MapExt
   use int.Int
   use ref.Refint
+  use string.OCaml as String
 
   use auxiliaries.OptionGet
-  use string.OCaml as String
+  use auxiliaries.TakeDrop
   use syntax.Syntax
+  use semantics.Arguments
   use semantics.Result
   use semantics.Buffers
   use semantics.Behaviour
   use semantics.Input
   use semantics.Config
+  use semantics.Context
   use semantics.Env as E
+  use semantics.Path
   use Filesystem as Fs
-  use auxiliaries.TakeDrop
   use import Semantics as S
   use import State as St
 
@@ -85,22 +92,22 @@ module Interpreter
 
   let empty_state () = {
     St.filesystem = ref Filesystem.empty;
-    St.var_env = ref S.empty_var_env;
-    St.func_env = S.empty_func_env;
+    St.var_env = ref empty_var_env;
+    St.func_env = empty_func_env;
     St.arguments = ref Nil;
     St.stdin = ref Stdin.empty;
     St.stdout = ref Stdout.empty;
     St.log = ref Stdout.empty;
-    St.cwd = ref Nil;
+    St.cwd = ref default_cwd;
     St.result = ref True;
   }
 
-  function sem_context (sta:state) : S.context = {
-    S.var_env = !(sta.var_env);
-    S.func_env = sta.func_env;
-    S.arguments = !(sta.arguments);
-    S.cwd = !(sta.cwd);
-    S.result = !(sta.result);
+  function sem_context (sta:state) : context = {
+    Context.var_env = !(sta.var_env);
+    Context.func_env = sta.func_env;
+    Context.arguments = !(sta.arguments);
+    Context.cwd = !(sta.cwd);
+    Context.result = !(sta.result);
   }
 
   lemma context_same: forall sta1 sta2.
@@ -139,22 +146,30 @@ module Interpreter
 
   (** {3 Imperative wrapper around the functional interpretation of utilties} *)
 
-  let interp_utility (inp:input) (sta:state) (id:identifier) (args:list string)
+  (** Interprete a command defined in the document *Specification of UNIX Commands*. *)
+  val interp_utility (params: (utility_context, identifier, S.state)) : (S.state, result bool)
+    ensures { S.interp_utility params result }
+
+  let interp_utility' (inp:input) (sta:state) (id:identifier) (args:list string)
     ensures {
-      interp_utility (!(old sta.cwd), filter_var_env !(old sta.var_env), args) id (old sem_state sta) = (sem_state sta, Ok !(sta.result)) /\
+      let utility_ctx = {S.cwd= !(old sta.cwd); env=filter_var_env !(old sta.var_env); args=args} in
+      interp_utility (utility_ctx, id, old sem_state sta) (sem_state sta, Ok !(sta.result)) /\
       behaviour inp !(sta.result) = BNormal
     }
     raises { EExit ->
-      interp_utility (!(old sta.cwd), filter_var_env !(old sta.var_env), args) id (old sem_state sta) = (sem_state sta, Ok !(sta.result)) /\
+      let utility_ctx = {S.cwd= !(old sta.cwd); env=filter_var_env !(old sta.var_env); args=args} in
+      interp_utility (utility_ctx, id, old sem_state sta) (sem_state sta, Ok !(sta.result)) /\
       behaviour inp !(sta.result) = BExit
     }
     raises { EIncomplete ->
-      interp_utility (!(old sta.cwd), filter_var_env !(old sta.var_env), args) id (old sem_state sta) = (sem_state sta, Incomplete)
+      let utility_ctx = {S.cwd= !(old sta.cwd); env=filter_var_env !(old sta.var_env); args=args} in
+      interp_utility (utility_ctx, id, old sem_state sta) (sem_state sta, Incomplete)
     }
     raises { EIncomplete ->
       sem_context sta = sem_context (old sta)
     }
-  = let sta', r = interp_utility (!(sta.cwd), filter_var_env !(sta.var_env), args) id (sem_state sta) in
+  = let utility_ctx = {S.cwd= !(sta.cwd); env=filter_var_env !(sta.var_env); args=args} in
+    let sta', r = interp_utility (utility_ctx, id, sem_state sta) in
     sta.filesystem := sta'.S.filesystem;
     assert { !(sta.filesystem) = sta'.S.filesystem };
     sta.stdin := sta'.S.stdin;
@@ -168,8 +183,6 @@ module Interpreter
       raise EIncomplete
     end
 
-  use semantics.Arguments
-
   let shift_arguments sta n
     requires { n >= 0 }
     ensures {
@@ -256,7 +269,7 @@ module Interpreter
 
     | IExport id ->
       let old_env = !(sta.var_env) in
-      let var_val = {old_env[id] with S.exported=True} in
+      let var_val = {old_env[id] with exported=True} in
       sta.var_env := old_env[id <- var_val];
       sta.result := True
 
@@ -339,7 +352,7 @@ module Interpreter
 
     | ICallUtility name le ->
       let args = interp_list_expr inp sta le in
-      interp_utility inp sta name args
+      interp_utility' inp sta name args
 
     | ICallFunction id le ->
       let args = interp_list_expr inp sta le in
@@ -430,7 +443,7 @@ module Interpreter
       let cwd_p = absolute_or_concat_relative !(sta.cwd) s in
       let pwd_s = normalized_path_to_string cwd_p in
       let args = Cons "-d" (Cons pwd_s Nil) in
-      interp_utility {inp with under_condition=True} sta identifier_test args;
+      interp_utility' {inp with under_condition=True} sta identifier_test args;
       if !(sta.result) then begin
         sta.var_env := !(sta.var_env)[identifier_pwd <- pwd_s]';
         sta.cwd := cwd_p