1 //===-- Generate random but valid function descriptors  ---------*- C++ -*-===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 
9 #ifndef LLVM_LIBC_BENCHMARKS_AUTOMEMCPY_RANDOM_FUNCTION_GENERATOR_H
10 #define LLVM_LIBC_BENCHMARKS_AUTOMEMCPY_RANDOM_FUNCTION_GENERATOR_H
11 
12 #include "automemcpy/FunctionDescriptor.h"
13 #include <cstddef>
14 #include <cstdint>
15 #include <llvm/ADT/ArrayRef.h>
16 #include <llvm/ADT/Optional.h>
17 #include <llvm/ADT/StringRef.h>
18 #include <vector>
19 #include <z3++.h>
20 
21 namespace llvm {
22 namespace automemcpy {
23 
24 // Holds the state for the constraint solver.
25 // It implements a single method that returns the next valid description.
26 struct RandomFunctionGenerator {
27   RandomFunctionGenerator();
28 
29   // Get the next valid FunctionDescriptor or llvm::None.
30   Optional<FunctionDescriptor> next();
31 
32 private:
33   // Returns an expression where `Variable` is forced to be one of the `Values`.
34   z3::expr inSetConstraint(z3::expr &Variable, ArrayRef<int> Values) const;
35   // Add constaints to `Begin` and `End` so that they are:
36   // - between 0 and kMaxSize (inclusive)
37   // - ordered (begin<=End)
38   // - amongst a set of predefined values.
39   void addBoundsAndAnchors(z3::expr &Begin, z3::expr &End);
40   // Add constraints to make sure that the loop block size is amongst a set of
41   // predefined values. Also makes sure that the loop that the loop is iterated
42   // at least `LoopMinIter` times.
43   void addLoopConstraints(const z3::expr &LoopBegin, const z3::expr &LoopEnd,
44                           z3::expr &LoopBlockSize, int LoopMinIter);
45 
46   z3::context Context;
47   z3::solver Solver;
48 
49   z3::expr Type;
50   z3::expr ContiguousBegin, ContiguousEnd;
51   z3::expr OverlapBegin, OverlapEnd;
52   z3::expr LoopBegin, LoopEnd, LoopBlockSize;
53   z3::expr AlignedLoopBegin, AlignedLoopEnd, AlignedLoopBlockSize,
54       AlignedAlignment, AlignedArg;
55   z3::expr AcceleratorBegin, AcceleratorEnd;
56   z3::expr ElementClass;
57 };
58 
59 } // namespace automemcpy
60 } // namespace llvm
61 
62 #endif /* LLVM_LIBC_BENCHMARKS_AUTOMEMCPY_RANDOM_FUNCTION_GENERATOR_H */
63