Skip to content

Commit

Permalink
Merge branch 'master' into cleanup/Simplify_PChecker
Browse files Browse the repository at this point in the history
  • Loading branch information
ankushdesai authored Oct 9, 2024
2 parents ad30f29 + ec89f7d commit 8c4c600
Show file tree
Hide file tree
Showing 15 changed files with 200 additions and 141 deletions.
40 changes: 0 additions & 40 deletions .github/workflows/pcover.yml

This file was deleted.

40 changes: 0 additions & 40 deletions .github/workflows/psym.yml

This file was deleted.

40 changes: 0 additions & 40 deletions .github/workflows/psymb.yml

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -579,7 +579,9 @@ private void WriteState(CompilationContext context, StringWriter output, State s

if (state.Entry != null)
{
context.WriteLine(output, $"[OnEntry(nameof({context.Names.GetNameForDecl(state.Entry)}))]");
var entryFunctionName = context.Names.GetNameForDecl(state.Entry);
entryFunctionName = state.Entry.IsAnon ? entryFunctionName : $"_{entryFunctionName}";
context.WriteLine(output, $"[OnEntry(nameof({entryFunctionName}))]");
}

var deferredEvents = new List<string>();
Expand Down Expand Up @@ -634,7 +636,9 @@ private void WriteState(CompilationContext context, StringWriter output, State s

if (state.Exit != null)
{
context.WriteLine(output, $"[OnExit(nameof({context.Names.GetNameForDecl(state.Exit)}))]");
var exitFunctionName = context.Names.GetNameForDecl(state.Exit);
exitFunctionName = state.Exit.IsAnon ? exitFunctionName : $"_{exitFunctionName}";
context.WriteLine(output, $"[OnExit(nameof({exitFunctionName}))]");
}

context.WriteLine(output, $"class {context.Names.GetNameForDecl(state)} : State");
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ public Interface(string name, ParserRuleContext sourceNode)

public IEventSet ReceivableEvents { get; set; }

public PLanguageType PayloadType { get; set; } = PrimitiveType.Null;
public PLanguageType PayloadType = null;

public string Name { get; }
public ParserRuleContext SourceLocation { get; }
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ public Machine(string name, ParserRuleContext sourceNode)
public IEnumerable<Function> Methods => methods;
public State StartState { get; set; }
public IEventSet Observes { get; set; }
public PLanguageType PayloadType { get; set; } = PrimitiveType.Null;
public PLanguageType PayloadType { get; set; } = null;

public Scope Scope { get; set; }
public ParserRuleContext SourceLocation { get; }
Expand Down
3 changes: 2 additions & 1 deletion Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,8 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
// Step 2: Validate machine specifications
foreach (var machine in globalScope.Machines)
{
MachineChecker.Validate(handler, machine, config);

MachineChecker.Validate(handler, machine, config, globalScope);
}

// Step 3: Fill function bodies
Expand Down
3 changes: 0 additions & 3 deletions Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs
Original file line number Diff line number Diff line change
Expand Up @@ -305,7 +305,6 @@ public override object VisitImplMachineDecl(PParser.ImplMachineDeclContext conte
// initialize the corresponding interface
currentScope.Value.Get(machine.Name, out Interface @interface);
@interface.ReceivableEvents = machine.Receives;
@interface.PayloadType = machine.PayloadType;

return machine;
}
Expand Down Expand Up @@ -455,8 +454,6 @@ public override object VisitStateDecl(PParser.StateDeclContext context)
if (CurrentMachine.StartState != null)
throw Handler.DuplicateStartState(context, state, CurrentMachine.StartState, CurrentMachine);
CurrentMachine.StartState = state;
CurrentMachine.PayloadType =
state.Entry?.Signature.Parameters.ElementAtOrDefault(0)?.Type ?? PrimitiveType.Null;
}

return state;
Expand Down
28 changes: 15 additions & 13 deletions Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Formats.Asn1;
using System.Linq;
using Antlr4.Runtime;
using Plang.Compiler.TypeChecker.AST.Declarations;
Expand All @@ -11,18 +12,26 @@ namespace Plang.Compiler.TypeChecker
{
public static class MachineChecker
{
public static void Validate(ITranslationErrorHandler handler, Machine machine, ICompilerConfiguration job)
public static void Validate(ITranslationErrorHandler handler, Machine machine, ICompilerConfiguration job, Scope gScope)
{
var startState = FindStartState(machine, handler);
var startStatePayloadType = GetStatePayload(startState);
Debug.Assert(startStatePayloadType.IsSameTypeAs(machine.PayloadType));
// before validating the machines, lets set the constructor types for machines and interfaces
if(!machine.IsSpec) InitializeContructorType(handler, machine, gScope);

ValidateHandlers(handler, machine);
ValidateTransitions(handler, machine);
// special validation for monitors:
// ensure that each eventhandler is in the observe set.
// ensure that each event handler is in the observe set.
ValidateSpecObservesList(handler, machine, job);
}

private static void InitializeContructorType(ITranslationErrorHandler handler, Machine machine, Scope gScope)
{
var startState = FindStartState(machine, handler);
machine.PayloadType = GetStatePayload(startState);
gScope.Get(machine.Name, out Interface @interface);
@interface.PayloadType = machine.PayloadType;
}

private static void ValidateSpecObservesList(ITranslationErrorHandler handler, Machine machine, ICompilerConfiguration job)
{
if (machine.IsSpec)
Expand Down Expand Up @@ -227,14 +236,7 @@ private static void ValidateEventPayloadToTransitionTarget(ITranslationErrorHand

private static PLanguageType GetStatePayload(State startState)
{
if (!(startState.Entry?.Signature.Parameters.Count > 0))
{
return PrimitiveType.Null;
}

Debug.Assert(startState.Entry.Signature.Parameters.Count == 1,
"Allowed start state entry with multiple parameters");
return startState.Entry.Signature.Parameters[0].Type;
return startState.Entry?.Signature.Parameters.ElementAtOrDefault(0)?.Type ?? PrimitiveType.Null;
}

private static State FindStartState(Machine machine, ITranslationErrorHandler handler)
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@

/* PSrc/FrontDesk.p */
type tRoomInfo = (roomNumber: int, isAvailable: bool);


machine Main {
var rooms: map[int, tRoomInfo];

start state Init {
entry Init_Entry;
exit {
assert true;
}
}

fun Init_Entry(initialRooms: map[int, tRoomInfo]) {
new Main(default(map[int, tRoomInfo]));
}
}


Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
machine Main {
var m1_machine: machine;
var m2_machine: machine;
var m3_machine: machine;
var m4_machine: machine;

var msg_map : map[int, seq[string]];
var seqOfMsgs: seq[string];
var msg_tuple: (int, bool, string);

start state S {
entry{
m1_machine = new m1(4);
msg_tuple = (1,true,"msg1");
m2_machine = new m2(msg_tuple);
seqOfMsgs += (0,"Hello");
seqOfMsgs += (1,"World");
msg_map += (1,seqOfMsgs);
m3_machine = new m3(msg_map);
}
}
}

machine m1 {
start state S{
entry foo1;
}
fun foo1 (payload: int){
assert payload == 4;
}
}

machine m2 {
start state S{
entry foo3;
}
fun foo3 (payload: (int, bool, string)){
assert payload == (1,true,"msg1");
}
}


machine m3 {
start state S{
entry foo4;
}
fun foo4 (payload: map[int, seq[string]]){
assert payload[1][0] == "Hello";
}
}

Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
event E0;

machine Main {
var m1_machine: machine;
var m2_machine: machine;

start state S {
entry{
m1_machine = new m1(4);
m2_machine = new m2(m1_machine);
}
}
}

machine m1 {
start state S{
entry foo1;

on E0 do {
assert false;
}
}
fun foo1 (payload: int){
assert payload != 4;
}

}


machine m2 {
start state S{
entry foo2;
}
fun foo2 (payload: machine){
send payload,E0;
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
machine Main {
var m1_machine: machine;
var m2_machine: machine;

start state S {
entry{
m1_machine = new m1("four");
m2_machine = new m2((1,2,3))
}
}
}

machine m1 {
start state S{
entry foo;
}
fun foo (payload: int){
assert payload == 4;
}
}

machine m2 {
start state S{
entry foo;
}
fun foo (payload: map){
assert payload == (1,2,3);
}
}

Loading

0 comments on commit 8c4c600

Please sign in to comment.