k/kernel/src/main/java/org/kframework/krun/KRunModule.java at dapphub · https-github-com-goodman-ops/k · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
// Copyright (c) 2014-2016 K Team. All Rights Reserved.
package org.kframework.krun;

import com.beust.jcommander.JCommander;
import com.google.inject.AbstractModule;
import com.google.inject.Provider;
import com.google.inject.Provides;
import com.google.inject.TypeLiteral;
import com.google.inject.multibindings.MapBinder;
import com.google.inject.multibindings.Multibinder;
import com.google.inject.name.Named;
import com.google.inject.throwingproviders.ThrowingProviderBinder;
import org.kframework.kompile.KompileOptions;
import org.kframework.krun.KRunOptions.ConfigurationCreationOptions;
import org.kframework.krun.api.io.FileSystem;
import org.kframework.krun.ioserver.filesystem.portable.PortableFileSystem;
import org.kframework.krun.modes.DebugMode.DebugExecutionMode;
import org.kframework.krun.modes.ExecutionMode;
import org.kframework.krun.modes.KRunExecutionMode;
import org.kframework.main.FrontEnd;
import org.kframework.main.GlobalOptions;
import org.kframework.main.Tool;
import org.kframework.rewriter.Rewriter;
import org.kframework.unparser.OutputModes;
import org.kframework.utils.errorsystem.KEMException;
import org.kframework.utils.errorsystem.KExceptionManager;
import org.kframework.utils.file.FileUtil;
import org.kframework.utils.inject.Options;
import org.kframework.utils.options.DefinitionLoadingOptions;
import org.kframework.utils.options.SMTOptions;

import java.util.Map;
import java.util.function.Function;

public class KRunModule extends AbstractModule {

    @Override
    protected void configure() {
        bind(FrontEnd.class).to(KRunFrontEnd.class);
        bind(Tool.class).toInstance(Tool.KRUN);

        Multibinder<Object> optionsBinder = Multibinder.newSetBinder(binder(), Object.class, Options.class);
        optionsBinder.addBinding().to(KRunOptions.class);
        Multibinder<Class<?>> experimentalOptionsBinder = Multibinder.newSetBinder(binder(), new TypeLiteral<Class<?>>() {}, Options.class);
        experimentalOptionsBinder.addBinding().toInstance(KRunOptions.Experimental.class);
        experimentalOptionsBinder.addBinding().toInstance(SMTOptions.class);

        ThrowingProviderBinder throwingBinder = ThrowingProviderBinder.create(binder());
    }

    @Provides
    SMTOptions smtOptions(KRunOptions options) {
        return options.experimental.smt;
    }

    @Provides
    GlobalOptions globalOptions(KRunOptions options) {
        return options.global;
    }

    @Provides
    PrettyPrintOptions prettyPrintOptions(KRunOptions options) {
        return options.prettyPrint;
    }

    @Provides
    OutputModes outputModes(PrettyPrintOptions options) {
        return options.output;
    }

    public static class CommonModule extends AbstractModule {

        @Override
        protected void configure() {
            install(new RewriterModule());

            //bind backend implementations of tools to their interfaces
            MapBinder<ToolActivation, ExecutionMode> executionBinder = MapBinder.newMapBinder(binder(),
                    ToolActivation.class, ExecutionMode.class);

            executionBinder.addBinding(new ToolActivation.OptionActivation("--debugger")).to(DebugExecutionMode.class);

        }

        @Provides
        DefinitionLoadingOptions defLoadingOptions(ConfigurationCreationOptions options) {
            return options.definitionLoading;
        }

        @Provides
        ConfigurationCreationOptions ccOptions(KRunOptions options) {
            return options.configurationCreation;
        }

        @Provides
        ExecutionMode getExecutionMode(JCommander jc, Map<ToolActivation, Provider<ExecutionMode>> map, KRunOptions kRunOptions, KExceptionManager kem, FileUtil files) {
            ExecutionMode res = null;
            ToolActivation previous = null;
            for (Map.Entry<ToolActivation, Provider<ExecutionMode>> entry : map.entrySet()) {
                if (entry.getKey().isActive(jc)) {
                    if (res != null) {
                        throw KEMException.criticalError("Multiple tool activations found: " + entry.getKey() + " and " + previous);
                    }
                    res = entry.getValue().get();
                    previous = entry.getKey();
                }
            }
            if (res == null)
                res = new KRunExecutionMode(kRunOptions, kem, files);
            return res;
        }


        @Provides
        @Named("checkpointIntervalValue")
        Integer getCheckpointLength(KompileOptions options, @Named("checkpointIntervalMap") Map<String, Integer> map) {
            Integer checkpointInterval = map.get(options.backend);
            if (checkpointInterval == null) {
                return new Integer(50);
            }
            return checkpointInterval;
        }
    }
}