Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/develop'
Browse files Browse the repository at this point in the history
  • Loading branch information
devops committed Nov 1, 2023
2 parents edfbe50 + c523139 commit 8b4ebd4
Show file tree
Hide file tree
Showing 289 changed files with 34,355 additions and 29,016 deletions.
28 changes: 25 additions & 3 deletions .github/workflows/test-pr.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,10 +29,32 @@ jobs:
git push origin HEAD:${GITHUB_HEAD_REF}
fi
format-check:
name: 'Check Java code formatting'
runs-on: ubuntu-latest
needs: version-sync
steps:
- name: 'Check out code'
uses: actions/checkout@v3
with:
token: ${{ secrets.JENKINS_GITHUB_PAT }}
# fetch-depth 0 means deep clone the repo
fetch-depth: 0
- name: 'Set up Java 17'
uses: actions/setup-java@v3
with:
distribution: 'zulu'
java-version: 17
- name: 'Check code is formatted correctly'
uses: axel-op/googlejavaformat-action@v3
with:
version: 1.18.1
args: "--dry-run --set-exit-if-changed"

nix-maven:
name: 'Nix: Maven'
runs-on: ubuntu-20.04
needs: version-sync
needs: format-check
steps:

- name: 'Check out code, set up Git'
Expand Down Expand Up @@ -75,7 +97,7 @@ jobs:
test-k:
name: 'K Tests'
runs-on: [self-hosted, linux, normal]
needs: version-sync
needs: format-check
steps:
- name: 'Check out code'
uses: actions/checkout@v3
Expand Down Expand Up @@ -112,7 +134,7 @@ jobs:
test-package-ubuntu-jammy:
name: 'K Ubuntu Jammy Package'
runs-on: [self-hosted, linux, normal]
needs: version-sync
needs: format-check
steps:
- uses: actions/checkout@v3
- name: 'Build and Test'
Expand Down
126 changes: 63 additions & 63 deletions haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,83 +2,83 @@
package org.kframework.backend.haskell;

import com.google.inject.Inject;
import java.io.IOException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
import org.kframework.attributes.Att;
import org.kframework.backend.kore.KoreBackend;
import org.kframework.compile.Backend;
import org.kframework.kompile.KompileOptions;
import org.kframework.main.GlobalOptions;
import org.kframework.main.Tool;
import org.kframework.utils.Stopwatch;
import org.kframework.utils.errorsystem.KExceptionManager;
import org.kframework.utils.errorsystem.KEMException;
import org.kframework.utils.errorsystem.KExceptionManager;
import org.kframework.utils.file.FileUtil;

import java.io.IOException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import java.util.Set;
import java.util.HashSet;

public class HaskellBackend extends KoreBackend {

private final KompileOptions kompileOptions;
private final GlobalOptions globalOptions;
private final FileUtil files;
private final HaskellKompileOptions haskellKompileOptions;

@Inject
public HaskellBackend(
KompileOptions kompileOptions,
GlobalOptions globalOptions,
HaskellKompileOptions haskellKompileOptions,
FileUtil files,
KExceptionManager kem,
Tool tool) {
super(kompileOptions, files, kem, false, tool);
this.files = files;
this.haskellKompileOptions = haskellKompileOptions;
this.kompileOptions = kompileOptions;
this.globalOptions = globalOptions;
}
private final KompileOptions kompileOptions;
private final GlobalOptions globalOptions;
private final FileUtil files;
private final HaskellKompileOptions haskellKompileOptions;

@Inject
public HaskellBackend(
KompileOptions kompileOptions,
GlobalOptions globalOptions,
HaskellKompileOptions haskellKompileOptions,
FileUtil files,
KExceptionManager kem,
Tool tool) {
super(kompileOptions, files, kem, false, tool);
this.files = files;
this.haskellKompileOptions = haskellKompileOptions;
this.kompileOptions = kompileOptions;
this.globalOptions = globalOptions;
}

@Override
public void accept(Backend.Holder h) {
Stopwatch sw = new Stopwatch(globalOptions);
String kore = getKompiledString(h.def, true);
h.def = null;
files.saveToKompiled("definition.kore", kore);
sw.printIntermediate(" Print definition.kore");
ProcessBuilder pb = files.getProcessBuilder();
List<String> args = new ArrayList<>();
if (haskellKompileOptions.noHaskellBinary) {
args.add("kore-parser");
args.add("--no-print-definition");
args.add("definition.kore");
} else {
args.add(haskellKompileOptions.haskellBackendCommand);
args.add("definition.kore");
args.add("--module");
args.add(kompileOptions.mainModule(files));
args.add("--output");
args.add("haskellDefinition.bin");
args.add("--serialize");
}
try {
Process p = pb.command(args).directory(files.resolveKompiled(".")).inheritIO().start();
int exit = p.waitFor();
if (exit != 0) {
throw KEMException.criticalError("Haskell backend reported errors validating compiled definition.\nExamine output to see errors.");
}
} catch (IOException | InterruptedException e) {
throw KEMException.criticalError("Error with I/O while executing kore-parser", e);
}
sw.printIntermediate(" Validate def");
@Override
public void accept(Backend.Holder h) {
Stopwatch sw = new Stopwatch(globalOptions);
String kore = getKompiledString(h.def, true);
h.def = null;
files.saveToKompiled("definition.kore", kore);
sw.printIntermediate(" Print definition.kore");
ProcessBuilder pb = files.getProcessBuilder();
List<String> args = new ArrayList<>();
if (haskellKompileOptions.noHaskellBinary) {
args.add("kore-parser");
args.add("--no-print-definition");
args.add("definition.kore");
} else {
args.add(haskellKompileOptions.haskellBackendCommand);
args.add("definition.kore");
args.add("--module");
args.add(kompileOptions.mainModule(files));
args.add("--output");
args.add("haskellDefinition.bin");
args.add("--serialize");
}

@Override
public Set<Att.Key> excludedModuleTags() {
return new HashSet<>(Arrays.asList(Att.CONCRETE(), Att.KAST()));
try {
Process p = pb.command(args).directory(files.resolveKompiled(".")).inheritIO().start();
int exit = p.waitFor();
if (exit != 0) {
throw KEMException.criticalError(
"Haskell backend reported errors validating compiled definition.\n"
+ "Examine output to see errors.");
}
} catch (IOException | InterruptedException e) {
throw KEMException.criticalError("Error with I/O while executing kore-parser", e);
}
sw.printIntermediate(" Validate def");
}

@Override
public Set<Att.Key> excludedModuleTags() {
return new HashSet<>(Arrays.asList(Att.CONCRETE(), Att.KAST()));
}
}
119 changes: 60 additions & 59 deletions haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,80 +6,81 @@
import com.google.inject.Module;
import com.google.inject.TypeLiteral;
import com.google.inject.multibindings.MapBinder;
import java.util.Collections;
import java.util.List;
import java.util.function.Function;
import org.apache.commons.lang3.tuple.Pair;
import org.kframework.definition.Definition;
import org.kframework.main.AbstractKModule;
import org.kframework.rewriter.Rewriter;

import java.util.Collections;
import java.util.List;
import java.util.function.Function;

/**
* Created by traiansf on 9/13/18.
*/
/** Created by traiansf on 9/13/18. */
public class HaskellBackendKModule extends AbstractKModule {

@Override
public List<Module> getKompileModules() {
List<Module> mods = super.getKompileModules();
mods.add(new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
installHaskellBackend(binder());
}
@Override
public List<Module> getKompileModules() {
List<Module> mods = super.getKompileModules();
mods.add(
new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
installHaskellBackend(binder());
}
});
return mods;
}
return mods;
}

private void installHaskellBackend(Binder binder) {
MapBinder<String, org.kframework.compile.Backend> mapBinder = MapBinder.newMapBinder(
binder, String.class, org.kframework.compile.Backend.class);
mapBinder.addBinding("haskell").to(HaskellBackend.class);
}
private void installHaskellBackend(Binder binder) {
MapBinder<String, org.kframework.compile.Backend> mapBinder =
MapBinder.newMapBinder(binder, String.class, org.kframework.compile.Backend.class);
mapBinder.addBinding("haskell").to(HaskellBackend.class);
}

@Override
public List<Pair<Class<?>, Boolean>> krunOptions() {
return Collections.singletonList(Pair.of(HaskellKRunOptions.class, true));
}
@Override
public List<Pair<Class<?>, Boolean>> krunOptions() {
return Collections.singletonList(Pair.of(HaskellKRunOptions.class, true));
}

@Override
public List<Pair<Class<?>, Boolean>> kompileOptions() {
return Collections.singletonList(Pair.of(HaskellKompileOptions.class, true));
}
@Override
public List<Pair<Class<?>, Boolean>> kompileOptions() {
return Collections.singletonList(Pair.of(HaskellKompileOptions.class, true));
}

@Override
public List<Module> getKRunModules() {
return Collections.singletonList(new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
installHaskellRewriter(binder());
}
@Override
public List<Module> getKRunModules() {
return Collections.singletonList(
new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
installHaskellRewriter(binder());
}
});
}

private void installHaskellRewriter(Binder binder) {
bindOptions(HaskellBackendKModule.this::krunOptions, binder);
}

MapBinder<String, Function<Definition, Rewriter>> rewriterBinder = MapBinder.newMapBinder(
binder, TypeLiteral.get(String.class), new TypeLiteral<Function<Definition, Rewriter>>() {
});
rewriterBinder.addBinding("haskell").to(HaskellRewriter.class);
}
private void installHaskellRewriter(Binder binder) {
bindOptions(HaskellBackendKModule.this::krunOptions, binder);

MapBinder<String, Function<Definition, Rewriter>> rewriterBinder =
MapBinder.newMapBinder(
binder,
TypeLiteral.get(String.class),
new TypeLiteral<Function<Definition, Rewriter>>() {});
rewriterBinder.addBinding("haskell").to(HaskellRewriter.class);
}

@Override
public List<Module> getKProveModules() {
return Collections.singletonList(new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
installHaskellBackend(binder());
installHaskellRewriter(binder());
}
@Override
public List<Module> getKProveModules() {
return Collections.singletonList(
new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
installHaskellBackend(binder());
installHaskellRewriter(binder());
}
});
}
}
}
Loading

0 comments on commit 8b4ebd4

Please sign in to comment.