Skip to content
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

Splitting fixes #326

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Splitting fixes #326

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
6 changes: 3 additions & 3 deletions VSharp.SILI.Core/API.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -556,8 +556,8 @@ module API =
| Ite iteType ->
let filtered = iteType.filter (fun r -> Pointers.isBadRef r |> isTrue |> not)
filtered.ToDisjunctiveGvs()
|> List.iter (fun (g, r) -> state.memory.GuardedWriteClassField (Some g) (extractAddress r) field value)
| _ -> state.memory.WriteClassField (extractAddress reference) field value
|> List.iter (fun (g, r) -> state.memory.WriteClassField (Some g) (extractAddress r) field value)
| _ -> state.memory.WriteClassField None (extractAddress reference) field value

let WriteClassField state reference field value =
WriteClassFieldUnsafe emptyReporter state reference field value
Expand Down Expand Up @@ -733,7 +733,7 @@ module API =
let symbolicCase address =
let address, arrayType = memory.StringArrayInfo address (Some length)
Copying.fillArray state address arrayType (makeNumber 0) length char
memory.WriteClassField address Reflection.stringLengthField length
memory.WriteClassField None address Reflection.stringLengthField length
match string.term, concreteChar, concreteLen with
| HeapRef({term = ConcreteHeapAddress a} as address, sightType), Some (:? char as c), Some (:? int as len)
when cm.Contains a ->
Expand Down
2 changes: 1 addition & 1 deletion VSharp.SILI.Core/Copying.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ module internal Copying =
let stringAddress = ConcreteHeapAddress stringConcreteAddress
let stringAddress, arrayType = memory.StringArrayInfo stringAddress (Some arrayLength)
copyArray state arrayAddress startIndex arrayType stringAddress (makeNumber 0) arrayType arrayLength
memory.WriteClassField stringAddress Reflection.stringLengthField arrayLength
memory.WriteClassField None stringAddress Reflection.stringLengthField arrayLength

let copyCharArrayToString (state : state) arrayAddress stringConcreteAddress startIndex length =
let memory = state.memory
Expand Down
4 changes: 1 addition & 3 deletions VSharp.SILI.Core/Memory.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2040,9 +2040,7 @@ module internal Memory =
self.CommonWriteArrayIndex None address indices arrayType value
member self.WriteArrayRange address fromIndices toIndices arrayType value =
self.CommonWriteArrayRange None address fromIndices toIndices arrayType value
member self.WriteClassField address field value =
self.CommonWriteClassField None address field value
member self.GuardedWriteClassField guard address field value =
member self.WriteClassField guard address field value =
self.CommonWriteClassField guard address field value

member self.WriteStackLocation key value = writeStackLocation key value
Expand Down
254 changes: 129 additions & 125 deletions VSharp.SILI.Core/MemoryRegion.fs
View file
Open in desktop

Large diffs are not rendered by default.

4 changes: 1 addition & 3 deletions VSharp.SILI.Core/State.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -257,9 +257,7 @@ and IMemory =

abstract WriteStackLocation : stackKey -> term -> unit

abstract WriteClassField : term -> fieldId -> term -> unit
abstract GuardedWriteClassField : term option -> term -> fieldId -> term -> unit

abstract WriteClassField : term option -> term -> fieldId -> term -> unit
abstract Write : IErrorReporter -> term -> term -> unit
abstract AllocateOnStack : stackKey -> term -> unit

Expand Down
8 changes: 7 additions & 1 deletion VSharp.SILI.Core/Terms.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -220,16 +220,22 @@ and iteType = genericIteType<term>
and genericIteType<'a> = {branches: (term * 'a) list; elseValue : 'a}
with
static member FromGvs gvs =
if List.length gvs < 2 then internalfail "Empty and one-element unions are forbidden!"
if List.length gvs < 2 then internalfail "Empty and one-element ite's are forbidden!"
let branches, e = List.splitAt (List.length gvs - 1) gvs
{branches = branches; elseValue = e |> List.head |> snd}

member x.mapValues mapper =
{branches = List.map (fun (g, v) -> (g, mapper v)) x.branches; elseValue = mapper x.elseValue}

member x.filter predicate =
if predicate x.elseValue then
{branches = List.filter (snd >> predicate) x.branches; elseValue = x.elseValue}
else
List.filter (snd >> predicate) x.branches |> genericIteType<'a>.FromGvs

member x.exists predicate =
predicate x.elseValue || List.exists (fun (g, v) -> predicate v) x.branches

member x.choose mapper =
let chooser (g, v) = Option.bind (fun w -> Some(g, w)) (mapper v)
match mapper x.elseValue with
Expand Down
132 changes: 0 additions & 132 deletions VSharp.Test/Tests/Lists.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -532,59 +532,6 @@ public static int TestOverlappingCopy1(int[] a, int i)
return 3;
}

[TestSvm(94)]
public static int TestSolvingCopyOverwrittenValueUnreachable1(string[] a, string[] b)
{
if (a != null && b != null && a.Length > b.Length)
{
a[0] = "42";
b[0] = "4";
Array.Copy(a, 0, b, 0, b.Length);
if (b[0] != "42") // unreachable
{
return -1;
}

return 0;
}

return 3;
}

[TestSvm(95)]
public static int TestSolvingCopyOverwrittenValueUnreachable2(string[] a, int i, string[] b)
{
if (a != null && b != null && a.Length > b.Length)
{
b[i] = "500";
Array.Copy(a, 0, b, 0, b.Length);
if (b.Length > 0 && a[i] != "500" && b[i] == "500") // unreachable
{
return -1;
}

return 0;
}

return 3;
}

[TestSvm(94)]
public static int TestSolvingCopy8(object[] a, object[] b, int i)
{
if (a.Length > b.Length && 0 <= i && i < b.Length)
{
Array.Fill(a, "abc");
Array.Copy(a, b, b.Length);

if (b[i] == b[i + 1])
return 42;
return 10;
}

return 3;
}

[TestSvm(97)]
public static int TestSolvingCopy9(object[] a, int i, object[] b)
{
Expand Down Expand Up @@ -785,20 +732,6 @@ public class MyClass
public int x;
}

[TestSvm(88)]
public static int LastRecordReachability(string[] a, string[] b, int i, string s)
{
a[i] = "1";
b[1] = s;
if (b[1] != s)
{
// unreachable
return -1;
}

return 0;
}

[TestSvm(90)]
public static int ArrayElementsAreReferences(MyClass[] a, int i, int j)
{
Expand Down Expand Up @@ -924,44 +857,6 @@ public static int ConcreteDictionaryTest(int v)
return 0;
}

[TestSvm(100)]
public static int ConcreteDictionaryTest1(int a, string b)
{
var d = new Dictionary<int, List<string>>();
d.Add(1, new List<string> { "2", "3" });
d.Add(4, new List<string> { "5", "6" });
if (d.TryGetValue(a, out var res))
{
if (res.Contains(b))
return 1;
return 0;
}

return 2;
}

public class Person
{
public string FirstName { get; set; }
public string LastName { get; init; }
};

[TestSvm(95)]
public static int IteKeyWrite(int i)
{
var a = new Person[4];
a[0] = new Person() {FirstName = "asd", LastName = "qwe"};
a[3] = new Person() {FirstName = "zxc", LastName = "vbn"};
var p = a[i];
p.FirstName = "323";
if (i == 0 && a[3].FirstName == "323")
{
return -1;
}

return 1;
}

[TestSvm(100)]
public static int ListContains(int a, int b)
{
Expand Down Expand Up @@ -1413,33 +1308,6 @@ public static int ConcurrentDict(int a, int b)
return -1;
return 0;
}
[TestSvm(95)]
public static int TestSplittingWithCopy(int srcI, int dstI, int len)
{
string[] arr = {"a", "b", "c", "d", "e"};
var a = new string[5];
Array.Copy(arr, srcI, a, dstI, len);
if (a[2].Length == 3)
return -1;
return 1;
}
[TestSvm(91)]
public static int TestSplittingWithCopyRegionsImportance(string[] a, int i)
{
a[i] = "a";
a[1] = "b";
var b = new string[a.Length];
Array.Copy(a, 0, b, 0, a.Length);
if (i == 1 && b[i] == "a") // unreachable
// record b[i], "a" exists only if i != 1
return -1;
if (i != 1 && b[i] != "a") // unreachable
{
return -2;
}

return 1;
}

[TestSvm(83)]
public static int VolatileWrite()
Expand Down
Loading
Loading