From a85b371c5584664083ed7e1a394607c3100534c2 Mon Sep 17 00:00:00 2001 From: Dmitry Vyukov Date: Thu, 8 Aug 2024 12:09:55 +0200 Subject: prog: optimize array minimization If there are at least 3 elements, try to remove all at once first. If will be faster than removing them one-by-one if all of them are not needed. --- prog/minimization.go | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'prog/minimization.go') diff --git a/prog/minimization.go b/prog/minimization.go index 8298ec812..260a15133 100644 --- a/prog/minimization.go +++ b/prog/minimization.go @@ -272,10 +272,24 @@ func (typ *PtrType) minimize(ctx *minimizeArgsCtx, arg Arg, path string) bool { func (typ *ArrayType) minimize(ctx *minimizeArgsCtx, arg Arg, path string) bool { a := arg.(*GroupArg) + // If there are at least 3 elements, try to remove all at once first. + // If will be faster than removing them one-by-one if all of them are not needed. + if allPath := path + "-all"; len(a.Inner) >= 3 && typ.RangeBegin == 0 && !ctx.triedPaths[allPath] { + ctx.triedPaths[allPath] = true + for _, elem := range a.Inner { + removeArg(elem) + } + a.Inner = nil + ctx.target.assignSizesCall(ctx.call) + if ctx.pred(ctx.p, ctx.callIndex0, statMinArray, allPath) { + *ctx.p0 = ctx.p + } + return true + } + // Try to remove individual elements one-by-one. for i := len(a.Inner) - 1; i >= 0; i-- { elem := a.Inner[i] elemPath := fmt.Sprintf("%v-%v", path, i) - // Try to remove individual elements one-by-one. if ctx.mode != MinimizeCrash && !ctx.triedPaths[elemPath] && (typ.Kind == ArrayRandLen || typ.Kind == ArrayRangeLen && uint64(len(a.Inner)) > typ.RangeBegin) { -- cgit mrf-deployment