Skip to content

Commit

Permalink
should be amended
Browse files Browse the repository at this point in the history
  • Loading branch information
@RipplB
RipplB authored and RipplB committed Apr 24, 2024
1 parent bb0ffe5 commit d99009c
Show file tree
Hide file tree
Showing 15 changed files with 545 additions and 313 deletions.
5 changes: 3 additions & 2 deletions ...cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@
import hu.bme.mit.theta.analysis.expr.refinement.SingleExprTraceRefiner;
import hu.bme.mit.theta.analysis.expr.refinement.VarsRefutation;
import hu.bme.mit.theta.analysis.multi.MultiAnalysis;
import hu.bme.mit.theta.analysis.multi.MultiAnalysisSide;
import hu.bme.mit.theta.analysis.pred.ExprSplitters;
import hu.bme.mit.theta.analysis.pred.ExprSplitters.ExprSplitter;
import hu.bme.mit.theta.analysis.pred.ItpRefToPredPrec;
Expand Down Expand Up @@ -466,8 +467,8 @@ public CfaConfig<CfaState<S>, CfaAction, CfaPrec<P>> buildConfig(CFA.Loc errLoc)
return CfaConfig.create(checker, createInitPrec());
}

public MultiAnalysis.Side<CfaState<S>, S, CfaState<UnitState>, CfaAction, CfaPrec<P>, CfaPrec<UnitPrec>> getMultiSide() {
return new MultiAnalysis.Side<>(
public MultiAnalysisSide<CfaState<S>, S, CfaState<UnitState>, CfaAction, CfaPrec<P>, CfaPrec<UnitPrec>> getMultiSide() {
return new MultiAnalysisSide<>(
getAnalysis(),
CfaUnitInitFuncKt.cfaUnitInitFunc(cfa.getInitLoc()),
CfaInUnWrappersKt::cfaCombineStates,
Expand Down
45 changes: 23 additions & 22 deletions subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.function.BiFunction;
import java.util.function.Function;
import java.util.stream.Stream;

Expand All @@ -52,38 +51,46 @@ public abstract class MultiAnalysis<LState extends State, RState extends State,

private final Function<MState, MultiSide> defineNextSide;

protected final Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide;
protected final Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide;
protected final MultiAnalysisSide<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide;
protected final MultiAnalysisSide<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide;

private final InitFunc<DataState, DataPrec> dataInitFunc;

protected MultiAnalysis(Function<MState, MultiSide> defineNextSide, Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide, Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide, InitFunc<DataState, DataPrec> dataInitFunc) {
protected MultiAnalysis(Function<MState, MultiSide> defineNextSide, MultiAnalysisSide<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide, MultiAnalysisSide<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide, InitFunc<DataState, DataPrec> dataInitFunc) {
this.defineNextSide = defineNextSide;
this.leftSide = leftSide;
this.rightSide = rightSide;
this.dataInitFunc = dataInitFunc;
}

public MultiAnalysisSide<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> getLeftSide() {
return leftSide;
}

public MultiAnalysisSide<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> getRightSide() {
return rightSide;
}

protected abstract MState createInitialState(LBlank leftState, RBlank rightState, DataState dataState);

protected abstract MState createState(LBlank leftState, RBlank rightState, DataState dataState, MultiSide sourceSide);
public abstract MState createState(LBlank leftState, RBlank rightState, DataState dataState, MultiSide sourceSide);

protected abstract MBlankState createBlankState(LBlank leftState, RBlank rightState);
public abstract MBlankState createBlankState(LBlank leftState, RBlank rightState);

@Override
public PartialOrd<MState> getPartialOrd() {
return ((state1, state2) -> leftSide.analysis.getPartialOrd().isLeq(leftSide.combineStates.apply(state1.getLeftState(), state1.getDataState()), leftSide.combineStates.apply(state2.getLeftState(), state2.getDataState()))
&& rightSide.analysis.getPartialOrd().isLeq(rightSide.combineStates.apply(state1.getRightState(), state1.getDataState()), rightSide.combineStates.apply(state2.getRightState(), state2.getDataState()))
return ((state1, state2) -> leftSide.getAnalysis().getPartialOrd().isLeq(leftSide.getCombineStates().invoke(state1.getLeftState(), state1.getDataState()), leftSide.getCombineStates().invoke(state2.getLeftState(), state2.getDataState()))
&& rightSide.getAnalysis().getPartialOrd().isLeq(rightSide.getCombineStates().invoke(state1.getRightState(), state1.getDataState()), rightSide.getCombineStates().invoke(state2.getRightState(), state2.getDataState()))
&& ((!state1.getSourceMattersInEquality() && !state2.getSourceMattersInEquality()) || (state1.getSourceSide() == state2.getSourceSide())));
}

@Override
public InitFunc<MState, MultiPrec<LPrec, RPrec, DataPrec>> getInitFunc() {
return (prec -> {
LBlankPrec leftInitPrec = leftSide.stripDataFromPrec.apply(prec.leftPrec());
RBlankPrec rightInitPrec = rightSide.stripDataFromPrec.apply(prec.rightPrec());
Collection<LBlank> leftInitStates = new HashSet<>(leftSide.initFunc.getInitStates(leftInitPrec));
Collection<RBlank> rightInitStates = new HashSet<>(rightSide.initFunc.getInitStates(rightInitPrec));
LBlankPrec leftInitPrec = leftSide.getStripDataFromPrec().invoke(prec.leftPrec());
RBlankPrec rightInitPrec = rightSide.getStripDataFromPrec().invoke(prec.rightPrec());
Collection<LBlank> leftInitStates = new HashSet<>(leftSide.getInitFunc().getInitStates(leftInitPrec));
Collection<RBlank> rightInitStates = new HashSet<>(rightSide.getInitFunc().getInitStates(rightInitPrec));
Collection<? extends DataState> dataInitStates = dataInitFunc.getInitStates(prec.dataPrec());
Collection<MState> resultSet = new HashSet<>();
for (LBlank leftInitState :
Expand All @@ -106,23 +113,17 @@ public TransFunc<MState, MAction, MultiPrec<LPrec, RPrec, DataPrec>> getTransFun
final MultiSide nextSide = defineNextSide.apply(state);
final List<MState> succStates = new LinkedList<>();
if (nextSide != MultiSide.RIGHT && action.getLeftAction() != null) {
final var leftSuccStates = leftSide.analysis.getTransFunc().getSuccStates(leftSide.combineStates().apply(state.getLeftState(), state.getDataState()), action.getLeftAction(), prec.leftPrec());
final Stream<MState> multiStateStream = leftSuccStates.stream().map(s -> createState(leftSide.stripDataFromState().apply(s), state.getRightState(), leftSide.extractDataFromState.apply(s), MultiSide.LEFT));
final var leftSuccStates = leftSide.getAnalysis().getTransFunc().getSuccStates(leftSide.getCombineStates().invoke(state.getLeftState(), state.getDataState()), action.getLeftAction(), prec.leftPrec());
final Stream<MState> multiStateStream = leftSuccStates.stream().map(s -> createState(leftSide.getStripDataFromState().invoke(s), state.getRightState(), leftSide.getExtractDataFromState().invoke(s), MultiSide.LEFT));
multiStateStream.forEach(succStates::add);
}
if (nextSide != MultiSide.LEFT && action.getRightAction() != null) {
final var rightSuccStates = rightSide.analysis.getTransFunc().getSuccStates(rightSide.combineStates.apply(state.getRightState(), state.getDataState()), action.getRightAction(), prec.rightPrec());
final Stream<MState> multiStateStream = rightSuccStates.stream().map(s -> createState(state.getLeftState(), rightSide.stripDataFromState.apply(s), rightSide.extractDataFromState.apply(s), MultiSide.RIGHT));
final var rightSuccStates = rightSide.getAnalysis().getTransFunc().getSuccStates(rightSide.getCombineStates().invoke(state.getRightState(), state.getDataState()), action.getRightAction(), prec.rightPrec());
final Stream<MState> multiStateStream = rightSuccStates.stream().map(s -> createState(state.getLeftState(), rightSide.getStripDataFromState().invoke(s), rightSide.getExtractDataFromState().invoke(s), MultiSide.RIGHT));
multiStateStream.forEach(succStates::add);
}
return succStates;
});
}

public record Side<S extends State, DataS extends State, BlankS extends State, A extends Action, P extends Prec, BlankP extends Prec>
(Analysis<S, ? super A, ? super P> analysis, InitFunc<BlankS, BlankP> initFunc,
BiFunction<BlankS, DataS, S> combineStates, Function<S, BlankS> stripDataFromState,
Function<S, DataS> extractDataFromState, Function<P, BlankP> stripDataFromPrec) {
}

}
Loading

0 comments on commit d99009c

Please sign in to comment.