Skip to content

[Fix] the order of composition of statements has changed. #73

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dvvrd merged 2 commits into from
Mar 29, 2018
Merged

[Fix] the order of composition of statements has changed. #73

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ae5bbc9
Style fix
MchKosticyn Mar 24, 2018
ec1de86
[Fix] the order of composition of statements has changed.
MchKosticyn Mar 24, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions VSharp.CSharpUtils/Tests/Conditional.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,5 +139,17 @@ public static int ExceptionInCondition3(NewBool nb)
return 56;
}
}

public static int DeclareAfterReturn(bool flag, bool f, int x)
{
if (f)
{
if (flag)
return 42;
int y = x + x;
return x + x + y;
}
return x;
}
}
}
3 changes: 2 additions & 1 deletion VSharp.SILI.Core/API.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,8 @@ module API =
let Explore id k = Explorer.explore id k

let Call funcId state body k = Explorer.call m.Value funcId state body k
let InvokeAfter consumeContinue (result, state) statement k = ControlFlow.invokeAfter consumeContinue (result, state) statement k
let ComposeStatements rs statements isContinueConsumer reduceStatement k =
ControlFlow.composeStatements statements isContinueConsumer reduceStatement (fun state -> Memory.newScope m.Value state []) rs k

let BranchStatements state condition thenBranch elseBranch k =
Common.statedConditionalExecution state condition thenBranch elseBranch ControlFlow.mergeResults ControlFlow.merge2Results ControlFlow.throwOrIgnore k
Expand Down
2 changes: 1 addition & 1 deletion VSharp.SILI.Core/API.fsi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ module API =
val Explore : IFunctionIdentifier -> (statementResult * state -> 'a) -> 'a

val Call : IFunctionIdentifier -> state -> (state -> (statementResult * state -> 'a) -> 'a) -> (statementResult * state -> 'a) -> 'a
val InvokeAfter : bool -> (statementResult * state) -> (state -> (statementResult * state -> 'a) -> 'a) -> (statementResult * state -> 'a) -> 'a
val ComposeStatements : (statementResult * state) -> seq<'a> -> ('a -> bool) -> (state -> 'a -> (statementResult * state -> 'b) -> 'b) -> (statementResult * state -> 'b) -> 'b

val BranchStatements : state -> (state -> (term * state -> 'a) -> 'b) -> (state -> (statementResult * state -> 'a) -> 'a) -> (state -> (statementResult * state -> 'a) -> 'a) -> (statementResult * state -> 'a) -> 'b
val BranchExpressions : state -> (state -> (term * state -> 'a) -> 'b) -> (state -> (term * state -> 'a) -> 'a) -> (state -> (term * state -> 'a) -> 'a) -> (term * state -> 'a) -> 'b
Expand Down
53 changes: 34 additions & 19 deletions VSharp.SILI.Core/ControlFlow.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,14 +111,14 @@ module internal ControlFlow =
match oldRes.result with
| NoResult -> newRes
| _ -> oldRes
match oldRes.result, newRes.result with
| NoResult, _ ->
match oldRes.result with
| NoResult ->
newRes, newState
| Break, _
| Continue, _
| Throw _, _
| Return _, _ -> oldRes, oldState
| Guarded gvs, _ ->
| Break
| Continue
| Throw _
| Return _ -> oldRes, oldState
| Guarded gvs ->
let conservativeGuard = List.fold (fun acc (g, v) -> if calculationDone v then acc ||| g else acc) False gvs
let result =
match newRes.result with
Expand All @@ -132,18 +132,6 @@ module internal ControlFlow =
let commonMetadata = Metadata.combine oldRes.metadata newRes.metadata
Guarded commonMetadata result, Merging.merge2States conservativeGuard !!conservativeGuard oldState newState

let invokeAfter consumeContinue (result, state) statement k =
let pathCondition = currentCalculationPathCondition consumeContinue result
match pathCondition with
| Terms.True -> statement state (fun (newRes, newState) -> k (composeSequentially result newRes state newState))
| Terms.False -> k (result, state)
| _ ->
statement
(State.withPathCondition state pathCondition)
(fun (newRes, newState) ->
let newState = State.popPathCondition newState
k (composeSequentially result newRes state newState))

let rec resultToTerm result =
match result.result with
| Return term -> Metadata.addMisc term (ReturnMarker()); { term = term.term; metadata = result.metadata }
Expand Down Expand Up @@ -173,6 +161,33 @@ module internal ControlFlow =
let mergeResults grs =
Merging.guardedMap resultToTerm grs |> throwOrReturn

let private invokeAfter consumeContinue (result, state) statement defaultCompose composeWithNewFrame k =
let pathCondition = currentCalculationPathCondition consumeContinue result
let compose newRS k =
if pathCondition = currentCalculationPathCondition consumeContinue (fst newRS)
then defaultCompose newRS k
else composeWithNewFrame newRS k
match pathCondition with //TODO: use statedConditionalExecution
| Terms.True -> statement state (fun newRS -> compose newRS k)
| Terms.False -> k (result, state)
| _ ->
statement
(State.withPathCondition state pathCondition)
(fun (newRes, newState) -> compose (newRes, State.popPathCondition newState) k)


let composeStatements statements isContinueConsumer statementMapper newScope (result, state) k =
let rec composeStatementsH statements isContinueConsumer statementMapper newScope rs localk =
match statements with
| Seq.Empty -> k rs
| Seq.Cons(statement, tail) ->
let cmpseTailIfNeed newRS modSt ifLastk k = if Seq.isEmpty tail then ifLastk newRS else composeStatementsH tail isContinueConsumer statementMapper newScope (mapsnd modSt newRS) k
invokeAfter (isContinueConsumer statement) rs (fun state -> statementMapper state statement)
(fun (newR, newS) k -> cmpseTailIfNeed (newR, newS) id k (fun (tailRes, tailState) -> k <| composeSequentially newR tailRes newS tailState))
(fun (newR, newS) k -> cmpseTailIfNeed (newR, newS) newScope k (fun (tailRes, tailState) -> k <| composeSequentially newR tailRes newS (State.popStack tailState)))
localk
composeStatementsH statements isContinueConsumer statementMapper newScope (result, state) (fun (newRes, newState) -> k <| composeSequentially result newRes state newState)

let unguardResults gvs =
let unguard gres =
match gres with
Expand Down
29 changes: 10 additions & 19 deletions VSharp.SILI/Interpreter.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -408,17 +408,11 @@ module internal Interpreter =
// ------------------------------- Linear control flow-------------------------------

and reduceSequentially state statements k =
Cps.Seq.foldlk
(InvokeAfter false)
(NoResult(), Memory.NewScope state [])
statements
(fun (res, state) -> k (res, Memory.PopStack state))
ComposeStatements (NoResult(), Memory.NewScope state []) statements (always false) (fun state stmt -> stmt state) (fun (res, state) -> k (res, Memory.PopStack state))

and reduceBlockStatement state (ast : IBlockStatement) k =
let compose rs statement k =
InvokeAfter (Transformations.isContinueConsumer statement) rs (fun state -> reduceStatement state statement) k
let k = Enter ast state k
Cps.Seq.foldlk compose (NoResult(), Memory.NewScope state []) ast.Statements (fun (res, state) -> k (res, Memory.PopStack state))
ComposeStatements (NoResult(), Memory.NewScope state []) ast.Statements Transformations.isContinueConsumer reduceStatement (fun (res, state) -> k (res, Memory.PopStack state))

and reduceCommentStatement state (ast : ICommentStatement) k =
k (NoComputation, state)
Expand Down Expand Up @@ -1066,24 +1060,21 @@ module internal Interpreter =
let state = Memory.NewScope state [((tempVar, tempVar), Specified freshValue, TypeOf freshValue)]
(Memory.ReferenceLocalVariable state (tempVar, tempVar) false, state)
initializeStaticMembersIfNeed caller state qualifiedTypeName (fun (result, state) ->
let finish r =
InvokeAfter false r
(fun state k ->
if isReferenceType || returnRef
then k (Return reference, state)
else
let term, state = Memory.Dereference state reference
k (Return term, Memory.PopStack state))
(fun (result, state) -> k (ControlFlow.ResultToTerm result, state))
let invokeInitializers result state (result', state') =
let r = ControlFlow.ComposeSequentially result result' state state'
InvokeAfter false r (fun state k ->
let reduceInitializers state k =
if objectInitializerList <> null then
reduceMemberInitializerList reference state objectInitializerList k
elif collectionInitializerList <> null then
reduceCollectionInitializerList constructedType reference state collectionInitializerList k
else k (NoComputation, state)
) finish
let finish state k =
if isReferenceType || returnRef
then k (Return reference, state)
else
let term, state = Memory.Dereference state reference
k (Return term, Memory.PopStack state)
ComposeStatements r (seq[reduceInitializers; finish]) (always false) (fun state stmt -> stmt state) (fun (result, state) -> k (ControlFlow.ResultToTerm result, state))
if constructorSpecification = null
then invokeInitializers result state (NoResult(), state)
else
Expand Down
19 changes: 14 additions & 5 deletions VSharp.Test/Tests/VSharp.CSharpUtils/Unix.gold
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3240,6 +3240,15 @@ System.Runtime.Serialization.SafeSerializationManager ==> STRUCT System.Runtime.
System.SystemException ==> STRUCT System.SystemException[]
VSharp.CSharpUtils.Tests.Conditional+NewBool ==> STRUCT VSharp.CSharpUtils.Tests.Conditional+NewBool[]
VSharp.CSharpUtils.Tests.Conditional ==> STRUCT VSharp.CSharpUtils.Tests.Conditional[]
METHOD: System.Int32 VSharp.CSharpUtils.Tests.Conditional.DeclareAfterReturn(System.Boolean, System.Boolean, System.Int32)
RESULT: UNION[
| !f ~> x
| !flag & f ~> x + x + x + x
| f & flag ~> 42]
HEAP:
{ heap = <empty>, statics = s0 } where
---------- s0 = ----------
VSharp.CSharpUtils.Tests.Conditional ==> STRUCT VSharp.CSharpUtils.Tests.Conditional[]
METHOD: System.Int32 VSharp.CSharpUtils.Tests.Fibonacci.Fib2()
RESULT: 2
HEAP:
Expand Down Expand Up @@ -3901,9 +3910,9 @@ System.SystemException ==> STRUCT System.SystemException[]
VSharp.CSharpUtils.Tests.Lists ==> STRUCT VSharp.CSharpUtils.Tests.Lists[]
METHOD: System.Array VSharp.CSharpUtils.Tests.Lists.RetSystemArray2(System.Array)
RESULT: UNION[
| !(0 == arr) & (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[])) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (ArrayTypeVariable1 <: int32[,,]) | (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[])) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) ~> <ERROR: (HeapRef 1)>
| !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[,]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,]) ~> <ERROR: (HeapRef 6)>
| !(0 == arr) & !(1 < arr.0_Length) & (!(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[,]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,])) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[]) ~> <ERROR: (HeapRef 1)>
| !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) ~> <ERROR: (HeapRef 9)>
| (!(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[,]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,])) & (!(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) ~> <ERROR: (HeapRef 6)>
| (!(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) ~> (HeapRef arr)]
HEAP:
{ heap = h0, statics = s1 } where
Expand Down Expand Up @@ -3986,11 +3995,11 @@ HEAP:
| System.Exception.native_trace_ips ~> null]
arr ==> TypeVariable1{System.Object}: [|
1, 1, 1: UNION[
| !(0 == arr) & (!(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[]) | !(ArrayTypeVariable1 <: int32[,]) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length ~> 42];
| !(0 == arr) & (!(ArrayTypeVariable1 <: int32[,]) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length ~> 42];
1, 1: UNION[
| !(0 == arr) & (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,])) & (ArrayTypeVariable1 <: int32[,]) & 1 < arr.0_Length & 1 < arr.1_Length | !(0 == arr) & (!(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,]) & 1 < arr.0_Length & 1 < arr.1_Length ~> 7];
| !(0 == arr) & (ArrayTypeVariable1 <: int32[,]) & 1 < arr.0_Length & 1 < arr.1_Length ~> 7];
1: UNION[
| !(0 == arr) & (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,])) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | (!(0 == arr) & !(ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (!(0 == arr) & (!(1 < arr.1_Length) | !(1 < arr.2_Length)) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,,])) & (!(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[]) | !(ArrayTypeVariable1 <: int32[,]) | 0 == arr | 1 < arr.0_Length & 1 < arr.1_Length) & (!(ArrayTypeVariable1 <: int32[,]) | !(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) & (!(ArrayTypeVariable1 <: int32[]) | (!(0 == arr) & (ArrayTypeVariable1 <: int32[,]) | 1 < arr.0_Length & 1 < arr.1_Length) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) | 0 == arr | 1 < arr.0_Length) ~> 5];
| (!(0 == arr) & !(1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | (!(0 == arr) & !(ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (!(0 == arr) & (!(1 < arr.1_Length) | !(1 < arr.2_Length)) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,,])) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr | 1 < arr.0_Length & 1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) ~> 5];
... ... |]
---------- s1 = ----------
System.Environment ==> STRUCT System.Environment[
Expand Down
Loading