diff --git a/src/colis.ml b/src/colis.ml
index a4efd82a..3676bda0 100644
--- a/src/colis.ml
+++ b/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
diff --git a/src/colis.mli b/src/colis.mli
index b0f2107c..cb00d6f2 100644
--- a/src/colis.mli
+++ b/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. *)
diff --git a/src/concrete/driver.drv b/src/concrete/driver.drv
index 44084ff4..51d8e573 100644
--- a/src/concrete/driver.drv
+++ b/src/concrete/driver.drv
@@ -3,6 +3,7 @@ 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
@@ -10,9 +11,18 @@ module semantics.Buffers
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
\ No newline at end of file
diff --git a/src/concrete/env.ml b/src/concrete/env.ml
index fc537cef..7f0cabbf 100644
--- a/src/concrete/env.ml
+++ b/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)
diff --git a/src/concrete/env.mli b/src/concrete/env.mli
index 442a585e..99d169d6 100644
--- a/src/concrete/env.mli
+++ b/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
diff --git a/src/concrete/interpreter.mlw b/src/concrete/interpreter.mlw
index c839995d..3e6dcea7 100644
--- a/src/concrete/interpreter.mlw
+++ b/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
diff --git a/src/concrete/interpreter/why3session.xml b/src/concrete/interpreter/why3session.xml
index 2f91eae1..9c11ac70 100644
--- a/src/concrete/interpreter/why3session.xml
+++ b/src/concrete/interpreter/why3session.xml
@@ -14,24 +14,24 @@
-
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
@@ -41,566 +41,566 @@
-
+
-
+
-
+
-
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -608,7 +608,7 @@
-
+
@@ -619,99 +619,99 @@
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -722,61 +722,61 @@
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -787,7 +787,7 @@
-
+
@@ -797,46 +797,46 @@
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -846,40 +846,40 @@
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
diff --git a/src/concrete/interpreter/why3shapes.gz b/src/concrete/interpreter/why3shapes.gz
index 6182b91c..c959bad5 100644
Binary files a/src/concrete/interpreter/why3shapes.gz and b/src/concrete/interpreter/why3shapes.gz differ
diff --git a/src/concrete/semantics.mlw b/src/concrete/semantics.mlw
index d641a898..b3a03889 100644
--- a/src/concrete/semantics.mlw
+++ b/src/concrete/semantics.mlw
@@ -32,20 +32,6 @@ module Behaviour
| BIncomplete, BIncomplete -> True
| _ -> False
end
-
- (* let function behaviour (under_condition res:bool) : behaviour *)
- (* ensures { result = BNormal \/ result = BExit } *)
- (* returns { *)
- (* | BNormal -> *)
- (* under_condition = True \/ res = True *)
- (* | BExit -> *)
- (* under_condition = False /\ res = False *)
- (* | BReturn | BIncomplete -> *)
- (* false *)
- (* } *)
- (* = if andb (strict under_condition) (notb res) *)
- (* then BExit *)
- (* else BNormal *)
end
(** {2 Stdin and stdout buffers} *)
@@ -159,7 +145,6 @@ module Buffers
| Cons l ls -> concat_empty_left {line=l; lines=ls}
end
-
let rec lemma concat_empty_right (out:t)
variant { out.lines }
ensures {
@@ -252,9 +237,14 @@ end
module Env
+ use option.Option
use syntax.Identifier
use map.Map as M
+ (** A partial environment *)
+ type env0 'a = abstract { to_map0 : M.map identifier (option 'a) }
+
+ (** A total environment with default *)
type env 'a = abstract { to_map : M.map identifier 'a; default: 'a }
meta coercion function to_map
@@ -315,26 +305,34 @@ module Arguments
shift_arguments n args = None
end
-(** {2 Concrete semantics of the CoLiS language} *)
-module Semantics
+module Path
+
+ use list.List
+
+ (** abstract type for filenames (excluding "." and ".."), named
+ "feature" in the tree constraint vocabulary *)
+ type feature
+
+ type normalized_path
+
+ val constant default_cwd : normalized_path
+
+ (** For `cd`: append `s` to `p` if `s` is relative or just `s` as path if it is absolute *)
+ val function absolute_or_concat_relative (p:normalized_path) (s:string) : normalized_path
+
+ val function normalized_path_to_string (p:normalized_path) : string
+end
+
+(** {2 Concrete evaluation context} *)
+module Context
- use int.Int
use list.List
- use list.Append
use option.Option
- use bool.Bool
use string.String
use syntax.Syntax
-
- use auxiliaries.OptionGet
- use Result
- use Arguments
- use Behaviour
- use Buffers
- use Config
- use Input
- use import Env as E
+ use Path
+ use Env
(** {3 The concrete evaluation context}
@@ -366,16 +364,6 @@ module Semantics
let constant empty_func_env : func_env =
empty_env None
- type normalized_path = list string
-
- let constant default_cwd : normalized_path = Nil
-
- (** For `cd` *)
- (** Append `s` to `p` if `s` is relative or just `s` as path if it is absolute *)
- val function absolute_or_concat_relative (p:normalized_path) (s:string) : normalized_path
-
- val function normalized_path_to_string (p:normalized_path) : string
-
let constant identifier_test = identifier_of_string "test"
let constant identifier_pwd = identifier_of_string "PWD"
@@ -403,12 +391,47 @@ module Semantics
result = True;
}
- val function filter_var_env (env:var_env) : env string
+ val function filter_var_env (env:var_env) : env0 string
(** A specification is not required because the result is not used inside the language
but only in utilities which are not specified. *)
(* ensures { forall x s. *)
(* env[x] = {value=Some s; exported=True} <-> result[x] = s *)
(* } *)
+end (* Context *)
+
+module Semantics
+ use bool.Bool
+ use int.Int
+ use list.Append
+ use list.List
+ use option.Option
+
+ use auxiliaries.OptionGet
+ use syntax.Identifier
+ use syntax.Syntax
+
+ use Arguments
+ use Behaviour
+ use Buffers
+ use Config
+ use Context as Context
+ use Env
+ use Input
+ use Path
+ use Result
+
+ type utility_context = {
+ cwd: normalized_path;
+ env: env0 string;
+ args: list string
+ }
+
+ let function utility_context args ctx = {
+ cwd = ctx.Context.cwd;
+ env = Context.filter_var_env ctx.Context.var_env;
+ args = args
+ }
+ use Context
(** {3 Evaluation state}
@@ -427,14 +450,11 @@ module Semantics
log: stdout; (** Combines stdout with utility traces and error messages *)
}
- type utility_context = (normalized_path, env string, list string)
-
- (** Interprete a command defined in the document *Specification of UNIX Commands*. *)
- val function interp_utility utility_context identifier state : (state, result bool)
+ predicate interp_utility (utility_context, identifier, state) (state, result bool)
- axiom interp_utility_extends_output : forall ctx id sta sta' r.
- interp_utility ctx id {sta with stdout=Stdout.empty} = (sta', r) ->
- interp_utility ctx id sta = ({sta' with stdout=Stdout.concat sta.stdout sta'.stdout}, r)
+ axiom interp_utility_extends_output : forall ctx id sta sta1 b.
+ interp_utility (ctx, id, {sta with stdout=Stdout.empty}) (sta1, b) ->
+ interp_utility (ctx, id, sta) ({sta with stdout=Stdout.concat sta.stdout sta1.stdout}, b)
let function bool_of_return_code (c:return_code) (previous:bool) : bool =
match c with
@@ -462,10 +482,10 @@ module Semantics
(* Reexport mixfix operators. *)
let function ([]) (e:env 'a) (id:identifier) : 'a =
- E.(e[id])
+ Env.(e[id])
let function ([<-]) (e:env 'a) (id:identifier) (value:'a) : env 'a =
- E.(e[id <- value])
+ Env.(e[id <- value])
(** Define mixfix operators for variable environments that retain or ignore the
export_state flag in the environment variable. *)
@@ -522,15 +542,17 @@ module Semantics
| eval_cd_incomplete : forall stk inp ctx sta se sta1 s _b sta2.
eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (s, _b)) ->
(* `test -d (CWD/)s` *)
- let cwd_p = absolute_or_concat_relative ctx.cwd s in
- interp_utility (ctx.cwd, filter_var_env ctx.var_env, Cons "-d" (Cons (normalized_path_to_string cwd_p) Nil)) identifier_test sta1 = (sta2, Incomplete) ->
+ let cwd_p = absolute_or_concat_relative ctx.Context.cwd s in
+ let args = Cons "-d" (Cons (normalized_path_to_string cwd_p) Nil) in
+ interp_utility (utility_context args ctx, identifier_test, sta1) (sta2, Incomplete) ->
eval_instruction stk (inp, ctx, sta) (ICd se) (sta2, ctx, BIncomplete)
| eval_cd_no_dir : forall stk inp ctx sta se sta1 s _b sta2.
eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (s, _b)) ->
(* `test -d (CWD/)s` *)
- let cwd_p = absolute_or_concat_relative ctx.cwd s in
- interp_utility (ctx.cwd, filter_var_env ctx.var_env, Cons "-d" (Cons (normalized_path_to_string cwd_p) Nil)) identifier_test sta1 = (sta2, Ok False) ->
+ let cwd_p = absolute_or_concat_relative ctx.Context.cwd s in
+ let args = Cons "-d" (Cons (normalized_path_to_string cwd_p) Nil) in
+ interp_utility (utility_context args ctx, identifier_test, sta1) (sta2, Ok False) ->
let ctx1 = {ctx with result = False} in
let bhv = behaviour inp False in
eval_instruction stk (inp, ctx, sta) (ICd se) (sta2, ctx1, bhv)
@@ -538,9 +560,10 @@ module Semantics
| eval_cd : forall stk inp ctx sta se sta1 s _b sta2.
eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (s, _b)) ->
(* `test -d (CWD/)s` *)
- let cwd_p = absolute_or_concat_relative ctx.cwd s in
- interp_utility (ctx.cwd, filter_var_env ctx.var_env, Cons "-d" (Cons (normalized_path_to_string cwd_p) Nil)) identifier_test sta1 = (sta2, Ok True) ->
- let ctx1 = {ctx with result = True; var_env = ctx.var_env[identifier_pwd <- normalized_path_to_string cwd_p]'; cwd = cwd_p} in
+ let cwd_p = absolute_or_concat_relative ctx.Context.cwd s in
+ let args = Cons "-d" (Cons (normalized_path_to_string cwd_p) Nil) in
+ interp_utility (utility_context args ctx, identifier_test, sta1) (sta2, Ok True) ->
+ let ctx1 = {ctx with result = True; var_env = ctx.var_env[identifier_pwd <- normalized_path_to_string cwd_p]'; Context.cwd = cwd_p} in
let bhv = behaviour inp True in
eval_instruction stk (inp, ctx, sta) (ICd se) (sta2, ctx1, bhv)
@@ -631,12 +654,12 @@ module Semantics
| eval_call_utility_incomplete: forall stk inp ctx sta sta' sta'' id es ss.
eval_list_expr stk (inp, ctx, sta) es (sta', Ok ss) ->
- interp_utility (ctx.cwd, filter_var_env ctx.var_env, ss) id sta' = (sta'', Incomplete) ->
+ interp_utility (utility_context ss ctx, id, sta') (sta'', Incomplete) ->
eval_instruction stk (inp, ctx, sta) (ICallUtility id es) (sta'', ctx, BIncomplete)
| eval_call_utility: forall stk inp ctx sta sta' sta'' id es ss b.
eval_list_expr stk (inp, ctx, sta) es (sta', Ok ss) ->
- interp_utility (ctx.cwd, filter_var_env ctx.var_env, ss) id sta' = (sta'', Ok b) ->
+ interp_utility (utility_context ss ctx, id, sta') (sta'', Ok b) ->
let ctx' = {ctx with result=b} in
let bhv = behaviour inp b in
eval_instruction stk (inp, ctx, sta) (ICallUtility id es) (sta'', ctx', bhv)
diff --git a/src/concrete/semantics/why3session.xml b/src/concrete/semantics/why3session.xml
index 3504f4ca..a7f18a9a 100644
--- a/src/concrete/semantics/why3session.xml
+++ b/src/concrete/semantics/why3session.xml
@@ -169,13 +169,15 @@
-
+
-
+
-
+
+
+
@@ -186,7 +188,7 @@
-
+
@@ -195,15 +197,15 @@
-
+
-
+
-
+
@@ -213,10 +215,10 @@
-
+
-
+
diff --git a/src/concrete/semantics/why3shapes.gz b/src/concrete/semantics/why3shapes.gz
index 6ca41a73..ce752958 100644
Binary files a/src/concrete/semantics/why3shapes.gz and b/src/concrete/semantics/why3shapes.gz differ
diff --git a/src/concrete/utilities.ml b/src/concrete/utilities.ml
index 187652b2..411c92e8 100644
--- a/src/concrete/utilities.ml
+++ b/src/concrete/utilities.ml
@@ -8,9 +8,7 @@ open Semantics__Result
open Semantics__Buffers
open Interpreter__Semantics
-module IdMap = Env.IdMap
-
-type env = string IdMap.t
+type env = string Env.SMap.t
let incomplete ~utility msg = fun sta ->
let str = utility ^ ": " ^ msg in
@@ -42,7 +40,7 @@ let dpkg_compare_versions args =
let dpkg_validate_thing subcmd arg =
Sys.command ("dpkg " ^ subcmd ^ " " ^arg) = 0
-let interp_utility (_cwd, var_env, args) id sta =
+let interp_utility ({env; args; _}, id, sta) =
match id with
| "echo" ->
let stdout =
@@ -69,7 +67,7 @@ let interp_utility (_cwd, var_env, args) id sta =
let print_line sta line =
{sta with stdout=Stdout.(sta.stdout |> output line |> newline)}
in
- IdMap.bindings var_env |>
+ Env.SMap.bindings env |>
List.map format_line |>
List.fold_left print_line sta, Ok true
| _arg :: _ ->
diff --git a/src/symbolic/driver.drv b/src/symbolic/driver.drv
index 220d850d..819185c7 100644
--- a/src/symbolic/driver.drv
+++ b/src/symbolic/driver.drv
@@ -1,21 +1,3 @@
-module symbolicInterpreter.Constraints
- syntax type clause "Colis_constraints.Clause.sat_conj"
- syntax type variable "Colis_constraints.Var.t"
- syntax type feature "Colis_constraints.Feat.t"
- syntax type path "Colis_constraints.Path.t"
-end
-
-module symbolicInterpreter.Semantics
- syntax val filter_var_env "Env.filter_var_env (fun v -> v.SymbolicInterpreter__Semantics.exported) (fun v -> v.SymbolicInterpreter__Semantics.value) %1"
- syntax val interp_utility "assert false"
- syntax val absolute_or_concat_relative "Colis_constraints.(List.map Feat.to_string (Path.normalize ~cwd:(List.map Feat.from_string %1) (Path.from_string %2)))"
- syntax val normalized_path_to_string "Colis_constraints.(Path.normal_to_string (List.map Feat.from_string %1))"
-end
-
-module symbolicInterpreter.Interpreter
- syntax val sym_interp_utility "BatSet.to_list (SymbolicUtility.dispatch' %1 %2 %3)"
-end
-
module collection.Collection
syntax type t "%1 list"
syntax val mem "List.mem %1 %2"
diff --git a/src/symbolic/symbolicInterpreter.mlw b/src/symbolic/symbolicInterpreter.mlw
index 9c6f5082..50dbf00e 100644
--- a/src/symbolic/symbolicInterpreter.mlw
+++ b/src/symbolic/symbolicInterpreter.mlw
@@ -1,1324 +1,1278 @@
-module Constraints
-
- type variable
- (** abstract type for variables denoting nodes in the file system *)
-
- type feature
- (** abstract type for filenames (excluding "." and ".."), named
- "feature" in the tree constraint vocabulary *)
-
- type clause
- (** abstract type for tree constraints, [IMPORTANT] which are always satisfiable *)
-
- type path
-end
-
-module Filesystem
- use option.Option
- use Constraints
-
- (** A symbolic filesystem composed by a variable indicating root, constraints, and the
- current working directory `cwd` as feature path. root₀ may refer to the initial root
- variable. When provided it should not be pruned (“quantified over”) during symbolic
- execution of utilities. *)
- type filesystem = {
- root : variable;
- clause : clause;
- root0 : option variable;
- }
-end
-
-module Semantics
- use list.List
- use Filesystem
- use Constraints
-
- (* Instantiate the concrete semantics with the symbolic filesystem *)
- clone export semantics.Semantics with
- type filesystem = filesystem,
- axiom interp_utility_extends_output
-end
-
-
-module SymState
-
- use list.List
- use Semantics
-
- (** A symbolic state combines a concrete context and a program state as defined in the
- semantics with a filesystem using feature constraints. *)
- type sym_state 'a = {
- context: context;
- state: state;
- data: 'a (* Used to fiddle additional information through interp_instr': A stdin in pipe and the last result in the loops *)
- }
-
- let function with_data data =
- fun sta ->
- {sta with data = data}
-end
-
-(** The symbolic interpretation of a program results describes multiple possible results
- *)
-module Results
-
- use set.Fset as Fset
- use collection.Collection as Cn
- use list.ListRich as L
- use semantics.Input
- use semantics.Behaviour
- use Semantics
- use SymState
-
- (** The results of a symbolic execution is a quadruple of sets of symbolic states, where
- each components corresponds to a behaviour. *)
- type t 'a = {
- normal : Cn.t (sym_state 'a);
- exit : Cn.t (sym_state 'a);
- return_ : Cn.t (sym_state 'a);
- failure : Cn.t (sym_state 'a);
- }
-
- let constant empty = {
- normal = Cn.empty;
- exit = Cn.empty;
- return_ = Cn.empty;
- failure = Cn.empty;
- }
-
- predicate mem (sta:sym_state 'a) (bhv:behaviour) (rs:t 'a) =
- match bhv with
- | BNormal -> Cn.mem sta rs.normal
- | BExit -> Cn.mem sta rs.exit
- | BReturn -> Cn.mem sta rs.return_
- | BIncomplete -> Cn.mem sta rs.failure
- end
-
- let function map (f:sym_state 'a -> sym_state 'b) (res:t 'a) : t 'b
- ensures { forall sta bhv. mem sta bhv res -> mem (f sta) bhv result }
- ensures { forall sta' bhv. mem sta' bhv result -> exists sta. mem sta bhv res /\ sta' = f sta }
- = { normal = Cn.map f res.normal;
- exit = Cn.map f res.exit;
- return_ = Cn.map f res.return_;
- failure = Cn.map f res.failure; }
-
- let function union (res1 res2: t 'a) : t 'a
- ensures { forall sta bhv. mem sta bhv res1 -> mem sta bhv result }
- ensures { forall sta bhv. mem sta bhv res2 -> mem sta bhv result }
- ensures { forall sta bhv. mem sta bhv result -> mem sta bhv res1 \/ mem sta bhv res2 }
- = { normal = Cn.union res1.normal res2.normal;
- exit = Cn.union res1.exit res2.exit;
- return_ = Cn.union res1.return_ res2.return_;
- failure = Cn.union res1.failure res2.failure; }
-
- lemma union_1: forall sta: sym_state 'a, bhv res1 res2.
- mem sta bhv res1 -> mem sta bhv (union res1 res2)
-
- lemma union_2: forall sta: sym_state 'a, bhv res1 res2.
- mem sta bhv res2 -> mem sta bhv (union res1 res2)
-
- let rec flatten_list (l: L.list (t 'a)) : t 'a
- variant { l }
- ensures { forall res sta bhv. L.mem res l -> mem sta bhv res -> mem sta bhv result }
- ensures { forall sta bhv. mem sta bhv result -> exists res. L.mem res l /\ mem sta bhv res }
- = match l with
- | L.Nil -> empty
- | L.Cons rs l' ->
- union rs (flatten_list l')
- end
-
- let flatten (c: Cn.t (t 'a)) : t 'a
- ensures { forall res sta bhv. Cn.mem res c -> mem sta bhv res -> mem sta bhv result }
- ensures { forall sta bhv. mem sta bhv result -> exists res. Cn.mem res c /\ mem sta bhv res }
- = flatten_list (Cn.to_list c)
-
- let bind_collection (f: 'a -> t 'b) (c: Cn.t 'a) : t 'b
- ensures {
- forall x sta bhv.
- Cn.mem x c ->
- mem sta bhv (f x) ->
- mem sta bhv result
- }
- ensures {
- forall sta bhv.
- mem sta bhv result ->
- exists x.
- Cn.mem x c /\
- mem sta bhv (f x)
- }
- = flatten (Cn.map f c)
-
- let separate_normal (res:t 'a) : (normal: Cn.t (sym_state 'a), other: t 'a)
- ensures { normal = res.normal }
- ensures { other.normal = Cn.empty }
- ensures { other.exit = res.exit }
- ensures { other.return_ = res.return_ }
- ensures { other.failure = res.failure }
- ensures { forall s. Cn.mem s normal -> Cn.mem s res.normal }
- ensures { forall s bhv. mem s bhv other -> bhv <> BNormal /\ mem s bhv res }
- = res.normal, {res with normal = Cn.empty}
-
- let function separate_non_failure (res:t 'a) : (Cn.t (sym_state 'a), Cn.t (sym_state 'a))
- = Cn.(union res.normal (union res.exit res.return_)), res.failure
-
- let function all_states (res:t 'a) : Cn.t (sym_state 'a) =
- Cn.(union res.normal (union res.exit (union res.return_ res.failure)))
-
- let stas_as_failures (ctx:context) (stas:Cn.t state) : t unit
- ensures { result.normal = Cn.empty }
- ensures { result.exit = Cn.empty }
- ensures { result.return_ = Cn.empty }
- ensures { forall s. Cn.mem s result.failure -> Cn.mem s.state stas /\ s.context=ctx /\ s.data = () }
- ensures { forall s. Cn.mem s stas -> Cn.mem {state=s; context=ctx; data=()} result.failure }
- = let aux sta = {state=sta; context=ctx; data=()} in
- {empty with failure=Cn.map aux stas}
-
- let function single_behaviour bhv (stas: Cn.t (sym_state 'a)) : t 'a =
- match bhv with
- | BNormal -> {empty with normal=stas}
- | BExit -> {empty with exit=stas}
- | BReturn -> {empty with return_=stas}
- | BIncomplete -> {empty with failure=stas}
- end
-
- let function inject (inp: input) (stas: Cn.t (sym_state 'a)) : t 'a
- (* ensures { forall sta bhv. mem sta bhv result <-> Cn.mem sta stas /\ bhv = behaviour inp sta.context.result } *)
- (* ensures { stas = Cn.union result.normal result.exit by Cn.(stas == union result.normal result.exit) } *)
- (* ensures { forall s. Cn.mem s result.normal -> Cn.mem s stas /\ behaviour inp s.context.result = BNormal } *)
- (* ensures { forall s. Cn.mem s result.exit -> Cn.mem s stas /\ behaviour inp s.context.result = BExit } *)
- (* ensures { result.return_ = Cn.empty } *)
- (* ensures { result.failure = Cn.empty } *)
- = let exit, normal = Cn.partition (fun sta -> exit_not_normal inp sta.context.result) stas in
- (* assert { forall sta. Cn.mem sta exit -> exit_not_normal inp sta.context.result = True }; *)
- (* assert { forall sta. Cn.mem sta normal -> exit_not_normal inp sta.context.result = False }; *)
- {empty with normal=normal; exit=exit}
- (* ensures { forall sta bhv. mem sta bhv result -> Cn.mem sta normal \/ Cn.mem sta exit } *)
-
- lemma mem_inject: forall res: t 'a, sta bhv inp stas.
- res = inject inp stas ->
- (mem sta bhv res <-> Cn.mem sta stas /\ bhv = behaviour inp sta.context.result)
-
- lemma inject_union: forall res: t 'a, inp stas.
- res = inject inp stas ->
- stas = Cn.union res.normal res.exit by
- Cn.(stas == union res.normal res.exit)
-
- lemma inject_return_empty: forall res: t 'a, inp stas.
- res = inject inp stas -> res.return_ = Cn.empty
-
- lemma inject_failure_empty: forall res: t 'a, inp stas.
- res = inject inp stas -> res.failure = Cn.empty
-
- lemma inject_normal_union_exit: forall inp, stas: Cn.t (sym_state 'a).
- stas = Cn.union (inject inp stas).normal (inject inp stas).exit
- by Cn.(stas == union (inject inp stas).normal (inject inp stas).exit)
-
- lemma inject_under_condition_normal: forall res: t 'a, inp stas.
- res = inject inp stas ->
- inp.under_condition = True ->
- res.normal = stas
- by Cn.(res.normal == stas)
-
- lemma inject_under_condition_exit: forall inp, stas: Cn.t (sym_state 'a).
- inp.under_condition = True ->
- (inject inp stas).exit = Cn.empty
- by Cn.((inject inp stas).exit == Cn.empty)
-
- lemma inject_outside_condition_normal: forall inp, stas: Cn.t (sym_state 'a).
- inp.under_condition = False ->
- (inject inp stas).normal = Cn.filter (fun sta -> sta.context.result) stas
- by Cn.((inject inp stas).normal == filter (fun sta -> sta.context.result) stas)
-
- lemma inject_outside_condition_exit: forall inp, stas: Cn.t (sym_state 'a).
- inp.under_condition = False ->
- (inject inp stas).exit = Cn.filter (fun sta -> not sta.context.result) stas
- by Cn.((inject inp stas).exit == filter (fun sta -> not sta.context.result) stas)
-
- lemma inject_map: forall f: sym_state 'a -> sym_state 'b, res inp sta sta' bhv stas.
- res = inject inp (Cn.map f stas) ->
- sta' = f sta ->
- bhv = behaviour inp (f sta).context.result ->
- Cn.mem sta stas ->
- mem sta' bhv res
-
- lemma inject_map': forall f: sym_state 'a -> sym_state 'b, res inp sta' bhv stas.
- res = inject inp (Cn.map f stas) ->
- mem sta' bhv res ->
- bhv = behaviour inp sta'.context.result /\
- exists sta. Cn.mem sta stas /\ sta' = f sta
-
- lemma union_inject: forall res: t 'a, inp stas.
- res = inject inp stas ->
- stas = Cn.union res.normal res.exit
- by
- Cn.(stas == union res.normal res.exit)
-
- lemma mem_union_inject: forall sta: sym_state 'a, bhv inp stas rs.
- mem sta bhv (union (inject inp stas) rs) <->
- ((Cn.mem sta stas /\ bhv = behaviour inp sta.context.result) \/
- mem sta bhv rs)
-
- lemma mem_union: forall sta bhv, rs1 rs2:t 'a.
- mem sta bhv (union rs1 rs2) <->
- (mem sta bhv rs1 \/ mem sta bhv rs2)
-
- lemma mem_map: forall sta': sym_state 'b, bhv, rs, f: sym_state 'a -> sym_state 'b.
- mem sta' bhv (map f rs) <->
- exists sta. mem sta bhv rs /\ sta' = f sta
-
- lemma failure_union: forall rs1 rs2: t 'a.
- failure (union rs1 rs2) = Cn.union (failure rs1) (failure rs2)
-
- lemma mem_mk_results: forall sta: sym_state 'a, bhv normal exit return_ failure.
- mem sta bhv { normal=normal; exit=exit; return_=return_; failure=failure } <->
- match bhv with
- | BNormal -> Cn.mem sta normal
- | BExit -> Cn.mem sta exit
- | BReturn -> Cn.mem sta return_
- | BIncomplete -> Cn.mem sta failure
- end
-
- lemma mem_union_results: forall sta: sym_state 'a, bhv rs1 rs2.
- mem sta bhv (union rs1 rs2) <->
- (match bhv with
- | BNormal -> Cn.mem sta rs1.normal
- | BExit -> Cn.mem sta rs1.exit
- | BReturn -> Cn.mem sta rs1.return_
- | BIncomplete -> Cn.mem sta rs1.failure
- end \/
- match bhv with
- | BNormal -> Cn.mem sta rs2.normal
- | BExit -> Cn.mem sta rs2.exit
- | BReturn -> Cn.mem sta rs2.return_
- | BIncomplete -> Cn.mem sta rs2.failure
- end)
-end
-
module Interpreter
-
- use bool.Bool
- use option.Option
- use int.Int
- use list.List
- use list.ListRich as L
- use set.Fset
- use string.OCaml as String
- use syntax.Syntax
- use auxiliaries.OptionGet
- use collection.Collection as Cn
- use semantics.Result
- use semantics.Behaviour
- use semantics.Input
- use semantics.Config
- use semantics.Buffers
- use semantics.Arguments
- use semantics.Env
- use Constraints
- use import Semantics as S
- use import SymState as St
- use Results as Rs
-
- (* Implemented in OCaml *)
- val function sym_interp_utility (ctx:utility_context) (id:identifier) (sta:state) : Cn.t (state, result bool)
- ensures {
- forall res.
- interp_utility ctx id sta = res <->
- Cn.mem res result
- }
-
- let rec separate_results_list (sta_opts: list ('a, result 'b)) : (results: list ('a, 'b), failures: list 'a)
- variant { sta_opts }
- ensures {
- forall sta x.
- L.mem (sta, x) results <->
- L.mem (sta, Ok x) sta_opts
- }
- ensures {
- forall sta.
- L.mem sta failures <->
- L.mem (sta, Incomplete) sta_opts
- }
- = match sta_opts with
- | Nil -> Nil, Nil
- | Cons (sta, opt_x) sta_opts' ->
- let results, failures = separate_results_list sta_opts' in
- match opt_x with
- | Ok x -> Cons (sta, x) results, failures
- | Incomplete -> results, Cons sta failures
- end
- end
-
- let separate_results (sta_opts: Cn.t ('a, result 'b)) : (results: Cn.t ('a, 'b), failures: Cn.t 'a)
- ensures {
- forall sta x.
- Cn.mem (sta, x) results <->
- Cn.mem (sta, Ok x) sta_opts
- }
- ensures {
- forall sta.
- Cn.mem sta failures <->
- Cn.mem (sta, Incomplete) sta_opts
- }
- = let results, failures = separate_results_list (Cn.to_list sta_opts) in
- Cn.of_list results, Cn.of_list failures
-
- let rec function size_instr (ins:instruction) : int
- variant { ins }
- ensures { 0 < result }
- = 1 + match ins with
- | IReturn _ | IExit _ | IShift _ | IExport _ ->
- 0
- | INot ins | INoOutput ins | ISubshell ins ->
- size_instr ins
- | ICd se | IAssignment _ se ->
- size_string_expr se
- | ICallUtility _ le | ICallFunction _ le ->
- size_list_expr le
- | ISequence ins1 ins2 | IPipe ins1 ins2 | IWhile ins1 ins2 ->
- size_instr ins1 + size_instr ins2
- | IForeach _ le ins ->
- size_list_expr le + size_instr ins
- | IIf ins1 ins2 ins3 ->
- size_instr ins1 + size_instr ins2 + size_instr ins3
- end
- with function size_list_expr (le:list_expression): int
- variant { le }
- ensures { 0 < result }
- = 1 + match le with
- | Nil -> 0
- | Cons se_sp le' ->
- size_pair se_sp + size_list_expr le'
- end
- with function size_pair (se_sp: (string_expression, split)) : int
- variant { se_sp }
- ensures { 0 < result }
- = let se, _ = se_sp in
- size_string_expr se
- with function size_string_expr (se:string_expression): int
- variant { se }
- ensures { 0 < result }
- = 1 + match se with
- | SLiteral _
- | SVariable _
- | SArgument _ -> 0
- | SSubshell ins -> size_instr ins
- | SConcat se1 se2 -> size_string_expr se1 + size_string_expr se2
+ scope MakeSemantics
+ use bool.Bool
+ use int.Int
+ use list.List
+ use list.ListRich as L
+ use option.Option
+ use set.Fset
+ use string.String
+
+ use syntax.Identifier
+ use syntax.Syntax
+ use auxiliaries.OptionGet
+ use collection.Collection as Cn
+ use semantics.Arguments
+ use semantics.Behaviour
+ use semantics.Buffers
+ use semantics.Config
+ use semantics.Context
+ use semantics.Input
+ use semantics.Path
+ use semantics.Result
+
+ scope import Filesystem
+ type filesystem
end
- let rec lemma size_string_expr_list_expr (le:list_expression)
- ensures { forall se sp. size_string_expr se < size_list_expr (Cons (se, sp) le) }
- = match le with
- | Nil -> ()
- | Cons _ le' -> size_string_expr_list_expr le'
- end
+ clone export semantics.Semantics with
+ type filesystem = filesystem,
+ axiom interp_utility_extends_output
- let function flip_result sta
- ensures { result.state = sta.state }
- ensures { result.data = sta.data }
- ensures { result.context = {sta.context with result=notb sta.context.result} }
- = let result = notb sta.context.result in
- let context = {sta.context with result=result} in
- {sta with context=context}
-
- let function reset_output sta sta' =
- let sta'' = {sta'.state with stdout = sta.stdout} in
- {sta' with state = sta''}
-
- let function assignment_for_str_sta ctx var arg =
- let sta', (str, result) = arg in
- let ctx' = {
- ctx with
- var_env = ctx.var_env[var <- str]';
- result = result;
- }
- in
- {state = sta'; context = ctx'; data = ()}
-
- let rec interp_instr (stk:int) (inp:input) (ctx:context) (sta:state) (ins:instruction)
- : Rs.t unit
- requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
- requires { within_limit stk inp.config.stack_size }
- variant { get_finite inp.config.stack_size - stk, size_instr ins, -1 }
- ensures { (* Over-approximation *)
- forall sta' ctx' bhv.
- eval_instruction stk (inp, ctx, sta) ins (sta', ctx', bhv) ->
- Rs.mem {state=sta'; context=ctx'; data=()} bhv result
- }
- (* (\* Under-approximation (->) and over-approximation (<-) *\) *)
- (* ensures { *)
- (* forall bhv sta'. *)
- (* Rs.mem sta' bhv result <-> *)
- (* eval_instruction stk (inp, ctx, sta) ins *)
- (* (sta'.state, sta'.context, bhv) *)
- (* } *)
- = match ins with
-
- | INot ins1 ->
- let res = interp_instr stk {inp with under_condition=True} ctx sta ins1 in
- Rs.({
- normal = Cn.map flip_result res.normal;
- return_ = Cn.map flip_result res.return_;
- exit = res.exit;
- failure = res.failure;
- })
- ensures {
- forall sta' ctx' bhv.
- eval_instruction stk ({inp with under_condition=True}, ctx, sta) ins1 (sta', ctx', bhv) ->
- match bhv with
- | BNormal | BReturn -> Rs.mem {state=sta'; context={ctx' with result=notb ctx'.result}; data=()} bhv result
- | BExit | BIncomplete -> Rs.mem {state=sta'; context=ctx'; data=()} bhv result
- end
- }
+ scope MakeInterpreter
- | IAssignment var se ->
- let str_stas, str_stas_failure =
- separate_results
- (interp_str_expr stk True inp ctx sta se)
- in
- let str_stas_failure = Rs.stas_as_failures ctx str_stas_failure in
- let res =
- Rs.inject inp
- (Cn.map (fun arg -> assignment_for_str_sta ctx var arg) str_stas)
- in
- Rs.(union res str_stas_failure)
- ensures {
- forall sta'.
- eval_str_expr stk True (inp, ctx, sta) se (sta', Incomplete) ->
- Cn.mem {state=sta'; context=ctx; data=()} result.Rs.failure
- }
+ scope import Arg
+ (* TODO Remove `function` from this and the below reformulation, use predicate in specifications below *)
+ val function sym_interp_utility (params: (utility_context, identifier, state)) : Cn.t (state, result bool)
+ ensures { forall res. interp_utility params res <-> Cn.mem res result }
+ end
- | IExport id ->
- let sta' =
- let ctx' =
- let var_val = {ctx.var_env[id] with exported=True} in
- let var_env' = ctx.var_env[id <- var_val] in
- {ctx with var_env = var_env'; result = True}
- in
- {state = sta; context = ctx'; data=()}
- in
- Rs.({empty with normal = Cn.singleton sta'})
-
- | ISequence ins1 ins2 ->
- let res1_normal, res1_other =
- Rs.separate_normal
- (interp_instr stk inp ctx sta ins1)
- in
- let res2 = interp_instr' stk inp res1_normal ins2 in
- Rs.union res2 res1_other
-
- | ISubshell ins ->
- let stas, stas_failure =
- Rs.separate_non_failure
- (interp_instr stk inp ctx sta ins)
- in
- assert {
- forall sta' ctx' bhv.
- bhv <> BIncomplete ->
- eval_instruction stk (inp, ctx, sta) ins (sta', ctx', bhv) ->
- Cn.mem {state=sta'; context=ctx'; data=()} stas
- };
- let stas' =
- let aux sta =
- let ctx' = {ctx with result = sta.context.result} in
- {state=sta.state; context=ctx'; data=()}
- in
- Cn.map aux stas
- in
- let old_ctx_with_res sta = {sta with context={ctx with result=sta.context.result}} in
- Rs.(union
- (inject inp stas')
- {empty with failure=Cn.map old_ctx_with_res stas_failure})
- ensures {
- forall sta' ctx'.
- eval_instruction stk (inp, ctx, sta) ins (sta', ctx', BIncomplete) ->
- Rs.mem {state=sta'; context={ctx with result=ctx'.result}; data=()} BIncomplete result
+ (** A symbolic state combines a concrete context and a program state as defined in the
+ semantics with a filesystem using feature constraints. *)
+ type sym_state 'a = {
+ context: context;
+ state: state;
+ data: 'a (* Used to fiddle additional information through interp_instr': A stdin in pipe and the last result in the loops *)
}
- | INoOutput ins ->
- Rs.map (reset_output sta)
- (interp_instr stk inp ctx sta ins)
-
- | IIf ins1 ins2 ins3 ->
- let res1_normal, res1_other =
- Rs.separate_normal
- (interp_instr stk {inp with under_condition=True} ctx sta ins1)
- in
- let res2 =
- let res1_true, res1_false =
- Cn.partition
- (fun sta -> sta.context.result)
- res1_normal
- in
- Rs.union
- (interp_instr' stk inp res1_true ins2)
- (interp_instr' stk inp res1_false ins3)
- in
- Rs.union res2 res1_other
-
- | ICd se ->
- let res1, res1_failures =
- separate_results
- (interp_str_expr stk True inp ctx sta se) in
- let function aux arg =
- let sta1, (s, (_:bool)) = arg in
- let cwd_p = absolute_or_concat_relative ctx.cwd s in
- let pwd_s = normalized_path_to_string cwd_p in
- let args = Cons "-d" (Cons pwd_s Nil) in
- Cn.map (fun arg -> let sta2, r = arg in ((sta2, cwd_p, pwd_s), r))
- (sym_interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) identifier_test sta1) in
- let res2a = Cn.bind aux res1 in
- let res2, res2_failures = separate_results res2a in
- let function aux' arg =
- let (sta2, cwd_p, pwd_s), b = arg in
- if b then
- let ctx' = {
- ctx with
- var_env = ctx.var_env[identifier_pwd <- pwd_s]';
- cwd = cwd_p;
- result = True } in
- {state = sta2; context = ctx'; data = ()}
- else
- let ctx' = {ctx with result = False} in
- {state = sta2; context = ctx'; data = ()} in
- let res2' = Cn.map aux' res2 in
- let res3 = Rs.inject inp res2' in
- let res2_failures' = Cn.map (fun arg -> let sta, _, _ = arg in sta) res2_failures in
- let res_failures = Rs.stas_as_failures ctx (Cn.union res1_failures res2_failures') in
- Rs.union res3 res_failures
- ensures { [@expl:cd_arg_failure]
- forall sta1.
- eval_str_expr stk True (inp, ctx, sta) se (sta1, Incomplete) ->
- Rs.mem {state=sta1; context=ctx; data=()} BIncomplete result
- }
- ensures { [@expl:cd_incomplete]
- forall sta1 s b sta2.
- eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (s, b)) ->
- let cwd_p = absolute_or_concat_relative ctx.cwd s in
- let pwd_s = normalized_path_to_string cwd_p in
- let args = Cons "-d" (Cons pwd_s Nil) in
- (sta2, Incomplete) = interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) identifier_test sta1 ->
- Rs.mem {state=sta2; context=ctx; data=()} BIncomplete result
- by Cn.mem (sta1, (s, b)) res1
- so Cn.mem (sta2, Incomplete) (sym_interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) identifier_test sta1)
- so Cn.mem (sta2, cwd_p, pwd_s) res2_failures
- }
- ensures { [@expl:cd_no_dir]
- forall sta1 s b sta2.
- eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (s, b)) ->
- let cwd_p = absolute_or_concat_relative ctx.cwd s in
- let pwd_s = normalized_path_to_string cwd_p in
- let args = Cons "-d" (Cons pwd_s Nil) in
- (sta2, Ok False) = interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) identifier_test sta1 ->
- let ctx' = {ctx with result = False} in
- let bhv = behaviour inp False in
- Rs.mem {state=sta2; context=ctx'; data=()} bhv result
- by Cn.mem (sta1, (s, b)) res1
- so Cn.mem (sta2, Ok False) (sym_interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) identifier_test sta1)
- so Cn.mem ((sta2, cwd_p, pwd_s), False) res2
- so Cn.mem {state=sta2; context=ctx'; data=()} res2'
- }
- ensures { [@expl:cd]
- forall sta1 s b sta2.
- eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (s, b)) ->
- let cwd_p = absolute_or_concat_relative ctx.cwd s in
- let pwd_s = normalized_path_to_string cwd_p in
- let args = Cons "-d" (Cons pwd_s Nil) in
- (sta2, Ok True) = interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) identifier_test sta1 ->
- let ctx1 = {ctx with result = True; var_env = ctx.var_env[identifier_pwd <- pwd_s]'; cwd = cwd_p} in
- let bhv = behaviour inp True in
- Rs.mem {state=sta2; context=ctx1; data=()} bhv result
- by Cn.mem (sta1, (s, b)) res1
- so Cn.mem (sta2, Ok True) (sym_interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) identifier_test sta1)
- so Cn.mem ((sta2, cwd_p, pwd_s), True) res2
- so Cn.mem {state=sta2; context=ctx1; data=()} res2'
- }
+ let function with_data data =
+ fun sta ->
+ {sta with data = data}
+
+ (** The symbolic interpretation of a program results describes multiple possible results
+ *)
+ scope Results
+
+ (** The results of a symbolic execution is a quadruple of sets of symbolic states, where
+ each components corresponds to a behaviour. *)
+ type t 'a = {
+ normal : Cn.t (sym_state 'a);
+ exit : Cn.t (sym_state 'a);
+ return_ : Cn.t (sym_state 'a);
+ failure : Cn.t (sym_state 'a);
+ }
- | ICallUtility id le ->
- let res, res_failures =
- separate_results
- (interp_list_expr stk inp ctx sta le) in
- let function aux arg =
- let sta', args = arg in
- sym_interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) id sta' in
- let res', res_failures' =
- separate_results (Cn.bind aux res) in
- let function aux' arg =
- let sta'', b = arg in
- {state=sta''; context={ctx with result=b}; data=()} in
- let res'' = Cn.map aux' res' in
- let res''' = Rs.inject inp res'' in
- let res_failures' = Rs.stas_as_failures ctx (Cn.union res_failures res_failures') in
- Rs.union res''' res_failures'
- ensures { [@expl:args_incomplete]
- forall sta'.
- eval_list_expr stk (inp, ctx, sta) le (sta', Incomplete) ->
- Rs.mem {state=sta'; context=ctx; data=()} BIncomplete result
- }
- ensures { [@expl:utility_incomplete]
- forall sta' ss sta''.
- eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
- (sta'', Incomplete) = interp_utility (ctx.cwd, filter_var_env ctx.var_env, ss) id sta' ->
- Rs.mem {state=sta''; context=ctx; data=()} BIncomplete result
- by Rs.mem {state=sta''; context=ctx; data=()} BIncomplete res_failures'
- }
- ensures { [@expl:utility]
- forall sta' ss sta'' b.
- eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
- (sta'', Ok b) = interp_utility (ctx.cwd, filter_var_env ctx.var_env, ss) id sta' ->
- let ctx' = {ctx with result=b} in
- Rs.mem {state=sta''; context=ctx'; data=()} (behaviour inp b) result
- by Cn.mem {state=sta''; context=ctx'; data=()} res''
- }
+ let constant empty = {
+ normal = Cn.empty;
+ exit = Cn.empty;
+ return_ = Cn.empty;
+ failure = Cn.empty;
+ }
- | ICallFunction id le ->
- let arg_res, arg_res_failures =
- separate_results
- (interp_list_expr stk inp ctx sta le)
- in
- assert { [@expl:callfun1]
- forall sta1 args.
- eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
- Cn.mem (sta1, args) arg_res
- };
- let res =
- match ctx.func_env[id] with
- | Some ins -> (* Function defined as `ins` *)
- if stk = get_finite inp.config.stack_size then (* Stack overflow *)
- let aux arg =
- let sta', _ = arg in
- let sta' = { sta' with log = Stdout.(newline (output stack_limit_message sta'.log)) } in
- {state=sta'; context=ctx; data=()}
- in
- Rs.({empty with failure = Cn.map aux arg_res})
- ensures { [@expl:callfun2]
- forall sta1 args ins.
- eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
- ctx.func_env[id] = Some ins ->
- inp.config.stack_size = Finite stk ->
- let sta1' = { sta1 with log = Stdout.(newline (output stack_limit_message sta1.log)) } in
- Rs.mem {state=sta1'; context=ctx; data=()} BIncomplete result
- }
- else (* Execute function *)
- let res2 =
- let function aux (arg: (state, list string)) =
- let sta1, args = arg in
- let inp1 = { inp with argument0 = identifier_to_string id } in
- let ctx1 = { ctx with arguments = args } in
- interp_instr (stk+1) inp1 ctx1 sta1 ins
- in
- Rs.bind_collection aux arg_res
- ensures { [@expl:callfun3]
- forall sta1 args ins sta2 ctx2 bhv2.
- eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
- ctx.func_env[id] = Some ins ->
- inp.config.stack_size <> Finite stk ->
- let inp1 = { inp with argument0 = identifier_to_string id } in
- let ctx1 = { ctx with arguments = args } in
- eval_instruction (stk+1) (inp1, ctx1, sta1) ins (sta2, ctx2, bhv2) ->
- Rs.mem {state=sta2; context=ctx2; data=()} bhv2 result
- }
- in
- let res2' =
- let function aux (sta2: sym_state unit) =
- {state=sta2.state; context={sta2.context with arguments = ctx.arguments}; data=()}
- in
- Rs.map aux res2
- ensures { [@expl:callfun4]
- forall sta1 args ins sta2 ctx2 bhv2.
- eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
- ctx.func_env[id] = Some ins ->
- inp.config.stack_size <> Finite stk ->
- let inp1 = { inp with argument0 = identifier_to_string id } in
- let ctx1 = { ctx with arguments = args } in
- eval_instruction (stk+1) (inp1, ctx1, sta1) ins (sta2, ctx2, bhv2) ->
- Rs.mem {state=sta2; context={ctx2 with arguments = ctx.arguments}; data=()} bhv2 result
- }
- in
- Rs.({res2' with normal=Cn.union res2'.normal res2'.return_; return_=Cn.empty})
- ensures { [@expl:callfun5]
- forall sta1 args ins sta2 ctx2 bhv2.
- eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
- ctx.func_env[id] = Some ins ->
- inp.config.stack_size <> Finite stk ->
- let inp1 = {inp with argument0=identifier_to_string id} in
- let ctx1 = {ctx with arguments=args} in
- eval_instruction (stk+1) (inp1, ctx1, sta1) ins (sta2, ctx2, bhv2) ->
- let bhv' = match bhv2 with BNormal | BReturn -> BNormal | BExit -> BExit | BIncomplete -> BIncomplete end in
- let ctx' = { ctx2 with arguments = ctx.arguments } in
- Rs.mem {state=sta2; context=ctx'; data=()} bhv' result
- }
- | None -> (* Undefined function *)
- let arg_res' =
- let function aux (arg: (state, list string)) =
- let sta', _ = arg in
- {state=sta'; context={ctx with result=False}; data=()}
- in
- Cn.map aux arg_res
- ensures {
- forall sta' ss.
- eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
- ctx.func_env[id] = None ->
- Cn.mem {state=sta'; context={ctx with result=False}; data=()} result
- by Cn.mem (sta', ss) arg_res
- }
- in
- Rs.single_behaviour (behaviour inp False) arg_res'
- ensures {
- forall sta' ss.
- eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
- ctx.func_env[id] = None ->
- Rs.mem {state=sta'; context={ctx with result=False}; data=()} (behaviour inp False) result
- }
- end
- in
- let res_failures = Rs.stas_as_failures ctx arg_res_failures in
- Rs.union res res_failures
-
- | IShift bn ->
- match shift_arguments (option_get (mk_nat 1) bn).nat ctx.arguments with
- | Some args ->
- let ctx' = {ctx with result = True; arguments = args} in
- let sta' = {state = sta; context = ctx'; data=()} in
- Rs.({empty with normal = Cn.singleton sta'})
- | None ->
- let ctx' = {ctx with result = False} in
- let sta' = {state = sta; context = ctx'; data=()} in
- Rs.inject inp (Cn.singleton sta')
+ predicate mem (sta:sym_state 'a) (bhv:behaviour) (rs:t 'a) =
+ match bhv with
+ | BNormal -> Cn.mem sta rs.normal
+ | BExit -> Cn.mem sta rs.exit
+ | BReturn -> Cn.mem sta rs.return_
+ | BIncomplete -> Cn.mem sta rs.failure
+ end
+
+ let function map (f:sym_state 'a -> sym_state 'b) (res:t 'a) : t 'b
+ ensures { forall sta bhv. mem sta bhv res -> mem (f sta) bhv result }
+ ensures { forall sta' bhv. mem sta' bhv result -> exists sta. mem sta bhv res /\ sta' = f sta }
+ = { normal = Cn.map f res.normal;
+ exit = Cn.map f res.exit;
+ return_ = Cn.map f res.return_;
+ failure = Cn.map f res.failure; }
+
+ let function union (res1 res2: t 'a) : t 'a
+ ensures { forall sta bhv. mem sta bhv res1 -> mem sta bhv result }
+ ensures { forall sta bhv. mem sta bhv res2 -> mem sta bhv result }
+ ensures { forall sta bhv. mem sta bhv result -> mem sta bhv res1 \/ mem sta bhv res2 }
+ = { normal = Cn.union res1.normal res2.normal;
+ exit = Cn.union res1.exit res2.exit;
+ return_ = Cn.union res1.return_ res2.return_;
+ failure = Cn.union res1.failure res2.failure; }
+
+ lemma union_1: forall sta: sym_state 'a, bhv res1 res2.
+ mem sta bhv res1 -> mem sta bhv (union res1 res2)
+
+ lemma union_2: forall sta: sym_state 'a, bhv res1 res2.
+ mem sta bhv res2 -> mem sta bhv (union res1 res2)
+
+ let rec flatten_list (l: L.list (t 'a)) : t 'a
+ variant { l }
+ ensures { forall res sta bhv. L.mem res l -> mem sta bhv res -> mem sta bhv result }
+ ensures { forall sta bhv. mem sta bhv result -> exists res. L.mem res l /\ mem sta bhv res }
+ = match l with
+ | L.Nil -> empty
+ | L.Cons rs l' ->
+ union rs (flatten_list l')
+ end
+
+ let flatten (c: Cn.t (t 'a)) : t 'a
+ ensures { forall res sta bhv. Cn.mem res c -> mem sta bhv res -> mem sta bhv result }
+ ensures { forall sta bhv. mem sta bhv result -> exists res. Cn.mem res c /\ mem sta bhv res }
+ = flatten_list (Cn.to_list c)
+
+ let bind_collection (f: 'a -> t 'b) (c: Cn.t 'a) : t 'b
+ ensures {
+ forall x sta bhv.
+ Cn.mem x c ->
+ mem sta bhv (f x) ->
+ mem sta bhv result
+ }
+ ensures {
+ forall sta bhv.
+ mem sta bhv result ->
+ exists x.
+ Cn.mem x c /\
+ mem sta bhv (f x)
+ }
+ = flatten (Cn.map f c)
+
+ let separate_normal (res:t 'a) : (normal: Cn.t (sym_state 'a), other: t 'a)
+ ensures { normal = res.normal }
+ ensures { other.normal = Cn.empty }
+ ensures { other.exit = res.exit }
+ ensures { other.return_ = res.return_ }
+ ensures { other.failure = res.failure }
+ ensures { forall s. Cn.mem s normal -> Cn.mem s res.normal }
+ ensures { forall s bhv. mem s bhv other -> bhv <> BNormal /\ mem s bhv res }
+ = res.normal, {res with normal = Cn.empty}
+
+ let function separate_non_failure (res:t 'a) : (Cn.t (sym_state 'a), Cn.t (sym_state 'a))
+ = Cn.(union res.normal (union res.exit res.return_)), res.failure
+
+ let function all_states (res:t 'a) : Cn.t (sym_state 'a) =
+ Cn.(union res.normal (union res.exit (union res.return_ res.failure)))
+
+ let stas_as_failures (ctx:context) (stas:Cn.t state) : t unit
+ ensures { result.normal = Cn.empty }
+ ensures { result.exit = Cn.empty }
+ ensures { result.return_ = Cn.empty }
+ ensures { forall s. Cn.mem s result.failure -> Cn.mem s.state stas /\ s.context=ctx /\ s.data = () }
+ ensures { forall s. Cn.mem s stas -> Cn.mem {state=s; context=ctx; data=()} result.failure }
+ = let aux sta = {state=sta; context=ctx; data=()} in
+ {empty with failure=Cn.map aux stas}
+
+ let function single_behaviour bhv (stas: Cn.t (sym_state 'a)) : t 'a =
+ match bhv with
+ | BNormal -> {empty with normal=stas}
+ | BExit -> {empty with exit=stas}
+ | BReturn -> {empty with return_=stas}
+ | BIncomplete -> {empty with failure=stas}
+ end
+
+ let function inject (inp: input) (stas: Cn.t (sym_state 'a)) : t 'a
+ (* ensures { forall sta bhv. mem sta bhv result <-> Cn.mem sta stas /\ bhv = behaviour inp sta.context.result } *)
+ (* ensures { stas = Cn.union result.normal result.exit by Cn.(stas == union result.normal result.exit) } *)
+ (* ensures { forall s. Cn.mem s result.normal -> Cn.mem s stas /\ behaviour inp s.context.result = BNormal } *)
+ (* ensures { forall s. Cn.mem s result.exit -> Cn.mem s stas /\ behaviour inp s.context.result = BExit } *)
+ (* ensures { result.return_ = Cn.empty } *)
+ (* ensures { result.failure = Cn.empty } *)
+ = let exit, normal = Cn.partition (fun sta -> exit_not_normal inp sta.context.result) stas in
+ (* assert { forall sta. Cn.mem sta exit -> exit_not_normal inp sta.context.result = True }; *)
+ (* assert { forall sta. Cn.mem sta normal -> exit_not_normal inp sta.context.result = False }; *)
+ {empty with normal=normal; exit=exit}
+ (* ensures { forall sta bhv. mem sta bhv result -> Cn.mem sta normal \/ Cn.mem sta exit } *)
+
+ lemma mem_inject: forall res: t 'a, sta bhv inp stas.
+ res = inject inp stas ->
+ (mem sta bhv res <-> Cn.mem sta stas /\ bhv = behaviour inp sta.context.result)
+
+ lemma inject_union: forall res: t 'a, inp stas.
+ res = inject inp stas ->
+ stas = Cn.union res.normal res.exit by
+ Cn.(stas == union res.normal res.exit)
+
+ lemma inject_return_empty: forall res: t 'a, inp stas.
+ res = inject inp stas -> res.return_ = Cn.empty
+
+ lemma inject_failure_empty: forall res: t 'a, inp stas.
+ res = inject inp stas -> res.failure = Cn.empty
+
+ lemma inject_normal_union_exit: forall inp, stas: Cn.t (sym_state 'a).
+ stas = Cn.union (inject inp stas).normal (inject inp stas).exit
+ by Cn.(stas == union (inject inp stas).normal (inject inp stas).exit)
+
+ lemma inject_under_condition_normal: forall res: t 'a, inp stas.
+ res = inject inp stas ->
+ inp.under_condition = True ->
+ res.normal = stas
+ by Cn.(res.normal == stas)
+
+ lemma inject_under_condition_exit: forall inp, stas: Cn.t (sym_state 'a).
+ inp.under_condition = True ->
+ (inject inp stas).exit = Cn.empty
+ by Cn.((inject inp stas).exit == Cn.empty)
+
+ lemma inject_outside_condition_normal: forall inp, stas: Cn.t (sym_state 'a).
+ inp.under_condition = False ->
+ (inject inp stas).normal = Cn.filter (fun sta -> sta.context.result) stas
+ by Cn.((inject inp stas).normal == filter (fun sta -> sta.context.result) stas)
+
+ lemma inject_outside_condition_exit: forall inp, stas: Cn.t (sym_state 'a).
+ inp.under_condition = False ->
+ (inject inp stas).exit = Cn.filter (fun sta -> not sta.context.result) stas
+ by Cn.((inject inp stas).exit == filter (fun sta -> not sta.context.result) stas)
+
+ lemma inject_map: forall f: sym_state 'a -> sym_state 'b, res inp sta sta' bhv stas.
+ res = inject inp (Cn.map f stas) ->
+ sta' = f sta ->
+ bhv = behaviour inp (f sta).context.result ->
+ Cn.mem sta stas ->
+ mem sta' bhv res
+
+ lemma inject_map': forall f: sym_state 'a -> sym_state 'b, res inp sta' bhv stas.
+ res = inject inp (Cn.map f stas) ->
+ mem sta' bhv res ->
+ bhv = behaviour inp sta'.context.result /\
+ exists sta. Cn.mem sta stas /\ sta' = f sta
+
+ lemma union_inject: forall res: t 'a, inp stas.
+ res = inject inp stas ->
+ stas = Cn.union res.normal res.exit
+ by
+ Cn.(stas == union res.normal res.exit)
+
+ lemma mem_union_inject: forall sta: sym_state 'a, bhv inp stas rs.
+ mem sta bhv (union (inject inp stas) rs) <->
+ ((Cn.mem sta stas /\ bhv = behaviour inp sta.context.result) \/
+ mem sta bhv rs)
+
+ lemma mem_union: forall sta bhv, rs1 rs2:t 'a.
+ mem sta bhv (union rs1 rs2) <->
+ (mem sta bhv rs1 \/ mem sta bhv rs2)
+
+ lemma mem_map: forall sta': sym_state 'b, bhv, rs, f: sym_state 'a -> sym_state 'b.
+ mem sta' bhv (map f rs) <->
+ exists sta. mem sta bhv rs /\ sta' = f sta
+
+ lemma failure_union: forall rs1 rs2: t 'a.
+ failure (union rs1 rs2) = Cn.union (failure rs1) (failure rs2)
+
+ lemma mem_mk_results: forall sta: sym_state 'a, bhv normal exit return_ failure.
+ mem sta bhv { normal=normal; exit=exit; return_=return_; failure=failure } <->
+ match bhv with
+ | BNormal -> Cn.mem sta normal
+ | BExit -> Cn.mem sta exit
+ | BReturn -> Cn.mem sta return_
+ | BIncomplete -> Cn.mem sta failure
+ end
+
+ lemma mem_union_results: forall sta: sym_state 'a, bhv rs1 rs2.
+ mem sta bhv (union rs1 rs2) <->
+ (match bhv with
+ | BNormal -> Cn.mem sta rs1.normal
+ | BExit -> Cn.mem sta rs1.exit
+ | BReturn -> Cn.mem sta rs1.return_
+ | BIncomplete -> Cn.mem sta rs1.failure
+ end \/
+ match bhv with
+ | BNormal -> Cn.mem sta rs2.normal
+ | BExit -> Cn.mem sta rs2.exit
+ | BReturn -> Cn.mem sta rs2.return_
+ | BIncomplete -> Cn.mem sta rs2.failure
+ end)
end
- | IForeach id le ins ->
- let lst_res, lst_res_failures =
- separate_results
- (interp_list_expr stk inp ctx sta le)
- in
- assert {
- forall sta' ss.
- eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
- Cn.mem (sta', ss) lst_res
- };
- let res_loop_cont =
- (* Execute foreach loop on a result from interp_list_expr *)
- let function aux arg =
- let sta', ss = arg in
- interp_foreach True stk inp ctx sta' id ss ins
- in
- Rs.bind_collection aux lst_res
+ let rec separate_results_list (sta_opts: list ('a, result 'b)) : (results: list ('a, 'b), failures: list 'a)
+ variant { sta_opts }
ensures {
- forall sta' ss sta'' ctx' bhv b.
- eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
- eval_foreach stk True (inp, ctx, sta') id ss ins (sta'', ctx', bhv) b ->
- Rs.mem {state=sta''; context=ctx'; data=b} bhv result
+ forall sta x.
+ L.mem (sta, x) results <->
+ L.mem (sta, Ok x) sta_opts
}
- in
- let res_loop_cont' =
- let function aux sta'' =
- let ctx'' = {sta''.context with result=sta''.data} in
- with_data () {sta'' with context = ctx''}
- in
- Rs.map aux res_loop_cont
ensures {
- forall sta' ss sta'' ctx' bhv b.
- eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
- eval_foreach stk True (inp, ctx, sta') id ss ins (sta'', ctx', bhv) b ->
-
- Rs.mem {state=sta''; context={ctx' with result=b}; data=()} bhv result
+ forall sta.
+ L.mem sta failures <->
+ L.mem (sta, Incomplete) sta_opts
}
- in
- let res_failure =
- Rs.stas_as_failures ctx lst_res_failures
- ensures {
- forall sta'.
- eval_list_expr stk (inp, ctx, sta) le (sta', Incomplete) ->
- Rs.mem {state=sta'; context=ctx; data=()} BIncomplete result
- }
- in
- Rs.(union res_loop_cont' res_failure)
-
- | IWhile ins1 ins2 ->
- let res = interp_while True 0 stk inp ctx sta ins1 ins2 in
- let function aux_normal (sta': sym_state (int, bool)) =
- let _, b = sta'.data in
- {state=sta'.state; context={sta'.context with result=b}; data=()}
- in
- let function aux_other (sta': sym_state (int, bool)) =
- {sta' with data=()}
- in
- Rs.({normal=Cn.map aux_normal res.normal;
- exit=Cn.map aux_other res.exit;
- return_=Cn.map aux_other res.return_;
- failure=Cn.map aux_other res.failure})
- ensures {
- forall sta' ctx' bhv ctr b.
- bhv <> BNormal ->
- eval_while stk 0 True (inp, ctx, sta) ins1 ins2 (sta', ctx', bhv) ctr b ->
- Rs.mem {state=sta'; context=ctx'; data=()} bhv result
- }
- ensures {
- forall sta' ctx' ctr b.
- eval_while stk 0 True (inp, ctx, sta) ins1 ins2 (sta', ctx', BNormal) ctr b ->
- Rs.mem {state=sta'; context={ctx' with result=b}; data=()} BNormal result
- }
+ = match sta_opts with
+ | Nil -> Nil, Nil
+ | Cons (sta, opt_x) sta_opts' ->
+ let results, failures = separate_results_list sta_opts' in
+ match opt_x with
+ | Ok x -> Cons (sta, x) results, failures
+ | Incomplete -> results, Cons sta failures
+ end
+ end
- | IPipe ins1 ins2 ->
- let stas1, stas1_failure =
- Rs.separate_non_failure
- (interp_instr stk inp ctx {sta with stdout=Stdout.empty} ins1)
- in
- assert {
- forall sta1 ctx1 bhv1.
- eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, bhv1) ->
- bhv1 <> BIncomplete ->
- Cn.mem {state=sta1; context=ctx1; data=()} stas1
- };
- let stas1': Cn.t (sym_state stdin) = (* data is sta1.state.stdin *)
- let function aux (sta1: sym_state unit) =
- {state={sta1.state with stdout=sta.stdout; stdin=Stdout.to_stdin sta1.state.stdout}; context=ctx; data=sta1.state.stdin}
- in
- Cn.map aux stas1
- ensures {
- forall sta1 ctx1 bhv1.
- eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, bhv1) ->
- bhv1 <> BIncomplete ->
- Cn.mem
- {state={sta1 with stdout=sta.stdout; stdin=Stdout.to_stdin sta1.stdout}; context=ctx; data=sta1.stdin}
- result
- }
- in
- let res2: Rs.t stdin = (* data is sta1.state.stdin *)
- interp_instr' stk inp stas1' ins2
+ let separate_results (sta_opts: Cn.t ('a, result 'b)) : (results: Cn.t ('a, 'b), failures: Cn.t 'a)
ensures {
- forall sta1 ctx1 bhv1 sta2 ctx2 bhv2.
- eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, bhv1) ->
- bhv1 <> BIncomplete ->
- eval_instruction stk (inp, ctx, {sta1 with stdout=sta.stdout; stdin=Stdout.to_stdin sta1.stdout}) ins2 (sta2, ctx2, bhv2) ->
- Rs.mem {state=sta2; context=ctx2; data=sta1.stdin} bhv2 result
+ forall sta x.
+ Cn.mem (sta, x) results <->
+ Cn.mem (sta, Ok x) sta_opts
}
- in
- let res2' =
- let function aux sta2 =
- {state={sta2.state with stdin=sta2.data};
- context={ctx with result=sta2.context.result};
- data=()}
- in
- Rs.map aux res2
- ensures {
- forall sta1 ctx1 bhv1 sta2 ctx2 bhv2.
- eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, bhv1) ->
- bhv1 <> BIncomplete ->
- eval_instruction stk (inp, ctx, {sta1 with stdout=sta.stdout; stdin=Stdout.to_stdin sta1.stdout}) ins2 (sta2, ctx2, bhv2) ->
- Rs.mem {state={sta2 with stdin=sta1.stdin}; context={ctx with result=ctx2.result}; data=()} bhv2 result
- }
- in
- let sta1_failure' =
- let function aux (sta1: sym_state unit) =
- {state={sta1.state with stdout=sta.stdout}; context=ctx; data=()}
- in
- Cn.map aux stas1_failure
ensures {
- forall sta1 ctx1.
- eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, BIncomplete) ->
- Cn.mem {state={sta1 with stdout=sta.stdout}; context=ctx; data=()} result
+ forall sta.
+ Cn.mem sta failures <->
+ Cn.mem (sta, Incomplete) sta_opts
}
- in
- Rs.(union res2' {empty with failure=sta1_failure'})
-
- | IExit code ->
- let r =
- match code with
- | RPrevious -> ctx.result
- | RSuccess -> True
- | RFailure -> False
+ = let results, failures = separate_results_list (Cn.to_list sta_opts) in
+ Cn.of_list results, Cn.of_list failures
+
+ let rec function size_instr (ins:instruction) : int
+ variant { ins }
+ ensures { 0 < result }
+ = 1 + match ins with
+ | IReturn _ | IExit _ | IShift _ | IExport _ ->
+ 0
+ | INot ins | INoOutput ins | ISubshell ins ->
+ size_instr ins
+ | ICd se | IAssignment _ se ->
+ size_string_expr se
+ | ICallUtility _ le | ICallFunction _ le ->
+ size_list_expr le
+ | ISequence ins1 ins2 | IPipe ins1 ins2 | IWhile ins1 ins2 ->
+ size_instr ins1 + size_instr ins2
+ | IForeach _ le ins ->
+ size_list_expr le + size_instr ins
+ | IIf ins1 ins2 ins3 ->
+ size_instr ins1 + size_instr ins2 + size_instr ins3
end
- in
- let sta = {state=sta; context={ctx with result=r}; data=()} in
- Rs.({empty with exit = Cn.singleton sta})
-
- | IReturn code ->
- let r =
- match code with
- | RPrevious -> ctx.result
- | RSuccess -> True
- | RFailure -> False
+ with function size_list_expr (le:list_expression): int
+ variant { le }
+ ensures { 0 < result }
+ = 1 + match le with
+ | Nil -> 0
+ | Cons se_sp le' ->
+ size_pair se_sp + size_list_expr le'
+ end
+ with function size_pair (se_sp: (string_expression, split)) : int
+ variant { se_sp }
+ ensures { 0 < result }
+ = let se, _ = se_sp in
+ size_string_expr se
+ with function size_string_expr (se:string_expression): int
+ variant { se }
+ ensures { 0 < result }
+ = 1 + match se with
+ | SLiteral _
+ | SVariable _
+ | SArgument _ -> 0
+ | SSubshell ins -> size_instr ins
+ | SConcat se1 se2 -> size_string_expr se1 + size_string_expr se2
end
- in
- let sta =
- let ctx' = {ctx with result = r} in
- {state = sta; context = ctx'; data=()}
- in
- Rs.({empty with return_ = Cn.singleton sta})
- end
- with interp_foreach (b:bool) (stk:int) (inp:input) (ctx:context) (sta:state) (id:identifier) (ss:list string) (ins:instruction) : Rs.t bool
- variant { get_finite inp.config.stack_size - stk, size_instr ins, L.length ss }
- requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
- requires { stk <= get_finite inp.config.stack_size }
- ensures {
- forall sta' ctx' bhv b'.
- eval_foreach stk b (inp, ctx, sta) id ss ins (sta', ctx', bhv) b' ->
- Rs.mem {state=sta'; context=ctx'; data=b'} bhv result
- }
- = match ss with
- | Nil ->
- Rs.({empty with normal=Cn.singleton {state=sta; context=ctx; data=b}})
- | Cons s ss' ->
- let res1_normal, res1_other =
- Rs.separate_normal
- (interp_instr stk inp {ctx with var_env = ctx.var_env[id <- s]'} sta ins)
- in
- let res_normal' =
- let function aux (sta1: sym_state unit) =
- interp_foreach sta1.context.result stk inp sta1.context sta1.state id ss' ins
- in
- Rs.bind_collection aux res1_normal
- ensures {
- forall sta1 ctx1 sta2 ctx2 bhv2 b2.
- eval_instruction stk (inp, {ctx with var_env=ctx.var_env[id <- s]'}, sta) ins (sta1, ctx1, BNormal) ->
- eval_foreach stk ctx1.result (inp, ctx1, sta1) id ss' ins (sta2, ctx2, bhv2) b2 ->
- Rs.mem {state=sta2; context=ctx2; data=b2} bhv2 result
+ let rec lemma size_string_expr_list_expr (le:list_expression)
+ ensures { forall se sp. size_string_expr se < size_list_expr (Cons (se, sp) le) }
+ = match le with
+ | Nil -> ()
+ | Cons _ le' -> size_string_expr_list_expr le'
+ end
+
+ let function flip_result sta
+ ensures { result.state = sta.state }
+ ensures { result.data = sta.data }
+ ensures { result.context = {sta.context with result=notb sta.context.result} }
+ = let result = notb sta.context.result in
+ let context = {sta.context with result=result} in
+ {sta with context=context}
+
+ let function reset_output sta sta' =
+ let sta'' = {sta'.state with stdout = sta.stdout} in
+ {sta' with state = sta''}
+
+ let function assignment_for_str_sta ctx var arg =
+ let sta', (str, result) = arg in
+ let ctx' = {
+ ctx with
+ var_env = ctx.var_env[var <- str]';
+ result = result;
}
- in
- let res1_other' =
- let function aux (sta: sym_state unit) =
- with_data sta.context.result sta
in
- Rs.map aux res1_other
- ensures {
- forall sta1 ctx1 bhv1.
- eval_instruction stk (inp, {ctx with var_env=ctx.var_env[id <- s]'}, sta) ins (sta1, ctx1, bhv1) ->
- bhv1 <> BNormal ->
- Rs.mem {state=sta1; context=ctx1; data=ctx1.result} bhv1 result
+ {state = sta'; context = ctx'; data = ()}
+
+ let rec interp_instr (stk:int) (inp:input) (ctx:context) (sta:state) (ins:instruction)
+ : Results.t unit
+ requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
+ requires { within_limit stk inp.config.stack_size }
+ variant { get_finite inp.config.stack_size - stk, size_instr ins, -1 }
+ ensures { (* Over-approximation *)
+ forall sta' ctx' bhv.
+ eval_instruction stk (inp, ctx, sta) ins (sta', ctx', bhv) ->
+ Results.mem {state=sta'; context=ctx'; data=()} bhv result
}
- in
- Rs.union res_normal' res1_other'
- end
+ (* (\* Under-approximation (->) and over-approximation (<-) *\) *)
+ (* ensures { *)
+ (* forall bhv sta'. *)
+ (* Results.mem sta' bhv result <-> *)
+ (* eval_instruction stk (inp, ctx, sta) ins *)
+ (* (sta'.state, sta'.context, bhv) *)
+ (* } *)
+ = match ins with
+
+ | INot ins1 ->
+ let res = interp_instr stk {inp with under_condition=True} ctx sta ins1 in
+ Results.({
+ normal = Cn.map flip_result res.normal;
+ return_ = Cn.map flip_result res.return_;
+ exit = res.exit;
+ failure = res.failure;
+ })
+ ensures {
+ forall sta' ctx' bhv.
+ eval_instruction stk ({inp with under_condition=True}, ctx, sta) ins1 (sta', ctx', bhv) ->
+ match bhv with
+ | BNormal | BReturn -> Results.mem {state=sta'; context={ctx' with result=notb ctx'.result}; data=()} bhv result
+ | BExit | BIncomplete -> Results.mem {state=sta'; context=ctx'; data=()} bhv result
+ end
+ }
- with interp_while b ctr stk inp ctx (sta:state) ins1 ins2 : Rs.t (int, bool)
- variant { get_finite inp.config.stack_size - stk, size_instr ins1+size_instr ins2, get_finite inp.config.loop_limit - ctr }
- requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
- requires { 0 <= ctr <= get_finite inp.config.loop_limit }
- requires { stk <= get_finite inp.config.stack_size }
- ensures {
- forall sta' ctx' bhv ctr' b'.
- eval_while stk ctr b (inp, ctx, sta) ins1 ins2 (sta', ctx', bhv) ctr' b' ->
- Rs.mem {state=sta'; context=ctx'; data=(ctr', b')} bhv result
- }
- = let loop_limit = get_finite inp.config.loop_limit in
- if ctr = loop_limit then
- let sta = { sta with log = Stdout.(newline (output loop_limit_message sta.log)) } in
- Rs.({empty with failure=Cn.singleton {state=sta; context=ctx; data=(ctr, b)}})
- else
- let res1_normal, res1_abort =
- Rs.separate_normal
- (interp_instr stk {inp with under_condition=True} ctx sta ins1)
- in
- assert {
- forall sta1 ctx1.
- eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
- Cn.mem {state=sta1; context=ctx1; data=()} res1_normal
- };
- assert {
- forall sta1 ctx1 bhv1.
- bhv1 <> BNormal ->
- eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, bhv1) ->
- Rs.mem {state=sta1; context=ctx1; data=()} bhv1 res1_abort
- };
- let res1_true, res1_false =
- Cn.partition (fun sta -> sta.context.result) res1_normal
- in
- assert {
- forall sta1 ctx1.
- eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
- ctx1.result = True ->
- Cn.mem {state=sta1; context=ctx1; data=()} res1_true
- };
- assert {
- forall sta1 ctx1.
- eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
- ctx1.result = False ->
- Cn.mem {state=sta1; context=ctx1; data=()} res1_false
- };
- let res2_normal, res2_abort =
- Rs.separate_normal
- (interp_instr' stk inp res1_true ins2)
- in
- assert {
- forall sta1 ctx1 sta2 ctx2.
- eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
- ctx1.result = True ->
- eval_instruction stk (inp, ctx1, sta1) ins2 (sta2, ctx2, BNormal) ->
- Cn.mem {state=sta2; context=ctx2; data=()} res2_normal
- };
- assert {
- forall sta1 ctx1 sta2 ctx2 bhv2.
- eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
- ctx1.result = True ->
- eval_instruction stk (inp, ctx1, sta1) ins2 (sta2, ctx2, bhv2) ->
- bhv2 <> BNormal ->
- Rs.mem {state=sta2; context=ctx2; data=()} bhv2 res2_abort
- };
- let res3 =
- let function aux (sta2:sym_state unit) =
- interp_while sta2.context.result (ctr+1) stk inp sta2.context sta2.state ins1 ins2
- in
- Rs.bind_collection aux res2_normal
- ensures {
- forall sta1 ctx1 sta2 ctx2 sta3 ctx3 bhv3 n b'.
- inp.config.loop_limit <> Finite ctr ->
- eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
- ctx1.result = True ->
- eval_instruction stk (inp, ctx1, sta1) ins2 (sta2, ctx2, BNormal) ->
- eval_while stk (ctr+1) ctx2.result (inp, ctx2, sta2) ins1 ins2 (sta3, ctx3, bhv3) n b' ->
- Rs.mem {state=sta3;context=ctx3;data=(n, b')} bhv3 result
- }
- in
- let function with_ctr_b (sta:sym_state unit) =
- {sta with data=(ctr, b)}
- in
- let res1_abort' =
- Rs.map with_ctr_b res1_abort
- ensures {
- forall sta1 ctx1 bhv1.
- inp.config.loop_limit <> Finite ctr ->
- bhv1 <> BNormal ->
- eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, bhv1) ->
- Rs.mem {state=sta1;context=ctx1;data=(ctr, b)} bhv1 result
- }
- in
- let res1_false' =
- Rs.({empty with normal=Cn.map with_ctr_b res1_false})
- ensures {
- forall sta1 ctx1.
- inp.config.loop_limit <> Finite ctr ->
- ctx1.result = False ->
- eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
- Rs.mem {state=sta1;context=ctx1;data=(ctr, b)} BNormal result
- }
- in
- let res2_abort' =
- Rs.map with_ctr_b res2_abort
- ensures {
- forall sta1 ctx1 sta2 ctx2 bhv2.
- inp.config.loop_limit <> Finite ctr ->
- eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
- ctx1.result = True ->
- eval_instruction stk (inp, ctx1, sta1) ins2 (sta2, ctx2, bhv2) ->
- bhv2 <> BNormal ->
- Rs.mem {state=sta2;context=ctx2;data=(ctr, b)} bhv2 result
- }
- in
- Rs.(union res3 (union res1_abort' (union res1_false' res2_abort')))
-
- with interp_instr' (stk:int) (inp:input) (stas: Cn.t (sym_state 'a)) (ins:instruction) : Rs.t 'a
- variant { get_finite inp.config.stack_size - stk, size_instr ins, Cn.size stas }
- requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
- requires { stk <= get_finite inp.config.stack_size }
- ensures { (* Over-approximation *)
- forall sta sta' ctx' bhv.
- Cn.mem sta stas ->
- eval_instruction stk (inp, sta.context, sta.state) ins (sta', ctx', bhv) ->
- Rs.mem {state=sta'; context=ctx'; data=sta.data} bhv result
- }
- = let interp_instr_with_data sta =
- ensures {
- forall sta' ctx' bhv.
- eval_instruction stk (inp, sta.context, sta.state) ins (sta', ctx', bhv) ->
- Rs.mem {state=sta'; context=ctx'; data=sta.data} bhv result
- }
- Rs.map (with_data sta.data)
- (interp_instr stk inp sta.context sta.state ins)
- in
- Rs.bind_collection interp_instr_with_data stas
-
- with interp_str_expr (stk:int) (b:bool) (inp:input) (ctx:context) (sta:state) (se:string_expression)
- : Cn.t (state, result (string, bool))
- variant { get_finite inp.config.stack_size - stk, size_string_expr se, -1 }
- requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
- requires { stk <= get_finite inp.config.stack_size }
- ensures { (* Over-approximation *)
- forall sta' res.
- eval_str_expr stk b (inp, ctx, sta) se (sta', res) ->
- Cn.mem (sta', res) result
- }
- = match se with
- | SLiteral str ->
- Cn.singleton (sta, Ok (str, b))
- | SVariable var ->
- let str = ctx.var_env[var]' in
- Cn.singleton (sta, Ok (str, b))
- | SArgument n ->
- let str = nth_argument (Cons inp.argument0 ctx.arguments) n.nat in
- Cn.singleton (sta, Ok (str, b))
- | SSubshell ins ->
- let res, stas_failure =
- Rs.separate_non_failure
- (interp_instr stk inp ctx {sta with stdout=Stdout.empty} ins)
- in
- assert {
- forall sta1 ctx1 bhv1.
- eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins (sta1, ctx1, bhv1) ->
- bhv1 <> BIncomplete ->
- Cn.mem {state=sta1; context=ctx1; data=()} res
- };
- assert {
- forall sta1 ctx1.
- eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins (sta1, ctx1, BIncomplete) ->
- Cn.mem {state=sta1; context=ctx1; data=()} stas_failure
- };
- let res' =
- let for_res (sta1:sym_state unit) =
- let str = Stdout.to_string sta1.state.stdout in
- let sta1' = {sta1.state with stdout=sta.stdout} in
- let b' = sta1.context.result in
- sta1', Ok (str, b')
- in
- Cn.map for_res res
- in
- let res_failure' =
- Cn.map (fun sta1 -> {sta1.state with stdout=sta.stdout}, Incomplete) stas_failure
- in
- Cn.union res' res_failure'
- ensures {
- forall sta1 ctx1.
- eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins (sta1, ctx1, BIncomplete) ->
- Cn.mem ({sta1 with stdout = sta.stdout}, Incomplete) result
- by Cn.mem ({sta1 with stdout = sta.stdout}, Incomplete) res_failure'
- }
- ensures {
- forall sta1 ctx1 bhv1.
- eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins (sta1, ctx1, bhv1) ->
- bhv1 <> BIncomplete ->
- Cn.mem ({sta1 with stdout = sta.stdout}, Ok (Stdout.to_string sta1.stdout, ctx1.result)) result
- by Cn.mem ({sta1 with stdout = sta.stdout}, Ok (Stdout.to_string sta1.stdout, ctx1.result)) res'
- }
- | SConcat se1 se2 ->
- let res1, res1_failure =
- separate_results
- (interp_str_expr stk b inp ctx sta se1)
- in
- let res1' =
- let for_res1 arg
+ | IAssignment var se ->
+ let str_stas, str_stas_failure =
+ separate_results
+ (interp_str_expr stk True inp ctx sta se)
+ in
+ let str_stas_failure = Results.stas_as_failures ctx str_stas_failure in
+ let res =
+ Results.inject inp
+ (Cn.map (fun arg -> assignment_for_str_sta ctx var arg) str_stas)
+ in
+ Results.(union res str_stas_failure)
ensures {
- let sta1, (str1, b1) = arg in
- forall sta2.
- eval_str_expr stk b (inp, ctx, sta) se1 (sta1, Ok (str1, b1)) ->
- eval_str_expr stk b1 (inp, ctx, sta1) se2 (sta2, Incomplete) ->
- Cn.mem (sta2, Incomplete) result
+ forall sta'.
+ eval_str_expr stk True (inp, ctx, sta) se (sta', Incomplete) ->
+ Cn.mem {state=sta'; context=ctx; data=()} result.Results.failure
}
+
+ | IExport id ->
+ let sta' =
+ let ctx' =
+ let var_val = {ctx.var_env[id] with exported=True} in
+ let var_env' = ctx.var_env[id <- var_val] in
+ {ctx with var_env = var_env'; result = True}
+ in
+ {state = sta; context = ctx'; data=()}
+ in
+ Results.({empty with normal = Cn.singleton sta'})
+
+ | ISequence ins1 ins2 ->
+ let res1_normal, res1_other =
+ Results.separate_normal
+ (interp_instr stk inp ctx sta ins1)
+ in
+ let res2 = interp_instr' stk inp res1_normal ins2 in
+ Results.union res2 res1_other
+
+ | ISubshell ins ->
+ let stas, stas_failure =
+ Results.separate_non_failure
+ (interp_instr stk inp ctx sta ins)
+ in
+ assert {
+ forall sta' ctx' bhv.
+ bhv <> BIncomplete ->
+ eval_instruction stk (inp, ctx, sta) ins (sta', ctx', bhv) ->
+ Cn.mem {state=sta'; context=ctx'; data=()} stas
+ };
+ let stas' =
+ let aux sta =
+ let ctx' = {ctx with result = sta.context.result} in
+ {state=sta.state; context=ctx'; data=()}
+ in
+ Cn.map aux stas
+ in
+ let old_ctx_with_res sta = {sta with context={ctx with result=sta.context.result}} in
+ Results.(union
+ (inject inp stas')
+ {empty with failure=Cn.map old_ctx_with_res stas_failure})
ensures {
- let sta1, (str1, b1) = arg in
- forall sta2 str2 b2.
- eval_str_expr stk b (inp, ctx, sta) se1 (sta1, Ok (str1, b1)) ->
- eval_str_expr stk b1 (inp, ctx, sta1) se2 (sta2, Ok (str2, b2)) ->
- Cn.mem (sta2, Ok (String.concat str1 str2, b2)) result
+ forall sta' ctx'.
+ eval_instruction stk (inp, ctx, sta) ins (sta', ctx', BIncomplete) ->
+ Results.mem {state=sta'; context={ctx with result=ctx'.result}; data=()} BIncomplete result
+ }
+
+ | INoOutput ins ->
+ Results.map (reset_output sta)
+ (interp_instr stk inp ctx sta ins)
+
+ | IIf ins1 ins2 ins3 ->
+ let res1_normal, res1_other =
+ Results.separate_normal
+ (interp_instr stk {inp with under_condition=True} ctx sta ins1)
+ in
+ let res2 =
+ let res1_true, res1_false =
+ Cn.partition
+ (fun sta -> sta.context.result)
+ res1_normal
+ in
+ Results.union
+ (interp_instr' stk inp res1_true ins2)
+ (interp_instr' stk inp res1_false ins3)
+ in
+ Results.union res2 res1_other
+
+ | ICd se ->
+ let res1, res1_failures =
+ separate_results
+ (interp_str_expr stk True inp ctx sta se) in
+ let res2a =
+ let function aux arg =
+ let sta1, (s, (_:bool)) = arg in
+ let cwd_p = absolute_or_concat_relative ctx.cwd s in
+ let pwd_s = normalized_path_to_string cwd_p in
+ let args = Cons "-d" (Cons pwd_s Nil) in
+ Cn.map (fun arg -> let sta2, r = arg in ((sta2, cwd_p, pwd_s), r))
+ (sym_interp_utility (utility_context args ctx, identifier_test, sta1)) in
+ Cn.bind aux res1 in
+ let res2, res2_failures = separate_results res2a in
+ let function aux' arg =
+ let (sta2, cwd_p, pwd_s), b = arg in
+ if b then
+ let ctx' = {
+ ctx with
+ var_env = ctx.var_env[identifier_pwd <- pwd_s]';
+ Context.cwd = cwd_p;
+ result = True } in
+ {state = sta2; context = ctx'; data = ()}
+ else
+ let ctx' = {ctx with result = False} in
+ {state = sta2; context = ctx'; data = ()} in
+ let res2' = Cn.map aux' res2 in
+ let res3 = Results.inject inp res2' in
+ let res2_failures' = Cn.map (fun arg -> let sta, _, _ = arg in sta) res2_failures in
+ let res_failures = Results.stas_as_failures ctx (Cn.union res1_failures res2_failures') in
+ Results.union res3 res_failures
+ ensures { [@expl:cd_arg_failure]
+ forall sta1.
+ eval_str_expr stk True (inp, ctx, sta) se (sta1, Incomplete) ->
+ Results.mem {state=sta1; context=ctx; data=()} BIncomplete result
+ }
+ ensures { [@expl:cd_incomplete]
+ forall sta1 s b sta2.
+ eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (s, b)) ->
+ let cwd_p = absolute_or_concat_relative ctx.Context.cwd s in
+ let pwd_s = normalized_path_to_string cwd_p in
+ let args = Cons "-d" (Cons pwd_s Nil) in
+ interp_utility (utility_context args ctx, identifier_test, sta1) (sta2, Incomplete) ->
+ Results.mem {state=sta2; context=ctx; data=()} BIncomplete result
+ by Cn.mem (sta1, (s, b)) res1
+ so Cn.mem (sta2, Incomplete) (sym_interp_utility (utility_context args ctx, identifier_test, sta1))
+ so Cn.mem (sta2, cwd_p, pwd_s) res2_failures
+ }
+ ensures { [@expl:cd_no_dir]
+ forall sta1 s b sta2.
+ eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (s, b)) ->
+ let cwd_p = absolute_or_concat_relative ctx.Context.cwd s in
+ let pwd_s = normalized_path_to_string cwd_p in
+ let args = Cons "-d" (Cons pwd_s Nil) in
+ interp_utility (utility_context args ctx, identifier_test, sta1) (sta2, Ok False) ->
+ let ctx' = {ctx with result = False} in
+ let bhv = behaviour inp False in
+ Results.mem {state=sta2; context=ctx'; data=()} bhv result
+ by Cn.mem (sta1, (s, b)) res1
+ so Cn.mem (sta2, Ok False) (sym_interp_utility (utility_context args ctx, identifier_test, sta1))
+ so Cn.mem ((sta2, cwd_p, pwd_s), False) res2
+ so Cn.mem {state=sta2; context=ctx'; data=()} res2'
}
- = let sta1, (str1, b1) = arg in
- let res2, res2_failure =
+ ensures { [@expl:cd]
+ forall sta1 s b sta2.
+ eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (s, b)) ->
+ let cwd_p = absolute_or_concat_relative ctx.Context.cwd s in
+ let pwd_s = normalized_path_to_string cwd_p in
+ let args = Cons "-d" (Cons pwd_s Nil) in
+ interp_utility (utility_context args ctx, identifier_test, sta1) (sta2, Ok True) ->
+ let ctx1 = {ctx with result = True; var_env = ctx.var_env[identifier_pwd <- pwd_s]'; Context.cwd = cwd_p} in
+ let bhv = behaviour inp True in
+ Results.mem {state=sta2; context=ctx1; data=()} bhv result
+ by Cn.mem (sta1, (s, b)) res1
+ so Cn.mem (sta2, Ok True) (sym_interp_utility (utility_context args ctx, identifier_test, sta1))
+ so Cn.mem ((sta2, cwd_p, pwd_s), True) res2
+ so Cn.mem {state=sta2; context=ctx1; data=()} res2'
+ }
+
+ | ICallUtility id le ->
+ let res, res_failures =
+ separate_results
+ (interp_list_expr stk inp ctx sta le) in
+ let function aux arg =
+ let sta', args = arg in
+ sym_interp_utility (utility_context args ctx, id, sta') in
+ let res', res_failures' =
+ separate_results (Cn.bind aux res) in
+ let function aux' arg =
+ let sta'', b = arg in
+ {state=sta''; context={ctx with result=b}; data=()} in
+ let res'' = Cn.map aux' res' in
+ let res''' = Results.inject inp res'' in
+ let res_failures' = Results.stas_as_failures ctx (Cn.union res_failures res_failures') in
+ Results.union res''' res_failures'
+ ensures { [@expl:args_incomplete]
+ forall sta'.
+ eval_list_expr stk (inp, ctx, sta) le (sta', Incomplete) ->
+ Results.mem {state=sta'; context=ctx; data=()} BIncomplete result
+ }
+ ensures { [@expl:utility_incomplete]
+ forall sta' ss sta''.
+ eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
+ interp_utility (utility_context ss ctx, id, sta') (sta'', Incomplete) ->
+ Results.mem {state=sta''; context=ctx; data=()} BIncomplete result
+ by Results.mem {state=sta''; context=ctx; data=()} BIncomplete res_failures'
+ }
+ ensures { [@expl:utility]
+ forall sta' ss sta'' b.
+ eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
+ interp_utility (utility_context ss ctx, id, sta') (sta'', Ok b) ->
+ let ctx' = {ctx with result=b} in
+ Results.mem {state=sta''; context=ctx'; data=()} (behaviour inp b) result
+ by Cn.mem {state=sta''; context=ctx'; data=()} res''
+ }
+
+ | ICallFunction id le ->
+ let arg_res, arg_res_failures =
separate_results
- (interp_str_expr stk b1 inp ctx sta1 se2)
+ (interp_list_expr stk inp ctx sta le)
in
- let res2_failure' =
- Cn.map (fun sta -> sta, Incomplete) res2_failure
+ assert { [@expl:callfun1]
+ forall sta1 args.
+ eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
+ Cn.mem (sta1, args) arg_res
+ };
+ let res =
+ match ctx.func_env[id] with
+ | Some ins -> (* Function defined as `ins` *)
+ if stk = get_finite inp.config.stack_size then (* Stack overflow *)
+ let aux arg =
+ let sta', _ = arg in
+ let sta' = { sta' with log = Stdout.(newline (output stack_limit_message sta'.log)) } in
+ {state=sta'; context=ctx; data=()}
+ in
+ Results.({empty with failure = Cn.map aux arg_res})
+ ensures { [@expl:callfun2]
+ forall sta1 args ins.
+ eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
+ ctx.func_env[id] = Some ins ->
+ inp.config.stack_size = Finite stk ->
+ let sta1' = { sta1 with log = Stdout.(newline (output stack_limit_message sta1.log)) } in
+ Results.mem {state=sta1'; context=ctx; data=()} BIncomplete result
+ }
+ else (* Execute function *)
+ let res2 =
+ let function aux (arg: (state, list string)) =
+ let sta1, args = arg in
+ let inp1 = { inp with argument0 = identifier_to_string id } in
+ let ctx1 = { ctx with arguments = args } in
+ interp_instr (stk+1) inp1 ctx1 sta1 ins
+ in
+ Results.bind_collection aux arg_res
+ ensures { [@expl:callfun3]
+ forall sta1 args ins sta2 ctx2 bhv2.
+ eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
+ ctx.func_env[id] = Some ins ->
+ inp.config.stack_size <> Finite stk ->
+ let inp1 = { inp with argument0 = identifier_to_string id } in
+ let ctx1 = { ctx with arguments = args } in
+ eval_instruction (stk+1) (inp1, ctx1, sta1) ins (sta2, ctx2, bhv2) ->
+ Results.mem {state=sta2; context=ctx2; data=()} bhv2 result
+ }
+ in
+ let res2' =
+ let function aux (sta2: sym_state unit) =
+ {state=sta2.state; context={sta2.context with arguments = ctx.arguments}; data=()}
+ in
+ Results.map aux res2
+ ensures { [@expl:callfun4]
+ forall sta1 args ins sta2 ctx2 bhv2.
+ eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
+ ctx.func_env[id] = Some ins ->
+ inp.config.stack_size <> Finite stk ->
+ let inp1 = { inp with argument0 = identifier_to_string id } in
+ let ctx1 = { ctx with arguments = args } in
+ eval_instruction (stk+1) (inp1, ctx1, sta1) ins (sta2, ctx2, bhv2) ->
+ Results.mem {state=sta2; context={ctx2 with arguments = ctx.arguments}; data=()} bhv2 result
+ }
+ in
+ Results.({res2' with normal=Cn.union res2'.normal res2'.return_; return_=Cn.empty})
+ ensures { [@expl:callfun5]
+ forall sta1 args ins sta2 ctx2 bhv2.
+ eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
+ ctx.func_env[id] = Some ins ->
+ inp.config.stack_size <> Finite stk ->
+ let inp1 = {inp with argument0=identifier_to_string id} in
+ let ctx1 = {ctx with arguments=args} in
+ eval_instruction (stk+1) (inp1, ctx1, sta1) ins (sta2, ctx2, bhv2) ->
+ let bhv' = match bhv2 with BNormal | BReturn -> BNormal | BExit -> BExit | BIncomplete -> BIncomplete end in
+ let ctx' = { ctx2 with arguments = ctx.arguments } in
+ Results.mem {state=sta2; context=ctx'; data=()} bhv' result
+ }
+ | None -> (* Undefined function *)
+ let arg_res' =
+ let function aux (arg: (state, list string)) =
+ let sta', _ = arg in
+ {state=sta'; context={ctx with result=False}; data=()}
+ in
+ Cn.map aux arg_res
+ ensures {
+ forall sta' ss.
+ eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
+ ctx.func_env[id] = None ->
+ Cn.mem {state=sta'; context={ctx with result=False}; data=()} result
+ by Cn.mem (sta', ss) arg_res
+ }
+ in
+ Results.single_behaviour (behaviour inp False) arg_res'
+ ensures {
+ forall sta' ss.
+ eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
+ ctx.func_env[id] = None ->
+ Results.mem {state=sta'; context={ctx with result=False}; data=()} (behaviour inp False) result
+ }
+ end
+ in
+ let res_failures = Results.stas_as_failures ctx arg_res_failures in
+ Results.union res res_failures
+
+ | IShift bn ->
+ match shift_arguments (option_get (mk_nat 1) bn).nat ctx.arguments with
+ | Some args ->
+ let ctx' = {ctx with result = True; arguments = args} in
+ let sta' = {state = sta; context = ctx'; data=()} in
+ Results.({empty with normal = Cn.singleton sta'})
+ | None ->
+ let ctx' = {ctx with result = False} in
+ let sta' = {state = sta; context = ctx'; data=()} in
+ Results.inject inp (Cn.singleton sta')
+ end
+
+ | IForeach id le ins ->
+ let lst_res, lst_res_failures =
+ separate_results
+ (interp_list_expr stk inp ctx sta le)
+ in
+ assert {
+ forall sta' ss.
+ eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
+ Cn.mem (sta', ss) lst_res
+ };
+ let res_loop_cont =
+ (* Execute foreach loop on a result from interp_list_expr *)
+ let function aux arg =
+ let sta', ss = arg in
+ interp_foreach True stk inp ctx sta' id ss ins
+ in
+ Results.bind_collection aux lst_res
+ ensures {
+ forall sta' ss sta'' ctx' bhv b.
+ eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
+ eval_foreach stk True (inp, ctx, sta') id ss ins (sta'', ctx', bhv) b ->
+ Results.mem {state=sta''; context=ctx'; data=b} bhv result
+ }
+ in
+ let res_loop_cont' =
+ let function aux sta'' =
+ let ctx'' = {sta''.context with result=sta''.data} in
+ with_data () {sta'' with context = ctx''}
+ in
+ Results.map aux res_loop_cont
+ ensures {
+ forall sta' ss sta'' ctx' bhv b.
+ eval_list_expr stk (inp, ctx, sta) le (sta', Ok ss) ->
+ eval_foreach stk True (inp, ctx, sta') id ss ins (sta'', ctx', bhv) b ->
+
+ Results.mem {state=sta''; context={ctx' with result=b}; data=()} bhv result
+ }
+ in
+ let res_failure =
+ Results.stas_as_failures ctx lst_res_failures
+ ensures {
+ forall sta'.
+ eval_list_expr stk (inp, ctx, sta) le (sta', Incomplete) ->
+ Results.mem {state=sta'; context=ctx; data=()} BIncomplete result
+ }
+ in
+ Results.(union res_loop_cont' res_failure)
+
+ | IWhile ins1 ins2 ->
+ let res = interp_while True 0 stk inp ctx sta ins1 ins2 in
+ let function aux_normal (sta': sym_state (int, bool)) =
+ let _, b = sta'.data in
+ {state=sta'.state; context={sta'.context with result=b}; data=()}
+ in
+ let function aux_other (sta': sym_state (int, bool)) =
+ {sta' with data=()}
+ in
+ Results.({normal=Cn.map aux_normal res.normal;
+ exit=Cn.map aux_other res.exit;
+ return_=Cn.map aux_other res.return_;
+ failure=Cn.map aux_other res.failure})
+ ensures {
+ forall sta' ctx' bhv ctr b.
+ bhv <> BNormal ->
+ eval_while stk 0 True (inp, ctx, sta) ins1 ins2 (sta', ctx', bhv) ctr b ->
+ Results.mem {state=sta'; context=ctx'; data=()} bhv result
+ }
+ ensures {
+ forall sta' ctx' ctr b.
+ eval_while stk 0 True (inp, ctx, sta) ins1 ins2 (sta', ctx', BNormal) ctr b ->
+ Results.mem {state=sta'; context={ctx' with result=b}; data=()} BNormal result
+ }
+
+ | IPipe ins1 ins2 ->
+ let stas1, stas1_failure =
+ Results.separate_non_failure
+ (interp_instr stk inp ctx {sta with stdout=Stdout.empty} ins1)
+ in
+ assert {
+ forall sta1 ctx1 bhv1.
+ eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, bhv1) ->
+ bhv1 <> BIncomplete ->
+ Cn.mem {state=sta1; context=ctx1; data=()} stas1
+ };
+ let stas1': Cn.t (sym_state stdin) = (* data is sta1.state.stdin *)
+ let function aux (sta1: sym_state unit) =
+ {state={sta1.state with stdout=sta.stdout; stdin=Stdout.to_stdin sta1.state.stdout}; context=ctx; data=sta1.state.stdin}
+ in
+ Cn.map aux stas1
+ ensures {
+ forall sta1 ctx1 bhv1.
+ eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, bhv1) ->
+ bhv1 <> BIncomplete ->
+ Cn.mem
+ {state={sta1 with stdout=sta.stdout; stdin=Stdout.to_stdin sta1.stdout}; context=ctx; data=sta1.stdin}
+ result
+ }
+ in
+ let res2: Results.t stdin = (* data is sta1.state.stdin *)
+ interp_instr' stk inp stas1' ins2
+ ensures {
+ forall sta1 ctx1 bhv1 sta2 ctx2 bhv2.
+ eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, bhv1) ->
+ bhv1 <> BIncomplete ->
+ eval_instruction stk (inp, ctx, {sta1 with stdout=sta.stdout; stdin=Stdout.to_stdin sta1.stdout}) ins2 (sta2, ctx2, bhv2) ->
+ Results.mem {state=sta2; context=ctx2; data=sta1.stdin} bhv2 result
+ }
in
let res2' =
- let for_res2 arg2 =
- let sta2, (str2, b2) = arg2 in
- sta2, Ok (String.concat str1 str2, b2)
+ let function aux sta2 =
+ {state={sta2.state with stdin=sta2.data};
+ context={ctx with result=sta2.context.result};
+ data=()}
in
- Cn.map for_res2 res2
+ Results.map aux res2
+ ensures {
+ forall sta1 ctx1 bhv1 sta2 ctx2 bhv2.
+ eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, bhv1) ->
+ bhv1 <> BIncomplete ->
+ eval_instruction stk (inp, ctx, {sta1 with stdout=sta.stdout; stdin=Stdout.to_stdin sta1.stdout}) ins2 (sta2, ctx2, bhv2) ->
+ Results.mem {state={sta2 with stdin=sta1.stdin}; context={ctx with result=ctx2.result}; data=()} bhv2 result
+ }
in
- Cn.(union res2' res2_failure')
- in
- Cn.bind for_res1 res1
- in
- let res1_failure' =
- Cn.map (fun sta -> sta, Incomplete) res1_failure
- in
- Cn.(union res1' res1_failure')
- end
+ let sta1_failure' =
+ let function aux (sta1: sym_state unit) =
+ {state={sta1.state with stdout=sta.stdout}; context=ctx; data=()}
+ in
+ Cn.map aux stas1_failure
+ ensures {
+ forall sta1 ctx1.
+ eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, BIncomplete) ->
+ Cn.mem {state={sta1 with stdout=sta.stdout}; context=ctx; data=()} result
+ }
+ in
+ Results.(union res2' {empty with failure=sta1_failure'})
+
+ | IExit code ->
+ let r =
+ match code with
+ | RPrevious -> ctx.result
+ | RSuccess -> True
+ | RFailure -> False
+ end
+ in
+ let sta = {state=sta; context={ctx with result=r}; data=()} in
+ Results.({empty with exit = Cn.singleton sta})
+
+ | IReturn code ->
+ let r =
+ match code with
+ | RPrevious -> ctx.result
+ | RSuccess -> True
+ | RFailure -> False
+ end
+ in
+ let sta =
+ let ctx' = {ctx with result = r} in
+ {state = sta; context = ctx'; data=()}
+ in
+ Results.({empty with return_ = Cn.singleton sta})
+ end
+
+ with interp_foreach (b:bool) (stk:int) (inp:input) (ctx:context) (sta:state) (id:identifier) (ss:list string) (ins:instruction) : Results.t bool
+ variant { get_finite inp.config.stack_size - stk, size_instr ins, L.length ss }
+ requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
+ requires { stk <= get_finite inp.config.stack_size }
+ ensures {
+ forall sta' ctx' bhv b'.
+ eval_foreach stk b (inp, ctx, sta) id ss ins (sta', ctx', bhv) b' ->
+ Results.mem {state=sta'; context=ctx'; data=b'} bhv result
+ }
+ = match ss with
+ | Nil ->
+ Results.({empty with normal=Cn.singleton {state=sta; context=ctx; data=b}})
+ | Cons s ss' ->
+ let res1_normal, res1_other =
+ Results.separate_normal
+ (interp_instr stk inp {ctx with var_env = ctx.var_env[id <- s]'} sta ins)
+ in
+ let res_normal' =
+ let function aux (sta1: sym_state unit) =
+ interp_foreach sta1.context.result stk inp sta1.context sta1.state id ss' ins
+ in
+ Results.bind_collection aux res1_normal
+ ensures {
+ forall sta1 ctx1 sta2 ctx2 bhv2 b2.
+ eval_instruction stk (inp, {ctx with var_env=ctx.var_env[id <- s]'}, sta) ins (sta1, ctx1, BNormal) ->
+ eval_foreach stk ctx1.result (inp, ctx1, sta1) id ss' ins (sta2, ctx2, bhv2) b2 ->
+ Results.mem {state=sta2; context=ctx2; data=b2} bhv2 result
+ }
+ in
+ let res1_other' =
+ let function aux (sta: sym_state unit) =
+ with_data sta.context.result sta
+ in
+ Results.map aux res1_other
+ ensures {
+ forall sta1 ctx1 bhv1.
+ eval_instruction stk (inp, {ctx with var_env=ctx.var_env[id <- s]'}, sta) ins (sta1, ctx1, bhv1) ->
+ bhv1 <> BNormal ->
+ Results.mem {state=sta1; context=ctx1; data=ctx1.result} bhv1 result
+ }
+ in
+ Results.union res_normal' res1_other'
+ end
- with interp_list_expr (stk:int) (inp:input) (ctx:context) (sta:state) (le:list_expression)
- : Cn.t (state, result (list string))
- variant { get_finite inp.config.stack_size - stk, size_list_expr le, -1 }
- requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
- requires { stk <= get_finite inp.config.stack_size }
- ensures { (* Over-approximation *)
- forall sta' res.
- eval_list_expr stk (inp, ctx, sta) le (sta', res) ->
- Cn.mem (sta', res) result
- }
- = match le with
- | Nil ->
- Cn.singleton (sta, Ok Nil)
- | Cons (se, sp) le' ->
- let str_res1, str_res1_failures =
- separate_results
- (interp_str_expr stk True inp ctx sta se : Cn.t (state, result (string, bool)))
- in
- let res2 =
- let for_sta_str (arg: (state, (string, bool)))
+ with interp_while b ctr stk inp ctx (sta:state) ins1 ins2 : Results.t (int, bool)
+ variant { get_finite inp.config.stack_size - stk, size_instr ins1+size_instr ins2, get_finite inp.config.loop_limit - ctr }
+ requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
+ requires { 0 <= ctr <= get_finite inp.config.loop_limit }
+ requires { stk <= get_finite inp.config.stack_size }
+ ensures {
+ forall sta' ctx' bhv ctr' b'.
+ eval_while stk ctr b (inp, ctx, sta) ins1 ins2 (sta', ctx', bhv) ctr' b' ->
+ Results.mem {state=sta'; context=ctx'; data=(ctr', b')} bhv result
+ }
+ = let loop_limit = get_finite inp.config.loop_limit in
+ if ctr = loop_limit then
+ let sta = { sta with log = Stdout.(newline (output loop_limit_message sta.log)) } in
+ Results.({empty with failure=Cn.singleton {state=sta; context=ctx; data=(ctr, b)}})
+ else
+ let res1_normal, res1_abort =
+ Results.separate_normal
+ (interp_instr stk {inp with under_condition=True} ctx sta ins1)
+ in
+ assert {
+ forall sta1 ctx1.
+ eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
+ Cn.mem {state=sta1; context=ctx1; data=()} res1_normal
+ };
+ assert {
+ forall sta1 ctx1 bhv1.
+ bhv1 <> BNormal ->
+ eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, bhv1) ->
+ Results.mem {state=sta1; context=ctx1; data=()} bhv1 res1_abort
+ };
+ let res1_true, res1_false =
+ Cn.partition (fun sta -> sta.context.result) res1_normal
+ in
+ assert {
+ forall sta1 ctx1.
+ eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
+ ctx1.result = True ->
+ Cn.mem {state=sta1; context=ctx1; data=()} res1_true
+ };
+ assert {
+ forall sta1 ctx1.
+ eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
+ ctx1.result = False ->
+ Cn.mem {state=sta1; context=ctx1; data=()} res1_false
+ };
+ let res2_normal, res2_abort =
+ Results.separate_normal
+ (interp_instr' stk inp res1_true ins2)
+ in
+ assert {
+ forall sta1 ctx1 sta2 ctx2.
+ eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
+ ctx1.result = True ->
+ eval_instruction stk (inp, ctx1, sta1) ins2 (sta2, ctx2, BNormal) ->
+ Cn.mem {state=sta2; context=ctx2; data=()} res2_normal
+ };
+ assert {
+ forall sta1 ctx1 sta2 ctx2 bhv2.
+ eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
+ ctx1.result = True ->
+ eval_instruction stk (inp, ctx1, sta1) ins2 (sta2, ctx2, bhv2) ->
+ bhv2 <> BNormal ->
+ Results.mem {state=sta2; context=ctx2; data=()} bhv2 res2_abort
+ };
+ let res3 =
+ let function aux (sta2:sym_state unit) =
+ interp_while sta2.context.result (ctr+1) stk inp sta2.context sta2.state ins1 ins2
+ in
+ Results.bind_collection aux res2_normal
+ ensures {
+ forall sta1 ctx1 sta2 ctx2 sta3 ctx3 bhv3 n b'.
+ inp.config.loop_limit <> Finite ctr ->
+ eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
+ ctx1.result = True ->
+ eval_instruction stk (inp, ctx1, sta1) ins2 (sta2, ctx2, BNormal) ->
+ eval_while stk (ctr+1) ctx2.result (inp, ctx2, sta2) ins1 ins2 (sta3, ctx3, bhv3) n b' ->
+ Results.mem {state=sta3;context=ctx3;data=(n, b')} bhv3 result
+ }
+ in
+ let function with_ctr_b (sta:sym_state unit) =
+ {sta with data=(ctr, b)}
+ in
+ let res1_abort' =
+ Results.map with_ctr_b res1_abort
+ ensures {
+ forall sta1 ctx1 bhv1.
+ inp.config.loop_limit <> Finite ctr ->
+ bhv1 <> BNormal ->
+ eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, bhv1) ->
+ Results.mem {state=sta1;context=ctx1;data=(ctr, b)} bhv1 result
+ }
+ in
+ let res1_false' =
+ Results.({empty with normal=Cn.map with_ctr_b res1_false})
+ ensures {
+ forall sta1 ctx1.
+ inp.config.loop_limit <> Finite ctr ->
+ ctx1.result = False ->
+ eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
+ Results.mem {state=sta1;context=ctx1;data=(ctr, b)} BNormal result
+ }
+ in
+ let res2_abort' =
+ Results.map with_ctr_b res2_abort
+ ensures {
+ forall sta1 ctx1 sta2 ctx2 bhv2.
+ inp.config.loop_limit <> Finite ctr ->
+ eval_instruction stk ({inp with under_condition = True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
+ ctx1.result = True ->
+ eval_instruction stk (inp, ctx1, sta1) ins2 (sta2, ctx2, bhv2) ->
+ bhv2 <> BNormal ->
+ Results.mem {state=sta2;context=ctx2;data=(ctr, b)} bhv2 result
+ }
+ in
+ Results.(union res3 (union res1_abort' (union res1_false' res2_abort')))
+
+ with interp_instr' (stk:int) (inp:input) (stas: Cn.t (sym_state 'a)) (ins:instruction) : Results.t 'a
+ variant { get_finite inp.config.stack_size - stk, size_instr ins, Cn.size stas }
+ requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
+ requires { stk <= get_finite inp.config.stack_size }
+ ensures { (* Over-approximation *)
+ forall sta sta' ctx' bhv.
+ Cn.mem sta stas ->
+ eval_instruction stk (inp, sta.context, sta.state) ins (sta', ctx', bhv) ->
+ Results.mem {state=sta'; context=ctx'; data=sta.data} bhv result
+ }
+ = let interp_instr_with_data sta =
ensures {
- let sta1, (str1, b1) = arg in
- forall sta2.
- eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (str1, b1)) ->
- eval_list_expr stk (inp, ctx, sta1) le' (sta2, Incomplete) ->
- Cn.mem (sta2, Incomplete) result
+ forall sta' ctx' bhv.
+ eval_instruction stk (inp, sta.context, sta.state) ins (sta', ctx', bhv) ->
+ Results.mem {state=sta'; context=ctx'; data=sta.data} bhv result
+ }
+ Results.map (with_data sta.data)
+ (interp_instr stk inp sta.context sta.state ins)
+ in
+ Results.bind_collection interp_instr_with_data stas
+
+ with interp_str_expr (stk:int) (b:bool) (inp:input) (ctx:context) (sta:state) (se:string_expression)
+ : Cn.t (state, result (string, bool))
+ variant { get_finite inp.config.stack_size - stk, size_string_expr se, -1 }
+ requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
+ requires { stk <= get_finite inp.config.stack_size }
+ ensures { (* Over-approximation *)
+ forall sta' res.
+ eval_str_expr stk b (inp, ctx, sta) se (sta', res) ->
+ Cn.mem (sta', res) result
+ }
+ = match se with
+ | SLiteral str ->
+ Cn.singleton (sta, Ok (str, b))
+ | SVariable var ->
+ let str = ctx.var_env[var]' in
+ Cn.singleton (sta, Ok (str, b))
+ | SArgument n ->
+ let str = nth_argument (Cons inp.argument0 ctx.arguments) n.nat in
+ Cn.singleton (sta, Ok (str, b))
+ | SSubshell ins ->
+ let res, stas_failure =
+ Results.separate_non_failure
+ (interp_instr stk inp ctx {sta with stdout=Stdout.empty} ins)
+ in
+ assert {
+ forall sta1 ctx1 bhv1.
+ eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins (sta1, ctx1, bhv1) ->
+ bhv1 <> BIncomplete ->
+ Cn.mem {state=sta1; context=ctx1; data=()} res
+ };
+ assert {
+ forall sta1 ctx1.
+ eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins (sta1, ctx1, BIncomplete) ->
+ Cn.mem {state=sta1; context=ctx1; data=()} stas_failure
+ };
+ let res' =
+ let for_res (sta1:sym_state unit) =
+ let str = Stdout.to_string sta1.state.stdout in
+ let sta1' = {sta1.state with stdout=sta.stdout} in
+ let b' = sta1.context.result in
+ sta1', Ok (str, b')
+ in
+ Cn.map for_res res
+ in
+ let res_failure' =
+ Cn.map (fun sta1 -> {sta1.state with stdout=sta.stdout}, Incomplete) stas_failure
+ in
+ Cn.union res' res_failure'
+ ensures {
+ forall sta1 ctx1.
+ eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins (sta1, ctx1, BIncomplete) ->
+ Cn.mem ({sta1 with stdout = sta.stdout}, Incomplete) result
+ by Cn.mem ({sta1 with stdout = sta.stdout}, Incomplete) res_failure'
}
ensures {
- let sta1, (str1, b1) = arg in
- forall sta2 l2.
- eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (str1, b1)) ->
- eval_list_expr stk (inp, ctx, sta1) le' (sta2, Ok l2) ->
- Cn.mem (sta2, Ok L.(split sp str1++l2)) result
+ forall sta1 ctx1 bhv1.
+ eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins (sta1, ctx1, bhv1) ->
+ bhv1 <> BIncomplete ->
+ Cn.mem ({sta1 with stdout = sta.stdout}, Ok (Stdout.to_string sta1.stdout, ctx1.result)) result
+ by Cn.mem ({sta1 with stdout = sta.stdout}, Ok (Stdout.to_string sta1.stdout, ctx1.result)) res'
}
- = let sta1, (str1, _) = arg in
- let lst_res2: Cn.t (state, list string), lst_res2_failures: Cn.t state =
+ | SConcat se1 se2 ->
+ let res1, res1_failure =
separate_results
- (interp_list_expr stk inp ctx sta1 le')
+ (interp_str_expr stk b inp ctx sta se1)
in
- let lst_res2' =
- Cn.map (fun arg -> let sta2, strs2 = arg in sta2, Ok L.(split sp str1++strs2)) lst_res2
+ let res1' =
+ let for_res1 arg
+ ensures {
+ let sta1, (str1, b1) = arg in
+ forall sta2.
+ eval_str_expr stk b (inp, ctx, sta) se1 (sta1, Ok (str1, b1)) ->
+ eval_str_expr stk b1 (inp, ctx, sta1) se2 (sta2, Incomplete) ->
+ Cn.mem (sta2, Incomplete) result
+ }
+ ensures {
+ let sta1, (str1, b1) = arg in
+ forall sta2 str2 b2.
+ eval_str_expr stk b (inp, ctx, sta) se1 (sta1, Ok (str1, b1)) ->
+ eval_str_expr stk b1 (inp, ctx, sta1) se2 (sta2, Ok (str2, b2)) ->
+ Cn.mem (sta2, Ok (String.concat str1 str2, b2)) result
+ }
+ = let sta1, (str1, b1) = arg in
+ let res2, res2_failure =
+ separate_results
+ (interp_str_expr stk b1 inp ctx sta1 se2)
+ in
+ let res2_failure' =
+ Cn.map (fun sta -> sta, Incomplete) res2_failure
+ in
+ let res2' =
+ let for_res2 arg2 =
+ let sta2, (str2, b2) = arg2 in
+ sta2, Ok (String.concat str1 str2, b2)
+ in
+ Cn.map for_res2 res2
+ in
+ Cn.(union res2' res2_failure')
+ in
+ Cn.bind for_res1 res1
in
- let lst_res2_failures' =
- Cn.map (fun sta -> sta, Incomplete) lst_res2_failures
+ let res1_failure' =
+ Cn.map (fun sta -> sta, Incomplete) res1_failure
in
- Cn.(union lst_res2' lst_res2_failures')
- in
- Cn.bind for_sta_str str_res1
- in
- let str_res1_failures' =
- Cn.map (fun sta -> sta, Incomplete) str_res1_failures
- in
- Cn.(union res2 str_res1_failures')
- end
+ Cn.(union res1' res1_failure')
+ end
- let rec interp_function_definitions (fenv:func_env) (defs:list function_definition)
- variant { defs }
- = match defs with
- | Nil -> fenv
- | Cons (id, instr) defs' ->
- interp_function_definitions fenv[id <- Some instr] defs'
- end
+ with interp_list_expr (stk:int) (inp:input) (ctx:context) (sta:state) (le:list_expression)
+ : Cn.t (state, result (list string))
+ variant { get_finite inp.config.stack_size - stk, size_list_expr le, -1 }
+ requires { inp.config.loop_limit <> Infinite /\ inp.config.stack_size <> Infinite }
+ requires { stk <= get_finite inp.config.stack_size }
+ ensures { (* Over-approximation *)
+ forall sta' res.
+ eval_list_expr stk (inp, ctx, sta) le (sta', res) ->
+ Cn.mem (sta', res) result
+ }
+ = match le with
+ | Nil ->
+ Cn.singleton (sta, Ok Nil)
+ | Cons (se, sp) le' ->
+ let str_res1, str_res1_failures =
+ separate_results
+ (interp_str_expr stk True inp ctx sta se : Cn.t (state, result (string, bool)))
+ in
+ let res2 =
+ let for_sta_str (arg: (state, (string, bool)))
+ ensures {
+ let sta1, (str1, b1) = arg in
+ forall sta2.
+ eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (str1, b1)) ->
+ eval_list_expr stk (inp, ctx, sta1) le' (sta2, Incomplete) ->
+ Cn.mem (sta2, Incomplete) result
+ }
+ ensures {
+ let sta1, (str1, b1) = arg in
+ forall sta2 l2.
+ eval_str_expr stk True (inp, ctx, sta) se (sta1, Ok (str1, b1)) ->
+ eval_list_expr stk (inp, ctx, sta1) le' (sta2, Ok l2) ->
+ Cn.mem (sta2, Ok L.(split sp str1++l2)) result
+ }
+ = let sta1, (str1, _) = arg in
+ let lst_res2: Cn.t (state, list string), lst_res2_failures: Cn.t state =
+ separate_results
+ (interp_list_expr stk inp ctx sta1 le')
+ in
+ let lst_res2' =
+ Cn.map (fun arg -> let sta2, strs2 = arg in sta2, Ok L.(split sp str1++strs2)) lst_res2
+ in
+ let lst_res2_failures' =
+ Cn.map (fun sta -> sta, Incomplete) lst_res2_failures
+ in
+ Cn.(union lst_res2' lst_res2_failures')
+ in
+ Cn.bind for_sta_str str_res1
+ in
+ let str_res1_failures' =
+ Cn.map (fun sta -> sta, Incomplete) str_res1_failures
+ in
+ Cn.(union res2 str_res1_failures')
+ end
+
+ let rec interp_function_definitions (fenv:func_env) (defs:list function_definition)
+ variant { defs }
+ = match defs with
+ | Nil -> fenv
+ | Cons (id, instr) defs' ->
+ interp_function_definitions fenv[id <- Some instr] defs'
+ end
- let function only_states_with_result (res: bool) (stas: Cn.t (sym_state unit)) : Cn.t state =
- Cn.(map (fun sta -> sta.state)
- (filter (fun sta -> notb (xorb res sta.context.result))
- stas))
-
- let interp_program inp stas pro : (Cn.t state, Cn.t state, Cn.t state)
- requires { inp.config.loop_limit <> Infinite }
- requires { inp.config.stack_size <> Infinite }
- = let stas, stas_failure =
- let stas =
- let aux sta =
- let fenv = interp_function_definitions sta.context.func_env pro.function_definitions in
- {sta with context={sta.context with func_env = fenv}}
+ let function only_states_with_result (res: bool) (stas: Cn.t (sym_state unit)) : Cn.t state =
+ Cn.(map (fun sta -> sta.state)
+ (filter (fun sta -> notb (xorb res sta.context.result))
+ stas))
+
+ let interp_program inp stas pro : (Cn.t state, Cn.t state, Cn.t state)
+ requires { inp.config.loop_limit <> Infinite }
+ requires { inp.config.stack_size <> Infinite }
+ = let stas, stas_failure =
+ let stas =
+ let aux sta =
+ let fenv = interp_function_definitions sta.context.func_env pro.function_definitions in
+ {sta with context={sta.context with func_env = fenv}}
+ in
+ Cn.map aux stas
+ in
+ Results.separate_non_failure
+ (interp_instr' 0 inp stas pro.instruction)
in
- Cn.map aux stas
- in
- Rs.separate_non_failure
- (interp_instr' 0 inp stas pro.instruction)
- in
- (only_states_with_result True stas,
- only_states_with_result False stas,
- Cn.map (fun sta -> sta.state) stas_failure)
+ (only_states_with_result True stas,
+ only_states_with_result False stas,
+ Cn.map (fun sta -> sta.state) stas_failure)
+ end
+ end
end
\ No newline at end of file
diff --git a/src/symbolic/symbolicInterpreter/why3session.xml b/src/symbolic/symbolicInterpreter/why3session.xml
index 66436e00..61fb9ca5 100644
--- a/src/symbolic/symbolicInterpreter/why3session.xml
+++ b/src/symbolic/symbolicInterpreter/why3session.xml
@@ -7,35 +7,66 @@
-
-
-
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
-
+
@@ -44,44 +75,44 @@
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -93,1229 +124,1207 @@
-
+
-
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
-
+
+
-
-
+
+
-
-
-
-
-
-
-
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
-
-
-
-
-
-
-
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
-
+
-
+
-
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
+
+
+
+
+
+
+
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
+
+
+
+
+
+
+
-
+
-
+
-
+
-
-
-
-
-
-
-
-
+
-
-
-
-
-
-
-
-
+
-
+
-
+
-
+
+
+
+
+
-
+
-
+
-
+
-
+
-
+
-
+
+
+
+
+
-
+
-
+
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
+
-
+
-
+
-
+
-
+
-
+
+
+
+
+
+
+
+
-
+
-
+
-
+
-
+
-
+
-
-
-
-
-
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
+
+
+
+
-
+
+
+
+
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -1324,7 +1333,7 @@
-
+
@@ -1335,1034 +1344,1041 @@
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
+
+
+
+
+
+
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -2370,126 +2386,137 @@
-
+
-
+
+
+
+
+
+
+
+
-
+
-
-
-
-
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
+
+
+
+
-
+
-
+
-
+
-
+
-
+
-
+
+
+
+
+
-
+
-
+
-
+
-
+
-
+
@@ -2497,25 +2524,41 @@
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
+
-
+
-
+
-
+
-
+
@@ -2532,79 +2575,69 @@
-
+
-
+
-
+
+
+
+
+
-
+
-
+
+
+
+
+
+
+
+
+
+
+
+
-
+
-
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -2612,64 +2645,49 @@
-
+
-
-
-
-
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
-
-
-
-
+
-
+
-
+
-
-
+
+
-
-
-
-
-
-
-
-
-
+
+
diff --git a/src/symbolic/symbolicInterpreter/why3shapes.gz b/src/symbolic/symbolicInterpreter/why3shapes.gz
index 8333f195..55bd1abb 100644
Binary files a/src/symbolic/symbolicInterpreter/why3shapes.gz and b/src/symbolic/symbolicInterpreter/why3shapes.gz differ
diff --git a/src/symbolic/symbolicUtility.ml b/src/symbolic/symbolicUtility.ml
index a419e265..1509df97 100644
--- a/src/symbolic/symbolicUtility.ml
+++ b/src/symbolic/symbolicUtility.ml
@@ -1,302 +1,352 @@
-open Colis_internals
open Colis_constraints
open Semantics__Result
open Semantics__Buffers
-open SymbolicInterpreter__Semantics
-
-type utility = state -> (state * bool result) list
-
-let return result : utility =
- function sta -> [sta, Ok result]
-
-let apply_to_list l u =
- (* apply utility [u] to a list [l] of states *)
- List.concat (List.map u l)
-
-let separate_states l =
- (* split a list of pairs state*bool into the list of states with flag
- [true] and the list of pairs with flag [false]
- *)
- let rec separate_aux posacc negacc incacc = function
- | [] -> (posacc,negacc,incacc)
- | (s, Ok true)::l -> separate_aux (s::posacc) negacc incacc l
- | (s, Ok false)::l -> separate_aux posacc (s::negacc) incacc l
- | (_, Incomplete) as s::l -> separate_aux posacc negacc (s::incacc) l
- in separate_aux [] [] [] l
-
-let choice u1 u2 =
- (* non-deterministic choice *)
- function state -> (u1 state) @ (u2 state)
-
-let if_then_else (cond:utility) (posbranch:utility) (negbranch:utility) =
- function sta ->
- let (posstates,negstates,incstates) = separate_states (cond sta)
- in
- (apply_to_list posstates posbranch)
- @ (apply_to_list negstates negbranch)
- @ incstates
-let if_then (cond:utility) (posbranch:utility) =
- function sta ->
- let (posstates,negstates,incstates) = separate_states (cond sta)
- in
- (apply_to_list posstates posbranch)
- @ (List.map (function sta -> (sta,Ok true)) negstates)
- @ incstates
-
-let uneg (u:utility) : utility = fun st ->
- List.map (function (s,Ok b) -> (s, Ok (not b)) | x -> x) (u st)
-
-let combine_results combinator u1 u2 : utility = fun st ->
- List.flatten
- (List.map
- (function (s1,Ok b1) ->
- List.map (function
- | (s2,Ok b2) -> (s2,Ok(combinator b1 b2))
- | x -> x) (u2 s1)
- | x -> [x])
- (u1 st))
-
-let uand =
- combine_results ( && )
-
-let uor =
- combine_results ( || )
-
-let multiple_times what args : utility =
- let rec aux = function
- | [] -> assert false (* By precondition. *)
- | [x] -> what x
- | x :: xs -> uand (what x) (aux xs)
- in
- aux args
-
-let compose_non_strict (u1:utility) (u2:utility) =
- function sta ->
- apply_to_list (List.map fst (u1 sta)) u2
-
-let compose_strict (u1:utility) (u2:utility) =
- function sta ->
- let (success1,failure1,incomplete1) = separate_states (u1 sta)
- in (apply_to_list success1 u2) @
- (List.map (function sta -> (sta,Ok false)) failure1) @
- incomplete1
-
-let print_output ~newline str output =
- let output = Stdout.output str output in
- if newline then Stdout.newline output else output
-
-let print_stdout ~newline str sta =
- let stdout = print_output ~newline str sta.stdout in
- let log = print_output ~newline str sta.log in
- {sta with stdout; log}
-
-let print_error str sta =
- let log = print_output ~newline:true ("[ERROR] "^str) sta.log in
- {sta with log}
-
-let print_utility_trace str sta =
- if String.equal str "" then
- sta
- else
- let log =
- print_output ~newline:true ("[TRACE] "^str) sta.log in
- {sta with log}
+module type FILESYSTEM = sig
+ type filesystem
+end
-let print_incomplete_trace str sta =
- if String.equal str "" then
- sta
- else
- let log = print_output ~newline:true ("[INCOMPLETE] "^str) sta.log in
- {sta with log}
+module type CASESPEC = sig
+ type case_spec
+ val noop : case_spec
+ type filesystem
+ val apply_spec : filesystem -> case_spec -> filesystem list
+end
-type case_spec = Var.t -> Var.t -> Clause.t
+module Make (Filesystem: FILESYSTEM) = struct
-let noop : case_spec =
- Clause.eq
+ module Semantics = SymbolicInterpreter__Interpreter.MakeSemantics (Filesystem)
+ open Semantics
-type case = {
- result : bool result;
- spec : case_spec;
- descr : string;
- stdout : Stdout.t ;
- error_message: string option;
-}
+ type utility = state -> (state * bool result) list
+
+ let print_output ~newline str output =
+ let output = Stdout.output str output in
+ if newline then Stdout.newline output else output
-let success_case ~descr ?(stdout=Stdout.empty) spec =
- { result = Ok true ; error_message = None ; stdout ; descr; spec }
-
-let error_case ~descr ?(stdout=Stdout.empty) ?error_message spec =
- { result = Ok false ; error_message ; stdout ; descr ; spec }
-
-let incomplete_case ~descr spec =
- { result = Incomplete ;
- descr ;
- stdout = Stdout.empty ;
- error_message = None;
- spec }
-
-(** Apply the case specifications to a filesystem, resulting in a list of possible filesystems. *)
-let apply_spec fs spec =
- let open SymbolicInterpreter__Filesystem in
- let root_is_root0 =
- (* fs.root0 = Some fs.root - garbare-collect fs.root only otherwise *)
- match fs.root0 with
- | Some root0 -> Var.equal root0 fs.root
- | None -> false in
- let root' = Var.fresh ~hint:(Var.hint fs.root) () in
- let clause = spec fs.root root' in
- let clauses = Clause.add_to_sat_conj clause fs.clause in
- let clauses =
- if root_is_root0 then
- clauses
+ let print_stdout ~newline str sta =
+ let stdout = print_output ~newline str sta.stdout in
+ let log = print_output ~newline str sta.log in
+ {sta with stdout; log}
+
+ let print_error str sta =
+ let log = print_output ~newline:true ("[ERROR] "^str) sta.log in
+ {sta with log}
+
+ let print_utility_trace str sta =
+ if String.equal str "" then
+ sta
else
- List.flatten
- (List.map (Clause.quantify_over_and_simplify fs.root)
- clauses) in
- List.map (fun clause -> {fs with clause; root=root'}) clauses
-
-(** Apply a case to a state.
-
- This may result in multiple states because the integration of the case clause in the
- filesystem may result in multiple clauses. *)
-let apply_case sta case : (state * bool result) list =
- (* First print the utility trace *)
- let sta =
- if case.result = Incomplete
- then sta (* Print incomplete trace last *)
- else print_utility_trace case.descr sta in
- let sta = {
- (* output case stdout to stdout and log *)
- stdout = Stdout.concat sta.stdout case.stdout;
- log = Stdout.concat sta.log case.stdout;
- (* don't touch stdin *)
- stdin = sta.stdin;
- (* and keep the filesystem (may be changed by apply_spec) *)
- filesystem = sta.filesystem;
- } in
- (* (Optionally) print error message *)
- let sta =
- match case.error_message with
- | Some msg -> print_error msg sta
- | None -> sta in
- let sta =
- if case.result = Incomplete
- then print_incomplete_trace case.descr sta
- else sta in
- (* Apply the case specifications to the filesystem *)
- apply_spec sta.filesystem case.spec |>
- (* Inject the resulting filesystems into the state *)
- List.map (fun filesystem -> {sta with filesystem}) |>
- (* Add the result to each result state *)
- List.map (fun sta -> sta, case.result)
-
-let specification_cases cases state =
- List.flatten (List.map (apply_case state) cases)
-
-(******************************************************************************)
-(* Auxiliaries *)
-(******************************************************************************)
-
-let last_comp_as_hint: root:Var.t -> Path.t -> string option =
- fun ~root path ->
- match Path.split_last path with
- | Some (_, Down f) ->
- Some (Feat.to_string f)
- | None -> (* Empty parent path => root *)
- Some (Var.hint root)
- | Some (_, (Here|Up)) ->
- (* We can’t know (if last component in parent path is a symbolic link) *)
- None
+ let log = print_output ~newline:true ("[TRACE] "^str) sta.log in
+ {sta with log}
-let error ~utility msg : utility =
- fun sta ->
- let str = utility ^ ": " ^ msg in
- let sta' = print_error str sta in
- [ sta', Ok false ]
+ let print_incomplete_trace str sta =
+ let log = print_output ~newline:true ("[INCOMPLETE] "^str) sta.log in
+ {sta with log}
-let incomplete ~utility msg : utility =
- fun sta ->
+ let error ~utility msg : utility =
+ fun sta ->
let str = utility ^ ": " ^ msg in
- [print_incomplete_trace str sta, Incomplete]
+ let sta = print_error str sta in
+ [sta, Ok false]
-let unknown ~utility msg : utility =
- match !Options.unknown_behaviour with
- | Exception -> raise (Errors.Unknown_behaviour (utility, msg))
- | Incomplete -> incomplete ~utility msg
- | Error -> error ~utility "not found"
+ let incomplete ~utility msg : utility =
+ fun sta ->
+ let str = utility ^ ": " ^ msg in
+ let sta = print_incomplete_trace str sta in
+ [sta, Incomplete]
+
+ let unknown ~utility msg : utility =
+ let open Colis_internals in
+ match !Options.unknown_behaviour with
+ | Exception -> raise (Errors.Unknown_behaviour (utility, msg))
+ | Incomplete -> incomplete ~utility msg
+ | Error -> error ~utility "not found"
+
+ let table : (string, utility_context -> utility) Hashtbl.t =
+ let table = Hashtbl.create 10 in
+ (* TODO Register all POSIX utilities as: incomplete ~descr:(name^": not implemented") *)
+ table
+
+ module type SYMBOLIC_UTILITY = sig
+ val name : string
+ val interprete : utility_context -> utility
+ end
+
+ let register (module M: SYMBOLIC_UTILITY) =
+ Hashtbl.replace table M.name M.interprete
+
+ let is_registered = Hashtbl.mem table
+
+ let dispatch ~name =
+ try Hashtbl.find table name
+ with Not_found ->
+ fun _ctx sta ->
+ unknown ~utility:name "command not found" sta
-module IdMap = Env.IdMap
+ module Arg = struct
+ let sym_interp_utility (ctx, name, sta) =
+ dispatch ~name ctx sta
+ end
+
+ module Interpreter = MakeInterpreter (Arg)
+
+ type sym_state = {
+ context : Semantics__Context.context;
+ state : Semantics.state;
+ }
+
+ let interp_program inp stas pro =
+ let stas = List.map (fun {context; state} -> Interpreter.({context; state; data=()})) stas in
+ Interpreter.interp_program inp stas pro
+
+ let call name ctx args =
+ dispatch ~name {ctx with args}
+
+ let return result : utility =
+ function sta ->
+ [sta, Ok result]
+
+ let apply_to_list l u =
+ (* apply utility [u] to a list [l] of states *)
+ List.concat (List.map u l)
+
+ let separate_states l =
+ (* split a list of pairs state*bool into the list of states with flag
+ [true] and the list of pairs with flag [false]
+ *)
+ let rec separate_aux posacc negacc incacc = function
+ | [] -> (posacc,negacc,incacc)
+ | (s, Ok true)::l -> separate_aux (s::posacc) negacc incacc l
+ | (s, Ok false)::l -> separate_aux posacc (s::negacc) incacc l
+ | (_, Incomplete) as s::l -> separate_aux posacc negacc (s::incacc) l
+ in separate_aux [] [] [] l
+
+ let choice u1 u2 =
+ (* non-deterministic choice *)
+ function state -> (u1 state) @ (u2 state)
+
+ let if_then_else (cond:utility) (posbranch:utility) (negbranch:utility) =
+ function sta ->
+ let (posstates,negstates,incstates) = separate_states (cond sta)
+ in
+ (apply_to_list posstates posbranch)
+ @ (apply_to_list negstates negbranch)
+ @ incstates
+
+ let if_then (cond:utility) (posbranch:utility) =
+ function sta ->
+ let (posstates,negstates,incstates) = separate_states (cond sta)
+ in
+ (apply_to_list posstates posbranch)
+ @ (List.map (function sta -> (sta,Ok true)) negstates)
+ @ incstates
+
+ let uneg (u:utility) : utility = fun st ->
+ List.map (function (s,Ok b) -> (s, Ok (not b)) | x -> x) (u st)
+
+ let combine_results combinator u1 u2 : utility = fun st ->
+ List.flatten
+ (List.map
+ (function (s1,Ok b1) ->
+ List.map (function
+ | (s2,Ok b2) -> (s2,Ok(combinator b1 b2))
+ | x -> x) (u2 s1)
+ | x -> [x])
+ (u1 st))
+
+ let uand =
+ combine_results ( && )
+
+ let uor =
+ combine_results ( || )
+
+ let multiple_times what args : utility =
+ let rec aux = function
+ | [] -> assert false (* By precondition. *)
+ | [x] -> what x
+ | x :: xs -> uand (what x) (aux xs)
+ in
+ aux args
+
+ let compose_non_strict (u1:utility) (u2:utility) =
+ function sta ->
+ apply_to_list (List.map fst (u1 sta)) u2
+
+ let compose_strict (u1:utility) (u2:utility) =
+ function sta ->
+ let (success1,failure1,incomplete1) = separate_states (u1 sta)
+ in (apply_to_list success1 u2) @
+ (List.map (function sta -> (sta,Ok false)) failure1) @
+ incomplete1
+
+ (******************************************************************************)
+ (* Auxiliaries *)
+ (******************************************************************************)
+
+ let null_formatter = Format.make_formatter (fun _ _ _ -> ()) (fun () -> ())
+
+ let with_formatter_to_string f =
+ let buf = Buffer.create 8 in
+ let fmt = Format.formatter_of_buffer buf in
+ let v =f fmt in
+ Format.pp_print_flush fmt ();
+ (Buffer.contents buf, v)
+
+ let cmdliner_eval_utility ~utility ?(empty_pos_args=false) fun_and_args ctx =
+ let pos_args = Cmdliner.Arg.(
+ (if empty_pos_args then value else non_empty)
+ & pos_all string []
+ & info [])
+ in
+ let argv = ctx.args |> List.cons utility |> Array.of_list in
+ let (err, result) =
+ with_formatter_to_string @@ fun err ->
+ Cmdliner.Term.(
+ eval
+ (
+ fun_and_args $ const ctx $ pos_args,
+ info utility ~exits:default_exits
+ )
+ ~argv
+ ~env:(fun var -> Env.SMap.find_opt var ctx.env)
+ ~help:null_formatter ~err ~catch:false
+ )
+ in
+ match result with
+ | `Ok a -> a
+ | `Version -> error ~utility "version"
+ | `Help -> error ~utility "help"
+ | `Error (`Parse | `Term) -> unknown ~utility ("parse error: " ^ err)
+ | `Error `Exn -> assert false (* because ~catch:false *)
+
+ (**/**)
+
+ module MakeSpecifications (CaseSpec: CASESPEC with type filesystem = Filesystem.filesystem) = struct
+
+ type case = {
+ result : bool result;
+ spec : CaseSpec.case_spec;
+ descr : string;
+ stdout : Stdout.t ;
+ error_message: string option;
+ }
+
+ let success_case ~descr ?(stdout=Stdout.empty) spec =
+ { result = Ok true ; error_message = None ; stdout ; descr; spec }
+
+ let error_case ~descr ?(stdout=Stdout.empty) ?error_message spec =
+ { result = Ok false ; error_message ; stdout ; descr ; spec }
+
+ let incomplete_case ~descr spec =
+ { result = Incomplete ;
+ descr ;
+ stdout = Stdout.empty ;
+ error_message = None;
+ spec }
+
+ (** Apply a case to a state.
+
+ This may result in multiple states because the integration of the case clause in the
+ filesystem may result in multiple clauses. *)
+ let apply_case sta case : (state * bool result) list =
+ (* First print the utility trace *)
+ let sta =
+ if case.result = Incomplete
+ then sta (* Print incomplete trace last *)
+ else print_utility_trace case.descr sta in
+ let sta = {
+ (* output case stdout to stdout and log *)
+ stdout = Stdout.concat sta.stdout case.stdout;
+ log = Stdout.concat sta.log case.stdout;
+ (* don't touch stdin *)
+ stdin = sta.stdin;
+ (* and keep the filesystem (may be changed by apply_spec) *)
+ filesystem = sta.filesystem;
+ } in
+ (* (Optionally) print error message *)
+ let sta =
+ match case.error_message with
+ | Some msg -> print_error msg sta
+ | None -> sta in
+ let sta =
+ if case.result = Incomplete
+ then print_incomplete_trace case.descr sta
+ else sta in
+ (* Apply the case specifications to the filesystem *)
+ CaseSpec.apply_spec sta.filesystem case.spec |>
+ (* Inject the resulting filesystems into the state *)
+ List.map (fun filesystem -> {sta with filesystem}) |>
+ (* Add the result to each result state *)
+ List.map (fun sta -> sta, case.result)
+
+ let specification_cases cases state =
+ List.flatten (List.map (apply_case state) cases)
+ end
+end
-type context = {
- args: string list;
- cwd: Path.normal;
- env: string IdMap.t;
+type symbolic_filesystem = {
+ root: Var.t;
+ clause: Clause.sat_conj;
+ root0: Var.t option;
}
-module type SYMBOLIC_UTILITY = sig
- val name : string
- val interprete : context -> utility
+module SymbolicImplementation = struct
+
+ type case_spec = Var.t -> Var.t -> Clause.t
+
+ let noop = Clause.eq
+
+ type filesystem = symbolic_filesystem
+
+ (** Apply the case specifications to a filesystem, resulting in a list of possible filesystems. *)
+ let apply_spec fs spec =
+ let root_is_root0 =
+ (* fs.root0 = Some fs.root - garbare-collect fs.root only otherwise *)
+ match fs.root0 with
+ | Some root0 -> Var.equal root0 fs.root
+ | None -> false in
+ let root' = Var.fresh ~hint:(Var.hint fs.root) () in
+ let clause = spec fs.root root' in
+ let clauses = Clause.add_to_sat_conj clause fs.clause in
+ let clauses =
+ if root_is_root0 then
+ clauses
+ else
+ List.flatten
+ (List.map (Clause.quantify_over_and_simplify fs.root)
+ clauses) in
+ List.map (fun clause -> {fs with clause; root=root'}) clauses
end
-let table =
- let table = Hashtbl.create 10 in
- (* TODO Register all POSIX utilities as: incomplete ~descr:(name^": not implemented") *)
- table
+module Symbolic = struct
-let register (module M:SYMBOLIC_UTILITY) =
- Hashtbl.replace table M.name M.interprete
+ include Make (SymbolicImplementation)
-let is_registered = Hashtbl.mem table
+ include MakeSpecifications (SymbolicImplementation)
-let dispatch ~name =
- try Hashtbl.find table name
- with Not_found ->
- fun _ctx sta ->
- unknown ~utility:name "command not found" sta
+ type context = Semantics.utility_context = {
+ cwd: Colis_constraints.Path.normal;
+ env: string Env.SMap.t;
+ args: string list;
+ }
-let call name ctx args =
- dispatch ~name {ctx with args}
-
-let dispatch' (cwd, env, args) name sta =
- let cwd = List.map Colis_constraints.Feat.from_string cwd in
- let ctx = {cwd; args; env} in
- BatSet.of_list (dispatch ~name ctx sta)
-
-(**/**)
-
-let null_formatter = Format.make_formatter (fun _ _ _ -> ()) (fun () -> ())
-
-let with_formatter_to_string f =
- let buf = Buffer.create 8 in
- let fmt = Format.formatter_of_buffer buf in
- let v =f fmt in
- Format.pp_print_flush fmt ();
- (Buffer.contents buf, v)
-
-let cmdliner_eval_utility ~utility ?(empty_pos_args=false) fun_and_args ctx =
- let pos_args = Cmdliner.Arg.(
- (if empty_pos_args then value else non_empty)
- & pos_all string []
- & info [])
- in
- let argv = ctx.args |> List.cons utility |> Array.of_list in
- let (err, result) =
- with_formatter_to_string @@ fun err ->
- Cmdliner.Term.(
- eval
- (
- fun_and_args $ const ctx $ pos_args,
- info utility ~exits:default_exits
- )
- ~argv
- ~env:(fun var -> Env.IdMap.find_opt var ctx.env)
- ~help:null_formatter ~err ~catch:false
- )
- in
- match result with
- | `Ok a -> a
- | `Version -> error ~utility "version"
- | `Help -> error ~utility "help"
- | `Error (`Parse | `Term) -> unknown ~utility ("parse error: " ^ err)
- | `Error `Exn -> assert false (* because ~catch:false *)
+ type filesystem = symbolic_filesystem = {
+ root: Var.t;
+ clause: Clause.sat_conj;
+ root0: Var.t option;
+ }
+
+ let noop = SymbolicImplementation.noop
+
+ let last_comp_as_hint: root:Var.t -> Path.t -> string option =
+ fun ~root path ->
+ match Path.split_last path with
+ | Some (_, Down f) ->
+ Some (Feat.to_string f)
+ | None -> (* Empty parent path => root *)
+ Some (Var.hint root)
+ | Some (_, (Here|Up)) ->
+ (* We can’t know (if last component in parent path is a symbolic link) *)
+ None
+end
diff --git a/src/symbolic/symbolicUtility.mli b/src/symbolic/symbolicUtility.mli
index a65a76c4..dfc4f55e 100644
--- a/src/symbolic/symbolicUtility.mli
+++ b/src/symbolic/symbolicUtility.mli
@@ -1,150 +1,203 @@
open Colis_constraints
-open SymbolicInterpreter__Semantics
-open Semantics__Result
+open Syntax__Syntax
open Semantics__Buffers
+open Semantics__Context
+open Semantics__Input
+open Semantics__Result
-(** {1 Basics of symbolic utility} *)
+(** Definition of a symbolic filesystem to instantiate the symbolic interpreter *)
+module type FILESYSTEM = sig
+ type filesystem
+end
-(** A utility transforms a symbolic state into a list of symbolic states
- with boolean results *)
-type utility = state -> (state * bool result) list
+(** Definition of a case specification and its application to a filesystem to define
+ utilities by specifications. *)
+module type CASESPEC = sig
-(** The concrete evaluation context. It contains the fields from
- Colis.Semantics.Context.context that are relevant to the utilities. *)
-type context = {
- args: string list; (** Command arguments *)
- cwd: Path.normal; (** Current working directory *)
- env: string Env.IdMap.t; (** Variable environment *)
-}
+ (** A case specification is a function from the old root variable and the new root root
+ variable to a clause. *)
+ type case_spec
+
+ (** The no-op case specification introduces an equality constraint between the old root
+ and the new root. *)
+ val noop : case_spec
-(** A symbolic utility is comprised of a name and a function that interpretes a [utility]
- in a [context]. *)
-module type SYMBOLIC_UTILITY = sig
- val name : string
- val interprete : context -> utility
+ type filesystem
+
+ (** Apply a case specification to a filesystem, resulting in possible multiple new
+ filesystems *)
+ val apply_spec : filesystem -> case_spec -> filesystem list
end
-(** {1 Specifications of a symbolic utility} *)
+module Make (Filesystem: FILESYSTEM) : sig
+
+ module Semantics : module type of SymbolicInterpreter__Interpreter.MakeSemantics (Filesystem)
+
+ open Semantics
-(** A case in the specification is either a success or an error *)
-type case
+ (** {1 Interpretation of a colis program} *)
-(** A case specification is a function from the old root variable and the new root root
- variable to a clause. *)
-type case_spec = Var.t -> Var.t -> Clause.t
+ type sym_state = {
+ context : context;
+ state : state;
+ }
-(** The no-op case specification introduces an equality constraint between the old root
- and the new root. *)
-val noop : case_spec
+ (** [interp_program inp stas p] symbolic interpretation configured by [inp] of a program
+ [p] in a list of symbolic input states [stas]. Returns the symbolic states
+ representing successful, errorneous, and incomplete interpretation. *)
+ val interp_program : input -> sym_state list -> program -> state list * state list * state list
-(** A success case (aka. return 0) *)
-val success_case: descr:string -> ?stdout:Stdout.t -> case_spec -> case
+ (** {1 Basics of symbolic utility} *)
-(** An error case (aka return 1) *)
-val error_case: descr:string -> ?stdout:Stdout.t -> ?error_message:string -> case_spec -> case
+ (** A utility transforms a symbolic state into a list of symbolic states
+ with boolean results *)
+ type utility = state -> (state * bool result) list
-(** An incomplete case (unknown behaviour, cannot be symbolically executed) *)
-val incomplete_case: descr:string -> case_spec -> case
+ (** {1 Registration and dispatch of utilities} *)
-(** Use a list of cases to specify a utility. Corresponds to a table in the
- document "Specification of UNIX Utilities "*)
-val specification_cases : case list -> utility
+ (** A symbolic utility is comprised of a name and a function that interpretes a [utility]
+ in a [context]. *)
+ module type SYMBOLIC_UTILITY = sig
+ val name : string
+ val interprete : utility_context -> utility
+ end
-(** {1 Registration} *)
+ (** Register a symbolic utility *)
+ val register : (module SYMBOLIC_UTILITY) -> unit
-(** Register a symbolic utility *)
-val register : (module SYMBOLIC_UTILITY) -> unit
+ val is_registered : string -> bool
-val is_registered : string -> bool
+ (** A saner way to call [dispatch] (e.g. in the implementation of utilities) *)
+ val call : string -> utility_context -> string list -> utility
-(** {1 Dispatch} *)
+ (** {1 Basic utilities} *)
-(** Entry-point for the interpretation of symbolic utilties *)
-val dispatch : name:string -> context -> utility
+ (** Error utility *)
+ val error : utility:string -> string -> utility
-(** A saner way to call [dispatch] (e.g. in the implementation of utilities) *)
-val call : string -> context -> string list -> utility
+ (** Unsupported stuff in a known utility. *)
+ val incomplete : utility:string -> string -> utility
-(** {1 Combinators} *)
+ (* Unknown-unknown behaviour *)
+ val unknown : utility:string -> string -> utility
-(** [choice u1 u2] yields the utility that non-deterministacillay
- behaves like [u1] or [u2]. *)
-val choice : utility -> utility -> utility
+ (** {2 Printing} *)
-(** [return b] yields the utility that does not change its state, and
- succeeds if and only if [b] is [true] *)
-val return : bool -> utility
+ (** Print to stdout and log *)
+ val print_stdout : newline:bool -> string -> state -> state
-(** [if_then_else u1 u2 u3] yields the utility that behaves like
- if [u1] then [u2] else [u3] fi *)
-val if_then_else : utility -> utility -> utility -> utility
+ (** Print message as utility trace to log if it is not empty (marked as [UTL]) *)
+ val print_utility_trace : string -> state -> state
-(** [if_then u1 u2] yields the utility that behaves like
- if [u1] then [u2] fi *)
-val if_then : utility -> utility -> utility
+ (** {1 Utility combinators} *)
-(** [uneg u] yields the utility that behaves like [u] but inverts its result *)
-val uneg : utility -> utility
+ (** [choice u1 u2] yields the utility that non-deterministacillay
+ behaves like [u1] or [u2]. *)
+ val choice : utility -> utility -> utility
-(** [uand u1 u2] yields the utility that behaves like [u1 && u2] in a NON-LAZY manner *)
-val uand : utility -> utility -> utility
+ (** [return b] yields the utility that does not change its state, and
+ succeeds if and only if [b] is [true] *)
+ val return : bool -> utility
-(** [uor u1 u2] yields the utility that behaves like [u1 || u2] in a NON-LAZY manner *)
-val uor : utility -> utility -> utility
+ (** [if_then_else u1 u2 u3] yields the utility that behaves like
+ if [u1] then [u2] else [u3] fi *)
+ val if_then_else : utility -> utility -> utility -> utility
-(** multiple_times [what] [args] executes [what] on every argument in
- [args]. It does not stop if one of these executions fails but the
- global utility fails in the case. *)
-val multiple_times : ('a -> utility) -> 'a list -> utility
+ (** [if_then u1 u2] yields the utility that behaves like
+ if [u1] then [u2] fi *)
+ val if_then : utility -> utility -> utility
-(** compose_non_strict [u1] [u2] yields the utility that behaves like
- [u1]; [u2] in non-strict mode, that is the error code of [u1] is
- ignored *)
-val compose_non_strict : utility -> utility -> utility
+ (** [uneg u] yields the utility that behaves like [u] but inverts its result *)
+ val uneg : utility -> utility
-(** compose_strict [u1] [u2] yields the utility that behaves like
- [u1]; [u2] in strict mode, that is if [u1] fails then the composition
- fails and [u2] is not executed *)
-val compose_strict : utility -> utility -> utility
+ (** [uand u1 u2] yields the utility that behaves like [u1 && u2] in a NON-LAZY manner *)
+ val uand : utility -> utility -> utility
-(** {1 Auxiliaries} *)
+ (** [uor u1 u2] yields the utility that behaves like [u1 || u2] in a NON-LAZY manner *)
+ val uor : utility -> utility -> utility
-(** Error utility *)
-val error : utility:string -> string -> utility
+ (** multiple_times [what] [args] executes [what] on every argument in
+ [args]. It does not stop if one of these executions fails but the
+ global utility fails in the case. *)
+ val multiple_times : ('a -> utility) -> 'a list -> utility
-(** Unsupported stuff in a known utility. *)
-val incomplete : utility:string -> string -> utility
+ (** compose_non_strict [u1] [u2] yields the utility that behaves like
+ [u1]; [u2] in non-strict mode, that is the error code of [u1] is
+ ignored *)
+ val compose_non_strict : utility -> utility -> utility
-(* Unknown-unknown behaviour *)
-val unknown : utility:string -> string -> utility
+ (** compose_strict [u1] [u2] yields the utility that behaves like
+ [u1]; [u2] in strict mode, that is if [u1] fails then the composition
+ fails and [u2] is not executed *)
+ val compose_strict : utility -> utility -> utility
-(** {2 Printing} *)
+ (** {1 Arguments Parsing} *)
-(** Print to stdout and log *)
-val print_stdout : newline:bool -> string -> state -> state
+ val cmdliner_eval_utility :
+ utility:string ->
+ ?empty_pos_args:bool ->
+ (utility_context -> string list -> utility) Cmdliner.Term.t ->
+ utility_context -> utility
+ (** A wrapper around [Cmdliner.Term.eval] for utilities. [utility] is the name
+ of the utility. [empty_pos_args] describe whether empty positional arguments
+ lists are accepted or not (refused by default). *)
-(** Print message as utility trace to log if it is not empty (marked as [UTL]) *)
-val print_utility_trace : string -> state -> state
+ (** {1 Specifications of a symbolic utility} *)
-(** {2 Path parsing}*)
+ module MakeSpecifications (CaseSpec: CASESPEC with type filesystem = Filesystem.filesystem) : sig
-(** Get the name of the last path component, if any, or of the hint
- root variable otherwise. The result is useful as a hint for
- creating variables for resolving the path. *)
-val last_comp_as_hint: root:Var.t -> Path.t -> string option
+ (** A case in the specification is either a success, an error, or incomplete *)
+ type case
-(** {2 Arguments Parsing} *)
+ (** A success case (aka. return 0) *)
+ val success_case: descr:string -> ?stdout:Stdout.t -> CaseSpec.case_spec -> case
-val cmdliner_eval_utility :
- utility:string ->
- ?empty_pos_args:bool ->
- (context -> string list -> utility) Cmdliner.Term.t ->
- context -> utility
-(** A wrapper around [Cmdliner.Term.eval] for utilities. [utility] is the name
- of the utility. [empty_pos_args] describe whether empty positional arguments
- lists are accepted or not (refused by default). *)
+ (** An error case (aka return 1) *)
+ val error_case: descr:string -> ?stdout:Stdout.t -> ?error_message:string -> CaseSpec.case_spec -> case
-(**/**)
+ (** An incomplete case (unknown behaviour, cannot be symbolically executed) *)
+ val incomplete_case: descr:string -> CaseSpec.case_spec -> case
+
+ (** Use a list of cases to specify a utility. Corresponds to a table in the
+ document "Specification of UNIX Utilities "*)
+ val specification_cases : case list -> utility
+ end
+end
-(** A wrapper of [dispatch] for use in the Why3 driver *)
-val dispatch' : (string list * string Env.IdMap.t * string list) -> string -> state -> (state * bool result) BatSet.t
+type symbolic_filesystem = {
+ root: Var.t;
+ clause: Clause.sat_conj;
+ root0: Var.t option;
+}
+
+(** Parameterization of the symbolic engine for constraint-based filesystem
+ [symbolic_filesystem] *)
+module SymbolicImplementation : CASESPEC
+ with type filesystem = symbolic_filesystem
+ and type case_spec = Var.t -> Var.t -> Clause.t
+
+(* Compatibility with module SymbolicUtility before functorization of the symbolic engine *)
+module Symbolic : sig
+
+ include module type of Make (SymbolicImplementation)
+ include module type of MakeSpecifications (SymbolicImplementation)
+
+ type context = Semantics.utility_context = {
+ cwd: Path.normal;
+ env: string Env.SMap.t;
+ args: string list;
+ }
+
+ type filesystem = symbolic_filesystem = {
+ root: Var.t;
+ clause: Clause.sat_conj;
+ root0: Var.t option;
+ }
+
+ val noop : SymbolicImplementation.case_spec
+
+ (** Get the name of the last path component, if any, or of the hint
+ root variable otherwise. The result is useful as a hint for
+ creating variables for resolving the path. *)
+ val last_comp_as_hint: root:Var.t -> Path.t -> string option
+end
diff --git a/src/symbolic/utilities/basics.ml b/src/symbolic/utilities/basics.ml
index 58cff4ff..8f10a5a9 100644
--- a/src/symbolic/utilities/basics.ml
+++ b/src/symbolic/utilities/basics.ml
@@ -1,5 +1,4 @@
-open SymbolicUtility
-
+open SymbolicUtility.Symbolic
module True = struct
let name = "true"
diff --git a/src/symbolic/utilities/colisInternalUnsafeTouch.ml b/src/symbolic/utilities/colisInternalUnsafeTouch.ml
index 44c6a86d..c52e4447 100644
--- a/src/symbolic/utilities/colisInternalUnsafeTouch.ml
+++ b/src/symbolic/utilities/colisInternalUnsafeTouch.ml
@@ -1,7 +1,7 @@
open Format
open Colis_constraints
open Clause
-open SymbolicUtility
+open SymbolicUtility.Symbolic
let name = "colis_internal_unsafe_touch"
diff --git a/src/symbolic/utilities/cp.ml b/src/symbolic/utilities/cp.ml
index 33b8835b..4adce308 100644
--- a/src/symbolic/utilities/cp.ml
+++ b/src/symbolic/utilities/cp.ml
@@ -1,8 +1,7 @@
open Format
open Colis_constraints
open Clause
-open SymbolicUtility
-
+open SymbolicUtility.Symbolic
let name = "cp"
(*
diff --git a/src/symbolic/utilities/cp.mli b/src/symbolic/utilities/cp.mli
index 7cc30031..269cb613 100644
--- a/src/symbolic/utilities/cp.mli
+++ b/src/symbolic/utilities/cp.mli
@@ -1,4 +1,5 @@
(** Symbolic execution of cp *)
+open SymbolicUtility.Symbolic
val name : string
-val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+val interprete : context -> utility
diff --git a/src/symbolic/utilities/dpkg.ml b/src/symbolic/utilities/dpkg.ml
index 8121487f..19dd5340 100644
--- a/src/symbolic/utilities/dpkg.ml
+++ b/src/symbolic/utilities/dpkg.ml
@@ -1,4 +1,4 @@
-open SymbolicUtility
+open SymbolicUtility.Symbolic
open Semantics__Result
let name = "dpkg"
diff --git a/src/symbolic/utilities/dpkgMaintscriptHelper.ml b/src/symbolic/utilities/dpkgMaintscriptHelper.ml
index 8db76ea4..85fdb309 100644
--- a/src/symbolic/utilities/dpkgMaintscriptHelper.ml
+++ b/src/symbolic/utilities/dpkgMaintscriptHelper.ml
@@ -1,7 +1,7 @@
(** Symbolic execution of dpkg-maintscript-helper. The structure of
this code follows the implementation of version 1.19.6. *)
-open SymbolicUtility
+open SymbolicUtility.Symbolic
let name = "dpkg-maintscript-helper"
@@ -429,19 +429,19 @@ let interprete ctx =
sub-commands except 'supports' has been factored out into the
main code. *)
let dms_package =
- try Env.IdMap.find "DPKG_MAINTSCRIPT_PACKAGE" ctx.env
+ try Env.SMap.find "DPKG_MAINTSCRIPT_PACKAGE" ctx.env
with Not_found ->
raise (Error
"environment variable DPKG_MAINTSCRIPT_PACKAGE is required")
in
let default_package =
try
- let dpkg_arch = Env.IdMap.find "DPKG_MAINTSCRIPT_ARCH" ctx.env
+ let dpkg_arch = Env.SMap.find "DPKG_MAINTSCRIPT_ARCH" ctx.env
in dms_package^":"^dpkg_arch
with Not_found -> dms_package
in
let dms_name =
- try Env.IdMap.find "DPKG_MAINTSCRIPT_NAME" ctx.env
+ try Env.SMap.find "DPKG_MAINTSCRIPT_NAME" ctx.env
with
| Not_found ->
raise (Error
diff --git a/src/symbolic/utilities/dpkgMaintscriptHelper.mli b/src/symbolic/utilities/dpkgMaintscriptHelper.mli
index 5b26b47b..93aaf109 100644
--- a/src/symbolic/utilities/dpkgMaintscriptHelper.mli
+++ b/src/symbolic/utilities/dpkgMaintscriptHelper.mli
@@ -1,4 +1,5 @@
(** Symbolic execution of dpkg-maintscript-helper *)
+open SymbolicUtility.Symbolic
val name : string
-val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+val interprete : context -> utility
diff --git a/src/symbolic/utilities/emacsPackage.ml b/src/symbolic/utilities/emacsPackage.ml
index 1bba2484..5a017050 100644
--- a/src/symbolic/utilities/emacsPackage.ml
+++ b/src/symbolic/utilities/emacsPackage.ml
@@ -1,5 +1,5 @@
open Format
-open SymbolicUtility
+open SymbolicUtility.Symbolic
module Install = struct
let name = "/usr/lib/emacsen-common/emacs-package-install"
diff --git a/src/symbolic/utilities/emacsPackage.mli b/src/symbolic/utilities/emacsPackage.mli
index c7eba2ee..789ced53 100644
--- a/src/symbolic/utilities/emacsPackage.mli
+++ b/src/symbolic/utilities/emacsPackage.mli
@@ -1,13 +1,14 @@
(** Symbolic execution of emacs-package-[install|remove] *)
+open SymbolicUtility.Symbolic
module Install : sig
val name : string
- val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+ val interprete : context -> utility
end
module Remove : sig
val name : string
- val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+ val interprete : context -> utility
end
diff --git a/src/symbolic/utilities/mkdir.ml b/src/symbolic/utilities/mkdir.ml
index 8afbed82..79b75ee8 100644
--- a/src/symbolic/utilities/mkdir.ml
+++ b/src/symbolic/utilities/mkdir.ml
@@ -1,7 +1,7 @@
open Format
open Colis_constraints
open Clause
-open SymbolicUtility
+open SymbolicUtility.Symbolic
let name = "mkdir"
diff --git a/src/symbolic/utilities/mkdir.mli b/src/symbolic/utilities/mkdir.mli
index 72649baf..84073e65 100644
--- a/src/symbolic/utilities/mkdir.mli
+++ b/src/symbolic/utilities/mkdir.mli
@@ -1,4 +1,5 @@
(** Symbolic execution of mkdir *)
+open SymbolicUtility.Symbolic
val name : string
-val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+val interprete : context -> utility
diff --git a/src/symbolic/utilities/mv.ml b/src/symbolic/utilities/mv.ml
index e34c5b5d..44c071b0 100644
--- a/src/symbolic/utilities/mv.ml
+++ b/src/symbolic/utilities/mv.ml
@@ -1,7 +1,7 @@
open Format
open Colis_constraints
open Clause
-open SymbolicUtility
+open SymbolicUtility.Symbolic
let name = "mv"
diff --git a/src/symbolic/utilities/mv.mli b/src/symbolic/utilities/mv.mli
index adbabc34..c2f67e93 100644
--- a/src/symbolic/utilities/mv.mli
+++ b/src/symbolic/utilities/mv.mli
@@ -1,4 +1,5 @@
(** Symbolic execution of mv *)
+open SymbolicUtility.Symbolic
val name : string
-val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+val interprete : context -> utility
diff --git a/src/symbolic/utilities/rm.ml b/src/symbolic/utilities/rm.ml
index 7f36f2c4..8ec80385 100644
--- a/src/symbolic/utilities/rm.ml
+++ b/src/symbolic/utilities/rm.ml
@@ -1,7 +1,7 @@
open Format
open Colis_constraints
open Clause
-open SymbolicUtility
+open SymbolicUtility.Symbolic
let name = "rm"
diff --git a/src/symbolic/utilities/rm.mli b/src/symbolic/utilities/rm.mli
index 29043abf..122237a7 100644
--- a/src/symbolic/utilities/rm.mli
+++ b/src/symbolic/utilities/rm.mli
@@ -1,2 +1,4 @@
+open SymbolicUtility.Symbolic
+
val name : string
-val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+val interprete : context -> utility
diff --git a/src/symbolic/utilities/test.ml b/src/symbolic/utilities/test.ml
index 99896fd1..43a5985f 100644
--- a/src/symbolic/utilities/test.ml
+++ b/src/symbolic/utilities/test.ml
@@ -2,7 +2,7 @@
open Format
open Colis_constraints
open Clause
-open SymbolicUtility
+open SymbolicUtility.Symbolic
let name = "test"
diff --git a/src/symbolic/utilities/test.mli b/src/symbolic/utilities/test.mli
index c93742c8..303e4061 100644
--- a/src/symbolic/utilities/test.mli
+++ b/src/symbolic/utilities/test.mli
@@ -1,7 +1,9 @@
+open SymbolicUtility.Symbolic
+
val name : string
-val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+val interprete : context -> utility
module Bracket : sig
val name : string
- val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+ val interprete : context -> utility
end
diff --git a/src/symbolic/utilities/touch.ml b/src/symbolic/utilities/touch.ml
index efd9cfc2..31cb56da 100644
--- a/src/symbolic/utilities/touch.ml
+++ b/src/symbolic/utilities/touch.ml
@@ -1,7 +1,7 @@
open Format
open Colis_constraints
open Clause
-open SymbolicUtility
+open SymbolicUtility.Symbolic
let name = "touch"
diff --git a/src/symbolic/utilities/touch.mli b/src/symbolic/utilities/touch.mli
index 29043abf..122237a7 100644
--- a/src/symbolic/utilities/touch.mli
+++ b/src/symbolic/utilities/touch.mli
@@ -1,2 +1,4 @@
+open SymbolicUtility.Symbolic
+
val name : string
-val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+val interprete : context -> utility
diff --git a/src/symbolic/utilities/updateAlternatives.ml b/src/symbolic/utilities/updateAlternatives.ml
index 53c0e82a..e2999537 100644
--- a/src/symbolic/utilities/updateAlternatives.ml
+++ b/src/symbolic/utilities/updateAlternatives.ml
@@ -1,4 +1,4 @@
-open SymbolicUtility
+open SymbolicUtility.Symbolic
let name = "update-alternatives"
diff --git a/src/symbolic/utilities/updateMenus.ml b/src/symbolic/utilities/updateMenus.ml
index 84743e7a..000a978e 100644
--- a/src/symbolic/utilities/updateMenus.ml
+++ b/src/symbolic/utilities/updateMenus.ml
@@ -1,4 +1,4 @@
-open SymbolicUtility
+open SymbolicUtility.Symbolic
let name = "update-menus"
diff --git a/src/symbolic/utilities/updateMenus.mli b/src/symbolic/utilities/updateMenus.mli
index 29043abf..122237a7 100644
--- a/src/symbolic/utilities/updateMenus.mli
+++ b/src/symbolic/utilities/updateMenus.mli
@@ -1,2 +1,4 @@
+open SymbolicUtility.Symbolic
+
val name : string
-val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+val interprete : context -> utility
diff --git a/src/symbolic/utilities/which.ml b/src/symbolic/utilities/which.ml
index 8bf40bff..5015e7ac 100644
--- a/src/symbolic/utilities/which.ml
+++ b/src/symbolic/utilities/which.ml
@@ -1,7 +1,7 @@
open Format
open Colis_constraints
open Clause
-open SymbolicUtility
+open SymbolicUtility.Symbolic
open Semantics__Result
open Semantics__Buffers
diff --git a/src/symbolic/utilities/which.mli b/src/symbolic/utilities/which.mli
index 09391ded..bb0514f9 100644
--- a/src/symbolic/utilities/which.mli
+++ b/src/symbolic/utilities/which.mli
@@ -1,7 +1,9 @@
+open SymbolicUtility.Symbolic
+
val name : string
-val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+val interprete : context -> utility
module Silent : sig
val name : string
- val interprete : SymbolicUtility.context -> SymbolicUtility.utility
+ val interprete : context -> utility
end