Merge pull request #325 from MchKosticyn/master

Concrete memory and unsafe operations fixes

Author: MchKosticyn

.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}"