Functorize symbolic engine

Fixes #116

Makefile

@@ -48,7 +48,7 @@ extract-why3:
     -L src/symbolic \
 		-o src/why3 \
 		interpreter.Interpreter \
-    symbolicInterpreter.Interpreter
+    symbolicInterpreter.SymbolicInterpreter
 
 clean-why3:
 	rm -rf src/why3

src/concrete/driver.drv

@@ -1,16 +1,26 @@
+module semantics.Paths
+  syntax type feature "Colis_constraints.Feat.t"
+  syntax val absolute_or_concat_relative "Colis_constraints.Path.(normalize ~cwd:%1 (from_string %2))"
+  syntax val normalized_path_to_string "Colis_constraints.Path.normal_to_string %1"
+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 semantics.Env
   syntax type env "%1 Env.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.IdMap.t"
+end
+
+module semantics.Context
+  syntax val filter_var_env "Env.filter_var_env (fun v -> v.Semantics__Context.exported) (fun v -> v.Semantics__Context.value) %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"
+module interpreter.Interpreter
   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"
-  syntax val identifier_test "\"test\""
-  syntax val string_dash_d "\"-d\""
-  syntax val identifier_pwd "\"PWD\""
 end

src/concrete/env.ml

@@ -8,7 +8,10 @@ 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 []
 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 IdMap.t =
+  let open IdMap 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 _ x -> Option.is_some x) |>
+  map Option.get

src/concrete/env.mli

@@ -13,4 +13,4 @@ module IdMap : Map.S with type key = string
 (** Conversion to a normal map without default value *)
 val to_map : 'a env -> 'a IdMap.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 IdMap.t

src/concrete/interpreter.mlw

@@ -11,22 +11,23 @@ end
 
 module Semantics
   use list.List
-  use mystring.String
+  use string.String
+  use Filesystem
 
   (* Instantiate the concrete semantics with our dummy filesystem *)
   clone export semantics.Semantics with
-    type filesystem = unit,
-    type normalized_path = list string,
-    val default_cwd = Nil,
-    axiom interp_utility_extends_output
+    type filesystem = Filesystem.filesystem
+    (* axiom interp_utility_extends_output *)
 end
 
 module State
   use ref.Ref
   use list.List
-  use mystring.String
+  use string.String
   use Filesystem
+  use semantics.Paths
   use semantics.Buffers
+  use semantics.Context
   use import Semantics as S
 
   type sem_state = state
@@ -45,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
@@ -64,14 +65,17 @@ module Interpreter
   use ref.Refint
 
   use auxiliaries.OptionGet
-  use mystring.String
+  use string.String
   use syntax.Syntax
   use semantics.Result
   use semantics.Buffers
   use semantics.Behaviour
   use semantics.Input
   use semantics.Config
+  use semantics.Paths
+  use semantics.Context as C
   use semantics.Env as E
+  use semantics.InterpUtility
   use Filesystem as Fs
   use auxiliaries.TakeDrop
   use import Semantics as S
@@ -88,8 +92,8 @@ 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 C.empty_var_env;
+    St.func_env = C.empty_func_env;
     St.arguments = ref Nil;
     St.stdin = ref Stdin.empty;
     St.stdout = ref Stdout.empty;
@@ -98,12 +102,12 @@ module Interpreter
     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) : C.context = {
+    C.var_env = !(sta.var_env);
+    C.func_env = sta.func_env;
+    C.arguments = !(sta.arguments);
+    C.cwd = !(sta.cwd);
+    C.result = !(sta.result);
   }
 
   lemma context_same: forall sta1 sta2.
@@ -140,18 +144,24 @@ module Interpreter
   = if andb (strict inp.under_condition) (notb !(sta.result)) then
       raise EExit
 
-  (** {3 Imperative wrapper around the functional interpretation of utilties} *)
+  (** {3 Interpretation of utilities and imperative wrapper} *)
+
+  (** Interprete a command defined in the document *Specification of UNIX Commands*. *)
+  val function interp_utility (ctx: utility_context) (id: identifier) (sta: S.state) : (sta1: S.state, b: bool)
+    ensures { S.interp_utility (ctx, id, sta) (sta1, b) }
 
-  let interp_utility (inp:input) (sta:state) (id:identifier) (args:list string)
+  let interp_utility1 (inp:input) (sta:state) (id:identifier) (args:list string)
     returns { () ->
-      interp_utility (!(old sta.cwd), filter_var_env !(old sta.var_env), args) id (old sem_state sta) = (sem_state sta, !(sta.result)) /\
+      let utility_ctx = (!(old sta.cwd), C.filter_var_env !(old sta.var_env), args) in
+      S.interp_utility (utility_ctx, id, old sem_state sta) (sem_state sta, !(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, !(sta.result)) /\
+      let utility_ctx = (!(old sta.cwd), C.filter_var_env !(old sta.var_env), args) in
+      S.interp_utility (utility_ctx, id, old sem_state sta) (sem_state sta, !(sta.result)) /\
       behaviour inp !(sta.result) = BExit
     }
-  = let sta', b = interp_utility (!(sta.cwd), filter_var_env !(sta.var_env), args) id (sem_state sta) in
+  = let sta', b = interp_utility (!(sta.cwd), C.filter_var_env !(sta.var_env), args) id (sem_state sta) in
     sta.filesystem := sta'.S.filesystem;
     sta.stdin := sta'.S.stdin;
     sta.stdout := sta'.S.stdout;
@@ -161,7 +171,7 @@ module Interpreter
 
   use semantics.Arguments
 
-  let shift_arguments sta n
+  let shift_arguments sta (n: int)
     requires { n >= 0 }
     ensures {
       !(sta.result) = True ->
@@ -175,7 +185,7 @@ module Interpreter
   = try
       let args = ref !(sta.arguments) in
       for i = 1 to n do
-        invariant { length !(sta.arguments) >= i-1  }
+        invariant { Length.length !(sta.arguments) >= i-1  }
         invariant { shift_arguments (i-1) !(sta.arguments) = Some !args }
         match !args with
         | Cons _ args' ->
@@ -193,7 +203,7 @@ module Interpreter
 
   (** {3 The interpretation of statements} *)
 
-  let ghost ref stk = 0
+  let ghost ref stk : int = 0
 
   let rec interp_instruction (inp:input) (sta:state) (ins:instruction) : unit
     diverges
@@ -243,7 +253,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 C.exported=True} in
       sta.var_env := old_env[id <- var_val];
       sta.result := True
 
@@ -326,7 +336,7 @@ module Interpreter
 
     | ICallUtility name le ->
       let args = interp_list_expr inp sta le in
-      interp_utility inp sta name args
+      interp_utility1 inp sta name args
 
     | ICallFunction id le ->
       let args = interp_list_expr inp sta le in
@@ -414,12 +424,12 @@ module Interpreter
     | ICd se ->
       (* TODO --realword should also use Unix.chdir *)
       let s, _b = interp_str_expr True inp sta se in
-      let cwd_p = absolute_or_concat_relative !(sta.cwd) s in
-      let pwd_s = normalized_path_to_string cwd_p in
-      let args = Cons string_dash_d (Cons pwd_s Nil) in
-      interp_utility {inp with under_condition=True} sta identifier_test args;
+      let cwd_p = Paths.absolute_or_concat_relative !(sta.cwd) s in
+      let pwd_s = Paths.normalized_path_to_string cwd_p in
+      let args = Cons "-d" (Cons pwd_s Nil) in
+      interp_utility1 {inp with under_condition=True} sta (identifier_of_string "test") args;
       if !(sta.result) then begin
-        sta.var_env := !(sta.var_env)[identifier_pwd <- pwd_s]';
+        sta.var_env := !(sta.var_env)[identifier_of_string "PWD" <- pwd_s]';
         sta.cwd := cwd_p
       end;
       maybe_exit inp sta
@@ -469,7 +479,7 @@ module Interpreter
       assert { eval_str_expr stk b (inp, sem_context sta, sem_state sta at L1) se1 (sem_state sta, Success (s1, b1)) };
       label L2 in let s2, b2 = interp_str_expr b1 inp sta se2 in
       assert { eval_str_expr stk b1 (inp, sem_context sta, sem_state sta at L2) se2 (sem_state sta, Success (s2, b2)) };
-      s1^s2, b2
+      String.concat s1 s2, b2
     end
 
   with interp_list_expr (inp:input) (sta:state) (le:list_expression) : list string