Stabilization: part XXIV #284
Conversation
- style fixes - fixed mul.ovf.un - fixed 'ErrorReporter' - fixed 'localloc' instruction
- added TODO's
- fixed 'bytesToObj' function - added trusted intrinsics
- added new internal calls - some internal calls moved to concrete calls
- fixed rendering boxed values
- deleted unsolvable generic tests - added new test
MchKosticyn
force-pushed
the
pointers
branch
from
ab7c118
to
adf368e
Compare
MchKosticyn
force-pushed
the
pointers
branch
from
adf368e
to
bf9b21b
Compare
VSharp.CSharpUtils/StringUtils.cs
Outdated
| @@ -13,6 +13,15 @@ public static int GetHashCode(string str) | |||
| [Implements("System.Boolean System.String.Equals(this, System.String)")] | |||
| public static bool Equals(string str1, string str2) | |||
| { | |||
| if (string.IsNullOrEmpty(str1) && string.IsNullOrEmpty(str2)) | |||
There was a problem hiding this comment.
Пустая и нулловая строки будут равны
VSharp.InternalCalls/Environment.fs
Outdated
| assert(List.length args = 0) | ||
| MakeBool false | ||
|
|
||
| let internal consoleClear (_ : state) (args : term list) = | ||
| let consoleClear (_ : state) (args : term list) = |
There was a problem hiding this comment.
Название этого метода лучше с большой буквы
| let dstSize = lazy(TypeUtils.internalSizeOf dstType.Value) | ||
| let srcSize = lazy(TypeUtils.internalSizeOf srcType.Value) | ||
| let allSafe() = | ||
| let isSafe = |
There was a problem hiding this comment.
Такой же код как в isSafeContextWrite
There was a problem hiding this comment.
Это сделано для эффективности, так как размеры используются в нескольких местах
| (fun x y k -> simplifyComparisonExt op x y resultIfSame k) | ||
| (fun x y -> simplifyComparison op x y resultIfSame) | ||
|
|
||
| and simplifyEqual x y k = simplifyComparison OperationType.Equal x y true k | ||
| and simplifyNotEqual x y k = simplifyEqual x y ((!!) >> k) |
There was a problem hiding this comment.
Может, неравенство тоже переписать?
There was a problem hiding this comment.
Зачем? Равенство определено хорошо.
| let endByte = makeNumber viewSize |> add startByte | ||
| (indices, element, startByte, endByte), add currentOffset elementSize | ||
| List.mapFold getElement (mul firstElement elementSize) [0 .. countToRead - 1] |> fst | ||
| let inBlock = checkBlockBounds reporter arraySize offset (makeNumber viewSize |> add offset) |
There was a problem hiding this comment.
Тут уже не нужна проверка на isValueType?
There was a problem hiding this comment.
Нет, так как индексы могут быть только у массивов, а они в куче располагаются
VSharp.Solver/Z3.fs
Outdated
| member private x.MkBVAdd operands : BitVecExpr = | ||
| x.ExtendIfNeed operands true |> ctx.MkBVAdd | ||
| x.ExtendIfNeed operands true |> ctx.MkBVAdd |
| for xs' in cartesian xss do | ||
| yield x::xs' | ||
| let xssCartesian = cartesian xss | ||
| if Seq.isEmpty xssCartesian |> not then |
There was a problem hiding this comment.
Что это за кейс? Когда какой-то из элементов, по которым строим декартово произведение -- пустой список?
VSharp.Utils/Collections.fs
Outdated
| @@ -92,6 +94,17 @@ module public List = | |||
| let list = List.foldBack folder list List.empty | |||
| removed, list | |||
|
|
|||
| let rec sequenceOption f list = | |||
There was a problem hiding this comment.
Эта функция -- не то же самое, что проверить, что для всех элементов списка f дает Some, и тогда обернуть список в Some? Если так, то можно переписать хвосторекурсивно
There was a problem hiding this comment.
Она unused, удалил ее
VSharp.Utils/TypeUtils.fs
Outdated
| let isReal = realTypes.Contains | ||
| let isUnsigned = unsignedTypes.Contains | ||
| let isPrimitive = primitiveTypes.Contains | ||
| let isLongTypes x = longTypes.Contains x |
There was a problem hiding this comment.
У нас уже есть функция isLong, которая проверяет на равенство с typeof(Int64). Эта же функция допускает еще и typeof(UInt64)
| for KeyValue(parameter, paramDependencies) in dependencies do | ||
| for dep in paramDependencies do | ||
| depsCounts[parameter] <- depsCounts[parameter] + 1 | ||
| reversedDeps[dep] <- parameter :: reversedDeps[dep] |
There was a problem hiding this comment.
Почему reversedDeps[dep] всегда будет существовать и мы не упадем с key not found?
There was a problem hiding this comment.
Видимо, по построению
No description provided.