Skip to content

Commit 7c7911b

Browse files
MchKosticynMchKosticyn
committed
[fix]
- using internal implementations for intrinsics - using internal implementations for complex functions - new externs - style fixes - method's generic arguments are passed as parameters into internal implementations
1 parent 764293a commit 7c7911b

27 files changed

+256
-28
lines changed

‎VSharp.CSharpUtils/Interop.cs

+1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ public unsafe class Interop
77
[Implements("System.Int32 Interop+Kernel32.LCMapStringEx(System.String, System.UInt32, System.Char*, System.Int32, System.Void*, System.Int32, System.Void*, System.Void*, System.IntPtr)")]
88
public static int LCMapStringEx(string a, uint b, char* c, int d, void* e, int f, void* g, void* h, IntPtr i)
99
{
10+
// TODO: for a locale specified by name, maps an input character string to another using a specified transformation, or generates a sort key for the input string
1011
return 0;
1112
}
1213
}

‎VSharp.CSharpUtils/NumberFormatInfo.cs

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
namespace VSharp.CSharpUtils
2+
{
3+
public static class NumberFormatInfo
4+
{
5+
[Implements("System.Globalization.NumberFormatInfo System.Globalization.NumberFormatInfo.get_CurrentInfo()")]
6+
public static System.Globalization.NumberFormatInfo get_CurrentInfo()
7+
{
8+
return new System.Globalization.NumberFormatInfo();
9+
}
10+
}
11+
}

‎VSharp.InternalCalls/ByReference.fs

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
namespace VSharp.System
2+
3+
open global.System
4+
open VSharp
5+
open VSharp.Core
6+
7+
// ------------------------------ System.ByReference --------------------------------
8+
9+
module ByReference =
10+
11+
let internal ctor (state : state) (args : term list) : (term * state) list =
12+
assert(List.length args = 2)
13+
let this, ref = List.item 0 args, List.item 1 args
14+
let ptr = Types.CastReferenceToPointer state ref
15+
let fields = Terms.TypeOf this |> Types.ToDotNetType |> Reflection.fieldsOf false
16+
assert(Array.length fields = 1)
17+
let field = Array.head fields |> fst
18+
let fieldRef = Memory.ReferenceField state this field
19+
Memory.WriteSafe state fieldRef ptr |> List.map (withFst Nop)

‎VSharp.InternalCalls/ByReference.fsi

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
namespace VSharp.System
2+
3+
open global.System
4+
open VSharp
5+
open VSharp.Core
6+
7+
module internal ByReference =
8+
9+
[<Implements("System.Void System.ByReference`1[System.Char]..ctor(this, System.Char&)")>]
10+
val internal ctor : state -> term list -> (term * state) list

‎VSharp.InternalCalls/ChessDotNet.fs

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
namespace VSharp.System
2+
3+
open global.System
4+
open VSharp
5+
open VSharp.Core
6+
7+
// ------------------------------ ChessDotNet --------------------------------
8+
9+
module ChessDotNet =
10+
11+
// TODO: now this works only for Span, made from String #do
12+
let internal Equals (state : state) (args : term list) : term * state =
13+
assert(List.length args = 2)
14+
let this, another = List.item 0 args, List.item 1 args
15+
let thisType = Terms.MostConcreteTypeOfHeapRef state this
16+
let anotherType = Terms.MostConcreteTypeOfHeapRef state another
17+
let checkContents () =
18+
let thisFields = Types.ToDotNetType thisType |> Reflection.fieldsOf false
19+
assert(Array.length thisFields = 2)
20+
let anotherFields = Types.ToDotNetType anotherType |> Reflection.fieldsOf false
21+
assert(Array.length anotherFields = 2)
22+
let thisFstField = fst thisFields.[0] |> Memory.ReadField state this
23+
let thisSndField = fst thisFields.[1] |> Memory.ReadField state this
24+
let anotherFstField = fst anotherFields.[0] |> Memory.ReadField state another
25+
let anotherSndField = fst anotherFields.[1] |> Memory.ReadField state another
26+
thisFstField === anotherFstField &&& thisSndField === anotherSndField, state
27+
if thisType <> anotherType then False, state // TODO: make this check symbolic #do
28+
else checkContents ()

‎VSharp.InternalCalls/ChessDotNet.fsi

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
namespace VSharp.System
2+
3+
open global.System
4+
open VSharp
5+
open VSharp.Core
6+
7+
module internal ChessDotNet =
8+
9+
[<Implements("System.Boolean ChessDotNet.Position.Equals(this, System.Object)")>]
10+
val internal Equals : state -> term list -> term * state

‎VSharp.InternalCalls/IntPtr.fs

+4-5
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,7 @@ open VSharp.Core
99
module IntPtr =
1010

1111
let internal ctor (state : state) (args : term list) : (term * state) list =
12-
match args with
13-
| this :: [term] ->
14-
let ptr = MakeIntPtr term state
15-
Memory.WriteSafe state this ptr |> List.map (withFst Nop)
16-
| _ -> __notImplemented__()
12+
assert(List.length args = 2)
13+
let this, term = List.item 0 args, List.item 1 args
14+
let ptr = MakeIntPtr term state
15+
Memory.WriteSafe state this ptr |> List.map (withFst Nop)

‎VSharp.InternalCalls/Loader.fs

+1
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ module Loader =
2222
Assembly.Load(new AssemblyName("VSharp.CSharpUtils")).GetType("VSharp.CSharpUtils.RuntimeHelpersUtils")
2323
Assembly.Load(new AssemblyName("VSharp.CSharpUtils")).GetType("VSharp.CSharpUtils.CLRConfig")
2424
Assembly.Load(new AssemblyName("VSharp.CSharpUtils")).GetType("VSharp.CSharpUtils.Interop")
25+
Assembly.Load(new AssemblyName("VSharp.CSharpUtils")).GetType("VSharp.CSharpUtils.NumberFormatInfo")
2526
]
2627
|> collectImplementations
2728

‎VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fs

+11-2
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ namespace VSharp.System
33
open global.System
44
open VSharp
55
open VSharp.Core
6+
open System.Runtime.InteropServices
7+
open System.Reflection
68

79
module Runtime_CompilerServices_RuntimeHelpers =
8-
open System.Runtime.InteropServices
9-
open System.Reflection
1010

1111
let private reinterpretValueTypeAsByteArray (value : obj) size =
1212
let rawData = Array.create size Byte.MinValue
@@ -132,3 +132,12 @@ module Runtime_CompilerServices_RuntimeHelpers =
132132
GuardedStatedApplyStatementK state arrayRef (fun state arrayRef k ->
133133
GuardedStatedApplyStatementK state handleTerm (fun state handleTerm k ->
134134
initializeArray state arrayRef handleTerm |> k) (List.map k >> List.concat)) (List.map snd)
135+
136+
// This function checks, whether type can be checked on equality using only it's bits
137+
// Example: any value type, because it doesn't have metadata
138+
let IsBitwiseEquatable (state : state) (args : term list) : term * state =
139+
assert(List.length args = 1)
140+
let typ = List.head args
141+
match typ with
142+
| {term = Concrete(:? System.Type as typ, _)} -> MakeBool typ.IsValueType, state
143+
| _ -> __unreachable__()

‎VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fsi

+5
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,12 @@
11
namespace VSharp.System
22

3+
open global.System
4+
open VSharp
35
open VSharp.Core
46

57
module Runtime_CompilerServices_RuntimeHelpers =
68

79
val InitializeArray : state -> term -> term -> state list
10+
11+
[<Implements("System.Boolean System.Runtime.CompilerServices.RuntimeHelpers.IsBitwiseEquatable()")>]
12+
val IsBitwiseEquatable : state -> term list -> term * state

‎VSharp.InternalCalls/Span.fs

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
namespace VSharp.System
2+
3+
open global.System
4+
open VSharp
5+
open VSharp.Core
6+
7+
// ------------------------------ System.ReadOnlySpan --------------------------------
8+
9+
module ReadOnlySpan =
10+
11+
// TODO: now this works only for Span, made from String #do
12+
let internal get_Item (state : state) (args : term list) : term * state =
13+
assert(List.length args = 2)
14+
let this, index = List.item 0 args, List.item 1 args
15+
let span = Memory.ReadSafe state this
16+
let spanFields = Terms.TypeOf span |> Types.ToDotNetType |> Reflection.fieldsOf false
17+
assert(Array.length spanFields = 2)
18+
let ptrField = fst spanFields.[0]
19+
// TODO: throw ThrowIndexOutOfRangeException if len is less or equal to index
20+
// let lenField = fst spanFields.[1]
21+
// let len = Memory.ReadField state span lenField
22+
let byRefStruct = Memory.ReadField state span ptrField
23+
let byRefFields = Terms.TypeOf byRefStruct |> Types.ToDotNetType |> Reflection.fieldsOf false
24+
assert(Array.length byRefFields = 1)
25+
let byRefField = fst byRefFields.[0]
26+
let ptrToStringArray = Memory.ReadField state byRefStruct byRefField
27+
match ptrToStringArray.term with
28+
| Ptr(Some(ClassField(addr, field)), _, None) when field = Reflection.stringFirstCharField ->
29+
let ref = HeapRef addr (ArrayType(Types.FromDotNetType typeof<char>, Vector))
30+
Memory.ReferenceArrayIndex ref [index], state
31+
| _ -> __insufficientInformation__ "now Span works only for String"

‎VSharp.InternalCalls/Span.fsi

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
namespace VSharp.System
2+
3+
open global.System
4+
open VSharp
5+
open VSharp.Core
6+
7+
module internal ReadOnlySpan =
8+
9+
[<Implements("System.Char& System.ReadOnlySpan`1[System.Char].get_Item(this, System.Int32)")>]
10+
// TODO: make this method works not only for char Span #do
11+
val internal get_Item : state -> term list -> term * state

‎VSharp.InternalCalls/String.fs

+29-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
namespace VSharp.System
22

3+
open FSharpx.Collections
34
open global.System
45
open VSharp
56
open VSharp.Core
@@ -26,6 +27,33 @@ module internal String =
2627
length, state
2728

2829
let GetChars (state : state) (args : term list) =
29-
assert (List.length args = 2)
30+
assert(List.length args = 2)
3031
let this, index = List.item 0 args, List.item 1 args
3132
Memory.ReadStringChar state this index, state
33+
34+
let ToUpperInvariant (state : state) (args : term list) =
35+
assert(List.length args = 1)
36+
let this = List.head args
37+
match this.term with
38+
| HeapRef({term = ConcreteHeapAddress _}, _) ->
39+
let readOneChar i =
40+
let index = Concrete i Types.IndexType
41+
match Memory.ReadStringChar state this index with
42+
| {term = Concrete(obj, _)} -> obj :?> char
43+
| _ -> __insufficientInformation__ "ToUpperInvariant works only for fully concrete strings right now"
44+
let length = Memory.ReadField state this Reflection.stringLengthField
45+
match length.term with
46+
| Concrete(obj, _) ->
47+
let len = obj :?> int
48+
let indices = List.init len id
49+
let string = List.map readOneChar indices |> String.Concat
50+
Memory.AllocateString string state
51+
| _ -> __insufficientInformation__ "ToUpperInvariant works only for concrete length strings right now"
52+
| _ -> __insufficientInformation__ "ToUpperInvariant works only for concrete address strings right now"
53+
54+
let CreateFromChar (state : state) (args : term list) : (term * state) list =
55+
assert(List.length args = 1)
56+
let char = List.head args
57+
let string, state = Memory.AllocateString " " state
58+
let states = Memory.WriteStringChar state string [Concrete 0 Types.IndexType] char
59+
List.map (withFst string) states

‎VSharp.InternalCalls/String.fsi

+8
Original file line numberDiff line numberDiff line change
@@ -16,3 +16,11 @@ module internal String =
1616

1717
[<Implements("System.Char System.String.get_Chars(this, System.Int32)")>]
1818
val GetChars : state -> term list -> term * state
19+
20+
[<Implements("System.String System.String.ToUpperInvariant(this)")>]
21+
// NOTE: this works only for fully concrete strings
22+
// TODO: delete this and explore .NET code (unsafe is needed)
23+
val ToUpperInvariant : state -> term list -> term * state
24+
25+
[<Implements("System.String System.String.CreateFromChar(System.Char)")>]
26+
val CreateFromChar : state -> term list -> (term * state) list

‎VSharp.InternalCalls/Type.fs

+11-8
Original file line numberDiff line numberDiff line change
@@ -6,30 +6,30 @@ open VSharp.Core
66

77
// ------------------------------ mscorlib.System.Type --------------------------------
88

9-
module Type =
9+
module internal Type =
1010

11-
let internal GetTypeFromHandle (state : state) (args : term list) : term * state =
11+
let GetTypeFromHandle (state : state) (args : term list) : term * state =
1212
assert (List.length args = 1)
1313
let handle = List.head args
1414
let t =
1515
match handle.term with
16-
| Concrete(:? System.RuntimeTypeHandle as handle, _) -> System.Type.GetTypeFromHandle handle
16+
| Concrete(:? System.RuntimeTypeHandle as handle, _) -> Type.GetTypeFromHandle handle
1717
| _ -> __notImplemented__()
1818
let t = typeof<Object>.GetType()
1919
Memory.AllocateDefaultClass state (Types.FromDotNetType t) // TODO: hack #do
2020
// TypeOfMethod state (Types.FromDotNetType state t)
2121
// TODO: restore it after rewriting marshaling/unmarshaling
2222
// __notImplemented__()
2323

24-
let internal GetAssembly (state : state) (args : term list) : term * state =
24+
let GetAssembly (state : state) (args : term list) : term * state =
2525
assert (List.length args = 1)
2626
let t = typeof<Object>.Assembly.GetType()
2727
Memory.AllocateDefaultClass state (Types.FromDotNetType t) // TODO: hack #do
2828
// TypeOfMethod state (Types.FromDotNetType state t)
2929
// TODO: restore it after rewriting marshaling/unmarshaling
3030
// __notImplemented__()
3131

32-
let internal GetType (state : state) (args : term list) : term * state =
32+
let GetType (state : state) (args : term list) : term * state =
3333
assert(List.length args = 1)
3434
let ref = List.head args
3535
// GetTypeMethod state ref
@@ -42,11 +42,14 @@ module Type =
4242
let typ2 = args |> List.tail |> List.head
4343
transform (typ1 === typ2), state
4444

45-
let internal op_Inequality (state : state) (args : term list) =
45+
let op_Inequality (state : state) (args : term list) =
4646
equality (!!) state args
4747

48-
let internal op_Equality (state : state) (args : term list) =
48+
let op_Equality (state : state) (args : term list) =
4949
equality id state args
5050

51-
let internal isGenericTypeDefinition (state : state) (args : term list) =
51+
let isGenericTypeDefinition (state : state) (_ : term list) =
5252
MakeBool false, state
53+
54+
let get_Name (state : state) (_ : term list) =
55+
Memory.AllocateString "RuntimeType" state

‎VSharp.InternalCalls/Type.fsi

+9-6
Original file line numberDiff line numberDiff line change
@@ -6,19 +6,22 @@ open VSharp.Core
66

77
module internal Type =
88
[<Implements("System.Type System.Type.GetTypeFromHandle(System.RuntimeTypeHandle)")>]
9-
val internal GetTypeFromHandle : state -> term list -> term * state
9+
val GetTypeFromHandle : state -> term list -> term * state
1010

1111
[<Implements("System.Reflection.RuntimeAssembly System.RuntimeTypeHandle.GetAssembly(System.RuntimeType)")>]
12-
val internal GetAssembly : state -> term list -> term * state
12+
val GetAssembly : state -> term list -> term * state
1313

1414
[<Implements("System.Type System.Object.GetType(this)")>]
15-
val internal GetType : state -> term list -> term * state
15+
val GetType : state -> term list -> term * state
1616

1717
[<Implements("System.Boolean System.Type.op_Inequality(System.Type, System.Type)")>]
18-
val internal op_Inequality : state -> term list -> term * state
18+
val op_Inequality : state -> term list -> term * state
1919

2020
[<Implements("System.Boolean System.Type.op_Equality(System.Type, System.Type)")>]
21-
val internal op_Equality : state -> term list -> term * state
21+
val op_Equality : state -> term list -> term * state
2222

2323
[<Implements("System.Boolean System.RuntimeTypeHandle.IsGenericTypeDefinition(System.RuntimeType)")>]
24-
val internal isGenericTypeDefinition : state -> term list -> term * state
24+
val isGenericTypeDefinition : state -> term list -> term * state
25+
26+
[<Implements("System.String System.RuntimeType.get_Name(this)")>]
27+
val get_Name : state -> term list -> term * state

‎VSharp.InternalCalls/Unsafe.fs

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
namespace VSharp.System
2+
3+
open global.System
4+
open VSharp
5+
open VSharp.Core
6+
7+
// ------------------------------ System.Unsafe --------------------------------
8+
9+
module Unsafe =
10+
11+
let internal AsPointer (state : state) (args : term list) : term * state =
12+
assert(List.length args = 2)
13+
let ref = List.item 1 args
14+
let ptr = Types.CastReferenceToPointer state ref
15+
Types.Cast ptr (Pointer Void), state

‎VSharp.InternalCalls/Unsafe.fsi

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
namespace VSharp.System
2+
3+
open global.System
4+
open VSharp
5+
open VSharp.Core
6+
7+
module internal Unsafe =
8+
9+
[<Implements("System.Void* Internal.Runtime.CompilerServices.Unsafe.AsPointer(System.RuntimeType&)")>]
10+
val internal AsPointer : state -> term list -> term * state

‎VSharp.InternalCalls/VSharp.InternalCalls.fsproj

+8
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,14 @@
2121
<Compile Include="Type.fs" />
2222
<Compile Include="IntPtr.fsi" />
2323
<Compile Include="IntPtr.fs" />
24+
<Compile Include="Unsafe.fsi" />
25+
<Compile Include="Unsafe.fs" />
26+
<Compile Include="ByReference.fsi" />
27+
<Compile Include="ByReference.fs" />
28+
<Compile Include="Span.fsi" />
29+
<Compile Include="Span.fs" />
30+
<Compile Include="ChessDotNet.fsi" />
31+
<Compile Include="ChessDotNet.fs" />
2432
<Compile Include="Loader.fs" />
2533
</ItemGroup>
2634

‎VSharp.SILI.Core/API.fs

+8
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,14 @@ module API =
242242
Memory.writeArrayIndex state addr indices arrayType value
243243
| _ -> internalfailf "Writing field of class: expected reference, but got %O" reference)
244244
state reference
245+
let WriteStringChar state reference index value =
246+
Memory.guardedStatedMap
247+
(fun state reference ->
248+
match reference.term with
249+
| HeapRef(addr, typ) when Memory.mostConcreteTypeOfHeapRef state addr typ = Types.String ->
250+
Memory.writeArrayIndex state addr index (Types.Char, 1, true) value
251+
| _ -> internalfailf "Writing field of class: expected reference, but got %O" reference)
252+
state reference
245253
let WriteStaticField state typ field value = Memory.writeStaticField state typ field value
246254

247255
let DefaultOf typ = makeDefaultValue typ

‎VSharp.SILI.Core/API.fsi

+1
Original file line numberDiff line numberDiff line change
@@ -158,6 +158,7 @@ module API =
158158
val WriteStructField : term -> fieldId -> term -> term
159159
val WriteClassField : state -> term -> fieldId -> term -> state list
160160
val WriteArrayIndex : state -> term -> term list -> term -> state list
161+
val WriteStringChar : state -> term -> term list -> term -> state list
161162
val WriteStaticField : state -> symbolicType -> fieldId -> term -> state
162163

163164
val DefaultOf : symbolicType -> term

0 commit comments

Comments
 (0)