Creating a Code Module

The K framwork has been restructured to support the modular inclusion of new features like a new backend or other tools that a developer may wish to include in the framework. In the interests of making it easier to create such a module, I am creating a high level example module here to showcase some of the things you can do with modules.

The module definition

public class ExampleKModule implements KModule {
    @Override
    public List<Module> getKompileModules() {
        return ImmutableList.<Module>of(new ExampleKompileModule());
    }

    @Override
    public List<Module> getKastModules() {
        return ImmutableList.of();
    }

    @Override
    public List<Module> getKRunModules(List<Module> definitionSpecificModules) {
        return ImmutableList.<Module>of(new ExampleKRunModule());
    }

    @Override
    public List<Module> getKTestModules() {
        return ImmutableList.of();
    }

    @Override
    public List<Module> getDefinitionSpecificKRunModules() {
        return ImmutableList.<Module>of(new ExampleDefinitionModule());
    }
}

Here we declare a K module that extends the functionality of Kompile and KRun. The Module instances returned by these methods are used in order to extend the functionality of the tools they are associated with. So ExampleKompileModule extends the functionality of kompile, and the other two modules extend the functionality of krun. Since krun is designed to operate over definitions, and some applications may wish to make use of more than one definition, we delineate between configuration global to all definitions (defined in ExampleKRunModule) and configuration specific to a single definition (defined in ExampleDefinitionModule). For more information about how to use this infrastructure in order to support such a tool, refer to either JavaBackendKModule in the K distribution, or talk to @dwightguth.

A configuration module

public class ExampleKRunModule extends AbstractModule {
    private final ExampleOptions options;

    public ExampleKRunModule() {
        this.options = new ExampleOptions();
    }

    @Override
    protected void configure() {
        //bind options to be accessed by our code
        bind(ExampleOptions.class).toInstance(options);

        // bind options to be parsed and be accessible to the user
        Multibinder<Object> optionsBinder = Multibinder.newSetBinder(binder(), Object.class, Options.class);
        optionsBinder.addBinding().toInstance(options);

        // declare options as experimental
        Multibinder<Class<?>> experimentalOptionsBinder = Multibinder.newSetBinder(binder(), 
                new TypeLiteral<Class<?>>() {}, Options.class);
        experimentalOptionsBinder.addBinding().toInstance(ExampleOptions.class);

    }
}

public class ExampleDefinitionModule extends AbstractModule {

    @Override
    protected void configure() {
        MapBinder<String, Executor> executorBinder = MapBinder.newMapBinder(
                binder(), String.class, Executor.class);
        executorBinder.addBinding("example").to(ExampleExecutor.class);
    }

    @Provides
    ExampleClass exampleProvider(Context context, ExampleOptions options) {
        // do stuff
    }
}

Here we define two modules used to configure information about krun. In the first module, we create a set of options using JCommander defined in ExampleOptions, and bind the appropriate configuration so that the options get parsed and can be accessed by our code. We also declare that these options are experimental.

In the second module, we get to the meat of what we are actually doing in this plugin. We declare that if the user specifies the backend "example", programs can be executed by means of the ExampleExecutor class which implements the execution interface. We also demonstrate how additional configuration can be specified using a Provides method. Here we declare that an ExampleClass depends on Context and on ExampleOptions, and we can use these dependencies in this method in order to construct the object, which will be accessible to the rest of the code.

Example implementation of API interface

public class ExampleExecutor implements Executor {
    private final ExampleOptions exampleOptions;
    private final KExceptionManager kem;
    private final KompileOptions kompileOptions;
    private final Context context;

    @Inject
    ExampleExecutor(
        Context context,
        ExampleOptions exampleOptions,
        KExceptionManager kem,
        KompileOptions kompileOptions) {
       this.context = context;
       this.exampleOptions = exampleOptions;
       this.kem = kem;
       this.kompileOptions = kompileOptions;
    }

    @Override
    public KRunResult<KRunState> run(org.kframework.kil.Term cfg) throws KRunExecutionException {
        // do stuff
    }

    @Override
    public KRunResult<SearchResults> search(
        Integer bound,
        Integer depth,
        SearchType searchType,
        org.kframework.kil.Rule pattern,
        org.kframework.kil.Term cfg,
        RuleCompilerSteps compilationInfo) throws KRunExecutionException {
        // do stuff
    }

    @Override
    public KRunResult<KRunState> step(org.kframework.kil.Term cfg, int steps)
        throws KRunExecutionException {
        // do stuff
    }
}

Here we implement the interface that is used to execute programs. Note the Inject annotation on the constructor and the list of arguments that it takes. These arguments are the dependencies of the class and can be anything that is bound by the dependency injection modules we looked at earlier, whether in the core or in one of your modules. For more information about Google Guice, refer to the rest of the code, or its documentation at https://github.com/google/guice/wiki

A similar mechanism exists to allow users to extend the framework by adding a new compilation backend, or by adding a new tool that is used to analyze programs. Information about how precisely to do these things is not included here. For more information, you may refer to the classes JavaSymbolicKompileModule and JavaSymbolicKRunModule, where this is being done with the simulation checker prototype (which is not currently functional, but demonstrates the concept) and the java backend.