From 25ae40ce9dacba0ed7a1acb7b4977ad54a114b85 Mon Sep 17 00:00:00 2001 From: Benedikt Becker Date: Sat, 8 Feb 2020 02:13:07 +0100 Subject: [PATCH] Functorize symbolic engine Fixes #116 --- Makefile | 2 +- src/concrete/driver.drv | 24 +- src/concrete/env.ml | 9 +- src/concrete/env.mli | 2 +- src/concrete/interpreter.mlw | 74 +- src/concrete/semantics.mlw | 180 +- src/language/driver.drv | 10 +- src/language/mystring.mlw | 27 - src/language/syntax.mlw | 6 +- src/symbolic/driver.drv | 23 +- src/symbolic/symbolicFilesystem.ml | 7 + src/symbolic/symbolicInterpreter.mlw | 2441 +++++++++++++------------- 12 files changed, 1409 insertions(+), 1396 deletions(-) delete mode 100644 src/language/mystring.mlw create mode 100644 src/symbolic/symbolicFilesystem.ml diff --git a/Makefile b/Makefile index f5d187e9..aa8df2fa 100644 --- a/Makefile +++ b/Makefile @@ -48,7 +48,7 @@ extract-why3: -L src/symbolic \ -o src/why3 \ interpreter.Interpreter \ - symbolicInterpreter.Interpreter + symbolicInterpreter.SymbolicInterpreter clean-why3: rm -rf src/why3 diff --git a/src/concrete/driver.drv b/src/concrete/driver.drv index 1d42d5be..67dc82f5 100644 --- a/src/concrete/driver.drv +++ b/src/concrete/driver.drv @@ -1,16 +1,26 @@ +module semantics.Paths + syntax type feature "Colis_constraints.Feat.t" + syntax val absolute_or_concat_relative "Colis_constraints.Path.(normalize ~cwd:%1 (from_string %2))" + syntax val normalized_path_to_string "Colis_constraints.Path.normal_to_string %1" +end + +module semantics.Buffers + syntax val concat_lines "String.concat \"\n\" %1" + syntax val split_on_default_ifs "Str.(split (regexp \"[ \t\n]+\") %1)" +end + module semantics.Env syntax type env "%1 Env.env" syntax val empty_env "Env.empty %1" syntax val ([]) "Env.get %1 %2" syntax val ([<-]) "Env.set %1 %2 %3" + syntax type env0 "%1 Env.IdMap.t" +end + +module semantics.Context + syntax val filter_var_env "Env.filter_var_env (fun v -> v.Semantics__Context.exported) (fun v -> v.Semantics__Context.value) %1" end -module interpreter.Semantics - syntax val filter_var_env "Env.filter_var_env (fun v -> v.Interpreter__Semantics.exported) (fun v -> v.Interpreter__Semantics.value) %1" +module interpreter.Interpreter syntax val interp_utility "Utilities.interp_utility %1 %2 %3" - syntax val normalized_path_to_string "String.concat \"/\" %1" - syntax val absolute_or_concat_relative "Utilities.absolute_or_concat_relative %1 %2" - syntax val identifier_test "\"test\"" - syntax val string_dash_d "\"-d\"" - syntax val identifier_pwd "\"PWD\"" end \ No newline at end of file diff --git a/src/concrete/env.ml b/src/concrete/env.ml index fc537cef..0bd4fb78 100644 --- a/src/concrete/env.ml +++ b/src/concrete/env.ml @@ -8,7 +8,10 @@ let map f default env = {map=IdMap.map f env.map; default} let elements env = IdMap.fold (fun k v t -> (k, v) :: t) env.map [] let to_map env = env.map -let filter_var_env (var_exported: 'a -> bool) (var_value: 'a -> string option) (env : 'a env) : string IdMap.t = +let filter_var_env (var_exported: 'a -> bool) (var_value: 'a -> 'b option) (env : 'a env) : 'b IdMap.t = + let open IdMap in env.map |> - IdMap.filter (fun _ v -> var_exported v && var_value v <> None) |> - IdMap.map (fun v -> match var_value v with Some s -> s | _ -> assert false) + filter (fun _ -> var_exported) |> + map var_value |> + filter (fun _ x -> Option.is_some x) |> + map Option.get diff --git a/src/concrete/env.mli b/src/concrete/env.mli index 442a585e..6eb58210 100644 --- a/src/concrete/env.mli +++ b/src/concrete/env.mli @@ -13,4 +13,4 @@ module IdMap : Map.S with type key = string (** Conversion to a normal map without default value *) val to_map : 'a env -> 'a IdMap.t -val filter_var_env : ('a -> bool) -> ('a -> string option) -> 'a env -> string IdMap.t +val filter_var_env : ('a -> bool) -> ('a -> 'b option) -> 'a env -> 'b IdMap.t diff --git a/src/concrete/interpreter.mlw b/src/concrete/interpreter.mlw index 68d0dc41..02540f74 100644 --- a/src/concrete/interpreter.mlw +++ b/src/concrete/interpreter.mlw @@ -11,22 +11,23 @@ end module Semantics use list.List - use mystring.String + use string.String + use Filesystem (* Instantiate the concrete semantics with our dummy filesystem *) clone export semantics.Semantics with - type filesystem = unit, - type normalized_path = list string, - val default_cwd = Nil, - axiom interp_utility_extends_output + type filesystem = Filesystem.filesystem + (* axiom interp_utility_extends_output *) end module State use ref.Ref use list.List - use mystring.String + use string.String use Filesystem + use semantics.Paths use semantics.Buffers + use semantics.Context use import Semantics as S type sem_state = state @@ -45,7 +46,7 @@ module State var_env : ref var_env; func_env : func_env; arguments: ref (list string); - cwd : ref (list string); + cwd : ref normalized_path; result : ref bool; } end @@ -64,14 +65,17 @@ module Interpreter use ref.Refint use auxiliaries.OptionGet - use mystring.String + use string.String use syntax.Syntax use semantics.Result use semantics.Buffers use semantics.Behaviour use semantics.Input use semantics.Config + use semantics.Paths + use semantics.Context as C use semantics.Env as E + use semantics.InterpUtility use Filesystem as Fs use auxiliaries.TakeDrop use import Semantics as S @@ -88,8 +92,8 @@ module Interpreter let empty_state () = { St.filesystem = ref Filesystem.empty; - St.var_env = ref S.empty_var_env; - St.func_env = S.empty_func_env; + St.var_env = ref C.empty_var_env; + St.func_env = C.empty_func_env; St.arguments = ref Nil; St.stdin = ref Stdin.empty; St.stdout = ref Stdout.empty; @@ -98,12 +102,12 @@ module Interpreter St.result = ref True; } - function sem_context (sta:state) : S.context = { - S.var_env = !(sta.var_env); - S.func_env = sta.func_env; - S.arguments = !(sta.arguments); - S.cwd = !(sta.cwd); - S.result = !(sta.result); + function sem_context (sta:state) : C.context = { + C.var_env = !(sta.var_env); + C.func_env = sta.func_env; + C.arguments = !(sta.arguments); + C.cwd = !(sta.cwd); + C.result = !(sta.result); } lemma context_same: forall sta1 sta2. @@ -140,18 +144,24 @@ module Interpreter = if andb (strict inp.under_condition) (notb !(sta.result)) then raise EExit - (** {3 Imperative wrapper around the functional interpretation of utilties} *) + (** {3 Interpretation of utilities and imperative wrapper} *) + + (** Interprete a command defined in the document *Specification of UNIX Commands*. *) + val function interp_utility (ctx: utility_context) (id: identifier) (sta: S.state) : (sta1: S.state, b: bool) + ensures { S.interp_utility (ctx, id, sta) (sta1, b) } - let interp_utility (inp:input) (sta:state) (id:identifier) (args:list string) + let interp_utility1 (inp:input) (sta:state) (id:identifier) (args:list string) returns { () -> - interp_utility (!(old sta.cwd), filter_var_env !(old sta.var_env), args) id (old sem_state sta) = (sem_state sta, !(sta.result)) /\ + let utility_ctx = (!(old sta.cwd), C.filter_var_env !(old sta.var_env), args) in + S.interp_utility (utility_ctx, id, old sem_state sta) (sem_state sta, !(sta.result)) /\ behaviour inp !(sta.result) = BNormal } raises { EExit -> - interp_utility (!(old sta.cwd), filter_var_env !(old sta.var_env), args) id (old sem_state sta) = (sem_state sta, !(sta.result)) /\ + let utility_ctx = (!(old sta.cwd), C.filter_var_env !(old sta.var_env), args) in + S.interp_utility (utility_ctx, id, old sem_state sta) (sem_state sta, !(sta.result)) /\ behaviour inp !(sta.result) = BExit } - = let sta', b = interp_utility (!(sta.cwd), filter_var_env !(sta.var_env), args) id (sem_state sta) in + = let sta', b = interp_utility (!(sta.cwd), C.filter_var_env !(sta.var_env), args) id (sem_state sta) in sta.filesystem := sta'.S.filesystem; sta.stdin := sta'.S.stdin; sta.stdout := sta'.S.stdout; @@ -161,7 +171,7 @@ module Interpreter use semantics.Arguments - let shift_arguments sta n + let shift_arguments sta (n: int) requires { n >= 0 } ensures { !(sta.result) = True -> @@ -175,7 +185,7 @@ module Interpreter = try let args = ref !(sta.arguments) in for i = 1 to n do - invariant { length !(sta.arguments) >= i-1 } + invariant { Length.length !(sta.arguments) >= i-1 } invariant { shift_arguments (i-1) !(sta.arguments) = Some !args } match !args with | Cons _ args' -> @@ -193,7 +203,7 @@ module Interpreter (** {3 The interpretation of statements} *) - let ghost ref stk = 0 + let ghost ref stk : int = 0 let rec interp_instruction (inp:input) (sta:state) (ins:instruction) : unit diverges @@ -243,7 +253,7 @@ module Interpreter | IExport id -> let old_env = !(sta.var_env) in - let var_val = {old_env[id] with S.exported=True} in + let var_val = {old_env[id] with C.exported=True} in sta.var_env := old_env[id <- var_val]; sta.result := True @@ -326,7 +336,7 @@ module Interpreter | ICallUtility name le -> let args = interp_list_expr inp sta le in - interp_utility inp sta name args + interp_utility1 inp sta name args | ICallFunction id le -> let args = interp_list_expr inp sta le in @@ -414,12 +424,12 @@ module Interpreter | ICd se -> (* TODO --realword should also use Unix.chdir *) let s, _b = interp_str_expr True inp sta se in - let cwd_p = absolute_or_concat_relative !(sta.cwd) s in - let pwd_s = normalized_path_to_string cwd_p in - let args = Cons string_dash_d (Cons pwd_s Nil) in - interp_utility {inp with under_condition=True} sta identifier_test args; + let cwd_p = Paths.absolute_or_concat_relative !(sta.cwd) s in + let pwd_s = Paths.normalized_path_to_string cwd_p in + let args = Cons "-d" (Cons pwd_s Nil) in + interp_utility1 {inp with under_condition=True} sta (identifier_of_string "test") args; if !(sta.result) then begin - sta.var_env := !(sta.var_env)[identifier_pwd <- pwd_s]'; + sta.var_env := !(sta.var_env)[identifier_of_string "PWD" <- pwd_s]'; sta.cwd := cwd_p end; maybe_exit inp sta @@ -469,7 +479,7 @@ module Interpreter assert { eval_str_expr stk b (inp, sem_context sta, sem_state sta at L1) se1 (sem_state sta, Success (s1, b1)) }; label L2 in let s2, b2 = interp_str_expr b1 inp sta se2 in assert { eval_str_expr stk b1 (inp, sem_context sta, sem_state sta at L2) se2 (sem_state sta, Success (s2, b2)) }; - s1^s2, b2 + String.concat s1 s2, b2 end with interp_list_expr (inp:input) (sta:state) (le:list_expression) : list string diff --git a/src/concrete/semantics.mlw b/src/concrete/semantics.mlw index ce0ba1c5..e66f4836 100644 --- a/src/concrete/semantics.mlw +++ b/src/concrete/semantics.mlw @@ -54,7 +54,7 @@ module Buffers use list.List use list.Append use list.Reverse - use mystring.String + use string.OCaml as String (* stdin and stdout are comprised of a list of lines, cf. NOTES[Stdin/stdout] *) @@ -73,6 +73,10 @@ module Buffers type stdin = Stdin.t + val function concat_lines (list string) : string + + val function split_on_default_ifs string : list string + scope Stdout use bool.Bool @@ -88,11 +92,11 @@ module Buffers Cons out.line out.lines let constant empty = - { line = String.empty; lines = Nil } + { line = ""; lines = Nil } let function is_empty out = andb - (String.(equal empty out.line)) + String.(out.line = "") (match out.lines with | Nil -> True | _ -> False @@ -103,10 +107,10 @@ module Buffers reverse (all_lines out) let output str out = - { out with line = out.line^str } + { out with line = String.concat out.line str } let newline out = - { line = String.empty; lines = Cons out.line out.lines } + { line = ""; lines = Cons out.line out.lines } (* http://pubs.opengroup.org/onlinepubs/9699919799/utilities/V3_chap02.html#tag_18_06_03 *) let function to_string out : string = @@ -114,7 +118,7 @@ module Buffers match lines with | Nil -> Nil | Cons l lines' -> - if String.(equal l empty) + if String.(l = "") then remove_trailing_newlines lines' else lines end @@ -136,7 +140,7 @@ module Buffers variant { out2.lines } (* ensures { concat_rel out1 out2 result } *) = match out2.lines with - | Nil -> {line=out1.line^out2.line; lines= out1.lines} + | Nil -> {line=String.concat out1.line out2.line; lines= out1.lines} | Cons line2 lines2 -> let out3 = concat out1 {line=line2; lines=lines2} in {line=out2.line; lines=all_lines out3} @@ -167,8 +171,8 @@ module Buffers variant { out2.lines } ensures { forall out1 line3. let out12 = concat out1 out2 in - concat out1 { line = out2.line^line3; lines = out2.lines } = - { line = out12.line^line3; lines = out12.lines } + concat out1 { line = String.concat out2.line line3; lines = out2.lines } = + { line = String.concat out12.line line3; lines = out12.lines } } = match out2.lines with | Nil -> () @@ -185,7 +189,7 @@ module Buffers | Nil -> assert { forall out2. concat out2 out3 = - { line = out2.line^out3.line; lines = out2.lines } + { line = String.concat out2.line out3.line; lines = out2.lines } } | Cons line3 lines3 -> concat_assoc {line = line3; lines = lines3} @@ -233,7 +237,7 @@ end module Input use bool.Bool - use mystring.String + use string.String use Config type input = { @@ -244,10 +248,14 @@ module Input end module Env - + use option.Option use syntax.Identifier use map.Map as M + (** Partial environment *) + type env0 'a = abstract { to_map0 : M.map identifier (option 'a) } + + (** Total environment with default *) type env 'a = abstract { to_map : M.map identifier 'a; default: 'a } meta coercion function to_map @@ -268,7 +276,7 @@ module Arguments use list.Length use int.Int use option.Option - use mystring.String + use string.String use Result let rec function nth_argument (args: list string) (n: int) : string @@ -279,13 +287,13 @@ module Arguments if n = 0 then arg else nth_argument args' (n-1) - | Nil -> String.empty + | Nil -> "" end let rec function shift_arguments (n: int) (args: list string) : option (list string) requires { 0 <= n } variant { args } - ensures { result = None <-> length args < n } + ensures { result = None <-> Length.length args < n } = if n = 0 then Some args else @@ -308,26 +316,36 @@ module Arguments shift_arguments n args = None end -(** {2 Concrete semantics of the CoLiS language} *) -module Semantics +module Paths + + use string.String + use syntax.Identifier + use list.List + + type feature + (** abstract type for filenames (excluding "." and ".."), named + "feature" in the tree constraint vocabulary *) + (* TODO replace with Why3 string and remove from extraction driver *) + + type normalized_path = list feature + + 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 +end + +module Context - use int.Int use list.List - use list.Append use option.Option - use bool.Bool - use mystring.String + 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 Paths + use Env (** {3 The concrete evaluation context} @@ -359,17 +377,6 @@ module Semantics let constant empty_func_env : func_env = empty_env None - 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 - val constant identifier_test : identifier - val constant string_dash_d : string - val constant identifier_pwd : identifier - type context = { var_env: var_env; func_env: func_env; @@ -394,12 +401,54 @@ 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 + +module InterpUtility + use list.List + use syntax.Syntax + use Env + use Paths + use Buffers + + type utility_context = (normalized_path, env0 string, list string) + + type state0 'filesystem = {filesystem: 'filesystem; stdin: stdin; stdout: stdout; log: stdout} + + predicate interp_utility (utility_context, identifier, state0 'fs) (state0 'fs, bool) + + axiom interp_utility_extends_output : forall ctx id, sta sta': state0 'fs, b. + interp_utility (ctx, id, {sta with stdout=Stdout.empty}) (sta', b) -> + interp_utility (ctx, id, sta) ({sta' with stdout=Stdout.concat sta.stdout sta'.stdout}, b) +end + +module Semantics + + 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 Paths + use Context + use import Env as E + use InterpUtility as InterpUtility (** {3 Evaluation state} @@ -418,14 +467,24 @@ module Semantics log: stdout; (** Combines stdout with utility traces and error messages *) } - type utility_context = (normalized_path, env string, list string) + let function to_state0 (s: state) : InterpUtility.state0 filesystem = { + InterpUtility.filesystem = s.filesystem; + InterpUtility.stdin = s.stdin; + InterpUtility.stdout = s.stdout; + InterpUtility.log = s.log + } - (** Interprete a command defined in the document *Specification of UNIX Commands*. *) - val function interp_utility utility_context identifier state : (state, bool) + let function of_state0 (s0: InterpUtility.state0 filesystem) : state = { + filesystem = s0.InterpUtility.filesystem; + stdin = s0.InterpUtility.stdin; + stdout = s0.InterpUtility.stdout; + log = s0.InterpUtility.log + } - axiom interp_utility_extends_output : forall ctx id sta sta' b. - interp_utility ctx id {sta with stdout=Stdout.empty} = (sta', b) -> - interp_utility ctx id sta = ({sta' with stdout=Stdout.concat sta.stdout sta'.stdout}, b) + predicate interp_utility (args: (InterpUtility.utility_context, identifier, state)) (res: (state, bool)) = + let ctx, id, sta = args in + let sta1, b = res in + InterpUtility.interp_utility (ctx, id, to_state0 sta) (to_state0 sta1, b) let function bool_of_return_code (c:return_code) (previous:bool) : bool = match c with @@ -434,11 +493,11 @@ module Semantics | RPrevious -> previous end - let function exit_not_normal inp result = - andb (strict inp.under_condition) (notb result) + let function exit_not_normal inp res = + andb (strict inp.under_condition) (notb res) - let function behaviour (inp:input) (result:bool) : behaviour - = if exit_not_normal inp result + let function behaviour (inp:input) (res:bool) : behaviour + = if exit_not_normal inp res then BExit else BNormal @@ -447,7 +506,7 @@ module Semantics let function split sp str = match sp with | DontSplit -> Cons str Nil - | Split -> String.split_on_default_ifs str + | Split -> split_on_default_ifs str end (* Reexport mixfix operators. *) @@ -466,7 +525,7 @@ module Semantics let var_val = e[id] in match var_val.value with | Some str -> str - | None -> String.empty + | None -> "" end let function ([<-]') (env:var_env) (id:identifier) (value:string) : var_env = @@ -514,7 +573,8 @@ module Semantics eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 string_dash_d (Cons (normalized_path_to_string cwd_p) Nil)) identifier_test sta1 = (sta2, False) -> + let utility_ctx = (ctx.cwd, filter_var_env ctx.var_env, Cons "-d" (Cons (normalized_path_to_string cwd_p) Nil)) in + interp_utility (utility_ctx, identifier_of_string "test", sta1) (sta2, 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) @@ -523,8 +583,9 @@ module Semantics eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 string_dash_d (Cons (normalized_path_to_string cwd_p) Nil)) identifier_test sta1 = (sta2, 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 utility_ctx = (ctx.cwd, filter_var_env ctx.var_env, Cons "-d" (Cons (normalized_path_to_string cwd_p) Nil)) in + interp_utility (utility_ctx, identifier_of_string "test", sta1) (sta2, True) -> + let ctx1 = {ctx with result = True; var_env = ctx.var_env[identifier_of_string "PWD" <- normalized_path_to_string cwd_p]'; cwd = cwd_p} in let bhv = behaviour inp True in eval_instruction stk (inp, ctx, sta) (ICd se) (sta2, ctx1, bhv) @@ -615,7 +676,8 @@ module Semantics | eval_call_utility: forall stk inp ctx sta sta' sta'' id es ss b. eval_list_expr stk (inp, ctx, sta) es (sta', Success ss) -> - interp_utility (ctx.cwd, filter_var_env ctx.var_env, ss) id sta' = (sta'', b) -> + let utility_ctx = (ctx.cwd, filter_var_env ctx.var_env, ss) in + interp_utility (utility_ctx, id, sta') (sta'', 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) @@ -793,7 +855,7 @@ module Semantics | eval_str_concat : forall stk b b1 b2 inp ctx sta sta1 sta2 e1 e2 str1 str2. eval_str_expr stk b (inp, ctx, sta) e1 (sta1, Success (str1, b1)) -> eval_str_expr stk b1 (inp, ctx, sta1) e2 (sta2, Success (str2, b2)) -> - let res = Success (str1^str2, b2) in + let res = Success (String.concat str1 str2, b2) in eval_str_expr stk b (inp, ctx, sta) (SConcat e1 e2) (sta2, res) (** Evaluation of expressions to a list of strings: diff --git a/src/language/driver.drv b/src/language/driver.drv index 81a2c3da..4a5cb4a1 100644 --- a/src/language/driver.drv +++ b/src/language/driver.drv @@ -1,14 +1,6 @@ -module mystring.String - syntax type string "string" - syntax val empty "\"\"" - syntax val equal "String.equal %1 %2" - syntax val concat_lines "String.concat \"\n\" %1" - syntax val split_on_default_ifs "Str.(split (regexp \"[ \t\n]+\") %1)" - syntax val (^) "%1 ^ %2" -end - module syntax.Identifier syntax type identifier "string" syntax val identifier_eq "String.equal %1 %2" syntax val identifier_to_string "%1" + syntax val identifier_of_string "%1" end \ No newline at end of file diff --git a/src/language/mystring.mlw b/src/language/mystring.mlw deleted file mode 100644 index 9e049827..00000000 --- a/src/language/mystring.mlw +++ /dev/null @@ -1,27 +0,0 @@ -module String - - use list.List - - type string - - (** "" *) - val constant empty : string - - val predicate equal (s1 s2:string) ensures { result <-> s1 = s2 } - - val function (^) string string : string - - axiom string_left_empty: forall s. - empty ^ s = s - - axiom string_right_empty: forall s. - s ^ empty = s - - axiom string_concat_assoc: forall s1 s2 s3. - s1 ^ (s2 ^ s3) = (s1 ^ s2) ^ s3 - - (* Concatenate lines using '\n' as separator *) - val function concat_lines (list string) : string - - val function split_on_default_ifs string : list string -end \ No newline at end of file diff --git a/src/language/syntax.mlw b/src/language/syntax.mlw index a862cde1..f68d6381 100644 --- a/src/language/syntax.mlw +++ b/src/language/syntax.mlw @@ -16,7 +16,7 @@ end (** Identifiers of variables and functions *) module Identifier - use mystring.String + use string.String type identifier @@ -24,6 +24,8 @@ module Identifier ensures { result <-> v1 = v2 } val function identifier_to_string identifier : string + + val function identifier_of_string string : identifier end (** Abstract syntax of the CoLiS language *) @@ -32,7 +34,7 @@ module Syntax use list.List use option.Option - use mystring.String + use string.String use export Nat use export Identifier diff --git a/src/symbolic/driver.drv b/src/symbolic/driver.drv index 167e045d..3d2250d4 100644 --- a/src/symbolic/driver.drv +++ b/src/symbolic/driver.drv @@ -1,24 +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.Path.(normalize ~cwd:%1 (from_string %2))" - syntax val normalized_path_to_string "Colis_constraints.Path.normal_to_string %1" - syntax val identifier_test "\"test\"" - syntax val string_dash_d "\"-d\"" - syntax val identifier_pwd "\"PWD\"" -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" @@ -33,4 +12,4 @@ module collection.Collection syntax val of_list "%1" syntax val to_list "%1" syntax val size "List.length %1" -end +end \ No newline at end of file diff --git a/src/symbolic/symbolicFilesystem.ml b/src/symbolic/symbolicFilesystem.ml new file mode 100644 index 00000000..275efb9a --- /dev/null +++ b/src/symbolic/symbolicFilesystem.ml @@ -0,0 +1,7 @@ +open Colis_constraints + +type t = { + root : Var.t; + clause : Clause.sat_conj; + root0 : Var.t option; +} diff --git a/src/symbolic/symbolicInterpreter.mlw b/src/symbolic/symbolicInterpreter.mlw index d1150e71..8e1c88f4 100644 --- a/src/symbolic/symbolicInterpreter.mlw +++ b/src/symbolic/symbolicInterpreter.mlw @@ -1,1334 +1,1309 @@ -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, - type normalized_path = list feature, - val default_cwd = Nil, - 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_ - | BFailure -> Cn.mem sta rs.failure +module SymbolicInterpreter + scope Make + + use bool.Bool + use option.Option + use int.Int + use list.List + use list.ListRich as L + use set.Fset + use string.String + use syntax.Identifier + use syntax.Syntax + use auxiliaries.OptionGet + use semantics.Context + use semantics.Paths + use semantics.InterpUtility as InterpUtility + use collection.Collection as Cn + + scope Arg + use semantics.InterpUtility + type filesystem + + val sym_interp_utility (ctx: utility_context) (id: identifier) (sta: state0 filesystem) : Cn.t (state0 filesystem, bool) + ensures { forall res. + interp_utility (ctx, id, sta) res <-> + Cn.mem res result + } end + import Arg - 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 + clone import semantics.Semantics as Semantics with + type filesystem = filesystem - 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) + let function of_states0 rs = + Cn.map (fun x -> let sta, b = x in of_state0 sta, b) rs + + let function sym_interp_utility (ctx: InterpUtility.utility_context) (id: identifier) (sta: state) : Cn.t (state, bool) + ensures { forall sta0 b. + InterpUtility.interp_utility (ctx, id, to_state0 sta) (sta0, b) <-> + Cn.mem (of_state0 sta0, b) result + } + = of_states0 (sym_interp_utility ctx id (to_state0 sta)) + + (** 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 *) } - = 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} - | BFailure -> {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_ - | BFailure -> Cn.mem sta failure - end + let function with_data data = + fun sta -> + {sta with data = data} + + (** The symbolic interpretation of a program results describes multiple possible results + *) + scope Results + + use set.Fset as Fset + use collection.Collection as Cn + use list.ListRich as L + use semantics.Input + use semantics.Behaviour + + (** 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); + } - 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_ - | BFailure -> 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_ - | BFailure -> 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 mystring.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, bool) - ensures { - forall res. - interp_utility ctx id sta = res <-> - Cn.mem res result - } + let constant empty = { + normal = Cn.empty; + exit = Cn.empty; + return_ = Cn.empty; + failure = Cn.empty; + } - let rec separate_results_list (sta_opts: list (state, result 'a)) : (results: list (state, 'a), failures: list state) - variant { sta_opts } - ensures { - forall sta x. - L.mem (sta, x) results <-> - L.mem (sta, Success x) sta_opts - } - ensures { - forall sta. - L.mem sta failures <-> - L.mem (sta, Error) 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 - | Success x -> Cons (sta, x) results, failures - | Error -> results, Cons sta failures - end - end + 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_ + | BFailure -> Cn.mem sta rs.failure + end - let separate_results (sta_opts: Cn.t (state, result 'a)) : (results: Cn.t (state, 'a), failures: Cn.t state) - ensures { - forall sta x. - Cn.mem (sta, x) results <-> - Cn.mem (sta, Success x) sta_opts - } - ensures { - forall sta. - Cn.mem sta failures <-> - Cn.mem (sta, Error) 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 - 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 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 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 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) -> + 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 | BReturn -> Rs.mem {state=sta'; context={ctx' with result=notb ctx'.result}; data=()} bhv result - | BExit | BFailure -> Rs.mem {state=sta'; context=ctx'; data=()} bhv result + | BNormal -> {empty with normal=stas} + | BExit -> {empty with exit=stas} + | BReturn -> {empty with return_=stas} + | BFailure -> {empty with failure=stas} end - } - | 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) + 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_ + | BFailure -> 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_ + | BFailure -> 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_ + | BFailure -> Cn.mem sta rs2.failure + end) + end + use semantics.Result + use semantics.Behaviour + use semantics.Input + use semantics.Config + use semantics.Buffers + use semantics.Arguments + use semantics.Env + import Results + + let rec separate_results_list (sta_opts: list (state, result 'a)) : (results: list (state, 'a), failures: list state) + variant { sta_opts } + ensures { + forall sta x. + L.mem (sta, x) results <-> + L.mem (sta, Success x) sta_opts + } ensures { - forall sta'. - eval_str_expr stk True (inp, ctx, sta) se (sta', Error) -> - Cn.mem {state=sta'; context=ctx; data=()} result.Rs.failure + forall sta. + L.mem sta failures <-> + L.mem (sta, Error) 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 + | Success x -> Cons (sta, x) results, failures + | Error -> results, Cons sta failures + end + 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'}) + let separate_results (sta_opts: Cn.t (state, result 'a)) : (results: Cn.t (state, 'a), failures: Cn.t state) + ensures { + forall sta x. + Cn.mem (sta, x) results <-> + Cn.mem (sta, Success x) sta_opts + } + ensures { + forall sta. + Cn.mem sta failures <-> + Cn.mem (sta, Error) 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 + end - | 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 + 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 - | ISubshell ins -> - let stas, stas_failure = - Rs.separate_non_failure - (interp_instr stk inp ctx sta ins) + 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 Semantics.stdout = sta.Semantics.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 - assert { + {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. - bhv <> BFailure -> 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', BFailure) -> - Rs.mem {state=sta'; context={ctx with result=ctx'.result}; data=()} BFailure result + Results.mem {state=sta'; context=ctx'; data=()} bhv result } + (* (\* 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 | BFailure -> Results.mem {state=sta'; context=ctx'; data=()} bhv result + end + } - | INoOutput ins -> - Rs.map (reset_output sta) - (interp_instr stk inp ctx sta ins) + | 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 { + forall sta'. + eval_str_expr stk True (inp, ctx, sta) se (sta', Error) -> + Cn.mem {state=sta'; context=ctx; data=()} result.Results.failure + } - | 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 + | 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.union - (interp_instr' stk inp res1_true ins2) - (interp_instr' stk inp res1_false ins3) - in - Rs.union res2 res1_other + Results.({empty with normal = Cn.singleton sta'}) - | ICd se -> - let res1, res_failures = - separate_results - (interp_str_expr stk True inp ctx sta se) - in - assert { [@expl:cd5] - forall sta1 str b. - eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (str, b)) -> - Cn.mem (sta1, (str, b)) res1 - }; - let res2 = - let function aux arg = - let sta1, (s, (_:bool)) = arg in - let cwd_p = absolute_or_concat_relative ctx.cwd s in - let res = sym_interp_utility (ctx.cwd, filter_var_env ctx.var_env, Cons string_dash_d (Cons (normalized_path_to_string cwd_p) Nil)) identifier_test sta1 in - Cn.map (fun sta_b -> (sta_b, cwd_p, normalized_path_to_string cwd_p)) res + | ISequence ins1 ins2 -> + let res1_normal, res1_other = + Results.separate_normal + (interp_instr stk inp ctx sta ins1) in - Cn.bind aux res1 - in - assert { [@expl:cd4] - forall sta1 s _b sta2 b. - eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 string_dash_d (Cons pwd_s Nil) in - (sta2, b) = interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) identifier_test sta1 -> - Cn.mem ((sta2, b), cwd_p, pwd_s) res2 - }; - let res2 = - let function aux' arg = - let (sta2, b), cwd_p, pwd_s = 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 = ()} + 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 - Cn.map aux' res2 - in - assert { [@expl:cd3a] - forall sta1 s _b sta2. - eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 string_dash_d (Cons pwd_s Nil) in - (sta2, False) = interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) identifier_test sta1 -> - let ctx1 = {ctx with result = False} in - Cn.mem {state=sta2; context=ctx1; data=()} res2 - }; - assert { [@expl:cd3b] - forall sta1 s _b sta2. - eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 string_dash_d (Cons pwd_s Nil) in - (sta2, 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 - Cn.mem {state=sta2; context=ctx1; data=()} res2 - }; - let res3 = Rs.inject inp res2 in - let res_failures = Rs.stas_as_failures ctx res_failures in - Rs.union res3 res_failures - ensures { [@expl:cd2a] - forall sta1 s _b sta2. - eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 string_dash_d (Cons pwd_s Nil) in - (sta2, False) = interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) identifier_test sta1 -> - let ctx1 = {ctx with result = False} in - let bhv = behaviour inp False in - Rs.mem {state=sta2; context=ctx1; data=()} bhv result - } - ensures { [@expl:cd2b] - forall sta1 s _b sta2. - eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 string_dash_d (Cons pwd_s Nil) in - (sta2, 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 - } - ensures { [@expl:cd1] - forall sta1. - eval_str_expr stk True (inp, ctx, sta) se (sta1, Error) -> - Rs.mem {state=sta1; context=ctx; data=()} BFailure result - } + assert { + forall sta' ctx' bhv. + bhv <> BFailure -> + 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 { + forall sta' ctx'. + eval_instruction stk (inp, ctx, sta) ins (sta', ctx', BFailure) -> + Results.mem {state=sta'; context={ctx with result=ctx'.result}; data=()} BFailure result + } - | ICallUtility id le -> - let res, res_failures = - separate_results - (interp_list_expr stk inp ctx sta le) - in - let res' = - let function aux arg = - let sta', args = arg in - sym_interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) id sta' + | 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 - Cn.bind aux res - in - let res'' = - let function aux arg = - let sta'', b = arg in - {state=sta''; context={ctx with result=b}; data=()} + 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 - Cn.map aux res' - in - let res''' = Rs.inject inp res'' in - let res_failures' = Rs.stas_as_failures ctx res_failures in - Rs.union res''' res_failures' - ensures { - forall sta' ss sta'' b. - eval_list_expr stk (inp, ctx, sta) le (sta', Success ss) -> - (sta'', b) = interp_utility (ctx.cwd, filter_var_env ctx.var_env, ss) id sta' -> - Rs.mem {state=sta''; context={ctx with result=b}; data=()} (behaviour inp b) result - by Rs.mem {state=sta''; context={ctx with result=b}; data=()} (behaviour inp b) res''' - } + Results.union res2 res1_other - | 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, Success 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 - {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, Success args) -> - ctx.func_env[id] = Some ins -> - inp.config.stack_size = Finite stk -> - Rs.mem {state=sta1; context=ctx; data=()} BFailure result + | ICd se -> + let res1, res_failures = + separate_results + (interp_str_expr stk True inp ctx sta se) + in + assert { [@expl:cd5] + forall sta1 str b. + eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (str, b)) -> + Cn.mem (sta1, (str, b)) res1 + }; + let res2 = + let function aux arg = + let sta1, (s, (_:bool)) = arg in + let cwd_p = absolute_or_concat_relative ctx.cwd s in + let utilty_ctx = (ctx.cwd, filter_var_env ctx.var_env, Cons "-d" (Cons (normalized_path_to_string cwd_p) Nil)) in + let res = sym_interp_utility utilty_ctx (identifier_of_string "test") sta1 in + Cn.map (fun sta_b -> (sta_b, cwd_p, normalized_path_to_string cwd_p)) res + in + Cn.bind aux res1 + in + assert { [@expl:cd4] + forall sta1 s _b sta2 b. + eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 + let utility_ctx = (ctx.cwd, filter_var_env ctx.var_env, args) in + Semantics.interp_utility (utility_ctx, identifier_of_string "test", sta1) (sta2, b) -> + Cn.mem ((sta2, b), cwd_p, pwd_s) res2 + }; + let res2 = + let function aux' arg = + let (sta2, b), cwd_p, pwd_s = arg in + if b then + let ctx' = { + ctx with + var_env = ctx.var_env[identifier_of_string "PWD" <- pwd_s]'; + cwd = cwd_p; + result = True } - 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 + {state = sta2; context = ctx'; data = ()} + else + let ctx' = {ctx with result = False} in + {state = sta2; context = ctx'; data = ()} + in + Cn.map aux' res2 + in + assert { [@expl:cd3a] + forall sta1 s _b sta2. + eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 + let utility_ctx = (ctx.cwd, filter_var_env ctx.var_env, args) in + interp_utility (utility_ctx, identifier_of_string "test", sta1) (sta2, False) -> + let ctx1 = {ctx with result = False} in + Cn.mem {state=sta2; context=ctx1; data=()} res2 + }; + assert { [@expl:cd3b] + forall sta1 s _b sta2. + eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 + let utility_ctx = (ctx.cwd, filter_var_env ctx.var_env, args) in + interp_utility (utility_ctx, identifier_of_string "test", sta1) (sta2, True) -> + let ctx1 = {ctx with result = True; var_env = ctx.var_env[identifier_of_string "PWD" <- pwd_s]'; cwd = cwd_p} in + Cn.mem {state=sta2; context=ctx1; data=()} res2 + }; + let res3 = Results.inject inp res2 in + let res_failures = Results.stas_as_failures ctx res_failures in + Results.union res3 res_failures + ensures { [@expl:cd2a] + forall sta1 s _b sta2. + eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 + let utility_ctx = (ctx.cwd, filter_var_env ctx.var_env, args) in + interp_utility (utility_ctx, identifier_of_string "test", sta1) (sta2, False)-> + let ctx1 = {ctx with result = False} in + let bhv = behaviour inp False in + Results.mem {state=sta2; context=ctx1; data=()} bhv result + } + ensures { [@expl:cd2b] + forall sta1 s _b sta2. + eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (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 + let utility_ctx = (ctx.cwd, filter_var_env ctx.var_env, args) in + interp_utility (utility_ctx, identifier_of_string "test", sta1) (sta2, True) -> + let ctx1 = {ctx with result = True; var_env = ctx.var_env[identifier_of_string "PWD" <- pwd_s]'; cwd = cwd_p} in + let bhv = behaviour inp True in + Results.mem {state=sta2; context=ctx1; data=()} bhv result + } + ensures { [@expl:cd1] + forall sta1. + eval_str_expr stk True (inp, ctx, sta) se (sta1, Error) -> + Results.mem {state=sta1; context=ctx; data=()} BFailure result + } + + | ICallUtility id le -> + let res, res_failures = + separate_results + (interp_list_expr stk inp ctx sta le) + in + let res' = + let function aux arg = + let sta', args = arg in + sym_interp_utility (ctx.cwd, filter_var_env ctx.var_env, args) id sta' + in + Cn.bind aux res + in + let res'' = + let function aux arg = + let sta'', b = arg in + {state=sta''; context={ctx with result=b}; data=()} + in + Cn.map aux res' + in + let res''' = Results.inject inp res'' in + let res_failures' = Results.stas_as_failures ctx res_failures in + Results.union res''' res_failures' + ensures { + forall sta' ss sta'' b. + eval_list_expr stk (inp, ctx, sta) le (sta', Success ss) -> + let utility_ctx = (ctx.cwd, filter_var_env ctx.var_env, ss) in + interp_utility (utility_ctx, id, sta') (sta'', b) -> + Results.mem {state=sta''; context={ctx with result=b}; data=()} (behaviour inp b) result + by Results.mem {state=sta''; context={ctx with result=b}; data=()} (behaviour inp b) res''' + } + + | 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, Success 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 + {state=sta'; context=ctx; data=()} in - Rs.bind_collection aux arg_res - ensures { [@expl:callfun3] - forall sta1 args ins sta2 ctx2 bhv2. + 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, Success 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 + inp.config.stack_size = Finite stk -> + Results.mem {state=sta1; context=ctx; data=()} BFailure result } - in - let res2' = - let function aux (sta2: sym_state unit) = - {state=sta2.state; context={sta2.context with arguments = ctx.arguments}; data=()} + 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, Success 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, Success 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 - Rs.map aux res2 - ensures { [@expl:callfun4] + 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, Success 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 + 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 + let bhv' = match bhv2 with BNormal | BReturn -> BNormal | BExit -> BExit | BFailure -> BFailure 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', Success 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.({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, Success 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 | BFailure -> BFailure 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 + Results.single_behaviour (behaviour inp False) arg_res' ensures { forall sta' ss. eval_list_expr stk (inp, ctx, sta) le (sta', Success ss) -> ctx.func_env[id] = None -> - Cn.mem {state=sta'; context={ctx with result=False}; data=()} result - by Cn.mem (sta', ss) arg_res + Results.mem {state=sta'; context={ctx with result=False}; data=()} (behaviour inp False) result } - in - Rs.single_behaviour (behaviour inp False) arg_res' - ensures { - forall sta' ss. - eval_list_expr stk (inp, ctx, sta) le (sta', Success 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 = 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 - 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') - 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', Success 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 + | IForeach id le ins -> + let lst_res, lst_res_failures = + separate_results + (interp_list_expr stk inp ctx sta le) in - Rs.bind_collection aux lst_res - ensures { - forall sta' ss sta'' ctx' bhv b. + assert { + forall sta' ss. eval_list_expr stk (inp, ctx, sta) le (sta', Success 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 - } - in - let res_loop_cont' = - let function aux sta'' = - let ctx'' = {sta''.context with result=sta''.data} in - with_data () {sta'' with context = ctx''} + 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', Success 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', Success 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 - Rs.map aux res_loop_cont + let res_failure = + Results.stas_as_failures ctx lst_res_failures + ensures { + forall sta'. + eval_list_expr stk (inp, ctx, sta) le (sta', Error) -> + Results.mem {state=sta'; context=ctx; data=()} BFailure 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' ss sta'' ctx' bhv b. - eval_list_expr stk (inp, ctx, sta) le (sta', Success 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' 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 } - in - let res_failure = - Rs.stas_as_failures ctx lst_res_failures ensures { - forall sta'. - eval_list_expr stk (inp, ctx, sta) le (sta', Error) -> - Rs.mem {state=sta'; context=ctx; data=()} BFailure result + 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 } - 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 - } - | 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 <> BFailure -> - 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} + | IPipe ins1 ins2 -> + let stas1, stas1_failure = + Results.separate_non_failure + (interp_instr stk inp ctx {sta with stdout=Stdout.empty} ins1) in - Cn.map aux stas1 - ensures { + assert { forall sta1 ctx1 bhv1. eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, bhv1) -> bhv1 <> BFailure -> - 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 - ensures { - forall sta1 ctx1 bhv1 sta2 ctx2 bhv2. - eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, bhv1) -> - bhv1 <> BFailure -> - 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 - } - in - let res2' = - let function aux sta2 = - {state={sta2.state with stdin=sta2.data}; - context={ctx with result=sta2.context.result}; - data=()} + 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 <> BFailure -> + Cn.mem + {state={sta1 with stdout=sta.stdout; stdin=Stdout.to_stdin sta1.stdout}; context=ctx; data=sta1.stdin} + result + } 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 <> BFailure -> - 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=()} + 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 <> BFailure -> + 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 - Cn.map aux stas1_failure - ensures { - forall sta1 ctx1. - eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins1 (sta1, ctx1, BFailure) -> - Cn.mem {state={sta1 with stdout=sta.stdout}; context=ctx; data=()} result - } - in - Rs.(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 - Rs.({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 - Rs.({empty with return_ = Cn.singleton sta}) - end + let res2' = + let function aux sta2 = + {state={sta2.state with stdin=sta2.data}; + context={ctx with result=sta2.context.result}; + data=()} + in + 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 <> BFailure -> + 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 + 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, BFailure) -> + 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) : 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 + 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 - 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 - } - in - let res1_other' = - let function aux (sta: sym_state unit) = - with_data sta.context.result sta + 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 - 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 - } - in - Rs.union res_normal' res1_other' - end + 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_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 - 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 + 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 + 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 - Rs.bind_collection aux res2_normal - ensures { - forall sta1 ctx1 sta2 ctx2 sta3 ctx3 bhv3 n b'. - inp.config.loop_limit <> Finite ctr -> + assert { + forall sta1 ctx1. 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 { + Cn.mem {state=sta1; context=ctx1; data=()} res1_normal + }; + assert { 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 { + 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. - inp.config.loop_limit <> Finite ctr -> + 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) -> - Rs.mem {state=sta1;context=ctx1;data=(ctr, b)} BNormal result - } - in - let res2_abort' = - Rs.map with_ctr_b res2_abort - ensures { + 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. - 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, Success (str, b)) - | SVariable var -> - let str = ctx.var_env[var]' in - Cn.singleton (sta, Success (str, b)) - | SArgument n -> - let str = nth_argument (Cons inp.argument0 ctx.arguments) n.nat in - Cn.singleton (sta, Success (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 <> BFailure -> - 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, BFailure) -> - 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', Success (str, b') - in - Cn.map for_res res - in - let res_failure' = - Cn.map (fun sta1 -> {sta1.state with stdout=sta.stdout}, Error) 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, BFailure) -> - Cn.mem ({sta1 with stdout = sta.stdout}, Error) result - by Cn.mem ({sta1 with stdout = sta.stdout}, Error) res_failure' - } - ensures { - forall sta1 ctx1 bhv1. - eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins (sta1, ctx1, bhv1) -> - bhv1 <> BFailure -> - Cn.mem ({sta1 with stdout = sta.stdout}, Success (Stdout.to_string sta1.stdout, ctx1.result)) result - by Cn.mem ({sta1 with stdout = sta.stdout}, Success (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 + 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 { - let sta1, (str1, b1) = arg in - forall sta2. - eval_str_expr stk b (inp, ctx, sta) se1 (sta1, Success (str1, b1)) -> - eval_str_expr stk b1 (inp, ctx, sta1) se2 (sta2, Error) -> - Cn.mem (sta2, Error) result + 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 { - let sta1, (str1, b1) = arg in - forall sta2 str2 b2. - eval_str_expr stk b (inp, ctx, sta) se1 (sta1, Success (str1, b1)) -> - eval_str_expr stk b1 (inp, ctx, sta1) se2 (sta2, Success (str2, b2)) -> - Cn.mem (sta2, Success (str1^str2, b2)) result + 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 } - = 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, Error) res2_failure - in - let res2' = - let for_res2 arg2 = - let sta2, (str2, b2) = arg2 in - sta2, Success (str1^str2, b2) - in - Cn.map for_res2 res2 - in - Cn.(union res2' res2_failure') in - Cn.bind for_res1 res1 - in - let res1_failure' = - Cn.map (fun sta -> sta, Error) res1_failure - in - Cn.(union res1' res1_failure') - 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, Success 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))) + let res1_false' = + Results.({empty with normal=Cn.map with_ctr_b res1_false}) ensures { - let sta1, (str1, b1) = arg in - forall sta2. - eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (str1, b1)) -> - eval_list_expr stk (inp, ctx, sta1) le' (sta2, Error) -> - Cn.mem (sta2, Error) result + 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 { - let sta1, (str1, b1) = arg in - forall sta2 l2. - eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (str1, b1)) -> - eval_list_expr stk (inp, ctx, sta1) le' (sta2, Success l2) -> - Cn.mem (sta2, Success L.(split sp str1++l2)) result + 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 } - = 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 + 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 { + 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, Success (str, b)) + | SVariable var -> + let str = ctx.var_env[var]' in + Cn.singleton (sta, Success (str, b)) + | SArgument n -> + let str = nth_argument (Cons inp.argument0 ctx.arguments) n.nat in + Cn.singleton (sta, Success (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 <> BFailure -> + 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, BFailure) -> + 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', Success (str, b') in - let lst_res2' = - Cn.map (fun arg -> let sta2, strs2 = arg in sta2, Success L.(split sp str1++strs2)) lst_res2 + Cn.map for_res res + in + let res_failure' = + Cn.map (fun sta1 -> {sta1.state with stdout=sta.stdout}, Error) 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, BFailure) -> + Cn.mem ({sta1 with stdout = sta.stdout}, Error) result + by Cn.mem ({sta1 with stdout = sta.stdout}, Error) res_failure' + } + ensures { + forall sta1 ctx1 bhv1. + eval_instruction stk (inp, ctx, {sta with stdout=Stdout.empty}) ins (sta1, ctx1, bhv1) -> + bhv1 <> BFailure -> + Cn.mem ({sta1 with stdout = sta.stdout}, Success (Stdout.to_string sta1.stdout, ctx1.result)) result + by Cn.mem ({sta1 with stdout = sta.stdout}, Success (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 + ensures { + let sta1, (str1, b1) = arg in + forall sta2. + eval_str_expr stk b (inp, ctx, sta) se1 (sta1, Success (str1, b1)) -> + eval_str_expr stk b1 (inp, ctx, sta1) se2 (sta2, Error) -> + Cn.mem (sta2, Error) result + } + ensures { + let sta1, (str1, b1) = arg in + forall sta2 str2 b2. + eval_str_expr stk b (inp, ctx, sta) se1 (sta1, Success (str1, b1)) -> + eval_str_expr stk b1 (inp, ctx, sta1) se2 (sta2, Success (str2, b2)) -> + Cn.mem (sta2, Success (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, Error) res2_failure + in + let res2' = + let for_res2 arg2 = + let sta2, (str2, b2) = arg2 in + sta2, Success (String.concat str1 str2, b2) + in + Cn.map for_res2 res2 + in + Cn.(union res2' res2_failure') in - let lst_res2_failures' = - Cn.map (fun sta -> sta, Error) lst_res2_failures + Cn.bind for_res1 res1 + in + let res1_failure' = + Cn.map (fun sta -> sta, Error) res1_failure + in + Cn.(union res1' res1_failure') + 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, Success 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, Success (str1, b1)) -> + eval_list_expr stk (inp, ctx, sta1) le' (sta2, Error) -> + Cn.mem (sta2, Error) result + } + ensures { + let sta1, (str1, b1) = arg in + forall sta2 l2. + eval_str_expr stk True (inp, ctx, sta) se (sta1, Success (str1, b1)) -> + eval_list_expr stk (inp, ctx, sta1) le' (sta2, Success l2) -> + Cn.mem (sta2, Success 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, Success L.(split sp str1++strs2)) lst_res2 + in + let lst_res2_failures' = + Cn.map (fun sta -> sta, Error) lst_res2_failures + in + Cn.(union lst_res2' lst_res2_failures') in - Cn.(union lst_res2' lst_res2_failures') + Cn.bind for_sta_str str_res1 in - Cn.bind for_sta_str str_res1 - in - let str_res1_failures' = - Cn.map (fun sta -> sta, Error) str_res1_failures - in - Cn.(union res2 str_res1_failures') - end + let str_res1_failures' = + Cn.map (fun sta -> sta, Error) 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 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 - Cn.map aux stas + Results.separate_non_failure + (interp_instr' 0 inp stas pro.instruction) 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 \ No newline at end of file