Concrete memory and unsafe operations fixes

.github/workflows/build_vsharp.yml

@@ -5,7 +5,7 @@ on:
 
 jobs:
   build:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     steps:
     - name: Checkout VSharp
       uses: actions/checkout@v3

VSharp.API/VSharpOptions.cs

@@ -89,7 +89,7 @@ public readonly record struct VSharpOptions
     private const string DefaultOutputDirectory = "";
     private const string DefaultRenderedTestsDirectory = "";
     private const bool DefaultRenderTests = false;
-    private const SearchStrategy DefaultSearchStrategy = SearchStrategy.BFS;
+    private const SearchStrategy DefaultSearchStrategy = SearchStrategy.ExecutionTreeContributedCoverage;
     private const Verbosity DefaultVerbosity = Verbosity.Quiet;
     private const uint DefaultRecursionThreshold = 0u;
     private const ExplorationMode DefaultExplorationMode = ExplorationMode.Sili;

VSharp.Explorer/Explorer.fs

@@ -75,7 +75,6 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
     let emptyState = Memory.EmptyIsolatedState()
     let interpreter = ILInterpreter()
 
-
     do
         if options.visualize then
             DotVisualizer explorationOptions.outputDirectory :> IVisualizer |> Application.setVisualizer

VSharp.Explorer/Statistics.fs

@@ -16,7 +16,6 @@ open VSharp.Interpreter.IL
 open VSharp.Utils
 
 open CilState
-open IpOperations
 open CodeLocation
 
 type pob = {loc : codeLocation; lvl : uint; pc : pathCondition}

VSharp.IL/MethodBody.fs

@@ -84,7 +84,13 @@ type MethodWithBody internal (m : MethodBase) =
 
     let actualMethod =
         if not isCSharpInternalCall.Value then m
-        else Loader.CSharpImplementations[fullGenericMethodName.Value]
+        else
+            let method = Loader.CSharpImplementations[fullGenericMethodName.Value]
+            if method.IsGenericMethod && (m.DeclaringType.IsGenericType || m.IsGenericMethod) then
+                let _, genericArgs, _ = Reflection.generalizeMethodBase m
+                method.MakeGenericMethod(genericArgs)
+            else method
+
     let methodBodyBytes =
         if isFSharpInternalCall.Value then null
         else actualMethod.GetMethodBody()

VSharp.InternalCalls/Buffer.fs

@@ -53,7 +53,7 @@ module internal Buffer =
             let checkDst (info, cilState : cilState) =
                 match info with
                 | Some (dstAddress : address) ->
-                    let checkSrc (info, cilState : cilState) =
+                    let checkSrc info (cilState : cilState) =
                         match info with
                         | Some (srcAddress : address) ->
                             let dstType = lazy dstAddress.TypeOfLocation
@@ -71,28 +71,26 @@ module internal Buffer =
                             match dstAddress, srcAddress with
                             | _ when allSafe() ->
                                 let value = cilState.Read (Ref srcAddress)
-                                let cilStates = cilState.Write (Ref dstAddress) value
-                                assert(List.length cilStates = 1)
-                                List.head cilStates
+                                cilState.Write (Ref dstAddress) value
                             | _ when dstSafe.Value ->
                                 let ptr = Types.Cast (Ref srcAddress) (dstType.Value.MakePointerType())
                                 let value = cilState.Read ptr
-                                let cilStates = cilState.Write (Ref dstAddress) value
-                                assert(List.length cilStates = 1)
-                                List.head cilStates
+                                cilState.Write (Ref dstAddress) value
                             | _ when srcSafe.Value ->
                                 let value = cilState.Read (Ref srcAddress)
                                 let ptr = Types.Cast (Ref dstAddress) (srcType.Value.MakePointerType())
-                                let cilStates = cilState.Write ptr value
-                                assert(List.length cilStates = 1)
-                                List.head cilStates
+                                cilState.Write ptr value
                             | ArrayIndex(dstAddress, dstIndices, dstArrayType), ArrayIndex(srcAddress, srcIndices, srcArrayType) ->
                                 Copy dstAddress dstIndex dstIndices dstArrayType srcAddress srcIndex srcIndices srcArrayType state bytesCount
-                                cilState
                             // TODO: implement unsafe copy
                             | _ -> internalfail $"CommonMemmove unexpected addresses {srcAddress}, {dstAddress}"
-                        | None -> cilState
-                    getAddress cilState src |> List.map checkSrc
+                        | None -> ()
+                    let addressesWithStates = getAddress cilState src
+                    let mutable resultCilStates = List.empty
+                    for address, cilState in addressesWithStates do
+                        checkSrc address cilState
+                        resultCilStates <- cilState :: resultCilStates
+                    resultCilStates
                 | None -> cilState |> List.singleton
             getAddress cilState dst |> List.collect checkDst
 

VSharp.InternalCalls/IntPtr.fs

@@ -12,7 +12,6 @@ module IntPtr =
         let ptr = MakeIntPtr term
         Memory.Write state this ptr
         Nop()
-
 
     let internal intPtrCtorFromInt (state : state) (args : term list) : term =
         assert(List.length args = 2)

VSharp.InternalCalls/Interlocked.fs

@@ -1,7 +1,7 @@
 namespace VSharp.System
 
 open global.System
-open VSharp
+
 open VSharp.Core
 open VSharp.Interpreter.IL
 open VSharp.Interpreter.IL.CilState
@@ -11,10 +11,9 @@ module internal Interlocked =
     let exchange (interpreter : IInterpreter) (cilState : cilState) location value =
         let exchange (cilState : cilState) k =
             let currentValue = cilState.Read location
-            let cilStates = cilState.Write location value
-            for cilState in cilStates do
-                cilState.Push currentValue
-            k cilStates
+            cilState.Write location value
+            cilState.Push currentValue
+            List.singleton cilState |> k
         interpreter.NpeOrInvoke cilState location exchange id
 
     let commonCompareExchange (interpreter : IInterpreter) (cilState : cilState) location value compared =
@@ -23,7 +22,7 @@ module internal Interlocked =
             let cilStates =
                 cilState.StatedConditionalExecutionCIL
                     (fun cilState k -> k (currentValue === compared, cilState))
-                    (fun cilState k -> k (cilState.Write location value))
+                    (fun cilState k -> k (cilState.Write location value; List.singleton cilState))
                     (fun cilState k -> k (List.singleton cilState))
                     id
             for cilState in cilStates do

VSharp.InternalCalls/Object.fs

@@ -41,12 +41,8 @@ module internal Object =
                 else t
             let newObject = Memory.AllocateDefaultClass state t
             let fields = Reflection.fieldsOf false t
-            let copyField cilStates (field, _) =
-                let copyForState (cilState : cilState) =
-                    let v = cilState.ReadField object field
-                    cilState.WriteClassField newObject field v
-                List.collect copyForState cilStates
-            let cilStates = Array.fold copyField (List.singleton cilState) fields
-            for cilState in cilStates do
-                cilState.Push newObject
-            cilStates
+            for field, _ in fields do
+                let v = cilState.ReadField object field
+                cilState.WriteClassField newObject field v
+            cilState.Push newObject
+            List.singleton cilState

VSharp.InternalCalls/Span.fs

@@ -137,6 +137,7 @@ module internal ReadOnlySpan =
         let span = cilState.Read this
         let initializedSpan = InitSpanStruct cilState span refToFirst length
         cilState.Write this initializedSpan
+        List.singleton cilState
 
     let CtorFromPtr (i : IInterpreter) (cilState : cilState) (args : term list) : cilState list =
         assert(List.length args = 4)
@@ -237,8 +238,7 @@ module internal ReadOnlySpan =
             let arrayRef = Memory.AllocateConcreteObject state rawData arrayType
             let refToFirstElement = Memory.ReferenceArrayIndex state arrayRef [MakeNumber 0] None
             let count = MakeNumber rawData.Length
-            let cilStates = cilState.Write countRef count
-            assert(List.length cilStates = 1 && cilStates[0] = cilState)
+            cilState.Write countRef count
             cilState.Push refToFirstElement
             List.singleton cilState
         | _ -> internalfail $"GetSpanDataFrom: unexpected field handle {fieldHandleTerm} or type handle {typeHandleTerm}"

VSharp.InternalCalls/String.fs

@@ -47,19 +47,18 @@ module internal String =
             (length >>= zero)
             &&& (startIndex >>= zero)
         let copy (cilState : cilState) k =
-            let cilStates = cilState.WriteClassField this Reflection.stringLengthField length
+            cilState.WriteClassField this Reflection.stringLengthField length
             let bytesCount = Mul length (MakeNumber sizeof<char>)
-            let memMove cilState =
-                Buffer.CommonMemmove cilState this None ptr (Some startIndex) bytesCount
-            List.collect memMove cilStates |> k
+            Buffer.CommonMemmove cilState this None ptr (Some startIndex) bytesCount |> k
         let checkPtr (cilState : cilState) k =
             cilState.StatedConditionalExecutionCIL
                 (fun state k -> k (!!(IsBadRef ptr), state))
                 copy
                 (i.Raise i.ArgumentOutOfRangeException)
                 k
         let emptyStringCase (cilState : cilState) k =
-            cilState.WriteClassField this Reflection.stringLengthField zero |> k
+            cilState.WriteClassField this Reflection.stringLengthField zero
+            List.singleton cilState |> k
         let checkLength (cilState : cilState) k =
             cilState.StatedConditionalExecutionCIL
                 (fun state k -> k (length === zero, state))

VSharp.InternalCalls/Thread.fs

@@ -33,7 +33,8 @@ module Thread =
         assert(List.length args = 2)
         let obj, resultRef = args[0], args[1]
         let success (cilState : cilState) k =
-            cilState.Write resultRef (True()) |> k
+            cilState.Write resultRef (True())
+            List.singleton cilState |> k
         cilState.BranchOnNullCIL obj
             (interpreter.Raise interpreter.ArgumentNullException)
             success

VSharp.InternalCalls/Unsafe.fs

@@ -92,14 +92,16 @@ module internal Unsafe =
         let typ = Helpers.unwrapType typ
         let castedPtr = Types.Cast ref (typ.MakePointerType())
         let writeByPtr (cilState : cilState) k =
-            cilState.Write castedPtr value |> k
+            cilState.Write castedPtr value
+            List.singleton cilState |> k
         i.NpeOrInvoke cilState castedPtr writeByPtr id
 
     let WriteUnaligned (i : IInterpreter) (cilState : cilState) (args : term list) =
         assert(List.length args = 2)
         let ref, value = args[0], args[1]
         let writeByPtr (cilState : cilState) k =
-            cilState.Write ref value |> k
+            cilState.Write ref value
+            List.singleton cilState |> k
         i.NpeOrInvoke cilState ref writeByPtr id
 
     let SizeOf (_ : state) (args : term list) : term =

VSharp.InternalCalls/Volatile.fs

@@ -21,3 +21,4 @@ module Volatile =
         assert(List.length args = 3)
         let ref, value = args[1], args[2]
         cilState.Write ref value
+        List.singleton cilState

VSharp.Runner/RunnerProgram.cs

@@ -2,7 +2,6 @@
 using System;
 using System.Collections.Generic;
 using System.CommandLine;
-using System.CommandLine.Invocation;
 using System.Diagnostics;
 using System.IO;
 using System.Linq;

VSharp.SILI.Core/ConcreteMemory.fs

@@ -30,18 +30,6 @@ type private ChildLocation =
         assert x.Type.IsValueType
         { x with structFields = fieldId :: x.structFields }
 
-    member x.Includes(childKind : ChildKind) = x.childKind = childKind
-
-    member x.Includes(childLoc : ChildLocation) =
-        x.childKind = childLoc.childKind
-        &&
-        let structFields = x.structFields
-        let otherStructFields = childLoc.structFields
-        let length = List.length structFields
-        let otherLength = List.length otherStructFields
-        length = otherLength && otherStructFields = structFields
-        || length > otherLength && otherStructFields = List.skip (length - otherLength) structFields
-
 type private Cell =
     | Concrete of physicalAddress
     | Symbolic
@@ -122,17 +110,15 @@ type public ConcreteMemory private (physToVirt, virtToPhys, children, parents, c
             assert(parent.object <> null)
             let childObj = child.object
             let childIsNull = childObj = null
+            let childType = childLoc.Type
             if childIsNull && update then
+                assert(not childType.IsValueType || TypeUtils.isNullable childType)
                 let exists, childDict = children.TryGetValue parent
-                if exists then
-                    for KeyValue(childLoc, _) in childDict do
-                        if childLoc.Includes childLoc then
-                            childDict.Remove childLoc |> ignore
+                if exists then childDict.Remove childLoc |> ignore
             elif not childIsNull then
-                let t = childLoc.Type
-                if t.IsValueType then
+                if childType.IsValueType then
                     assert(childObj :? ValueType)
-                    let fields = Reflection.fieldsOf false t
+                    let fields = Reflection.fieldsOf false childType
                     for fieldId, fieldInfo in fields do
                         if Reflection.isReferenceOrContainsReferences fieldId.typ then
                             let child = { object = fieldInfo.GetValue childObj }
@@ -531,6 +517,13 @@ type public ConcreteMemory private (physToVirt, virtToPhys, children, parents, c
         let removed = virtToPhys.Remove address
         assert removed
         x.RemoveFromFullyConcretesRec phys
+        x.MarkSymbolic phys
+
+    member private x.MarkSymbolic phys =
+        let exists, parentDict = parents.TryGetValue phys
+        if exists then
+            for KeyValue(parent, childKind) in parentDict do
+                children[parent][childKind] <- Symbolic
 
     member private x.RemoveFromFullyConcretesRec phys =
         let removed = HashSet<physicalAddress>()
@@ -543,6 +536,5 @@ type public ConcreteMemory private (physToVirt, virtToPhys, children, parents, c
                 fullyConcretes.Remove child |> ignore
                 let exists, parentDict = parents.TryGetValue child
                 if exists then
-                    for KeyValue(parent, childKind) in parentDict do
-                        children[parent][childKind] <- Symbolic
+                    for KeyValue(parent, _) in parentDict do
                         queue.Enqueue parent