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.

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

SE: Pass states per stack #7059

Open
wants to merge 19 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
Expand Up @@ -70,19 +70,25 @@ internal static class OperationDispatcher
{ OperationKindEx.Unary, new Unary() }
};

public static IEnumerable<SymbolicContext> Process(SymbolicContext context)
public static SymbolicContexts Process(SymbolicContext context)
{
if (Simple.TryGetValue(context.Operation.Instance.Kind, out var simple)) // Operations that return single state
{
return new[] { context.WithState(simple.Process(context)) };
return new(context.WithState(simple.Process(context)));
}
else if (Branching.TryGetValue(context.Operation.Instance.Kind, out var processor)) // Operations that can return multiple states
{
return processor.Process(context).Select(context.WithState);
var states = processor.Process(context);
var result = new SymbolicContexts();
foreach (var state in states)
{
result += new SymbolicContexts(context.WithState(state));
}
return result;
}
else
{
return new[] { context };
return new(context);
}
}
}
Expand Up @@ -36,25 +36,23 @@ internal abstract class BranchingProcessor<T> : MultiProcessor<T>
protected virtual ProgramState PreProcess(ProgramState state, T operation, bool isInLoop) =>
state;

protected override ProgramState[] Process(SymbolicContext context, T operation)
protected override ProgramStates Process(SymbolicContext context, T operation)
{
var state = PreProcess(context.State, operation, context.IsInLoop);
if (BoolConstraintFromOperation(state, operation) is { } constraint)
{
return state.SetOperationConstraint(context.Operation, constraint).ToArray(); // We already know the answer from existing constraints
return new(state.SetOperationConstraint(context.Operation, constraint)); // We already know the answer from existing constraints
}
else
{
var beforeLearningState = state;
var positive = LearnBranchingConstraint(state, operation, false);
var negative = LearnBranchingConstraint(state, operation, true);
return positive == beforeLearningState && negative == beforeLearningState
? beforeLearningState.ToArray() // We can't learn anything, just move on
: new[]
{
? new(beforeLearningState) // We can't learn anything, just move on
: new(
positive.SetOperationConstraint(context.Operation, BoolConstraint.True),
negative.SetOperationConstraint(context.Operation, BoolConstraint.False)
};
negative.SetOperationConstraint(context.Operation, BoolConstraint.False));
}
}
}
Expand Up @@ -71,23 +71,23 @@ internal sealed partial class Invocation
nameof(Enumerable.Zip),
};

private static ProgramState[] ProcessLinqEnumerableAndQueryable(ProgramState state, IInvocationOperationWrapper invocation)
private static ProgramStates ProcessLinqEnumerableAndQueryable(ProgramState state, IInvocationOperationWrapper invocation)
{
var name = invocation.TargetMethod.Name;
if (ReturningNotNull.Contains(name))
{
return state.SetOperationConstraint(invocation, ObjectConstraint.NotNull).ToArray();
return new(state.SetOperationConstraint(invocation, ObjectConstraint.NotNull));
}
// ElementAtOrDefault is intentionally not supported. It's causing many FPs
else if (name is nameof(Enumerable.FirstOrDefault) or nameof(Enumerable.LastOrDefault) or nameof(Enumerable.SingleOrDefault))
{
return invocation.TargetMethod.ReturnType.IsReferenceType
? [state.SetOperationConstraint(invocation, ObjectConstraint.Null), state.SetOperationConstraint(invocation, ObjectConstraint.NotNull)]
: state.ToArray();
? new(state.SetOperationConstraint(invocation, ObjectConstraint.Null), state.SetOperationConstraint(invocation, ObjectConstraint.NotNull))
: new(state);
}
else
{
return state.ToArray();
return new(state);
}
}
}
Expand Up @@ -55,19 +55,19 @@ internal sealed partial class Invocation
nameof(string.TrimStart)
};

private static ProgramState[] ProcessSystemStringInvocation(ProgramState state, IInvocationOperationWrapper invocation)
private static ProgramStates ProcessSystemStringInvocation(ProgramState state, IInvocationOperationWrapper invocation)
{
if (invocation.TargetMethod.Name is nameof(string.IsNullOrEmpty) or nameof(string.IsNullOrWhiteSpace))
{
return ProcessIsNotNullWhen(state, invocation.WrappedOperation, invocation.Arguments[0].ToArgument(), false, true);
}
else if (StringMethodReturningNotNull.Contains(invocation.TargetMethod.Name))
{
return state.SetOperationConstraint(invocation, ObjectConstraint.NotNull).ToArray();
return new(state.SetOperationConstraint(invocation, ObjectConstraint.NotNull));
}
else
{
return state.ToArray();
return new(state);
}
}
}