diff --git a/Src/PCompiler/CompilerCore/Backend/Debugging/IrToPseudoP.cs b/Src/PCompiler/CompilerCore/Backend/Debugging/IrToPseudoP.cs index a135656da..df37c7ff2 100644 --- a/Src/PCompiler/CompilerCore/Backend/Debugging/IrToPseudoP.cs +++ b/Src/PCompiler/CompilerCore/Backend/Debugging/IrToPseudoP.cs @@ -175,6 +175,10 @@ private void WriteTree(IPAST tree) WriteStmt("assert ", assertStmt.Assertion, ", \"", assertStmt.Message, "\";"); break; + case AssumeStmt assumeStmt: + WriteStmt("assume ", assumeStmt.Assumption, ", \"", assumeStmt.Message, "\";"); + break; + case AssignStmt assignStmt: WriteStmt(assignStmt.Location, " = ", assignStmt.Value, ";"); break; diff --git a/Src/PCompiler/CompilerCore/Backend/IRTransformer.cs b/Src/PCompiler/CompilerCore/Backend/IRTransformer.cs index 943eba0df..7f9fe44a3 100644 --- a/Src/PCompiler/CompilerCore/Backend/IRTransformer.cs +++ b/Src/PCompiler/CompilerCore/Backend/IRTransformer.cs @@ -364,6 +364,22 @@ private List SimplifyStatement(IPStmt statement) }).ToList())); return assertDeps.Concat(new List{ifStmtForAssert}) .ToList(); + + case AssumeStmt assumeStmt: + (var assumeExpr, var assumeDeps) = SimplifyExpression(assumeStmt.Assumption); + (var amessageExpr, var amessageDeps) = SimplifyExpression(assumeStmt.Message); + if (assumeExpr is BoolLiteralExpr) + { + return assumeDeps.Concat(amessageDeps).Concat(new []{new AssumeStmt(location, assumeExpr, amessageExpr)}).ToList(); + } + + var aifStmtForAssert = new IfStmt(location, assumeExpr, new NoStmt(location), new CompoundStmt( + location, amessageDeps.Concat(new[] + { + new AssumeStmt(location, assumeExpr, amessageExpr) + }).ToList())); + return assumeDeps.Concat(new List{aifStmtForAssert}) + .ToList(); case AssignStmt assignStmt: (var assignLV, var assignLVDeps) = SimplifyLvalue(assignStmt.Location); @@ -434,7 +450,6 @@ private List SimplifyStatement(IPStmt statement) new CompoundStmt(ifStmt.ElseBranch.SourceLocation, elseBranch)) }) .ToList(); - case AddStmt addStmt: var (addVar, addVarDeps) = SimplifyLvalue(addStmt.Variable); var (addVal, addValDeps) = SimplifyArgPack(new[] { addStmt.Value }); diff --git a/Src/PCompiler/CompilerCore/Backend/Symbolic/TransformASTPass.cs b/Src/PCompiler/CompilerCore/Backend/Symbolic/TransformASTPass.cs index a2b60ac3e..071a55686 100644 --- a/Src/PCompiler/CompilerCore/Backend/Symbolic/TransformASTPass.cs +++ b/Src/PCompiler/CompilerCore/Backend/Symbolic/TransformASTPass.cs @@ -349,6 +349,8 @@ static private IPStmt ReplaceVars(IPStmt stmt, Dictionary var return new AnnounceStmt(announceStmt.SourceLocation, ReplaceVars(announceStmt.PEvent, varMap), ReplaceVars(announceStmt.Payload, varMap)); case AssertStmt assertStmt: return new AssertStmt(assertStmt.SourceLocation, ReplaceVars(assertStmt.Assertion, varMap), ReplaceVars(assertStmt.Message, varMap)); + case AssumeStmt assumeStmt: + return new AssumeStmt(assumeStmt.SourceLocation, ReplaceVars(assumeStmt.Assumption, varMap), ReplaceVars(assumeStmt.Message, varMap)); case AssignStmt assignStmt: return new AssignStmt(assignStmt.SourceLocation, ReplaceVars(assignStmt.Location, varMap), ReplaceVars(assignStmt.Value, varMap)); case CompoundStmt compoundStmt: diff --git a/Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs b/Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs index b8786954c..f0e65b4b8 100644 --- a/Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs +++ b/Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs @@ -3,6 +3,7 @@ using Plang.Compiler.Backend.Java; using Plang.Compiler.Backend.Stately; using Plang.Compiler.Backend.Symbolic; +using Plang.Compiler.Backend.Uclid5; namespace Plang.Compiler.Backend { @@ -17,6 +18,7 @@ static TargetLanguage() RegisterCodeGenerator(CompilerOutput.Java, new JavaCompiler()); RegisterCodeGenerator(CompilerOutput.Symbolic, new SymbolicCodeGenerator()); RegisterCodeGenerator(CompilerOutput.Stately, new StatelyCodeGenerator()); + RegisterCodeGenerator(CompilerOutput.Uclid5, new Uclid5CodeGenerator()); } private static void RegisterCodeGenerator(CompilerOutput name, ICodeGenerator generator) diff --git a/Src/PCompiler/CompilerCore/Backend/Uclid5/CompilationContext.cs b/Src/PCompiler/CompilerCore/Backend/Uclid5/CompilationContext.cs new file mode 100644 index 000000000..f80c4d89c --- /dev/null +++ b/Src/PCompiler/CompilerCore/Backend/Uclid5/CompilationContext.cs @@ -0,0 +1,11 @@ +namespace Plang.Compiler.Backend.Uclid5; + +internal class CompilationContext : CompilationContextBase +{ + public CompilationContext(ICompilerConfiguration job) : base(job) + { + FileName = $"{ProjectName}.ucl"; + } + + public string FileName { get; set; } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs new file mode 100644 index 000000000..d091f7274 --- /dev/null +++ b/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs @@ -0,0 +1,1643 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Text.RegularExpressions; + +using Plang.Compiler.TypeChecker; +using Plang.Compiler.TypeChecker.AST; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.AST.Expressions; +using Plang.Compiler.TypeChecker.AST.Statements; +using Plang.Compiler.TypeChecker.AST.States; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.Backend.Uclid5; + +public class Uclid5CodeGenerator : ICodeGenerator +{ + private CompilationContext _ctx; + private CompiledFile _src; + private HashSet _optionsToDeclare; + private HashSet _chooseToDeclare; + private HashSet _setCheckersToDeclare; + private Dictionary> _specListenMap; // keep track of the procedure names for each event + private Scope _globalScope; + + public bool HasCompilationStage => true; + + public void Compile(ICompilerConfiguration job) + { + var filename = $"{job.ProjectName}.ucl"; + var stdout = ""; + var stderr = ""; + + // compile the csproj file + var args = new[] { "-M", filename }; + + var exitCode = Compiler.RunWithOutput(job.OutputDirectory.FullName, out stdout, out stderr, "uclid", args); + if (exitCode != 0) + { + throw new TranslationException($"Verifying generated UCLID5 code FAILED!\n" + $"{stdout}\n" + $"{stderr}\n"); + } + + var failed = Regex.Matches(stdout, "UNDEF -> ").Count + Regex.Matches(stdout, "FAILED -> ").Count; + var succeeded = Regex.Matches(stdout, "PASSED -> ").Count; + + job.Output.WriteInfo($"Successfully verified {succeeded} conditions."); + job.Output.WriteInfo($"Failed to verify {failed} conditions."); + + var undefs = Regex.Matches(stdout, @"UNDEF -> (.*), line (\d+)"); + var fails = Regex.Matches(stdout, @"FAILED -> (.*), line (\d+)"); + + var query = File.ReadLines(job.OutputDirectory.FullName + "/" + filename).ToArray(); + + foreach (Match match in fails.Concat(undefs)) + { + foreach (var feedback in match.Groups[1].Captures.Zip(match.Groups[2].Captures)) + { + var line = query[Int32.Parse(feedback.Second.ToString()) - 1]; + var step = feedback.First.ToString().Contains("[Step #0]") ? "(base case)" : ""; + job.Output.WriteInfo($" -{line.Split("//").Last()} {step}"); + } + } + } + + public IEnumerable GenerateCode(ICompilerConfiguration job, Scope globalScope) + { + _ctx = new CompilationContext(job); + _src = new CompiledFile(_ctx.FileName); + _optionsToDeclare = []; + _chooseToDeclare = []; + _specListenMap = new Dictionary>(); + _setCheckersToDeclare = []; + _globalScope = globalScope; + GenerateMain(); + return new List { _src }; + } + + private void EmitLine(string str) + { + _ctx.WriteLine(_src.Stream, str); + } + + // Prefixes to avoid name clashes and keywords + private static string BuiltinPrefix => "P_"; + private static string UserPrefix => "User_"; + private static string EventPrefix => "PEvent_"; + private static string GotoPrefix => "PGoto_"; + private static string MachinePrefix => "PMachine_"; + private static string LocalPrefix => "PLocal_"; + private static string OptionPrefix => "POption_"; + private static string ChoosePrefix => "PChoose_"; + private static string CheckerPrefix => "PChecklist_"; + private static string SpecPrefix => "PSpec_"; + private static string InvariantPrefix => "PInv_"; + + // P values that don't have a direct UCLID5 equivalent + private static string PNull => $"{BuiltinPrefix}Null"; + private static string PNullDeclaration => $"type {PNull} = enum {{{PNull}}};"; + + private static string DefaultMachineRef => $"{BuiltinPrefix}DefaultMachine"; + private static string DefaultMachineDeclaration => $"const {DefaultMachineRef}: {MachineRefT};"; + + // P types that don't have a direct UCLID5 equivalent + private static string StringT => $"{BuiltinPrefix}String"; + private static string StringTDeclaration => $"type {StringT};"; + private static string DefaultString => $"{BuiltinPrefix}DefaultString"; + private static string DefaultStringDeclaration => $"const {DefaultString}: {StringT};"; + + /******************************** + * type StateADT = record {sent: [LabelADT]boolean, received: [LabelADT]boolean, machines: [MachineRefT]MachineStateADT}; + * var state: StateT; + *******************************/ + private static string StateAdt => $"{BuiltinPrefix}StateAdt"; + private static string StateAdtSentSelector => $"{StateAdt}_Sent"; + private static string StateAdtReceivedSelector => $"{StateAdt}_Received"; + private static string StateAdtMachinesSelector => $"{StateAdt}_Machines"; + + private static string StateAdtConstruct(string sent, string received, string machines) + { + return $"const_record({StateAdtSentSelector} := {sent}, {StateAdtReceivedSelector} := {received}, {StateAdtMachinesSelector} := {machines})"; + } + + private static string StateAdtSelectSent(string state) + { + return $"{state}.{StateAdtSentSelector}"; + } + private static string StateAdtSelectReceived(string state) + { + return $"{state}.{StateAdtReceivedSelector}"; + } + + private static string StateAdtSelectMachines(string state) + { + return $"{state}.{StateAdtMachinesSelector}"; + } + + private static string StateAdtDeclaration() + { + return + $"type {StateAdt} = record {{{StateAdtSentSelector}: [{LabelAdt}]boolean, {StateAdtReceivedSelector}: [{LabelAdt}]boolean, {StateAdtMachinesSelector}: [{MachineRefT}]{MachineStateAdt}}};"; + } + + private static string InFlight(string state, string action) + { + return $"({StateAdtSelectSent(state)}[{action}] && !{StateAdtSelectReceived(state)}[{action}])"; + } + + private static string StateVar => $"{BuiltinPrefix}State"; + private static string StateVarDeclaration => $"var {StateVar}: {StateAdt};"; + + private static string Deref(string r) + { + return $"{StateAdtSelectMachines(StateVar)}[{r}]"; + } + + /******************************** + * type MachineRef; + * + * type MachineStateADT = record {stage: boolean; machine: MachineADT}; + * + * // where Mi are the declared machines, Si their P state names, and MiFjl their fields + * type MachineADT = | M0(M0_State: S0, M0F00, ..., M0F0n) + * | ... + * | Mk(Mk_State: Sk, MkFk0, ..., MkFkm) + *******************************/ + private static string MachineRefT => $"{MachinePrefix}Ref_t"; + private static string MachineRefTDeclaration => $"type {MachineRefT};"; + private static string MachineStateAdt => $"{MachinePrefix}State_ADT"; + private static string MachineStateAdtStageSelector => $"{MachineStateAdt}_Stage"; + private static string MachineStateAdtMachineSelector => $"{MachineStateAdt}_Machine"; + + private static string MachineStateAdtConstruct(string stage, string machine) + { + return + $"const_record({MachineStateAdtStageSelector} := {stage}, {MachineStateAdtMachineSelector} := {machine})"; + } + + private static string MachineStateAdtSelectStage(string state) + { + return $"{state}.{MachineStateAdtStageSelector}"; + } + + private static string MachineStateAdtSelectMachine(string state) + { + return $"{state}.{MachineStateAdtMachineSelector}"; + } + + private static string MachineStateAdtDeclaration() + { + return + $"type {MachineStateAdt} = record {{{MachineStateAdtStageSelector}: boolean, {MachineStateAdtMachineSelector}: {MachineAdt}}};"; + } + + private static string MachineAdt => $"{MachinePrefix}ADT"; + + private string MachineAdtDeclaration(List machines) + { + var sum = string.Join("\n\t\t| ", machines.Select(ProcessMachine)); + return $"datatype {MachineAdt} = \n\t\t| {sum};"; + + string ProcessMachine(Machine m) + { + var fields = string.Join(", ", + m.Fields.Select(f => $"{MachinePrefix}{m.Name}_{f.Name}: {TypeToString(f.Type)}")); + if (m.Fields.Any()) fields = ", " + fields; + + return $"{MachinePrefix}{m.Name} ({MachinePrefix}{m.Name}_State: {MachinePrefix}{m.Name}_StateAdt{fields})"; + } + } + + private static string MachineAdtConstructM(Machine m, List args) + { + return $"{MachinePrefix}{m.Name}({string.Join(", ", args)})"; + } + + private static string MachineAdtSelectState(string instance, Machine m) + { + return $"{instance}.{MachinePrefix}{m.Name}_State"; + } + + private static string MachineStateAdtSelectState(string state, Machine m) + { + return MachineAdtSelectState(MachineStateAdtSelectMachine(state), m); + } + + private static string MachineAdtSelectField(string instance, Machine m, Variable f) + { + return $"{instance}.{MachinePrefix}{m.Name}_{f.Name}"; + } + + private static string MachineStateAdtSelectField(string state, Machine m, Variable f) + { + return MachineAdtSelectField(MachineStateAdtSelectMachine(state), m, f); + } + + private static string MachinePStateDeclaration(Machine m) + { + var states = string.Join(", ", m.States.Select(s => $"{MachinePrefix}{m.Name}_{s.Name}")); + return $"type {MachinePrefix}{m.Name}_StateAdt = enum {{{states}}};"; + } + + private static string MachineAdtIsM(string instance, Machine machine) + { + return $"is_{MachinePrefix}{machine.Name}({instance})"; + } + + private static string MachineStateAdtIsM(string state, Machine machine) + { + return $"is_{MachinePrefix}{machine.Name}({MachineStateAdtSelectMachine(state)})"; + } + + private static string MachineStateAdtInS(string state, Machine m, State s) + { + return $"({MachineStateAdtIsM(state, m)} && {MachineStateAdtSelectState(state, m)} == {MachinePrefix}{m.Name}_{s.Name})"; + } + + + private static string InStartPredicateDeclaration(List machines) + { + var input = $"{LocalPrefix}state"; + var cases = machines.Select(ProcessMachine).ToList(); + var body = cases.Aggregate("false", (acc, pair) => $"if ({pair.Item1}) then ({pair.Item2})\n\t\telse ({acc})"); + return $"define {BuiltinPrefix}InStart({input}: {MachineStateAdt}) : boolean =\n\t\t{body};"; + + (string, string) ProcessMachine(Machine m) + { + var machine = $"{MachineStateAdtSelectMachine(input)}"; + var state = $"{machine}.{MachinePrefix}{m.Name}_State"; + var start = $"{MachinePrefix}{m.Name}_{m.StartState.Name}"; + var check = $"{state} == {start}"; + var guard = MachineAdtIsM(machine, m); + return (guard, check); + } + } + + private static string InEntryPredicateDeclaration() + { + var input = $"{LocalPrefix}state"; + return + $"define {BuiltinPrefix}InEntry({input}: {MachineStateAdt}) : boolean = {MachineStateAdtSelectStage(input)};"; + } + + /******************************** + * type LabelAdt = record {target: MachineRef, action: EitherEventOrGotoAdt} + * + * datatype EitherEventOrGotoAdt = | EventLabel (event: EventAdt) + * | GotoLabel (goto: GotoAdt) + * + * // where Ei is an event, Pi is the payload of the event and Ti is the type of the payload + * datatype EventAdt = | E0 (P0: T0) + * | ... + * | En (Pn: Tn) + * + * // where Si are as in MachineAdt and A0 are the arguments to the entry handler of the state + * datatype GotoAdt = | M0 (M0_State: S0, A0: T0) + * | ... + * | Mn (Mn_State: Sn, An: Tn) + *******************************/ + private static string LabelAdt => $"{BuiltinPrefix}Label"; + private static string LabelAdtTargetSelector => $"{LabelAdt}_Target"; + private static string LabelAdtActionSelector => $"{LabelAdt}_Action"; + private static string LabelAdtActionCountSelector => $"{LabelAdt}_ActionCount"; + + private static string LabelAdtDeclaration() + { + return + $"type {LabelAdt} = record {{{LabelAdtTargetSelector}: {MachineRefT}, {LabelAdtActionSelector}: {EventOrGotoAdt}, {LabelAdtActionCountSelector}: integer}};"; + } + + private void IncrementActionCount() + { + EmitLine($"{BuiltinPrefix}ActionCount = {BuiltinPrefix}ActionCount + 1;"); + } + + private static string LabelAdtConstruct(string target, string action) + { + return $"const_record({LabelAdtTargetSelector} := {target}, {LabelAdtActionSelector} := {action}, {LabelAdtActionCountSelector} := {BuiltinPrefix}ActionCount)"; + } + + private static string LabelAdtSelectTarget(string label) + { + return $"{label}.{LabelAdtTargetSelector}"; + } + + private static string LabelAdtSelectAction(string label) + { + return $"{label}.{LabelAdtActionSelector}"; + } + + private static string LabelAdtSelectActionCount(string label) + { + return $"{label}.{LabelAdtActionCountSelector}"; + } + + + private static string EventOrGotoAdt => $"{BuiltinPrefix}EventOrGoto"; + private static string EventOrGotoAdtEventConstructor => $"{EventOrGotoAdt}_Event"; + private static string EventOrGotoAdtGotoConstructor => $"{EventOrGotoAdt}_Goto"; + private static string EventOrGotoAdtEventSelector => $"{EventOrGotoAdt}_Event_Event"; + private static string EventOrGotoAdtGotoSelector => $"{EventOrGotoAdt}_Goto_Goto"; + + private static string EventOrGotoAdtDeclaration() + { + var e = $"| {EventOrGotoAdtEventConstructor}({EventOrGotoAdtEventSelector}: {EventAdt})"; + var g = $"| {EventOrGotoAdtGotoConstructor}({EventOrGotoAdtGotoSelector}: {GotoAdt})"; + return $"datatype {EventOrGotoAdt} = \n\t\t{e}\n\t\t{g};"; + } + + private static string EventOrGotoAdtConstructEvent(string e) + { + return $"{EventOrGotoAdtEventConstructor}({e})"; + } + + private string EventOrGotoAdtConstructEvent(PEvent ev, IPExpr arg) + { + var payload = arg is null ? "" : ExprToString(arg); + var e = EventAdtConstruct(payload, ev); + return $"{EventOrGotoAdtEventConstructor}({e})"; + } + + + private static string EventOrGotoAdtConstructGoto(string g) + { + return $"{EventOrGotoAdtGotoConstructor}({g})"; + } + + private string EventOrGotoAdtConstructGoto(State state, IPExpr payload) + { + var g = GotoAdtConstruct(state, payload); + return $"{EventOrGotoAdtGotoConstructor}({g})"; + } + + private static string EventOrGotoAdtSelectEvent(string eventOrGoto) + { + return $"{eventOrGoto}.{EventOrGotoAdtEventSelector}"; + } + + private static string EventOrGotoAdtSelectGoto(string eventOrGoto) + { + return $"{eventOrGoto}.{EventOrGotoAdtGotoSelector}"; + } + + private static string EventOrGotoAdtIsEvent(string eventOrGoto) + { + return $"is_{EventOrGotoAdtEventConstructor}({eventOrGoto})"; + } + + private static string EventOrGotoAdtIsGoto(string eventOrGoto) + { + return $"is_{EventOrGotoAdtGotoConstructor}({eventOrGoto})"; + } + + private static string EventAdt => $"{EventPrefix}Adt"; + + private string EventAdtDeclaration(List events) + { + var declarationSum = string.Join("\n\t\t| ", events.Select(EventDeclarationCase)); + return $"datatype {EventAdt} = \n\t\t| {declarationSum};"; + + string EventDeclarationCase(PEvent e) + { + var pt = e.PayloadType.IsSameTypeAs(PrimitiveType.Null) ? "" : $"{EventPrefix}{e.Name}_Payload: {TypeToString(e.PayloadType)}"; + return + $"{EventPrefix}{e.Name} ({pt})"; + } + } + + private static string EventAdtSelectPayload(string eadt, PEvent e) + { + return $"{eadt}.{EventPrefix}{e.Name}_Payload"; + } + + private static string EventAdtConstruct(string payload, PEvent e) + { + return $"{EventPrefix}{e.Name}({payload})"; + } + + private static string EventAdtIsE(string instance, PEvent e) + { + return $"is_{EventPrefix}{e.Name}({instance})"; + } + + private static string EventOrGotoAdtIsE(string instance, PEvent e) + { + var isEvent = EventOrGotoAdtIsEvent(instance); + var selectEvent = EventOrGotoAdtSelectEvent(instance); + var correctEvent = EventAdtIsE(selectEvent, e); + return $"({isEvent} && {correctEvent})"; + } + + private static string LabelAdtIsE(string instance, PEvent e) + { + var action = LabelAdtSelectAction(instance); + return EventOrGotoAdtIsE(action, e); + } + + private static string LabelAdtSelectPayloadField(string instance, PEvent e, NamedTupleEntry field) + { + var action = LabelAdtSelectAction(instance); + return $"{EventAdtSelectPayload(EventOrGotoAdtSelectEvent(action), e)}.{field.Name}"; + } + + private static string GotoAdt => $"{GotoPrefix}Adt"; + + private string GotoAdtDeclaration(IEnumerable machines) + { + List<(State, Variable)> gotos = []; + foreach (var m in machines) + foreach (var s in m.States) + { + var f = s.Entry; + // get the arguments to the entry handler + Variable a = null; + if (f is not null && s.Entry.Signature.Parameters.Count > 0) + { + a = s.Entry.Signature.Parameters[0]; + } + + gotos.Add((s, a)); + } + + var sum = string.Join("\n\t\t| ", gotos.Select(ProcessGoto)); + + return $"datatype {GotoAdt} = \n\t\t| {sum};"; + + string ProcessGoto((State, Variable) g) + { + var prefix = $"{GotoPrefix}{g.Item1.OwningMachine.Name}_{g.Item1.Name}"; + if (g.Item2 is null) + { + return prefix + "()"; + } + + return prefix + $"({prefix}_{g.Item2.Name}: {TypeToString(g.Item2.Type)})"; + } + } + + private string GotoAdtConstruct(State s, IPExpr p) + { + var payload = p is null ? "" : ExprToString(p); + return $"{GotoPrefix}{s.OwningMachine.Name}_{s.Name}({payload})"; + } + + private string GotoAdtSelectParam(string instance, string param, State s) + { + return $"{instance}.{GotoPrefix}{s.OwningMachine.Name}_{s.Name}_{param}"; + } + + private static string GotoAdtIsS(string instance, State s) + { + return $"is_{GotoPrefix}{s.OwningMachine.Name}_{s.Name}({instance})"; + } + + private static string EventOrGotoAdtIsS(string instance, State s) + { + var isGoto = EventOrGotoAdtIsGoto(instance); + var selectGoto = EventOrGotoAdtSelectGoto(instance); + var correctGoto = GotoAdtIsS(selectGoto, s); + return $"({isGoto} && {correctGoto})"; + } + + private static string LabelAdtIsS(string instance, State s) + { + var action = LabelAdtSelectAction(instance); + return EventOrGotoAdtIsS(action, s); + } + + + /******************************** + * Spec machines are treated differently than regular machines. For example, there is only ever a single instance of + * each spec machine. + * + * To handle spec machines, + * 1) we create a global variable for each of their fields; + * 2) keep track of what events the spec machines are listening to and the corresponding handleers; + * 3) create a procedure per spec machine handler that operates on the variables from (1); and + * 4) whenever a regular machine sends an event, we call the appropriate handler from (2). + *******************************/ + private void SpecVariableDeclarations(List specs) + { + foreach (var spec in specs) + { + EmitLine($"type {SpecPrefix}{spec.Name}_StateAdt = enum {{{string.Join(", ", spec.States.Select(n => $"{SpecPrefix}{spec.Name}_{n.Name}"))}}};"); + EmitLine($"var {SpecPrefix}{spec.Name}_State: {SpecPrefix}{spec.Name}_StateAdt;"); + foreach (var f in spec.Fields) + { + EmitLine($"var {SpecPrefix}{spec.Name}_{f.Name}: {TypeToString(f.Type)};"); + } + } + } + + private void GenerateSpecProcedures(List specs) + { + foreach (var spec in specs) + { + foreach (var f in spec.Methods) + { + var ps = f.Signature.Parameters.Select(p => $"{GetLocalName(p)}: {TypeToString(p.Type)}"); + var line = _ctx.LocationResolver.GetLocation(f.SourceLocation).Line; + var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name; + EmitLine($"procedure [inline] {name}({string.Join(", ", ps)})"); + if (!f.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null)) + { + EmitLine($"\treturns ({BuiltinPrefix}Return: {TypeToString(f.Signature.ReturnType)})"); + } + EmitLine("{"); + + // declare local variables corresponding to the global spec variables + EmitLine($"var {LocalPrefix}state: {SpecPrefix}{spec.Name}_StateAdt;"); + foreach (var v in spec.Fields) + { + EmitLine($"var {GetLocalName(v)}: {TypeToString(v.Type)};"); + } + + // declare local variables for the method + foreach (var v in f.LocalVariables) EmitLine($"var {GetLocalName(v)}: {TypeToString(v.Type)};"); + // foreach (var v in f.LocalVariables) EmitLine($"{GetLocalName(v)} = {DefaultValue(v.Type)};"); + + // Set the local variables corresponding to the global spec variables to the correct starting value + foreach (var v in spec.Fields) + EmitLine($"{GetLocalName(v)} = {SpecPrefix}{spec.Name}_{v.Name};"); + + GenerateStmt(f.Body, spec); + + // update the global variables + EmitLine($"{SpecPrefix}{spec.Name}_State = {LocalPrefix}state;"); + foreach (var v in spec.Fields) + { + EmitLine($"{SpecPrefix}{spec.Name}_{v.Name} = {GetLocalName(v)};"); + } + + EmitLine("}\n"); + } + } + } + + private void GenerateSpecHandlers(List specs) + { + foreach (var spec in specs) + { + var events = spec.Observes.Events; + foreach (var e in events) + { + var procedureName = $"{SpecPrefix}{spec.Name}_{e.Name}"; + if (_specListenMap.ContainsKey(e)) + { + _specListenMap[e].Add(procedureName); + } + else + { + _specListenMap.Add(e, [procedureName]); + } + EmitLine($"procedure [inline] {procedureName}({SpecPrefix}Payload: {TypeToString(e.PayloadType)})"); + EmitLine("{"); + EmitLine("case"); + foreach (var state in spec.States) + { + var handlers = state.AllEventHandlers.ToDictionary(); + if (state.HasHandler(e)) + { + var handler = handlers[e]; + var precondition = $"{SpecPrefix}{spec.Name}_State == {SpecPrefix}{spec.Name}_{state.Name}"; + EmitLine($"({precondition}) : {{"); + switch (handler) + { + case EventDoAction eventDoAction: + var f = eventDoAction.Target; + var line = _ctx.LocationResolver.GetLocation(f.SourceLocation).Line; + var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name; + var payload = f.Signature.Parameters.Count > 0 ? $"{SpecPrefix}Payload" : ""; + EmitLine($"call {name}({payload});"); + break; + default: + throw new NotSupportedException($"Not supported handler ({handler}) at {GetLocation(handler)}"); + } + EmitLine("}"); + } + } + EmitLine("esac"); + EmitLine("}"); + } + } + } + + /******************************** + * Traverse the P AST and generate the UCLID5 code using the types and helpers defined above + *******************************/ + private void GenerateMain() + { + EmitLine("module main {"); + + var machines = (from m in _globalScope.AllDecls.OfType() where !m.IsSpec select m).ToList(); + var specs = (from m in _globalScope.AllDecls.OfType() where m.IsSpec select m).ToList(); + var events = _globalScope.AllDecls.OfType().ToList(); + var invariants = _globalScope.AllDecls.OfType().ToList(); + var axioms = _globalScope.AllDecls.OfType().ToList(); + var pures = _globalScope.AllDecls.OfType().ToList(); + + EmitLine(PNullDeclaration); + EmitLine(DefaultMachineDeclaration); + EmitLine(StringTDeclaration); + EmitLine(DefaultStringDeclaration); + EmitLine(""); + + GenerateUserEnums(_globalScope.AllDecls.OfType()); + GenerateUserTypes(_globalScope.AllDecls.OfType()); + EmitLine(""); + + EmitLine(EventAdtDeclaration(events)); + EmitLine(""); + EmitLine(GotoAdtDeclaration(machines)); + EmitLine(""); + EmitLine(EventOrGotoAdtDeclaration()); + EmitLine(LabelAdtDeclaration()); + EmitLine($"var {BuiltinPrefix}ActionCount: integer;"); + EmitLine(""); + + EmitLine(MachineRefTDeclaration); + foreach (var m in machines) + { + EmitLine(MachinePStateDeclaration(m)); + } + + EmitLine(MachineAdtDeclaration(machines)); + EmitLine(MachineStateAdtDeclaration()); + EmitLine(""); + + EmitLine(StateAdtDeclaration()); + EmitLine(StateVarDeclaration); + EmitLine(""); + + SpecVariableDeclarations(specs); + EmitLine(""); + + EmitLine(InStartPredicateDeclaration(machines)); + EmitLine(InEntryPredicateDeclaration()); + EmitLine(""); + + GenerateInitBlock(machines, specs, _globalScope.AllDecls.OfType()); + EmitLine(""); + + // pick a random label and handle it (with some guards to make sure we always handle gotos before events) + if (_ctx.Job.HandlesAll) + { + GenerateNextBlock(machines, events); + EmitLine(""); + } + + // global functions + GenerateGlobalProcedures(_globalScope.AllDecls.OfType()); + + // Spec support + GenerateSpecProcedures(specs); // generate spec methods, called by spec handlers + GenerateSpecHandlers(specs); // will populate _specListenMap, which is used when ever there is a send statement + EmitLine(""); + + // non-handler functions for handlers + GenerateMachineProcedures(machines); // generate machine methods, called by handlers below + EmitLine(""); + + // generate the handlers + foreach (var m in machines) + { + foreach (var s in m.States) + { + GenerateEntryHandler(s, invariants); + foreach (var e in events.Where(e => !e.IsNullEvent && s.HasHandler(e))) + { + GenerateEventHandler(s, e, invariants); + } + } + } + + EmitLine(""); + + // These have to be done at the end because we don't know what we need until we generate the rest of the code + GenerateOptionTypes(); + EmitLine(""); + GenerateCheckerVars(); + EmitLine(""); + GenerateChooseProcedures(); + EmitLine(""); + + foreach (var pure in pures) + { + var args = string.Join(", ", pure.Signature.Parameters.Select(p => $"{LocalPrefix}{p.Name}: {TypeToString(p.Type)}")); + if (pure.Body is null) + { + EmitLine($"function {pure.Name}({args}): {TypeToString(pure.Signature.ReturnType)};"); + } + else + { + EmitLine($"define {pure.Name}({args}): {TypeToString(pure.Signature.ReturnType)} = {ExprToString(pure.Body)};"); + } + } + EmitLine(""); + + foreach (var inv in invariants) + { + EmitLine($"define {InvariantPrefix}{inv.Name}(): boolean = {ExprToString(inv.Body)};"); + EmitLine($"invariant _{InvariantPrefix}{inv.Name}: {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name} globally"); + } + EmitLine(""); + + foreach (var ax in axioms) + { + EmitLine($"axiom {ExprToString(ax.Body)};"); + } + EmitLine(""); + + // invariants to ensure unique action IDs + EmitLine($"define {InvariantPrefix}Unique_Actions(): boolean = forall (a1: {LabelAdt}, a2: {LabelAdt}) :: (a1 != a2 && {StateAdtSelectSent(StateVar)}[a1] && {StateAdtSelectSent(StateVar)}[a2]) ==> {LabelAdtSelectActionCount("a1")} != {LabelAdtSelectActionCount("a2")};"); + EmitLine($"invariant _{InvariantPrefix}Unique_Actions: {InvariantPrefix}Unique_Actions();"); + EmitLine($"define {InvariantPrefix}Increasing_Action_Count(): boolean = forall (a: {LabelAdt}) :: {StateAdtSelectSent(StateVar)}[a] ==> {LabelAdtSelectActionCount("a")} < {BuiltinPrefix}ActionCount;"); + EmitLine($"invariant _{InvariantPrefix}Increasing_Action_Count: {InvariantPrefix}Increasing_Action_Count();"); + // invariants to ensure received is a subset of sent + EmitLine($"define {InvariantPrefix}Received_Subset_Sent(): boolean = forall (a: {LabelAdt}) :: {StateAdtSelectReceived(StateVar)}[a] ==> {StateAdtSelectSent(StateVar)}[a];"); + EmitLine($"invariant _{InvariantPrefix}Received_Subset_Sent: {InvariantPrefix}Received_Subset_Sent();"); + EmitLine(""); + + GenerateControlBlock(machines, events); + + // close the main module + EmitLine("}"); + } + + private void GenerateUserEnums(IEnumerable enums) + { + foreach (var e in enums) + { + var variants = string.Join(", ", e.Values.Select(v => UserPrefix + v.Name)); + EmitLine($"type {UserPrefix}{e.Name} = enum {{{variants}}};"); + } + } + + private void GenerateUserTypes(IEnumerable types) + { + foreach (var t in types) EmitLine($"type {UserPrefix}{t.Name} = {TypeToString(t.Type)};"); + } + + private void GenerateInitBlock(List machines, List specs, IEnumerable starts) + { + var state = Deref("r"); + EmitLine("init {"); + EmitLine("// Every machine begins in their start state"); + EmitLine($"assume(forall (r: {MachineRefT}) :: {BuiltinPrefix}InStart({state}));"); + EmitLine("// Every machine begins with their entry flag set"); + EmitLine($"assume(forall (r: {MachineRefT}) :: {BuiltinPrefix}InEntry({state}));"); + EmitLine("// The buffer starts completely empty"); + EmitLine($"{StateAdtSelectSent(StateVar)} = const(false, [{LabelAdt}]boolean);"); + EmitLine($"{StateAdtSelectReceived(StateVar)} = const(false, [{LabelAdt}]boolean);"); + + EmitLine("// User assumptions"); + foreach (var assumes in starts) + { + EmitLine($"assume ({ExprToString(assumes.Body)}); // {assumes.Name}"); + } + + // close the init block + EmitLine("}"); + } + + private void GenerateNextBlock(List machines, List events) + { + var currentLabel = $"{BuiltinPrefix}CurrentLabel"; + // pick a random label and handle it + EmitLine("next {"); + EmitLine($"var {currentLabel}: {LabelAdt};"); + EmitLine($"if ({InFlight(StateVar, currentLabel)}) {{"); + EmitLine("case"); + foreach (var m in machines) + { + foreach (var s in m.States) + { + foreach (var e in events.Where(e => !e.IsNullEvent && !e.IsHaltEvent)) + { + if (!s.HasHandler(e)) + { + if (_ctx.Job.CheckOnly is null || _ctx.Job.CheckOnly == m.Name || _ctx.Job.CheckOnly == s.Name || _ctx.Job.CheckOnly == e.Name) + { + EmitLine($"({EventGuard(m, s, e)}) : {{"); + EmitLine($"assert false; // Failed to verify that {m.Name} never receives {e.Name} in {s.Name}"); + EmitLine("}"); + } + } + } + } + } + + EmitLine("esac"); + EmitLine("}"); + // close the next block + EmitLine("}"); + return; + + string EventGuard(Machine m, State s, PEvent e) + { + var correctMachine = MachineStateAdtIsM(Deref(LabelAdtSelectTarget(currentLabel)), m); + var correctState = MachineStateAdtInS(Deref(LabelAdtSelectTarget(currentLabel)), m, s); + var correctEvent = LabelAdtIsE(currentLabel, e); + return string.Join(" && ", [correctMachine, correctState, correctEvent]); + } + } + + private void GenerateGlobalProcedures(IEnumerable functions) + { + // TODO: these should be side-effect free and we should enforce that + foreach (var f in functions) + { + var ps = f.Signature.Parameters.Select(p => $"{GetLocalName(p)}: {TypeToString(p.Type)}"); + + if (f.Body is null) + { + EmitLine($"procedure [noinline] {f.Name}({string.Join(", ", ps)})"); + } + else + { + EmitLine($"procedure [inline] {f.Name}({string.Join(", ", ps)})"); + } + + if (!f.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null)) + { + EmitLine($"\treturns ({BuiltinPrefix}Return: {TypeToString(f.Signature.ReturnType)})"); + } + + EmitLine("{"); + // declare local variables for the method + foreach (var v in f.LocalVariables) EmitLine($"var {GetLocalName(v)}: {TypeToString(v.Type)};"); + GenerateStmt(f.Body, null); + EmitLine("}\n"); + } + } + + private void GenerateMachineProcedures(List machines) + { + foreach (var m in machines) + { + foreach (var f in m.Methods) + { + var ps = f.Signature.Parameters.Select(p => $"{GetLocalName(p)}: {TypeToString(p.Type)}").Prepend($"this: {MachineRefT}"); + var line = _ctx.LocationResolver.GetLocation(f.SourceLocation).Line; + var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name; + EmitLine($"procedure [inline] {name}({string.Join(", ", ps)})"); + + var currState = Deref("this"); + + if (!f.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null)) + { + EmitLine($"\treturns ({BuiltinPrefix}Return: {TypeToString(f.Signature.ReturnType)})"); + } + + EmitLine("{"); + + // declare necessary local variables + EmitLine($"var {LocalPrefix}state: {MachinePrefix}{m.Name}_StateAdt;"); + EmitLine($"var {LocalPrefix}stage: boolean;"); + EmitLine($"var {LocalPrefix}sent: [{LabelAdt}]boolean;"); + foreach (var v in m.Fields) EmitLine($"var {GetLocalName(v)}: {TypeToString(v.Type)};"); + foreach (var v in f.LocalVariables) EmitLine($"var {GetLocalName(v)}: {TypeToString(v.Type)};"); + + // initialize all the local variables to the correct values + EmitLine($"{LocalPrefix}state = {MachineStateAdtSelectState(currState, m)};"); + EmitLine($"{LocalPrefix}stage = false;"); // this can be set to true by a goto statement + EmitLine($"{LocalPrefix}sent = {StateAdtSelectSent(StateVar)};"); + foreach (var v in m.Fields) + EmitLine($"{GetLocalName(v)} = {MachineStateAdtSelectField(currState, m, v)};"); + // foreach (var v in f.LocalVariables) EmitLine($"{GetLocalName(v)} = {DefaultValue(v.Type)};"); + + GenerateStmt(f.Body, null); + + var fields = m.Fields.Select(GetLocalName).Prepend($"{LocalPrefix}state").ToList(); + + // make a new machine + var newMachine = MachineAdtConstructM(m, fields); + // make a new machine state + var newMachineState = MachineStateAdtConstruct($"{LocalPrefix}stage", newMachine); + // update the machine map + EmitLine( + $"{StateAdtSelectMachines(StateVar)} = {StateAdtSelectMachines(StateVar)}[this -> {newMachineState}];"); + // update the buffer + EmitLine($"{StateAdtSelectSent(StateVar)} = {LocalPrefix}sent;"); + + EmitLine("}\n"); + } + } + } + + private void GenerateEntryHandler(State s, List invariants) + { + var label = $"{LocalPrefix}Label"; + var target = LabelAdtSelectTarget(label); + var targetMachineState = Deref(target); + var action = LabelAdtSelectAction(label); + var g = EventOrGotoAdtSelectGoto(action); + var received = StateAdtSelectReceived(StateVar); + + EmitLine($"procedure [noinline] {s.OwningMachine.Name}_{s.Name}({label}: {LabelAdt})"); + EmitLine($"\trequires {InFlight(StateVar, label)};"); + EmitLine($"\trequires {EventOrGotoAdtIsGoto(action)};"); + EmitLine($"\trequires {GotoAdtIsS(g, s)};"); + EmitLine($"\trequires {MachineStateAdtInS(targetMachineState, s.OwningMachine, s)};"); + EmitLine($"\trequires {InvariantPrefix}Unique_Actions();"); + EmitLine($"\tensures {InvariantPrefix}Unique_Actions();"); + EmitLine($"\trequires {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\tensures {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\trequires {InvariantPrefix}Received_Subset_Sent();"); + EmitLine($"\tensures {InvariantPrefix}Received_Subset_Sent();"); + + + foreach (var inv in invariants) + { + EmitLine($"\trequires {InvariantPrefix}{inv.Name}();"); + EmitLine($"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name} at {GetLocation(s)}"); + } + + EmitLine("{"); + + if (s.Entry is null) + { + EmitLine($"var {LocalPrefix}stage: boolean;"); + EmitLine($"var {LocalPrefix}state: {MachinePrefix}{s.OwningMachine.Name}_StateAdt;"); + EmitLine($"var {LocalPrefix}received: [{LabelAdt}]boolean;"); + + EmitLine($"{LocalPrefix}stage = false;"); + EmitLine($"{LocalPrefix}state = {MachineStateAdtSelectState(targetMachineState, s.OwningMachine)};"); + EmitLine($"{received} = {received}[{label} -> true];"); + EmitLine($"{LocalPrefix}received = {received};"); + + var fields = s.OwningMachine.Fields.Select(v => MachineStateAdtSelectField(targetMachineState, s.OwningMachine, v)).Prepend($"{LocalPrefix}state").ToList(); + // make a new machine + var newMachine = MachineAdtConstructM(s.OwningMachine, fields); + // make a new machine state + var newMachineState = MachineStateAdtConstruct($"{LocalPrefix}stage", newMachine); + // update the machine map + EmitLine( + $"{StateAdtSelectMachines(StateVar)} = {StateAdtSelectMachines(StateVar)}[{target} -> {newMachineState}];"); + // update the buffer + EmitLine($"{received} = {LocalPrefix}received;"); + } + else + { + var f = s.Entry; + var line = _ctx.LocationResolver.GetLocation(f.SourceLocation).Line; + var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name; + var payload = f.Signature.Parameters.Count > 0 ? $", {GotoAdtSelectParam(g, f.Signature.Parameters[0].Name, s)}" : ""; + EmitLine($"{received} = {received}[{label} -> true];"); + EmitLine($"call {name}({target}{payload});"); + } + + EmitLine("}\n"); + } + + + private void GenerateEventHandler(State s, PEvent ev, List invariants) + { + var label = $"{LocalPrefix}Label"; + EmitLine($"procedure [noinline] {s.OwningMachine.Name}_{s.Name}_{ev.Name}({label}: {LabelAdt})"); + + var target = LabelAdtSelectTarget(label); + var targetMachineState = Deref(target); + var action = LabelAdtSelectAction(label); + var e = EventOrGotoAdtSelectEvent(action); + var received = StateAdtSelectReceived(StateVar); + + EmitLine($"\trequires {InFlight(StateVar, label)};"); + EmitLine($"\trequires {MachineStateAdtInS(targetMachineState, s.OwningMachine, s)};"); + EmitLine($"\trequires {EventOrGotoAdtIsEvent(action)};"); + EmitLine($"\trequires {EventAdtIsE(e, ev)};"); + EmitLine($"\trequires {InvariantPrefix}Unique_Actions();"); + EmitLine($"\tensures {InvariantPrefix}Unique_Actions();"); + EmitLine($"\trequires {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\tensures {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\trequires {InvariantPrefix}Received_Subset_Sent();"); + EmitLine($"\tensures {InvariantPrefix}Received_Subset_Sent();"); + + var handler = s.AllEventHandlers.ToDictionary()[ev]; + + foreach (var inv in invariants) + { + EmitLine($"\trequires {InvariantPrefix}{inv.Name}();"); + EmitLine($"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name} at {GetLocation(handler)}"); + } + + switch (handler) + { + case EventDefer _: + EmitLine("{"); + EmitLine("}\n"); + return; + case EventDoAction eventDoAction: + var f = eventDoAction.Target; + var line = _ctx.LocationResolver.GetLocation(f.SourceLocation).Line; + var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name; + var payload = f.Signature.Parameters.Count > 0 ? $", {EventAdtSelectPayload(e, ev)}" : ""; + EmitLine("{"); + EmitLine($"{received} = {received}[{label} -> true];"); + EmitLine($"call {name}({target}{payload});"); + EmitLine("}\n"); + return; + case EventIgnore _: + EmitLine("{"); + EmitLine("}\n"); + return; + default: + throw new NotSupportedException($"Not supported handler ({handler}) at {GetLocation(handler)}"); + } + } + + + private void GenerateControlBlock(List machines, List events) + { + EmitLine("control {"); + EmitLine($"set_solver_option(\":Timeout\", {_ctx.Job.Timeout});"); // timeout per query in seconds + + EmitLine("induction(1);"); + + foreach (var m in machines) + { + foreach (var s in m.States) + { + if (_ctx.Job.CheckOnly is null || _ctx.Job.CheckOnly == m.Name || _ctx.Job.CheckOnly == s.Name) + { + EmitLine($"verify({m.Name}_{s.Name});"); + } + + foreach (var e in events.Where(e => !e.IsNullEvent && !e.IsHaltEvent && s.HasHandler(e))) + { + if (_ctx.Job.CheckOnly is null || _ctx.Job.CheckOnly == m.Name || _ctx.Job.CheckOnly == s.Name || _ctx.Job.CheckOnly == e.Name) + { + EmitLine($"verify({m.Name}_{s.Name}_{e.Name});"); + } + } + } + } + + EmitLine("check;"); + EmitLine("print_results;"); + EmitLine("}"); + } + + private string DefaultValue(PLanguageType ty) + { + return ty switch + { + EnumType enumType => UserPrefix + enumType.EnumDecl.Values.First().Name, + MapType mapType => + $"const({GetOptionName(mapType.ValueType)}_None(), {TypeToString(mapType)})", + NamedTupleType ntt => + $"const_record({string.Join(", ", ntt.Fields.Select(f => $"{f.Name} := {DefaultValue(f.Type)}"))})", + PermissionType _ => DefaultMachineRef, + PrimitiveType pt when pt.Equals(PrimitiveType.Bool) => "false", + PrimitiveType pt when pt.Equals(PrimitiveType.Int) => "0", + PrimitiveType pt when pt.Equals(PrimitiveType.String) => DefaultString, + PrimitiveType pt when pt.Equals(PrimitiveType.Machine) => DefaultMachineRef, + SetType setType => $"const(false, {TypeToString(setType)})", + TypeDefType tdType => DefaultValue(tdType.TypeDefDecl.Type), + _ => throw new NotSupportedException($"Not supported default: {ty} ({ty.OriginalRepresentation})"), + }; + } + + private void GenerateOptionTypes() + { + foreach (var ptype in _optionsToDeclare) + { + var opt = GetOptionName(ptype); + EmitLine($"datatype {opt} = "); + EmitLine($"\t| {opt}_Some ({opt}_Some_Value: {TypeToString(ptype)})"); + EmitLine($"\t| {opt}_None ();"); + } + } + + private void GenerateChooseProcedures() + { + foreach (var choosePt in _chooseToDeclare) + { + var proc = GetChooseName(choosePt); + EmitLine($"procedure [noinline] {proc}(inp: {TypeToString(choosePt)})"); + switch (choosePt) + { + case MapType mapType: + EmitLine($"\treturns (outp: {TypeToString(mapType.KeyType)})"); + EmitLine($"\tensures {OptionIsSome(mapType.ValueType, "inp[outp]")};"); + break; + case SetType setType: + EmitLine($"\treturns (outp: {TypeToString(setType.ElementType)})"); + EmitLine($"\tensures inp[outp];"); + break; + case PrimitiveType pt when pt.Equals(PrimitiveType.Int): + EmitLine($"\treturns (outp: {TypeToString(pt)})"); + EmitLine($"\tensures 0 <= outp && outp <= inp;"); + break; + default: + throw new NotSupportedException($"Not supported choose type: {choosePt} ({choosePt.OriginalRepresentation})"); + } + EmitLine("{"); + EmitLine("}\n"); + } + } + + private string OptionConstructSome(PLanguageType t, string value) + { + return $"{GetOptionName(t)}_Some({value})"; + } + + private string OptionConstructNone(PLanguageType t) + { + return $"{GetOptionName(t)}_None()"; + } + + private string OptionIsSome(PLanguageType t, string instance) + { + return $"is_{GetOptionName(t)}_Some({instance})"; + } + + private string OptionIsNone(PLanguageType t, string instance) + { + return $"is_{GetOptionName(t)}_None({instance})"; + } + + private string OptionSelectValue(PLanguageType t, string instance) + { + return $"{instance}.{GetOptionName(t)}_Some_Value"; + } + + private void GenerateCheckerVars() + { + foreach (var ptype in _setCheckersToDeclare) + { + var name = GetCheckerName(ptype); + EmitLine($"var {name}: {TypeToString(ptype)};"); + } + } + + // specMachine is null iff we are not generating a statement for a spec machine + private void GenerateStmt(IPStmt stmt, Machine specMachine) + { + switch (stmt) + { + case CompoundStmt cstmt: + foreach (var s in cstmt.Statements) GenerateStmt(s, specMachine); + return; + case AssignStmt { Value: FunCallExpr, Location: VariableAccessExpr} cstmt: + var call = cstmt.Value as FunCallExpr; + var avax = cstmt.Location as VariableAccessExpr; + if (call == null) return; + var v = ExprToString(avax); + var f = call.Function.Name; + var fargs = call.Arguments.Select(ExprToString); + if (call.Function.Owner is not null) + { + fargs = fargs.Prepend("this"); + } + EmitLine($"call ({v}) = {f}({string.Join(", ", fargs)});"); + return; + case AssignStmt {Value: ChooseExpr, Location: VariableAccessExpr} cstmt: + var chooseExpr = (ChooseExpr)cstmt.Value; + _chooseToDeclare.Add(chooseExpr.SubExpr.Type); + var cvax = (VariableAccessExpr)cstmt.Location; + var cv = ExprToString(cvax); + var cf = GetChooseName(chooseExpr.SubExpr.Type); + var arg = ExprToString(chooseExpr.SubExpr); + EmitLine($"call ({cv}) = {cf}({arg});"); + return; + case AssignStmt astmt: + switch (astmt.Location) + { + case VariableAccessExpr vax: + EmitLine($"{ExprToString(vax)} = {ExprToString(astmt.Value)};"); + return; + case MapAccessExpr {MapExpr: VariableAccessExpr} max: + var map = ExprToString(max.MapExpr); + var index = ExprToString(max.IndexExpr); + var t = ((MapType)max.MapExpr.Type).ValueType; + EmitLine($"{map} = {map}[{index} -> {OptionConstructSome(t, ExprToString(astmt.Value))}];"); + return; + case NamedTupleAccessExpr { SubExpr: VariableAccessExpr } tax: + var subExpr = ExprToString(tax.SubExpr); + var entry = tax.Entry.Name; + var field = tax.FieldName; + var fields = ((NamedTupleType)((TypeDefType)tax.SubExpr.Type).TypeDefDecl.Type).Fields; + var rhs = ExprToString(astmt.Value); + var build = string.Join(", ", + fields.Select( + f => f.Name == entry ? $"{entry} := {rhs}" : $"{f.Name} := {subExpr}.{f.Name}")); + EmitLine($"{subExpr} = const_record({build});"); + return; + } + + throw new NotSupportedException( + $"Not supported assignment expression: {astmt.Location} = {astmt.Value} ({GetLocation(astmt)})"); + case IfStmt ifstmt: + var cond = (ifstmt.Condition) switch + { + NondetExpr => "*", + _ => ExprToString(ifstmt.Condition), + }; + EmitLine($"if ({cond}) {{"); + GenerateStmt(ifstmt.ThenBranch, specMachine); + EmitLine("} else {"); + GenerateStmt(ifstmt.ElseBranch, specMachine); + EmitLine("}"); + return; + case AssertStmt astmt: + EmitLine($"// {((StringExpr)astmt.Message).BaseString}"); + EmitLine($"assert({ExprToString(astmt.Assertion)}); // Failed to verify assertion at {GetLocation(astmt)}"); + return; + case AssumeStmt astmt: + EmitLine($"// {((StringExpr)astmt.Message).BaseString}"); + EmitLine($"assume({ExprToString(astmt.Assumption)});"); + return; + case PrintStmt { Message: StringExpr } pstmt: + EmitLine($"// {((StringExpr)pstmt.Message).BaseString}"); + return; + case FunCallStmt fapp: + EmitLine( + $"call {fapp.Function.Name}({string.Join(", ", fapp.ArgsList.Select(ExprToString).Prepend("this"))});"); + return; + case AddStmt {Variable: VariableAccessExpr} astmt: + // v += (y) + var aset = ExprToString(astmt.Variable); + var akey = ExprToString(astmt.Value); + EmitLine($"{aset} = {aset}[{akey} -> true];"); + return; + case AddStmt {Variable: MapAccessExpr} astmt when ((MapAccessExpr)astmt.Variable).MapExpr is VariableAccessExpr: + // m[x] += (y) + // m = m[x -> some((m[x].some)[y -> true])] + var mapInP = ((MapAccessExpr)astmt.Variable); + var mapTypeInP = (MapType) mapInP.MapExpr.Type; + var mapM = ExprToString(mapInP.MapExpr); + var locX = ExprToString(mapInP.IndexExpr); + var valY = ExprToString(astmt.Value); + var someMx = OptionSelectValue(mapTypeInP.ValueType, $"{mapM}[{locX}]"); + var someUpdated = OptionConstructSome(mapTypeInP.ValueType, $"{someMx}[{valY} -> true]"); + EmitLine($"{mapM} = {mapM}[{locX} -> {someUpdated}];"); + return; + case RemoveStmt {Variable: VariableAccessExpr} rstmt: + var rset = ExprToString(rstmt.Variable); + var rkey = ExprToString(rstmt.Value); + + switch (rstmt.Variable.Type) + { + case MapType mapType: + EmitLine($"{rset} = {rset}[{rkey} -> {OptionConstructNone(mapType.ValueType)}];"); + return; + case SetType _: + EmitLine($"{rset} = {rset}[{rkey} -> false];"); + return; + default: + throw new NotSupportedException( + $"Only support remove statements for sets and maps, got {rstmt.Variable.Type}"); + } + case InsertStmt {Variable: VariableAccessExpr} istmt: + var imap = ExprToString(istmt.Variable); + var idx = ExprToString(istmt.Index); + var value = OptionConstructSome(istmt.Value.Type, ExprToString(istmt.Value)); + EmitLine($"{imap} = {imap}[{idx} -> {value}];"); + return; + case ForeachStmt fstmt: + + switch (fstmt.IterCollection) + { + case KeysExpr keysExpr: + fstmt = new ForeachStmt(fstmt.SourceLocation, fstmt.Item, keysExpr.Expr, fstmt.Body, fstmt.Invariants); + break; + } + + var item = GetLocalName(fstmt.Item); + var checker = GetCheckerName(fstmt.IterCollection.Type); + var collection = ExprToString(fstmt.IterCollection); + + switch (fstmt.IterCollection.Type) + { + case SetType setType: + // set the checker to default + EmitLine($"{checker} = {DefaultValue(setType)};"); + // remember to declare it later + _setCheckersToDeclare.Add(setType); + // havoc the item + EmitLine($"havoc {item};"); + EmitLine($"while ({checker} != {collection})"); + foreach (var inv in _globalScope.AllDecls.OfType()) + { + EmitLine($"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name} at {GetLocation(fstmt)}"); + } + EmitLine($"\tinvariant {InvariantPrefix}Unique_Actions();"); + EmitLine($"\tinvariant {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\tinvariant {InvariantPrefix}Received_Subset_Sent();"); + // ensure uniqueness for the new ones too + EmitLine($"\tinvariant forall (a1: {LabelAdt}, a2: {LabelAdt}) :: (a1 != a2 && {LocalPrefix}sent[a1] && {LocalPrefix}sent[a2]) ==> {LabelAdtSelectActionCount("a1")} != {LabelAdtSelectActionCount("a2")};"); + EmitLine($"\tinvariant forall (a: {LabelAdt}) :: {LocalPrefix}sent[a] ==> {LabelAdtSelectActionCount("a")} < {BuiltinPrefix}ActionCount;"); + + // ensure we only ever add sends + EmitLine($"\tinvariant forall (e: {LabelAdt}) :: {StateAdtSelectSent(StateVar)}[e] ==> {LocalPrefix}sent[e];"); + + // user given invariants + foreach (var inv in fstmt.Invariants) + { + EmitLine($"\tinvariant {ExprToString(inv)}; // Failed to verify loop invariant at {GetLocation(inv)}"); + } + + EmitLine("{"); + // assume that the item is in the set but hasn't been visited + EmitLine($"if ({collection}[{item}] && !{checker}[{item}]) {{"); + // the body of the loop + GenerateStmt(fstmt.Body, specMachine); + // update the checker + EmitLine($"{checker} = {checker}[{item} -> true];"); + EmitLine("}"); + // havoc the item + EmitLine($"havoc {item};"); + EmitLine("}"); + return; + case MapType mapType: + // set the checker to default + EmitLine($"{checker} = {DefaultValue(mapType)};"); + // remember to declare it later + _setCheckersToDeclare.Add(mapType); + // havoc the item, in this case it is a key + EmitLine($"havoc {item};"); + EmitLine($"while ({checker} != {collection})"); + foreach (var inv in _globalScope.AllDecls.OfType()) + { + EmitLine($"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name} at {GetLocation(fstmt)}"); + } + EmitLine($"\tinvariant {InvariantPrefix}Unique_Actions();"); + EmitLine($"\tinvariant {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\tinvariant {InvariantPrefix}Received_Subset_Sent();"); + // ensure uniqueness for the new ones too + EmitLine($"\tinvariant forall (a1: {LabelAdt}, a2: {LabelAdt}) :: (a1 != a2 && {LocalPrefix}sent[a1] && {LocalPrefix}sent[a2]) ==> {LabelAdtSelectActionCount("a1")} != {LabelAdtSelectActionCount("a2")};"); + EmitLine($"\tinvariant forall (a: {LabelAdt}) :: {LocalPrefix}sent[a] ==> {LabelAdtSelectActionCount("a")} < {BuiltinPrefix}ActionCount;"); + + // ensure we only ever add sends + EmitLine($"\tinvariant forall (e: {LabelAdt}) :: {StateAdtSelectSent(StateVar)}[e] ==> {LocalPrefix}sent[e];"); + + // user given invariants + foreach (var inv in fstmt.Invariants) + { + EmitLine($"\tinvariant {ExprToString(inv)}; // Failed to verify loop invariant at {GetLocation(inv)}"); + } + + EmitLine("{"); + // assume that the item is in the set but hasn't been visited + EmitLine($"if ({OptionIsSome(mapType.ValueType, $"{collection}[{item}]")} && {OptionIsNone(mapType.ValueType, $"{checker}[{item}]")}) {{"); + // the body of the loop + GenerateStmt(fstmt.Body, specMachine); + // update the checker + EmitLine($"{checker} = {checker}[{item} -> {collection}[{item}]];"); + EmitLine("}"); + // havoc the item + EmitLine($"havoc {item};"); + EmitLine("}"); + return; + default: + throw new NotSupportedException( + $"Foreach over non-sets is not supported yet: {fstmt} ({GetLocation(fstmt)}"); + } + case GotoStmt gstmt when specMachine is null: + var gaction = EventOrGotoAdtConstructGoto(gstmt.State, gstmt.Payload); + var glabel = LabelAdtConstruct("this", gaction); + var glabels = StateAdtSelectSent(StateVar); + var newState = $"{MachinePrefix}{gstmt.State.OwningMachine.Name}_{gstmt.State.Name}"; + EmitLine($"{glabels} = {glabels}[{glabel} -> true];"); + IncrementActionCount(); + EmitLine($"{LocalPrefix}state = {newState};"); + EmitLine($"{LocalPrefix}stage = true;"); + return; + case GotoStmt gstmts: // when specMachine is not null + EmitLine($"{LocalPrefix}state = {SpecPrefix}{specMachine.Name}_{gstmts.State.Name};"); + EmitLine($"{LocalPrefix}stage = true;"); + return; + case SendStmt sstmt when specMachine is null: + if (sstmt.Arguments.Count > 1) + { + throw new NotSupportedException("We only support at most one argument to a send"); + } + + var ev = ((EventRefExpr)sstmt.Evt).Value; + var saction = EventOrGotoAdtConstructEvent(ev, sstmt.Arguments.Any() ? sstmt.Arguments.First() : null); + var slabel = LabelAdtConstruct(ExprToString(sstmt.MachineExpr), saction); + var slabels = $"{LocalPrefix}sent"; + EmitLine($"{slabels} = {slabels}[{slabel} -> true];"); + IncrementActionCount(); + foreach (var procedureName in _specListenMap.GetValueOrDefault(ev, [])) + { + var argument = sstmt.Arguments.Count > 0 ? $"{ExprToString(sstmt.Arguments[0])}" : PNull; + EmitLine($"call {procedureName}({argument});"); + } + + return; + case ReturnStmt rstmt: + EmitLine($"{BuiltinPrefix}Return = {ExprToString(rstmt.ReturnValue)};"); + return; + case null: + return; + } + + throw new NotSupportedException($"Not supported statement: {stmt} ({GetLocation(stmt)})"); + } + + private string ExprToString(IPExpr expr) + { + return expr switch + { + NamedTupleAccessExpr ntax => $"{ExprToString(ntax.SubExpr)}.{ntax.FieldName}", + VariableAccessExpr vax => GetLocalName(vax.Variable), + IntLiteralExpr i => i.Value.ToString(), + BoolLiteralExpr b => b.Value.ToString().ToLower(), + BinOpExpr bexpr => + $"({ExprToString(bexpr.Lhs)} {BinOpToString(bexpr.Operation)} {ExprToString(bexpr.Rhs)})", + UnaryOpExpr uexpr => $"({UnaryOpToString(uexpr.Operation)} {ExprToString(uexpr.SubExpr)})", + ThisRefExpr => "this", + EnumElemRefExpr e => $"{UserPrefix}{e.Value.Name}", + NamedTupleExpr t => NamedTupleExprHelper(t), + StringExpr s => + $"\"{s.BaseString}\" {(s.Args.Count != 0 ? "%" : "")} {string.Join(", ", s.Args.Select(ExprToString))}", + MapAccessExpr maex => + OptionSelectValue(((MapType)maex.MapExpr.Type).ValueType, + $"{ExprToString(maex.MapExpr)}[{ExprToString(maex.IndexExpr)}]"), + ContainsExpr cexp when cexp.Collection.Type.Canonicalize() is MapType => OptionIsSome(((MapType) cexp.Collection.Type).ValueType, $"{ExprToString(cexp.Collection)}[{ExprToString(cexp.Item)}]"), + ContainsExpr cexp when cexp.Collection.Type.Canonicalize() is SetType => $"{ExprToString(cexp.Collection)}[{ExprToString(cexp.Item)}]", + DefaultExpr dexp => DefaultValue(dexp.Type), + QuantExpr {Quant: QuantType.Forall} qexpr => $"(forall ({BoundVars(qexpr.Bound)}) :: {Guard(qexpr.Bound, qexpr.Difference, true)}({ExprToString(qexpr.Body)}))", + QuantExpr {Quant: QuantType.Exists} qexpr => $"(exists ({BoundVars(qexpr.Bound)}) :: {Guard(qexpr.Bound, qexpr.Difference, false)}({ExprToString(qexpr.Body)}))", + MachineAccessExpr max => MachineStateAdtSelectField(Deref(ExprToString(max.SubExpr)), max.Machine, max.Entry), + SpecAccessExpr sax => $"{SpecPrefix}{sax.Spec.Name}_{sax.FieldName}", + EventAccessExpr eax => LabelAdtSelectPayloadField(ExprToString(eax.SubExpr), eax.PEvent, eax.Entry), + TestExpr {Kind: Machine m} texpr => MachineStateAdtIsM(Deref(ExprToString(texpr.Instance)), m), // must deref because or else we don't have an ADT! + TestExpr {Kind: PEvent e} texpr => LabelAdtIsE(ExprToString(texpr.Instance), e), + TestExpr {Kind: State s} texpr => MachineStateAdtInS(Deref(ExprToString(texpr.Instance)), s.OwningMachine, s), // must deref for ADT! + PureCallExpr pexpr => $"{pexpr.Pure.Name}({string.Join(", ", pexpr.Arguments.Select(ExprToString))})", + FlyingExpr fexpr => $"{InFlight(StateVar, ExprToString(fexpr.Instance))}", + SentExpr sexpr => $"{StateAdtSelectSent(StateVar)}[{ExprToString(sexpr.Instance)}]", + TargetsExpr texpr => $"({LabelAdtSelectTarget(ExprToString(texpr.Instance))} == {ExprToString(texpr.Target)})", + _ => throw new NotSupportedException($"Not supported expr ({expr}) at {GetLocation(expr)}") + // _ => $"NotHandledExpr({expr})" + }; + + string BoundVars(List bound) + { + return $"{string.Join(", ", bound.Select(b => $"{LocalPrefix}{b.Name}: {TypeToString(b.Type)}"))}"; + } + + string Guard(List bound, bool difference, bool universal) + { + var impliesOrAnd = universal ? "==>" : "&&"; + + List bounds = []; + foreach (var b in bound) + { + switch (b.Type) + { + case PermissionType {Origin: Machine} pt: + bounds.Add(ExprToString(new TestExpr(b.SourceLocation, new VariableAccessExpr(b.SourceLocation, b), pt.Origin))); + break; + case PermissionType {Origin: Interface} pt: + var name = pt.OriginalRepresentation; + + if (_globalScope.Lookup(name, out Machine m)) + { + bounds.Add(ExprToString(new TestExpr(b.SourceLocation, new VariableAccessExpr(b.SourceLocation, b), m))); + } + + break; + case PermissionType {Origin: NamedEventSet} pt: + var e = ((NamedEventSet)pt.Origin).Events.First(); + bounds.Add(ExprToString(new TestExpr(b.SourceLocation, new VariableAccessExpr(b.SourceLocation, b), e))); + if (difference) + { + bounds.Add($"{LocalPrefix}sent[{LocalPrefix}{b.Name}]"); + bounds.Add($"!{StateAdtSelectSent(StateVar)}[{LocalPrefix}{b.Name}]"); + } + break; + case PrimitiveType pt when pt.IsSameTypeAs(PrimitiveType.Event): + if (difference) + { + bounds.Add($"{LocalPrefix}sent[{LocalPrefix}{b.Name}]"); + bounds.Add($"!{StateAdtSelectSent(StateVar)}[{LocalPrefix}{b.Name}]"); + } + break; + } + } + + if (bounds.Count != 0) + { + return "(" + string.Join(" && ", bounds) + $") {impliesOrAnd} "; + } + + return ""; + } + } + + private string NamedTupleExprHelper(NamedTupleExpr t) + { + var ty = (NamedTupleType)t.Type; + var names = ty.Fields.Select(f => f.Name); + var values = t.TupleFields.Select(ExprToString); + var args = string.Join(", ", names.Zip(values).Select(p => $"{p.First} := {p.Second}")); + return $"const_record({args})"; + } + + private static string BinOpToString(BinOpType op) + { + return op switch + { + BinOpType.Add => "+", + BinOpType.Sub => "-", + BinOpType.Mul => "*", + BinOpType.Div => "/", + BinOpType.Mod => "%", + BinOpType.Lt => "<", + BinOpType.Le => "<=", + BinOpType.Gt => ">", + BinOpType.Ge => ">=", + BinOpType.And => "&&", + BinOpType.Or => "||", + BinOpType.Eq => "==", + BinOpType.Neq => "!=", + BinOpType.Then => "==>", + _ => throw new NotImplementedException($"{op} is not implemented yet!") + }; + } + + private static string UnaryOpToString(UnaryOpType op) + { + return op switch + { + UnaryOpType.Negate => "-", + UnaryOpType.Not => "!", + _ => throw new NotImplementedException($"{op} is not implemented yet!") + }; + } + + private string TypeToString(PLanguageType t) + { + switch (t.Canonicalize()) + { + case NamedTupleType ntt: + var fields = string.Join(", ", + ntt.Fields.Select(nte => $"{nte.Name}: {TypeToString(nte.Type)}")); + return $"record {{{fields}}}"; + case PrimitiveType pt when pt.Equals(PrimitiveType.Bool): + return "boolean"; + case PrimitiveType pt when pt.Equals(PrimitiveType.Int): + return "integer"; + case PrimitiveType pt when pt.Equals(PrimitiveType.String): + return StringT; + case PrimitiveType pt when pt.Equals(PrimitiveType.Null): + return PNull; + case PrimitiveType pt when pt.Equals(PrimitiveType.Machine): + return MachineRefT; + case PrimitiveType pt when pt.Equals(PrimitiveType.Event): + return LabelAdt; + case TypeDefType tdt: + return $"{UserPrefix}{tdt.TypeDefDecl.Name}"; + case PermissionType {Origin: Machine} _: + return MachineRefT; + case PermissionType {Origin: Interface} _: + return MachineRefT; + case PermissionType {Origin: NamedEventSet} _: + return LabelAdt; + case EnumType et: + return $"{UserPrefix}{et.EnumDecl.Name}"; + case SetType st: + return $"[{TypeToString(st.ElementType)}]boolean"; + case MapType mt: + _optionsToDeclare.Add(mt.ValueType.Canonicalize()); + return $"[{TypeToString(mt.KeyType)}]{GetOptionName(mt.ValueType)}"; + } + + throw new NotSupportedException($"Not supported type expression {t} ({t.OriginalRepresentation})"); + } + + private string GetLocalName(Variable v) + { + return $"{LocalPrefix}{v.Name}"; + } + + + private string GetCheckerName(PLanguageType t) + { + var output = $"{CheckerPrefix}{TypeToString(t)}"; + return Regex.Replace(output, "[^a-zA-Z0-9_.]+", "", RegexOptions.Compiled); + } + + private string GetOptionName(PLanguageType t) + { + var output = $"{OptionPrefix}{TypeToString(t)}"; + return Regex.Replace(output, "[^a-zA-Z0-9_.]+", "", RegexOptions.Compiled); + } + + + private string GetChooseName(PLanguageType t) + { + var output = $"{ChoosePrefix}{TypeToString(t)}"; + return Regex.Replace(output, "[^a-zA-Z0-9_.]+", "", RegexOptions.Compiled); + } + + private string GetLocation(IPAST node) + { + return _ctx.LocationResolver.GetLocation(node.SourceLocation).ToString(); + } +} diff --git a/Src/PCompiler/CompilerCore/Compiler.cs b/Src/PCompiler/CompilerCore/Compiler.cs index 99e94c02b..cf5dc740e 100644 --- a/Src/PCompiler/CompilerCore/Compiler.cs +++ b/Src/PCompiler/CompilerCore/Compiler.cs @@ -47,12 +47,23 @@ public int Compile(ICompilerConfiguration job) return Environment.ExitCode; } - // Convert functions to lowered SSA form with explicit cloning - foreach (var fun in scope.GetAllMethods()) + if (job.OutputLanguages.Contains(CompilerOutput.Uclid5)) { - IRTransformer.SimplifyMethod(fun); + // If outputing UCLID5, don't output anything else + if (job.OutputLanguages.Count > 1) + { + throw new NotSupportedException("UCLID5 backend must be used on its own!"); + } } - + else + { + // Convert functions to lowered SSA form with explicit cloning + foreach (var fun in scope.GetAllMethods()) + { + IRTransformer.SimplifyMethod(fun); + } + } + DirectoryInfo parentDirectory = job.OutputDirectory; foreach (var entry in job.OutputLanguages.Distinct()) { diff --git a/Src/PCompiler/CompilerCore/CompilerConfiguration.cs b/Src/PCompiler/CompilerCore/CompilerConfiguration.cs index 7c6c4db1a..a1a0503cc 100644 --- a/Src/PCompiler/CompilerCore/CompilerConfiguration.cs +++ b/Src/PCompiler/CompilerCore/CompilerConfiguration.cs @@ -24,6 +24,9 @@ public CompilerConfiguration() Backend = null; ProjectDependencies = new List(); Debug = false; + Timeout = 60; + HandlesAll = true; + CheckOnly = null; } public CompilerConfiguration(ICompilerOutput output, DirectoryInfo outputDir, IList outputLanguages, IList inputFiles, string projectName, DirectoryInfo projectRoot = null, IList projectDependencies = null, string pObservePackageName = null, bool debug = false) @@ -73,6 +76,9 @@ public CompilerConfiguration(ICompilerOutput output, DirectoryInfo outputDir, IL public IList ProjectDependencies { get; set; } public bool Debug { get; set; } + public int Timeout { get; set; } + public bool HandlesAll { get; set; } + public string CheckOnly { get; set; } public void Copy(CompilerConfiguration parsedConfig) { diff --git a/Src/PCompiler/CompilerCore/CompilerCore.csproj b/Src/PCompiler/CompilerCore/CompilerCore.csproj index c3cf7ad18..3bd716aff 100644 --- a/Src/PCompiler/CompilerCore/CompilerCore.csproj +++ b/Src/PCompiler/CompilerCore/CompilerCore.csproj @@ -9,6 +9,7 @@ + diff --git a/Src/PCompiler/CompilerCore/CompilerOutput.cs b/Src/PCompiler/CompilerCore/CompilerOutput.cs index caada3e59..ce2bff2d3 100644 --- a/Src/PCompiler/CompilerCore/CompilerOutput.cs +++ b/Src/PCompiler/CompilerCore/CompilerOutput.cs @@ -6,6 +6,7 @@ public enum CompilerOutput Symbolic, CSharp, Java, - Stately + Stately, + Uclid5, } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs index cd2466484..8308c1c01 100644 --- a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs +++ b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs @@ -117,6 +117,17 @@ public Exception MissingNamedTupleEntry(PParser.IdenContext location, $"named tuple type {namedTuple.OriginalRepresentation} has no '{location.GetText()}' field"); } + public Exception MissingMachineField(PParser.IdenContext location, Machine machine) + { + return IssueError(location, + $"machine {machine.Name} has no '{location.GetText()}' field"); + } + public Exception MissingEventField(PParser.IdenContext location, PEvent pevent) + { + return IssueError(location, + $"machine {pevent.Name} payload has no '{location.GetText()}' field"); + } + public Exception OutOfBoundsTupleAccess(PParser.IntContext location, TupleType tuple) { return IssueError( diff --git a/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs b/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs index 1aa20f9dc..c82285453 100644 --- a/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs +++ b/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs @@ -20,5 +20,8 @@ public interface ICompilerConfiguration ILocationResolver LocationResolver { get; } ITranslationErrorHandler Handler { get; } bool Debug { get; } + int Timeout { get; } + bool HandlesAll { get; } + string CheckOnly { get; } } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs index 371885fe8..71d923e6f 100644 --- a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs +++ b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs @@ -37,6 +37,8 @@ Exception DuplicateStartState( Exception TypeMismatch(IPExpr expr, params TypeKind[] expected); Exception MissingNamedTupleEntry(PParser.IdenContext location, NamedTupleType namedTuple); + Exception MissingMachineField(PParser.IdenContext location, Machine machine); + Exception MissingEventField(PParser.IdenContext location, PEvent pevent); Exception OutOfBoundsTupleAccess(PParser.IntContext location, TupleType tuple); diff --git a/Src/PCompiler/CompilerCore/Parser/PLexer.g4 b/Src/PCompiler/CompilerCore/Parser/PLexer.g4 index 8f7511ac8..8f9e8af85 100644 --- a/Src/PCompiler/CompilerCore/Parser/PLexer.g4 +++ b/Src/PCompiler/CompilerCore/Parser/PLexer.g4 @@ -36,6 +36,7 @@ EXIT : 'exit' ; FOREACH : 'foreach'; FORMAT : 'format' ; FUN : 'fun' ; +PURE : 'pure' ; GOTO : 'goto' ; HALT : 'halt' ; HOT : 'hot' ; @@ -63,6 +64,13 @@ WHILE : 'while' ; WITH : 'with' ; CHOOSE : 'choose' ; +INVARIANT : 'invariant'; +AXIOM : 'axiom'; +IS : 'is'; +FLYING : 'inflight'; +TARGETS : 'targets'; +SENT : 'sent'; + // module-system-specific keywords // module-test-implementation declarations @@ -109,6 +117,7 @@ NONDET : '$' ; LNOT : '!' ; LAND : '&&' ; LOR : '||' ; +LTHEN : '==>'; EQ : '==' ; NE : '!=' ; @@ -139,6 +148,10 @@ COMMA : ',' ; DOT : '.' ; COLON : ':' ; +FORALL : 'forall' ; +EXISTS : 'exists' ; +INIT : 'init'; + // Identifiers Iden : PLetter PLetterOrDigit* ; diff --git a/Src/PCompiler/CompilerCore/Parser/PParser.g4 b/Src/PCompiler/CompilerCore/Parser/PParser.g4 index dc00fca47..24bcf8e74 100644 --- a/Src/PCompiler/CompilerCore/Parser/PParser.g4 +++ b/Src/PCompiler/CompilerCore/Parser/PParser.g4 @@ -57,9 +57,13 @@ topDecl : typeDefDecl | implMachineDecl | specMachineDecl | funDecl + | pureDecl | namedModuleDecl | testDecl | implementationDecl + | invariantDecl + | axiomDecl + | assumeOnStartDecl ; @@ -106,6 +110,13 @@ varDecl : VAR idenList COLON type SEMI ; funDecl : FUN name=iden LPAREN funParamList? RPAREN (COLON type)? (CREATES interfaces+=iden)? SEMI # ForeignFunDecl | FUN name=iden LPAREN funParamList? RPAREN (COLON type)? functionBody # PFunDecl ; + +pureDecl : PURE name=iden LPAREN funParamList? RPAREN COLON type (ASSIGN body=expr)? SEMI ; + +invariantDecl: INVARIANT name=iden COLON body=expr SEMI ; +axiomDecl: AXIOM body=expr SEMI ; + +assumeOnStartDecl: INIT body=expr SEMI ; stateDecl : START? temperature=(HOT | COLD)? STATE name=iden LBRACE stateBodyItem* RBRACE ; @@ -133,6 +144,7 @@ stateName : state=iden ; functionBody : LBRACE varDecl* statement* RBRACE ; statement : LBRACE statement* RBRACE # CompoundStmt | ASSERT assertion=expr (COMMA message=expr)? SEMI # AssertStmt + | ASSUME assumption=expr (COMMA message=expr)? SEMI # AssumeStmt | PRINT message=expr SEMI # PrintStmt | RETURN expr? SEMI # ReturnStmt | BREAK SEMI # BreakStmt @@ -142,8 +154,9 @@ statement : LBRACE statement* RBRACE # CompoundStmt | lvalue INSERT LPAREN rvalue RPAREN SEMI # AddStmt | lvalue REMOVE expr SEMI # RemoveStmt | WHILE LPAREN expr RPAREN statement # WhileStmt - | FOREACH LPAREN item=iden IN collection=expr - RPAREN statement # ForeachStmt + | FOREACH LPAREN item=iden IN collection=expr RPAREN + (INVARIANT invariants+=expr SEMI)* + statement # ForeachStmt | IF LPAREN expr RPAREN thenBranch=statement (ELSE elseBranch=statement)? # IfStmt | NEW iden LPAREN rvalueList? RPAREN SEMI # CtorStmt @@ -173,6 +186,10 @@ expr : primitive # PrimitiveExpr | LPAREN expr RPAREN # ParenExpr | expr DOT field=iden # NamedTupleAccessExpr | expr DOT field=int # TupleAccessExpr + | instance=expr IS kind=iden # TestExpr + | instance=expr TARGETS target=expr # TargetsExpr + | FLYING instance=expr # FlyingExpr + | SENT instance=expr # SentExpr | seq=expr LBRACK index=expr RBRACK # SeqAccessExpr | fun=KEYS LPAREN expr RPAREN # KeywordExpr | fun=VALUES LPAREN expr RPAREN # KeywordExpr @@ -189,6 +206,11 @@ expr : primitive # PrimitiveExpr | lhs=expr op=(EQ | NE) rhs=expr # BinExpr | lhs=expr op=LAND rhs=expr # BinExpr | lhs=expr op=LOR rhs=expr # BinExpr + | lhs=expr op=LTHEN rhs=expr # BinExpr + | quant=(FORALL | EXISTS) + diff=NEW? + LPAREN bound=funParamList RPAREN + COLON COLON body=expr # QuantExpr | CHOOSE LPAREN expr? RPAREN # ChooseExpr | formatedString # StringExpr ; diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/AssumeOnStart.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/AssumeOnStart.cs new file mode 100644 index 000000000..7d8cc0f53 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/AssumeOnStart.cs @@ -0,0 +1,24 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Expressions; + +namespace Plang.Compiler.TypeChecker.AST.Declarations +{ + public class AssumeOnStart : IPDecl + { + public AssumeOnStart(string name, IPExpr body, ParserRuleContext sourceNode) + { + Debug.Assert(sourceNode is PParser.AssumeOnStartDeclContext); + Body = body; + Name = name; + SourceLocation = sourceNode; + } + + public IPExpr Body { get; set; } + + public string Name { get; set; } + public ParserRuleContext SourceLocation { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Axiom.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Axiom.cs new file mode 100644 index 000000000..a646cc76f --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Axiom.cs @@ -0,0 +1,24 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Expressions; + +namespace Plang.Compiler.TypeChecker.AST.Declarations +{ + public class Axiom : IPDecl + { + public Axiom(string name, IPExpr body, ParserRuleContext sourceNode) + { + Debug.Assert(sourceNode is PParser.AxiomDeclContext); + Name = name; + Body = body; + SourceLocation = sourceNode; + } + + public IPExpr Body { get; set; } + + public string Name { get; set; } + public ParserRuleContext SourceLocation { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Invariant.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Invariant.cs new file mode 100644 index 000000000..a712c30b2 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Invariant.cs @@ -0,0 +1,24 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Expressions; + +namespace Plang.Compiler.TypeChecker.AST.Declarations +{ + public class Invariant : IPDecl + { + public Invariant(string name, IPExpr body, ParserRuleContext sourceNode) + { + Debug.Assert(sourceNode is PParser.InvariantDeclContext); + Name = name; + Body = body; + SourceLocation = sourceNode; + } + + public IPExpr Body { get; set; } + + public string Name { get; set; } + public ParserRuleContext SourceLocation { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs index 58af64ec1..b56f937a4 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs @@ -1,3 +1,4 @@ +using System; using System.Collections.Generic; using System.Diagnostics; using System.Linq; @@ -83,5 +84,11 @@ public void AddFields(IEnumerable variables) { fields.AddRange(variables); } + + public bool LookupEntry(string name, out Variable entry) + { + var lookupTable = fields.ToDictionary(f => f.Name, f => f); + return lookupTable.TryGetValue(name, out entry); + } } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Pure.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Pure.cs new file mode 100644 index 000000000..acb93fdf7 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Pure.cs @@ -0,0 +1,27 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Statements; + +namespace Plang.Compiler.TypeChecker.AST.Declarations +{ + public class Pure : IPDecl, IHasScope + { + + public Pure(string name, ParserRuleContext sourceNode) + { + Debug.Assert(sourceNode is PParser.PureDeclContext); + Name = name; + SourceLocation = sourceNode; + } + + public FunctionSignature Signature { get; } = new FunctionSignature(); + + public string Name { get; set; } + public IPExpr Body { get; set; } + public ParserRuleContext SourceLocation { get; } + + public Scope Scope { get; set; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/BinOpType.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/BinOpType.cs index 30b3adc2b..bbe3f4525 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/BinOpType.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/BinOpType.cs @@ -16,7 +16,8 @@ public enum BinOpType Gt, Ge, And, - Or + Or, + Then } public enum BinOpKind diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/EventAccessExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/EventAccessExpr.cs new file mode 100644 index 000000000..ee471d269 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/EventAccessExpr.cs @@ -0,0 +1,25 @@ +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class EventAccessExpr : IPExpr + { + public EventAccessExpr(ParserRuleContext sourceLocation, PEvent pevent, IPExpr subExpr, NamedTupleEntry entry) + { + SourceLocation = sourceLocation; + PEvent = pevent; + SubExpr = subExpr; + Entry = entry; + } + + public PEvent PEvent { get; } + public IPExpr SubExpr { get; } + public NamedTupleEntry Entry { get; } + public string FieldName => Entry.Name; + + public ParserRuleContext SourceLocation { get; } + public PLanguageType Type => Entry.Type; + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/FlyingExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/FlyingExpr.cs new file mode 100644 index 000000000..2f24f3bb8 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/FlyingExpr.cs @@ -0,0 +1,23 @@ +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class FlyingExpr : IPExpr + { + public FlyingExpr(ParserRuleContext sourceLocation, IPExpr instance) + { + SourceLocation = sourceLocation; + Instance = instance; + Type = PrimitiveType.Bool; + } + + public IPExpr Instance { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/MachineAccessExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/MachineAccessExpr.cs new file mode 100644 index 000000000..e97d1c8d7 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/MachineAccessExpr.cs @@ -0,0 +1,25 @@ +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class MachineAccessExpr : IPExpr + { + public MachineAccessExpr(ParserRuleContext sourceLocation, Machine machine, IPExpr subExpr, Variable entry) + { + SourceLocation = sourceLocation; + Machine = machine; + SubExpr = subExpr; + Entry = entry; + } + + public Machine Machine { get; } + public IPExpr SubExpr { get; } + public Variable Entry { get; } + public string FieldName => Entry.Name; + + public ParserRuleContext SourceLocation { get; } + public PLanguageType Type => Entry.Type; + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/PureCallExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/PureCallExpr.cs new file mode 100644 index 000000000..9470331dc --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/PureCallExpr.cs @@ -0,0 +1,25 @@ +using System.Collections.Generic; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class PureCallExpr : IPExpr + { + public PureCallExpr(ParserRuleContext sourceLocation, Pure function, IReadOnlyList arguments) + { + SourceLocation = sourceLocation; + Pure = function; + Arguments = arguments; + Type = function.Signature.ReturnType; + } + + public Pure Pure { get; } + public IReadOnlyList Arguments { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantExpr.cs new file mode 100644 index 000000000..160e0adcc --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantExpr.cs @@ -0,0 +1,30 @@ +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class QuantExpr : IPExpr + { + public QuantExpr(ParserRuleContext sourceLocation, QuantType operation, List bound, IPExpr body, bool difference) + { + SourceLocation = sourceLocation; + Quant = operation; + Bound = bound; + Body = body; + Difference = difference; + Type = PrimitiveType.Bool; + } + + public QuantType Quant { get; } + public List Bound { get; } + public IPExpr Body { get; } + public bool Difference { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantType.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantType.cs new file mode 100644 index 000000000..3a00765fd --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantType.cs @@ -0,0 +1,10 @@ +using System; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public enum QuantType + { + Forall, + Exists, + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SentExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SentExpr.cs new file mode 100644 index 000000000..7b31d32d6 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SentExpr.cs @@ -0,0 +1,23 @@ +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class SentExpr : IPExpr + { + public SentExpr(ParserRuleContext sourceLocation, IPExpr instance) + { + SourceLocation = sourceLocation; + Instance = instance; + Type = PrimitiveType.Bool; + } + + public IPExpr Instance { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecAccessExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecAccessExpr.cs new file mode 100644 index 000000000..845b41665 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecAccessExpr.cs @@ -0,0 +1,25 @@ +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class SpecAccessExpr : IPExpr + { + public SpecAccessExpr(ParserRuleContext sourceLocation, Machine machine, IPExpr subExpr, Variable entry) + { + SourceLocation = sourceLocation; + Spec = machine; + SubExpr = subExpr; + Entry = entry; + } + + public Machine Spec { get; } + public IPExpr SubExpr { get; } + public Variable Entry { get; } + public string FieldName => Entry.Name; + + public ParserRuleContext SourceLocation { get; } + public PLanguageType Type => Entry.Type; + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecRefExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecRefExpr.cs new file mode 100644 index 000000000..e204d3ca5 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecRefExpr.cs @@ -0,0 +1,20 @@ +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class SpecRefExpr : IStaticTerm + { + public SpecRefExpr(ParserRuleContext sourceLocation, Machine value) + { + Value = value; + SourceLocation = sourceLocation; + } + + public Machine Value { get; } + + public PLanguageType Type { get; } = PrimitiveType.Machine; + public ParserRuleContext SourceLocation { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TargetsExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TargetsExpr.cs new file mode 100644 index 000000000..36a9ffcfb --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TargetsExpr.cs @@ -0,0 +1,25 @@ +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class TargetsExpr : IPExpr + { + public TargetsExpr(ParserRuleContext sourceLocation, IPExpr instance, IPExpr target) + { + SourceLocation = sourceLocation; + Instance = instance; + Target = target; + Type = PrimitiveType.Bool; + } + + public IPExpr Instance { get; } + public IPExpr Target { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TestExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TestExpr.cs new file mode 100644 index 000000000..edec8814b --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TestExpr.cs @@ -0,0 +1,25 @@ +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class TestExpr : IPExpr + { + public TestExpr(ParserRuleContext sourceLocation, IPExpr instance, IPDecl kind) + { + SourceLocation = sourceLocation; + Instance = instance; + Kind = kind; + Type = PrimitiveType.Bool; + } + + public IPExpr Instance { get; } + public IPDecl Kind { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/AssumeStmt.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/AssumeStmt.cs new file mode 100644 index 000000000..cd4b2dd94 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/AssumeStmt.cs @@ -0,0 +1,19 @@ +using Antlr4.Runtime; + +namespace Plang.Compiler.TypeChecker.AST.Statements +{ + public class AssumeStmt : IPStmt + { + public AssumeStmt(ParserRuleContext sourceLocation, IPExpr assumption, IPExpr message) + { + SourceLocation = sourceLocation; + Assumption = assumption; + Message = message; + } + + public IPExpr Assumption { get; } + public IPExpr Message { get; } + + public ParserRuleContext SourceLocation { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/ForeachStmt.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/ForeachStmt.cs index bcda223e7..3d318d206 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/ForeachStmt.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/ForeachStmt.cs @@ -1,3 +1,4 @@ +using System.Collections.Generic; using Antlr4.Runtime; using Plang.Compiler.TypeChecker.AST.Declarations; @@ -5,17 +6,19 @@ namespace Plang.Compiler.TypeChecker.AST.Statements { public class ForeachStmt : IPStmt { - public ForeachStmt(ParserRuleContext sourceLocation, Variable item, IPExpr collection, IPStmt body) + public ForeachStmt(ParserRuleContext sourceLocation, Variable item, IPExpr collection, IPStmt body, List invariants) { SourceLocation = sourceLocation; Item = item; IterCollection = collection; Body = CompoundStmt.FromStatement(body); + Invariants = invariants; } public Variable Item { get; } public IPExpr IterCollection { get; } public CompoundStmt Body { get; } + public List Invariants { get; } public ParserRuleContext SourceLocation { get; } } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs index 8277355fb..22c8335f0 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs @@ -16,8 +16,8 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config, // Step 1: Build the global scope of declarations var globalScope = BuildGlobalScope(config, programUnits); - - // Step 2: Validate machine specifications + + // Step 2a: Validate machine specifications foreach (var machine in globalScope.Machines) { MachineChecker.Validate(handler, machine, config); @@ -31,7 +31,7 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config, FunctionValidator.CheckAllPathsReturn(handler, machineFunction); } - // Step 2: Validate no static handlers + // Step 2b: Validate no static handlers foreach (var machine in globalScope.Machines) { MachineChecker.ValidateNoStaticHandlers(handler, machine); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ControlFlowChecker.cs b/Src/PCompiler/CompilerCore/TypeChecker/ControlFlowChecker.cs index ea0900293..75324dfbe 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ControlFlowChecker.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ControlFlowChecker.cs @@ -71,6 +71,7 @@ private void CheckStmt(IPStmt stmt) case AddStmt _: case AnnounceStmt _: case AssertStmt _: + case AssumeStmt _: case AssignStmt _: case CtorStmt _: case FunCallStmt _: diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs index 77782e730..21f43b23d 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs @@ -1,3 +1,4 @@ +using System.Linq; using Antlr4.Runtime.Misc; using Antlr4.Runtime.Tree; using Plang.Compiler.TypeChecker.AST; @@ -30,6 +31,38 @@ public static void PopulateStubs( visitor.Visit(context); } + public override object VisitInvariantDecl(PParser.InvariantDeclContext context) + { + var name = context.name.GetText(); + var decl = CurrentScope.Put(name, context); + nodesToDeclarations.Put(context, decl); + return null; + } + + public override object VisitAxiomDecl(PParser.AxiomDeclContext context) + { + var name = $"axiom{CurrentScope.Axioms.Count()}"; + var decl = CurrentScope.Put(name, context); + nodesToDeclarations.Put(context, decl); + return null; + } + + public override object VisitAssumeOnStartDecl(PParser.AssumeOnStartDeclContext context) + { + var name = $"init{CurrentScope.AssumeOnStarts.Count()}"; + var decl = CurrentScope.Put(name, context); + nodesToDeclarations.Put(context, decl); + return null; + } + + public override object VisitPureDecl(PParser.PureDeclContext context) + { + var name = context.name.GetText(); + var decl = CurrentScope.Put(name, context); + nodesToDeclarations.Put(context, decl); + return VisitChildrenWithNewScope(decl, context); + } + #region Events public override object VisitEventDecl(PParser.EventDeclContext context) @@ -265,6 +298,10 @@ public override object VisitBinExpr(PParser.BinExprContext context) { return null; } + public override object VisitQuantExpr(PParser.QuantExprContext context) + { + return null; + } public override object VisitUnaryExpr(PParser.UnaryExprContext context) { @@ -380,6 +417,10 @@ public override object VisitAssertStmt(PParser.AssertStmtContext context) { return null; } + public override object VisitAssumeStmt(PParser.AssumeStmtContext context) + { + return null; + } public override object VisitReturnStmt(PParser.ReturnStmtContext context) { diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs index b726380da..6b45d60cf 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs @@ -604,7 +604,118 @@ public override object VisitOnEventGotoState(PParser.OnEventGotoStateContext con } #endregion + + public override object VisitPureDecl(PParser.PureDeclContext context) + { + // PURE name=Iden body=Expr + var pure = (Pure) nodesToDeclarations.Get(context); + + // LPAREN funParamList? RPAREN + var paramList = context.funParamList() != null + ? (Variable[]) Visit(context.funParamList()) + : new Variable[0]; + pure.Signature.Parameters.AddRange(paramList); + + var temporaryFunction = new Function(pure.Name, context) + { + Scope = CurrentScope.MakeChildScope() + }; + + foreach (var p in paramList) + { + var param = temporaryFunction.Scope.Put(p.Name, p.SourceLocation, VariableRole.Param); + param.Type = p.Type; + nodesToDeclarations.Put(p.SourceLocation, param); + temporaryFunction.Signature.Parameters.Add(param); + } + + pure.Scope = temporaryFunction.Scope; + + // (COLON type)? + pure.Signature.ReturnType = ResolveType(context.type()); + + if (context.body is not null) + { + var exprVisitor = new ExprVisitor(temporaryFunction, Handler); + var body = exprVisitor.Visit(context.body); + + if (!pure.Signature.ReturnType.IsSameTypeAs(body.Type)) + { + throw Handler.TypeMismatch(context.body, body.Type, pure.Signature.ReturnType); + } + + pure.Body = body; + } + + return pure; + } + + public override object VisitInvariantDecl(PParser.InvariantDeclContext context) + { + // INVARIANT name=Iden body=Expr + var inv = (Invariant) nodesToDeclarations.Get(context); + + var temporaryFunction = new Function(inv.Name, context); + temporaryFunction.Scope = CurrentScope.MakeChildScope(); + + var exprVisitor = new ExprVisitor(temporaryFunction, Handler); + + var body = exprVisitor.Visit(context.body); + + if (!PrimitiveType.Bool.IsSameTypeAs(body.Type)) + { + throw Handler.TypeMismatch(context.body, body.Type, PrimitiveType.Bool); + } + inv.Body = body; + + return inv; + } + + public override object VisitAxiomDecl(PParser.AxiomDeclContext context) + { + // Axiom body=Expr + var inv = (Axiom) nodesToDeclarations.Get(context); + + var temporaryFunction = new Function(inv.Name, context); + temporaryFunction.Scope = CurrentScope.MakeChildScope(); + + var exprVisitor = new ExprVisitor(temporaryFunction, Handler); + + var body = exprVisitor.Visit(context.body); + + if (!PrimitiveType.Bool.IsSameTypeAs(body.Type)) + { + throw Handler.TypeMismatch(context.body, body.Type, PrimitiveType.Bool); + } + + inv.Body = body; + + return inv; + } + + public override object VisitAssumeOnStartDecl(PParser.AssumeOnStartDeclContext context) + { + // assume on start: body=Expr + var assume = (AssumeOnStart) nodesToDeclarations.Get(context); + + var temporaryFunction = new Function(assume.Name, context); + temporaryFunction.Scope = CurrentScope.MakeChildScope(); + + var exprVisitor = new ExprVisitor(temporaryFunction, Handler); + + var body = exprVisitor.Visit(context.body); + + if (!PrimitiveType.Bool.IsSameTypeAs(body.Type)) + { + throw Handler.TypeMismatch(context.body, body.Type, PrimitiveType.Bool); + } + + assume.Body = body; + + return assume; + } + #region Functions public override object VisitPFunDecl(PParser.PFunDeclContext context) diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs index 82fd330db..6095a5357 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs @@ -6,6 +6,7 @@ using Plang.Compiler.TypeChecker.AST; using Plang.Compiler.TypeChecker.AST.Declarations; using Plang.Compiler.TypeChecker.AST.Expressions; +using Plang.Compiler.TypeChecker.AST.States; using Plang.Compiler.TypeChecker.Types; namespace Plang.Compiler.TypeChecker @@ -14,7 +15,7 @@ public class ExprVisitor : PParserBaseVisitor { private readonly ITranslationErrorHandler handler; private readonly Function method; - private readonly Scope table; + private Scope table; public ExprVisitor(Function method, ITranslationErrorHandler handler) { @@ -45,19 +46,82 @@ public override IPExpr VisitParenExpr(PParser.ParenExprContext context) public override IPExpr VisitNamedTupleAccessExpr(PParser.NamedTupleAccessExprContext context) { - var subExpr = Visit(context.expr()); - if (!(subExpr.Type.Canonicalize() is NamedTupleType tuple)) - { - throw handler.TypeMismatch(subExpr, TypeKind.NamedTuple); - } - + IPExpr subExpr = Visit(context.expr()); var fieldName = context.field.GetText(); - if (!tuple.LookupEntry(fieldName, out var entry)) + + switch (subExpr.Type.Canonicalize()) { - throw handler.MissingNamedTupleEntry(context.field, tuple); - } + case NamedTupleType tuple: + if (!tuple.LookupEntry(fieldName, out var entry)) + { + throw handler.MissingNamedTupleEntry(context.field, tuple); + } + + return new NamedTupleAccessExpr(context, subExpr, entry); + + case PermissionType {Origin: Machine} permission: + var machine = (Machine) permission.Origin; + + if (!machine.LookupEntry(fieldName, out var field)) + { + throw handler.MissingMachineField(context.field, machine); + } + return new MachineAccessExpr(context, machine, subExpr, field); + + case PermissionType {Origin: Interface} permission: + var pname = permission.Origin.Name; + + if (!table.Lookup(pname, out Machine m)) + { + throw handler.TypeMismatch(subExpr, [TypeKind.NamedTuple, TypeKind.Base]); + } + + if (!m.LookupEntry(fieldName, out var mfield)) + { + throw handler.MissingMachineField(context.field, m); + } + return new MachineAccessExpr(context, m, subExpr, mfield); + + case PermissionType {Origin: NamedEventSet} permission: + + var pevents = ((NamedEventSet)permission.Origin).Events.ToList(); + + foreach (var pevent in pevents) + { + switch (pevent.PayloadType.Canonicalize()) + { + case NamedTupleType namedTupleType: + if (namedTupleType.LookupEntry(fieldName, out var pentry)) + { + return new EventAccessExpr(context, pevent, subExpr, pentry); + } + break; + } + } + + throw handler.MissingEventField(context.field, pevents.First()); + + case PrimitiveType pt when pt.IsSameTypeAs(PrimitiveType.Machine): + Machine spec; - return new NamedTupleAccessExpr(context, subExpr, entry); + switch (subExpr) + { + case SpecRefExpr specRefExpr: + spec = specRefExpr.Value; + break; + default: + throw handler.TypeMismatch(subExpr, [TypeKind.NamedTuple, TypeKind.Base]); + } + + if (!spec.LookupEntry(fieldName, out var sfield)) + { + throw handler.MissingMachineField(context.field, spec); + } + return new SpecAccessExpr(context, spec, subExpr, sfield); + + default: + throw handler.TypeMismatch(subExpr, [TypeKind.NamedTuple, TypeKind.Base]); + } } public override IPExpr VisitTupleAccessExpr(PParser.TupleAccessExprContext context) @@ -181,33 +245,68 @@ public override IPExpr VisitCtorExpr(PParser.CtorExprContext context) public override IPExpr VisitFunCallExpr(PParser.FunCallExprContext context) { var funName = context.fun.GetText(); - if (!table.Lookup(funName, out Function function)) + if (table.Lookup(funName, out Function function)) { - throw handler.MissingDeclaration(context.fun, "function", funName); - } + // Check the arguments + var arguments = TypeCheckingUtils.VisitRvalueList(context.rvalueList(), this).ToArray(); + ISet linearVariables = new System.Collections.Generic.HashSet(); - // Check the arguments - var arguments = TypeCheckingUtils.VisitRvalueList(context.rvalueList(), this).ToArray(); - ISet linearVariables = new HashSet(); + if (function.Signature.Parameters.Count != arguments.Length) + { + throw handler.IncorrectArgumentCount(context, arguments.Length, function.Signature.Parameters.Count); + } - if (function.Signature.Parameters.Count != arguments.Length) - { - throw handler.IncorrectArgumentCount(context, arguments.Length, function.Signature.Parameters.Count); - } + for (var i = 0; i < arguments.Length; i++) + { + var argument = arguments[i]; + var paramType = function.Signature.Parameters[i].Type; + if (!paramType.IsAssignableFrom(argument.Type)) + { + throw handler.TypeMismatch(context.rvalueList().rvalue(i), argument.Type, paramType); + } - for (var i = 0; i < arguments.Length; i++) + } + + method.AddCallee(function); + return new FunCallExpr(context, function, arguments); + } + if (table.Lookup(funName, out Pure pure)) { - var argument = arguments[i]; - var paramType = function.Signature.Parameters[i].Type; - if (!paramType.IsAssignableFrom(argument.Type)) + // Check the arguments + var arguments = TypeCheckingUtils.VisitRvalueList(context.rvalueList(), this).ToArray(); + ISet linearVariables = new System.Collections.Generic.HashSet(); + + if (pure.Signature.Parameters.Count != arguments.Length) { - throw handler.TypeMismatch(context.rvalueList().rvalue(i), argument.Type, paramType); + throw handler.IncorrectArgumentCount(context, arguments.Length, pure.Signature.Parameters.Count); } + for (var i = 0; i < arguments.Length; i++) + { + var argument = arguments[i]; + var paramType = pure.Signature.Parameters[i].Type; + if (!paramType.IsAssignableFrom(argument.Type)) + { + switch (paramType) + { + case PrimitiveType pt when pt.IsSameTypeAs(PrimitiveType.Event): + switch (argument.Type) + { + case PermissionType {Origin: NamedEventSet} per when ((NamedEventSet)(per.Origin)).Events.Count() == 1: + continue; + } + break; + } + throw handler.TypeMismatch(context.rvalueList().rvalue(i), argument.Type, paramType); + } + + } + + return new PureCallExpr(context, pure, arguments); } + + throw handler.MissingDeclaration(context.fun, "function", funName); - method.AddCallee(function); - return new FunCallExpr(context, function, arguments); } public override IPExpr VisitUnaryExpr(PParser.UnaryExprContext context) @@ -241,6 +340,100 @@ public override IPExpr VisitUnaryExpr(PParser.UnaryExprContext context) } } + public override IPExpr VisitQuantExpr(PParser.QuantExprContext context) + { + var oldTable = table; + table = table.MakeChildScope(); + + bool diff = context.diff != null; + + var bound = context.bound.funParam().Select(p => + { + var symbolName = p.name.GetText(); + var param = table.Put(symbolName, p, VariableRole.Param); + param.Type = TypeResolver.ResolveType(p.type(), table, handler); + return param; + }).Cast().ToArray(); + + if (diff && bound.ToList().Count != 1) + { + // we have the "new" annotation so the bound must be a single thing and it must be an event + throw handler.InternalError(context, new ArgumentException($"Difference quantifiers must have exactly one bound variable", nameof(context))); + } + + if (diff) + { + switch (bound[0].Type.Canonicalize()) + { + case PrimitiveType pt when pt.IsSameTypeAs(PrimitiveType.Event): + break; + case PermissionType {Origin: NamedEventSet} _: + break; + default: + throw handler.TypeMismatch(context.bound, bound[0].Type, PrimitiveType.Event); + } + } + + var body = Visit(context.body); + + table = oldTable; + + if (context.quant.Text == "forall") + { + return new QuantExpr(context, QuantType.Forall, bound.ToList(), body, diff); + } + + return new QuantExpr(context, QuantType.Exists, bound.ToList(), body, diff); + } + + public override IPExpr VisitTestExpr(PParser.TestExprContext context) + { + var instance = Visit(context.instance); + string name = context.kind.GetText(); + + if (table.Lookup(name, out Machine m)) + { + return new TestExpr(context, instance, m); + } + + if (table.Lookup(name, out PEvent e)) + { + return new TestExpr(context, instance, e); + } + + if (table.Lookup(name, out State s)) + { + return new TestExpr(context, instance, s); + } + + throw handler.MissingDeclaration(context, "machine, event, or state", name); + } + + public override IPExpr VisitTargetsExpr(PParser.TargetsExprContext context) + { + var instance = Visit(context.instance); + var target = Visit(context.target); + + // TODO: type check to make sure instance is an event and machine is a machine + return new TargetsExpr(context, instance, target); + } + + public override IPExpr VisitFlyingExpr(PParser.FlyingExprContext context) + { + var instance = Visit(context.instance); + + // TODO: type check to make sure instance is an event + return new FlyingExpr(context, instance); + } + + public override IPExpr VisitSentExpr(PParser.SentExprContext context) + { + var instance = Visit(context.instance); + + // TODO: type check to make sure instance is an event + return new SentExpr(context, instance); + } + public override IPExpr VisitBinExpr(PParser.BinExprContext context) { var lhs = Visit(context.lhs); @@ -263,7 +456,8 @@ public override IPExpr VisitBinExpr(PParser.BinExprContext context) var logicCtors = new Dictionary> { {"&&", (elhs, erhs) => new BinOpExpr(context, BinOpType.And, elhs, erhs)}, - {"||", (elhs, erhs) => new BinOpExpr(context, BinOpType.Or, elhs, erhs)} + {"||", (elhs, erhs) => new BinOpExpr(context, BinOpType.Or, elhs, erhs)}, + {"==>", (elhs, erhs) => new BinOpExpr(context, BinOpType.Then, elhs, erhs)} }; var compCtors = new Dictionary> @@ -350,7 +544,8 @@ public override IPExpr VisitBinExpr(PParser.BinExprContext context) return compCtors[op](lhs, rhs); case "&&": - case "||": + case "||": + case "==>": if (!PrimitiveType.Bool.IsAssignableFrom(lhs.Type)) { throw handler.TypeMismatch(context.lhs, lhs.Type, PrimitiveType.Bool); @@ -518,7 +713,12 @@ public override IPExpr VisitPrimitive(PParser.PrimitiveContext context) return new EventRefExpr(context, evt); } - throw handler.MissingDeclaration(context.iden(), "variable, enum element, or event", symbolName); + if (table.Lookup(symbolName, out Machine mac) && mac.IsSpec) + { + return new SpecRefExpr(context, mac); + } + + throw handler.MissingDeclaration(context.iden(), "variable, enum element, spec machine, or event", symbolName); } if (context.floatLiteral() != null) @@ -599,7 +799,7 @@ public override IPExpr VisitNamedTupleBody(PParser.NamedTupleBodyContext context var fields = context._values.Select(Visit).ToArray(); var entries = new NamedTupleEntry[fields.Length]; - var names = new HashSet(); + var names = new System.Collections.Generic.HashSet(); for (var i = 0; i < fields.Length; i++) { var entryName = context._names[i].GetText(); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/FunctionValidator.cs b/Src/PCompiler/CompilerCore/TypeChecker/FunctionValidator.cs index 16b1204a1..5a765e030 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/FunctionValidator.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/FunctionValidator.cs @@ -40,6 +40,10 @@ public static bool SurelyReturns(IPStmt stmt) when (assertStmt.Assertion as BoolLiteralExpr)?.Value == false: return true; + case AssumeStmt assumeStmt + when (assumeStmt.Assumption as BoolLiteralExpr)?.Value == false: + return true; + case GotoStmt _: return true; diff --git a/Src/PCompiler/CompilerCore/TypeChecker/InferMachineCreates.cs b/Src/PCompiler/CompilerCore/TypeChecker/InferMachineCreates.cs index bb8e43493..e5852b7a0 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/InferMachineCreates.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/InferMachineCreates.cs @@ -53,6 +53,10 @@ private static IEnumerable InferCreates(IPAST tree, ITranslationError case AssertStmt assertStmt: return InferCreatesForExpr(assertStmt.Assertion, handler) .Union(InferCreatesForExpr(assertStmt.Message, handler)); + + case AssumeStmt assumeStmt: + return InferCreatesForExpr(assumeStmt.Assumption, handler) + .Union(InferCreatesForExpr(assumeStmt.Message, handler)); case AssignStmt assignStmt: return InferCreatesForExpr(assignStmt.Location, handler) diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ModuleSystemTypeChecker.cs b/Src/PCompiler/CompilerCore/TypeChecker/ModuleSystemTypeChecker.cs index d8cf61fd6..bd8bdcc94 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ModuleSystemTypeChecker.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ModuleSystemTypeChecker.cs @@ -129,7 +129,7 @@ private void CheckWellFormedness(AssertModuleExpr assertExpr) currentModule.InterfaceDef.Add(ipItem.Key, ipItem.Value); } } - + internal void CheckRefinementTest(RefinementTest test) { //check that the test module is closed with respect to creates diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs b/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs index 9eff2b90c..1775634ac 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs @@ -22,6 +22,10 @@ public class Scope private readonly IDictionary events = new Dictionary(); private readonly IDictionary eventSets = new Dictionary(); private readonly IDictionary functions = new Dictionary(); + private readonly IDictionary pures = new Dictionary(); + private readonly IDictionary invariants = new Dictionary(); + private readonly IDictionary axioms = new Dictionary(); + private readonly IDictionary assumeOnStarts = new Dictionary(); private readonly ICompilerConfiguration config; private readonly IDictionary implementations = new Dictionary(); private readonly IDictionary interfaces = new Dictionary(); @@ -56,6 +60,10 @@ private Scope(ICompilerConfiguration config, Scope parent = null) .Concat(Events) .Concat(EventSets) .Concat(Functions) + .Concat(Invariants) + .Concat(Axioms) + .Concat(AssumeOnStarts) + .Concat(Pures) .Concat(Interfaces) .Concat(Machines) .Concat(States) @@ -71,6 +79,10 @@ private Scope(ICompilerConfiguration config, Scope parent = null) public IEnumerable Events => events.Values; public IEnumerable EventSets => eventSets.Values; public IEnumerable Functions => functions.Values; + public IEnumerable Invariants => invariants.Values; + public IEnumerable Axioms => axioms.Values; + public IEnumerable AssumeOnStarts => assumeOnStarts.Values; + public IEnumerable Pures => pures.Values; public IEnumerable Interfaces => interfaces.Values; public IEnumerable Machines => machines.Values; public IEnumerable States => states.Values; @@ -160,6 +172,26 @@ public bool Get(string name, out Function tree) { return functions.TryGetValue(name, out tree); } + + public bool Get(string name, out Invariant tree) + { + return invariants.TryGetValue(name, out tree); + } + + public bool Get(string name, out Axiom tree) + { + return axioms.TryGetValue(name, out tree); + } + + public bool Get(string name, out AssumeOnStart tree) + { + return assumeOnStarts.TryGetValue(name, out tree); + } + + public bool Get(string name, out Pure tree) + { + return pures.TryGetValue(name, out tree); + } public bool Get(string name, out Interface tree) { @@ -294,7 +326,58 @@ public bool Lookup(string name, out Function tree) tree = null; return false; } + + public bool Lookup(string name, out Invariant tree) + { + var current = this; + while (current != null) + { + if (current.Get(name, out tree)) + { + return true; + } + + current = current.Parent; + } + + tree = null; + return false; + } + + public bool Lookup(string name, out Axiom tree) + { + var current = this; + while (current != null) + { + if (current.Get(name, out tree)) + { + return true; + } + + current = current.Parent; + } + + tree = null; + return false; + } + + public bool Lookup(string name, out Pure tree) + { + var current = this; + while (current != null) + { + if (current.Get(name, out tree)) + { + return true; + } + + current = current.Parent; + } + tree = null; + return false; + } + public bool Lookup(string name, out Interface tree) { var current = this; @@ -339,6 +422,16 @@ public bool Lookup(string name, out State tree) return true; } + // look inside machines to find the state. + // TODO: bug if multiple machines have the same state name + foreach (var m in current.Machines) + { + if (m.Scope.Get(name, out tree)) + { + return true; + } + } + current = current.Parent; } @@ -548,6 +641,39 @@ public Function Put(string name, PParser.FunDeclContext tree) return function; } + + public Pure Put(string name, PParser.PureDeclContext tree) + { + var pure = new Pure(name, tree); + CheckConflicts(pure, Namespace(pures)); + pures.Add(name, pure); + return pure; + } + + public Invariant Put(string name, PParser.InvariantDeclContext tree) + { + var invariant = new Invariant(name, null, tree); // need to add expr later + CheckConflicts(invariant, Namespace(invariants)); + invariants.Add(name, invariant); + return invariant; + } + + public Axiom Put(string name, PParser.AxiomDeclContext tree) + { + var axiom = new Axiom(name, null, tree); // need to add expr later + CheckConflicts(axiom, Namespace(axioms)); + axioms.Add(name, axiom); + return axiom; + } + + public AssumeOnStart Put(string name, PParser.AssumeOnStartDeclContext tree) + { + var assumeOnStart = new AssumeOnStart(name, null, tree); // need to add expr later + CheckConflicts(assumeOnStart, Namespace(assumeOnStarts)); + assumeOnStarts.Add(name, assumeOnStart); + return assumeOnStart; + } + public EnumElem Put(string name, PParser.EnumElemContext tree) { var enumElem = new EnumElem(name, tree); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs index 1287e10ac..8e73c5338 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs @@ -63,6 +63,30 @@ public override IPStmt VisitAssertStmt(PParser.AssertStmtContext context) return new AssertStmt(context, assertion, assertMessage); } + + + public override IPStmt VisitAssumeStmt(PParser.AssumeStmtContext context) + { + var assumption = exprVisitor.Visit(context.assumption); + if (!PrimitiveType.Bool.IsSameTypeAs(assumption.Type)) + { + throw handler.TypeMismatch(context.assumption, assumption.Type, PrimitiveType.Bool); + } + IPExpr assertMessage = new StringExpr(context, @$"{config.LocationResolver.GetLocation(context).ToString().Replace(@"\", @"\\")}",new List()); + if (context.message != null) + { + var message = exprVisitor.Visit(context.message); + if (!message.Type.IsSameTypeAs(PrimitiveType.String)) + { + throw handler.TypeMismatch(context.message, message.Type, PrimitiveType.String); + } + + assertMessage = new StringExpr(message.SourceLocation, "{0} {1}",new List() {assertMessage, + message}); + } + + return new AssumeStmt(context, assumption, assertMessage); + } public override IPStmt VisitPrintStmt(PParser.PrintStmtContext context) { @@ -258,9 +282,12 @@ public override IPStmt VisitForeachStmt(PParser.ForeachStmtContext context) throw handler.TypeMismatch(context.item, itemType, expectedItemType); var body = Visit(context.statement()); - return new ForeachStmt(context, var, collection, body); - } + var invs = context._invariants.Select(exprVisitor.Visit).ToList(); + + return new ForeachStmt(context, var, collection, body, invs); + } + public override IPStmt VisitIfStmt(PParser.IfStmtContext context) { var condition = exprVisitor.Visit(context.expr()); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/TypeResolver.cs b/Src/PCompiler/CompilerCore/TypeChecker/TypeResolver.cs index 39b22c368..262c96ee5 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/TypeResolver.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/TypeResolver.cs @@ -93,6 +93,13 @@ public override PLanguageType VisitNamedType(PParser.NamedTypeContext context) { return new PermissionType(machine); } + + if (scope.Lookup(typeName, out PEvent pevent)) + { + var eset = new NamedEventSet(pevent.Name, pevent.SourceLocation); + eset.AddEvent(pevent); + return new PermissionType(eset); + } throw handler.MissingDeclaration(context.name, "enum, typedef, event set, machine, or interface", typeName); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Types/PermissionType.cs b/Src/PCompiler/CompilerCore/TypeChecker/Types/PermissionType.cs index 302e248dc..f005a08a5 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/Types/PermissionType.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/Types/PermissionType.cs @@ -8,28 +8,28 @@ namespace Plang.Compiler.TypeChecker.Types { public class PermissionType : PLanguageType { - private readonly IPDecl origin; - public PermissionType(Machine machine) : base(TypeKind.Base) { - origin = machine; + Origin = machine; AllowedPermissions = new Lazy>(() => machine.Receives.Events.ToList()); } public PermissionType(Interface pInterface) : base(TypeKind.Base) { - origin = pInterface; + Origin = pInterface; AllowedPermissions = new Lazy>(() => pInterface.ReceivableEvents.Events.ToList()); } public PermissionType(NamedEventSet eventSet) : base(TypeKind.Base) { - origin = eventSet; + Origin = eventSet; AllowedPermissions = new Lazy>(() => eventSet.Events.ToList()); } + + public IPDecl Origin { get; } - public override string OriginalRepresentation => origin.Name; - public override string CanonicalRepresentation => origin.Name; + public override string OriginalRepresentation => Origin.Name; + public override string CanonicalRepresentation => Origin.Name; public override Lazy> AllowedPermissions { get; } diff --git a/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs index a6a3b88ed..03299aa22 100644 --- a/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs +++ b/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs @@ -45,6 +45,11 @@ internal PCompilerOptions() Parser.AddArgument("pobserve-package", "po", "PObserve package name").IsHidden = true; Parser.AddArgument("debug", "d", "Enable debug logs", typeof(bool)).IsHidden = true; + + Parser.AddArgument("timeout", "t", "Set SMT solver timeout in seconds", typeof(int)).IsHidden = true; + + Parser.AddArgument("no-event-handler-checks", "nch", "Do not check that all events are handled", typeof(bool)).IsHidden = true; + Parser.AddArgument("check-only", "co", "Check only the specified machine", typeof(string)).IsHidden = true; } /// @@ -161,6 +166,15 @@ private static void UpdateConfigurationWithParsedArgument(CompilerConfiguration case "debug": compilerConfiguration.Debug = true; break; + case "timeout": + compilerConfiguration.Timeout = (int)option.Value; + break; + case "no-event-handler-checks": + compilerConfiguration.HandlesAll = false; + break; + case "check-only": + compilerConfiguration.CheckOnly = (string)option.Value; + break; case "mode": compilerConfiguration.OutputLanguages = new List(); switch (((string)option.Value).ToLowerInvariant()) diff --git a/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs b/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs index ceb53c701..e1aaaa61f 100644 --- a/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs +++ b/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs @@ -242,9 +242,12 @@ private IList GetTargetLanguages(FileInfo fullPathName) case "stately": outputLanguages.Add(CompilerOutput.Stately); break; + case "uclid5": + outputLanguages.Add(CompilerOutput.Uclid5); + break; default: throw new CommandlineParsingError( - $"Expected CSharp, Java, Stately, or Symbolic as target, received {projectXml.Element("Target")?.Value}"); + $"Expected CSharp, Java, Stately, UCLID5, or Symbolic as target, received {projectXml.Element("Target")?.Value}"); } } } diff --git a/Tutorial/5_ChainReplicationVerification/.gitignore b/Tutorial/5_ChainReplicationVerification/.gitignore new file mode 100644 index 000000000..161a65f6d --- /dev/null +++ b/Tutorial/5_ChainReplicationVerification/.gitignore @@ -0,0 +1,7 @@ +*.out +*.err +portfolio/ +Test.cs +pom.xml +*.csproj +PCheckerOutput/ diff --git a/Tutorial/5_ChainReplicationVerification/ChainReplicationVerification.pproj b/Tutorial/5_ChainReplicationVerification/ChainReplicationVerification.pproj new file mode 100644 index 000000000..dd4bb952f --- /dev/null +++ b/Tutorial/5_ChainReplicationVerification/ChainReplicationVerification.pproj @@ -0,0 +1,8 @@ + +ChainReplicationVerification + + ./PSrc/ + +./PGenerated/ +UCLID5 + diff --git a/Tutorial/5_ChainReplicationVerification/PSrc/System.p b/Tutorial/5_ChainReplicationVerification/PSrc/System.p new file mode 100644 index 000000000..d20a1e7ec --- /dev/null +++ b/Tutorial/5_ChainReplicationVerification/PSrc/System.p @@ -0,0 +1,128 @@ +type tWriteRequest = (source: machine, k: int, v: int); +type tReadRequest = (source: machine, k: int); +type tReadResponse = (source: machine, k: int, v: int, status: bool); + +event eWriteRequest : tWriteRequest; +event eWriteResponse : tWriteRequest; + +event ePropagateWrite: tWriteRequest; + +event eReadRequest : tReadRequest; +event eReadResponse : tReadResponse; + +machine Head { + var kv: map[int, int]; + + start state Receiving { + on eWriteRequest do (req: tWriteRequest) { + kv[req.k] = req.v; + send next_(this), ePropagateWrite, (source = req.source, k = req.k, v = req.v); + } + } +} + +machine Body { + var kv: map[int, int]; + + start state Forwarding { + on ePropagateWrite do (req: tWriteRequest) { + kv[req.k] = req.v; + send next_(this), ePropagateWrite, (source = req.source, k = req.k, v = req.v); + } + } +} + + +machine Tail { + var kv: map[int, int]; + + start state Replying { + on ePropagateWrite do (req: tWriteRequest) { + kv[req.k] = req.v; + send req.source, eWriteResponse, (source = req.source, k = req.k, v = req.v); + } + + on eReadRequest do (req: tReadRequest) { + if (req.k in kv) { + send req.source, eReadResponse, (source = req.source, k = req.k, v = kv[req.k], status = true); + } else { + send req.source, eReadResponse, (source = req.source, k = req.k, v = -1, status = false); + } + } + } +} + +machine Client { + start state Loop { + entry { + var k: int; + var v: int; + + k = RandomInt(); + + if ($) { + v = RandomInt(); + send head(), eWriteRequest, (source = this, k = k, v = v); + } else { + send tail(), eReadRequest, (source = this, k = k); + } + + goto Loop; + } + ignore eWriteResponse, eReadResponse; // not actually doing anything with these in the client + } +} + +fun RandomInt(): int; + +spec StrongConsistency observes eReadResponse, eWriteResponse { + var kv : map[int, int]; + start state WaitForEvents { + on eWriteResponse do (resp: tWriteRequest) { + kv[resp.k] = resp.v; + } + on eReadResponse do (resp: tReadResponse) { + if (resp.k in kv) { + assert resp.status == true; + assert resp.v == kv[resp.k]; + } else { + assert resp.status == false; + } + } + } +} + +// begin proof +pure head(): machine; +pure tail(): machine; +pure next_(m: machine): machine; + +// set all the fields to their default values +init forall (p: Head) :: p.kv == default(map[int, int]); +init forall (p: Body) :: p.kv == default(map[int, int]); +init forall (p: Tail) :: p.kv == default(map[int, int]); +init StrongConsistency.kv == default(map[int, int]); + +// assume the pure functions match the state at the start +init forall (m: machine) :: m == head() == m is Head; +init forall (m: machine) :: m == tail() == m is Tail; +init forall (m: machine) :: next_(m) is Body || next_(m) is Tail; +// ensure that the pure functions continue to match the state as time goes on +invariant next_1: forall (m: machine) :: m == head() == m is Head; +invariant next_2: forall (m: machine) :: m == tail() == m is Tail; +invariant next_3: forall (m: machine) :: next_(m) is Body || next_(m) is Tail; + +// Aux invariants for P obligations +invariant only_head_receives_writes: forall (m: machine, e: event) :: (inflight e && e is eWriteRequest && e targets m) ==> (m is Head); +invariant only_tail_receives_reads: forall (m: machine, e: event) :: (inflight e && e is eReadRequest && e targets m) ==> (m is Tail); +invariant only_client_receives_read_response: forall (m: machine, e: event) :: (inflight e && e is eReadResponse && e targets m) ==> (m is Client); +invariant only_client_receives_write_response: forall (m: machine, e: event) :: (inflight e && e is eWriteResponse && e targets m) ==> (m is Client); +invariant only_body_or_tail_receive_props: forall (m: machine, e: event) :: (inflight e && e is ePropagateWrite && e targets m) ==> (m is Tail || m is Body); +invariant source_is_always_client_1: forall (e: eWriteRequest) :: inflight e ==> e.source is Client; +invariant source_is_always_client_2: forall (e: eReadRequest) :: inflight e ==> e.source is Client; +invariant source_is_always_client_3: forall (e: ePropagateWrite) :: inflight e ==> e.source is Client; +invariant source_is_always_client_4: forall (e: eReadResponse) :: inflight e ==> e.source is Client; +invariant source_is_always_client_5: forall (e: eWriteResponse) :: inflight e ==> e.source is Client; + +// Aux invariant for spec machine +invariant tail_sync: forall (t: Tail) :: t.kv == StrongConsistency.kv; diff --git a/Tutorial/5_ChainReplicationVerification/portfolio-config.json b/Tutorial/5_ChainReplicationVerification/portfolio-config.json new file mode 100644 index 000000000..f91140416 --- /dev/null +++ b/Tutorial/5_ChainReplicationVerification/portfolio-config.json @@ -0,0 +1,7 @@ +{ + "pproj": { + "help" : "Name of the .pproj file in the project directory", + "default" : "ChainReplicationVerification.pproj", + "metavar" : "F" + } +} diff --git a/Tutorial/6_TwoPhaseCommitVerification/.gitignore b/Tutorial/6_TwoPhaseCommitVerification/.gitignore new file mode 100644 index 000000000..161a65f6d --- /dev/null +++ b/Tutorial/6_TwoPhaseCommitVerification/.gitignore @@ -0,0 +1,7 @@ +*.out +*.err +portfolio/ +Test.cs +pom.xml +*.csproj +PCheckerOutput/ diff --git a/Tutorial/6_TwoPhaseCommitVerification/KeyValue/PSrc/System.p b/Tutorial/6_TwoPhaseCommitVerification/KeyValue/PSrc/System.p new file mode 100644 index 000000000..0ed77833c --- /dev/null +++ b/Tutorial/6_TwoPhaseCommitVerification/KeyValue/PSrc/System.p @@ -0,0 +1,240 @@ +/********************************************************* +Clients send read and write requests to a coordinator. On write requests, the coordinator does a two phase commit with +all participants. On read requests, the coordinator just asks a random participant to respond to the client. + +All participants must agree on every commited write. The monitor keeps track of all write responses, which is the ground +truth for what is commited. Every participant must be maintaining a subset of this. +**********************************************************/ + +enum tVote {YES, NO} + +type tRound = int; +type tKey = int; +type tValue = int; + +type rvPair = (round: tRound, value: tValue); +type krvTriple = (key: tKey, round: tRound, value: tValue); + +type tVoteResp = (origin: machine, triple: krvTriple, vote: tVote, source: machine); +type tVoteReq = (origin: machine, triple: krvTriple); +type tWriteReq = (origin: machine, key: tKey, value: tValue); +type tReadReq = (origin: machine, key: tKey); +type tWriteResp = (triple: krvTriple, vote: tVote); +type tReadResp = (key: tKey, versions: set[rvPair], source: machine); + +event eVoteReq : tVoteReq; +event eVoteResp: tVoteResp; +event eAbort : tVoteReq; +event eCommit : tVoteReq; + +event eWriteReq : tWriteReq; +event eWriteResp: tWriteResp; +event eReadReq : tReadReq; +event eReadResp : tReadResp; + +fun RandomInt(): int; + +machine Client { + start state Loop { + entry { + var k: int; + var v: int; + + k = RandomInt(); + v = RandomInt(); + + if ($) { + v = RandomInt(); + send coordinator(), eWriteReq, (origin = this, key = k, value = v); + } else { + send coordinator(), eReadReq, (origin = this, key = k); + } + + goto Loop; + } + ignore eWriteResp, eReadResp; + } +} + +machine Coordinator +{ + var yesVotes: map[krvTriple, set[machine]]; + var commited: set[krvTriple]; + var aborted : set[krvTriple]; + + start state Serving { + on eReadReq do (req: tReadReq) { + var p: machine; + assume (p in participants()); + send p, eReadReq, req; + } + + on eWriteReq do (req: tWriteReq) { + var p: machine; + var r: tRound; + assume (forall (t: krvTriple) :: t in yesVotes ==> t.round != r); + + yesVotes[(key = req.key, round = r, value = req.value)] = default(set[machine]); + + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eVoteReq; + invariant forall new (e: eVoteReq) :: e.triple.round == r && e.triple.key == req.key && e.triple.value == req.value && e.origin == req.origin; + { + send p, eVoteReq, (origin = req.origin, triple = (key = req.key, round = r, value = req.value)); + } + } + + on eVoteResp do (resp: tVoteResp) { + var p: machine; + + if (resp.vote == YES) { + yesVotes[resp.triple] += (resp.source); + + if (yesVotes[resp.triple] == participants()) { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eCommit; + invariant forall new (e: eCommit) :: e.triple == resp.triple && e.origin == resp.origin; + { + send p, eCommit, (origin = resp.origin, triple = resp.triple); + } + + commited += (resp.triple); + send resp.origin, eWriteResp, (triple = resp.triple, vote = resp.vote); + goto Serving; + } + + } else { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eAbort; + invariant forall new (e: eAbort) :: e.triple == resp.triple && e.origin == resp.origin; + { + send p, eAbort, (origin = resp.origin, triple = resp.triple); + } + + aborted += (resp.triple); + send resp.origin, eWriteResp, (triple = resp.triple, vote = resp.vote); + goto Serving; + } + } + } +} + +machine Participant { + var commited: set[krvTriple]; + var aborted: set[krvTriple]; + var kv: map[tKey, set[rvPair]]; + + start state Acting { + on eVoteReq do (req: tVoteReq) { + send coordinator(), eVoteResp, (origin = req.origin, triple = req.triple, vote = preference(this, req.triple), source = this); + } + + on eCommit do (req: tVoteReq) { + commited += (req.triple); + if (!(req.triple.key in kv)) { + kv[req.triple.key] = default(set[rvPair]); + } + kv[req.triple.key] += ((round = req.triple.round, value = req.triple.value)); + } + + on eAbort do (req: tVoteReq) { + aborted += (req.triple); + } + + on eReadReq do (req: tReadReq) { + if (req.key in kv) { + send req.origin, eReadResp, (key = req.key, versions = kv[req.key], source = this); + } else { + send req.origin, eReadResp, (key = req.key, versions = default(set[rvPair]), source = this); + } + } + } +} + +spec Consistency observes eReadResp, eWriteResp { + var kv: map[tKey, set[rvPair]]; + start state WaitForEvents { + on eWriteResp do (resp: tWriteResp) { + if (resp.vote == YES) { + kv[resp.triple.key] += ((round = resp.triple.round, value = resp.triple.value)); + } + } + on eReadResp do (resp: tReadResp) { + // Everything we send back was actually written. + assert subset(resp.versions, kv[resp.key]); + // Everyone agrees on what we send back + assert (forall (t: krvTriple) :: (resp.key == t.key && (round = t.round, value = t.value) in resp.versions) ==> (forall (p: Participant) :: preference(p, t) == YES)); + } + } +} + +// using these to avoid initialization +pure participants(): set[machine]; +pure coordinator(): machine; +pure preference(m: machine, triple: krvTriple) : tVote; + +pure subset(small: set[rvPair], large: set[rvPair]) : bool = forall (rv: rvPair) :: rv in small ==> rv in large; + +// assumptions about how the system is setup and the pure functions above +init coordinator() is Coordinator; +init forall (c1: machine, c2: machine) :: (c1 is Coordinator && c2 is Coordinator) ==> c1 == c2; +init forall (m: machine) :: m in participants() == m is Participant; + +// making sure that our assumptions about pure functions are not pulled out from underneath us +invariant c_is_coordinator: coordinator() is Coordinator; +invariant one_coordinator: forall (c1: machine, c2: machine) :: (c1 is Coordinator && c2 is Coordinator) ==> c1 == c2; +invariant participant_set: forall (m: machine) :: m in participants() == m is Participant; + +// set all the fields to their default values +init forall (c: Coordinator) :: c.yesVotes == default(map[krvTriple, set[machine]]); +init forall (c: Coordinator) :: c.commited == default(set[krvTriple]); +init forall (c: Coordinator) :: c.aborted == default(set[krvTriple]); +init forall (p: Participant) :: p.commited == default(set[krvTriple]); +init forall (p: Participant) :: p.aborted == default(set[krvTriple]); +init forall (p: Participant) :: p.kv == default(map[tKey, set[rvPair]]); +init Consistency.kv == default(map[tKey, set[rvPair]]); + +// make sure we never get a message that we're not expecting +invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e; +invariant never_abort_to_coordinator: forall (e: event) :: e is eAbort && e targets coordinator() ==> !inflight e; +invariant never_req_to_coordinator: forall (e: event) :: e is eVoteReq && e targets coordinator() ==> !inflight e; +invariant never_resp_to_participant: forall (e: event, p: Participant) :: e is eVoteResp && e targets p ==> !inflight e; +invariant never_writeReq_to_participant: forall (e: event, p: Participant) :: e is eWriteReq && e targets p ==> !inflight e; +invariant never_writeResp_to_participant: forall (e: event, p: Participant) :: e is eWriteResp && e targets p ==> !inflight e; +invariant never_readResp_to_participant: forall (e: event, p: Participant) :: e is eReadResp && e targets p ==> !inflight e; +invariant never_writeResp_to_coordinator: forall (e: event, c: Coordinator) :: e is eWriteResp && e targets c ==> !inflight e; +invariant never_readResp_to_coordinator: forall (e: event, c: Coordinator) :: e is eReadResp && e targets c ==> !inflight e; +invariant never_voteReq_to_client: forall (e: event, c: Client) :: e is eVoteReq && e targets c ==> !inflight e; +invariant never_voteResp_to_client: forall (e: event, c: Client) :: e is eVoteResp && e targets c ==> !inflight e; +invariant never_abort_to_client: forall (e: event, c: Client) :: e is eAbort && e targets c ==> !inflight e; +invariant never_commit_to_client: forall (e: event, c: Client) :: e is eCommit && e targets c ==> !inflight e; +invariant never_writeReq_to_client: forall (e: event, c: Client) :: e is eWriteReq && e targets c ==> !inflight e; +invariant never_readReq_to_client: forall (e: event, c: Client) :: e is eReadReq && e targets c ==> !inflight e; +invariant readReq_origin_is_client: forall (e: eReadReq) :: inflight e ==> e.origin is Client; +invariant writeReq_origin_is_client: forall (e: eWriteReq) :: inflight e ==> e.origin is Client; +invariant voteReq_origin_is_client: forall (e: eVoteReq) :: inflight e ==> e.origin is Client; +invariant voteResp_origin_is_client: forall (e: eVoteResp) :: inflight e ==> e.origin is Client; + +// aux invariants for consistency monitor first assertion +invariant p_subset_monitor_kv: forall (p: Participant, k: tKey) :: k in p.kv ==> subset(p.kv[k], Consistency.kv[k]); +invariant c_commited_means_in_monitor_kv: forall (c: Coordinator, t: krvTriple) :: t in c.commited ==> ((round = t.round, value = t.value) in Consistency.kv[t.key]); + +// aux invariants for consistency monitor second assertion +// essentially the 2pc property, but restated for kv elements +invariant in_kv_means_all_preferred: forall (p1: Participant, t: krvTriple) :: (t.key in p1.kv && (round = t.round, value = t.value) in p1.kv[t.key]) ==> (forall (p2: Participant) :: preference(p2, t) == YES); + +// supporting invariants for the 2pc property +invariant a1: forall (e: eVoteResp) :: sent e ==> e.source is Participant; +invariant a2: forall (e: eVoteResp) :: sent e ==> e.vote == preference(e.source, e.triple); +invariant a3a: forall (c: Coordinator, e: eCommit) :: sent e ==> e.triple in c.commited; +invariant a3b: forall (c: Coordinator, e: eAbort) :: sent e ==> e.triple in c.aborted; +invariant a4: forall (c: Coordinator, t: krvTriple, p1: Participant) :: t in p1.commited ==> t in c.commited; +invariant a5: forall (p: Participant, c: Coordinator, t: krvTriple) :: (t in c.yesVotes && p in c.yesVotes[t]) ==> preference(p, t) == YES; +invariant a6: forall (c: Coordinator, t: krvTriple) :: t in c.commited ==> (forall (p2: Participant) :: preference(p2, t) == YES); +invariant a7a: forall (c: Coordinator, e: eVoteReq) :: sent e ==> e.triple in c.yesVotes; +invariant a7b: forall (c: Coordinator, e: eVoteResp) :: sent e ==> e.triple in c.yesVotes; + + diff --git a/Tutorial/6_TwoPhaseCommitVerification/KeyValue/TwoPhaseCommitVerification.pproj b/Tutorial/6_TwoPhaseCommitVerification/KeyValue/TwoPhaseCommitVerification.pproj new file mode 100644 index 000000000..d60d0d2f7 --- /dev/null +++ b/Tutorial/6_TwoPhaseCommitVerification/KeyValue/TwoPhaseCommitVerification.pproj @@ -0,0 +1,8 @@ + +TwoPhaseCommitVerification + + ./PSrc/ + +./PGenerated/ +UCLID5 + diff --git a/Tutorial/6_TwoPhaseCommitVerification/Rounds/PSrc/System.p b/Tutorial/6_TwoPhaseCommitVerification/Rounds/PSrc/System.p new file mode 100644 index 000000000..78de16a95 --- /dev/null +++ b/Tutorial/6_TwoPhaseCommitVerification/Rounds/PSrc/System.p @@ -0,0 +1,136 @@ +enum Vote {YES, NO} +type Round = int; +type tVoteResp = (source: machine, round: Round, vote: Vote); +type tVoteReq = (round: Round); + +event eVoteReq: tVoteReq; +event eVoteResp: tVoteResp; +event eAbort: tVoteReq; +event eCommit: tVoteReq; + +machine Coordinator +{ + var yesVotes: map[Round, set[machine]]; + var commited: set[Round]; + var aborted: set[Round]; + + start state Init { + entry { + var p: machine; + var r: Round; + assume !(r in yesVotes); + + yesVotes[r] = default(set[machine]); + + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eVoteReq; + invariant forall new (e: eVoteReq) :: e.round == r; + { + send p, eVoteReq, (round = r,); + } + + goto WaitForResponses; + } + + defer eVoteResp; + } + + state WaitForResponses { + on eVoteResp do (resp: tVoteResp) { + var p: machine; + + if (resp.vote == YES) { + yesVotes[resp.round] += (resp.source); + + if (yesVotes[resp.round] == participants()) { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eCommit; + invariant forall new (e: eCommit) :: e.round == resp.round; + { + send p, eCommit, (round = resp.round,); + } + + commited += (resp.round); + goto Init; + } + + } else { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eAbort; + invariant forall new (e: eAbort) :: e.round == resp.round; + { + send p, eAbort, (round = resp.round,); + } + + aborted += (resp.round); + goto Init; + } + } + } +} + +machine Participant { + var commited: set[Round]; + var aborted: set[Round]; + + start state Undecided { + on eVoteReq do (req: tVoteReq) { + send coordinator(), eVoteResp, (source = this, round = req.round, vote = preference(this, req.round)); + } + + on eCommit do (req: tVoteReq) { + commited += (req.round); + } + + on eAbort do (req: tVoteReq) { + aborted += (req.round); + } + } +} + +// using these to avoid initialization +pure participants(): set[machine]; +pure coordinator(): machine; +pure preference(m: machine, r: Round) : Vote; + +// assumptions about how the system is setup and the pure functions above +init forall (m: machine) :: m == coordinator() == m is Coordinator; +init forall (m: machine) :: m in participants() == m is Participant; + +// making sure that our assumptions about pure functions are not pulled out from underneath us +invariant one_coordinator: forall (m: machine) :: m == coordinator() == m is Coordinator; +invariant participant_set: forall (m: machine) :: m in participants() == m is Participant; + +// set all the fields to their default values +init forall (c: Coordinator) :: c.yesVotes == default(map[Round, set[machine]]); +init forall (c: Coordinator) :: c.commited == default(set[Round]); +init forall (c: Coordinator) :: c.aborted == default(set[Round]); +init forall (p: Participant) :: p.commited == default(set[Round]); +init forall (p: Participant) :: p.aborted == default(set[Round]); + +// make sure we never get a message that we're not expecting +invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e; +invariant never_abort_to_coordinator: forall (e: event) :: e is eAbort && e targets coordinator() ==> !inflight e; +invariant never_req_to_coordinator: forall (e: event) :: e is eVoteReq && e targets coordinator() ==> !inflight e; +invariant never_resp_to_participant: forall (e: event, p: Participant) :: e is eVoteResp && e targets p ==> !inflight e; + +// the main invariant we care about +invariant safety: forall (c: Coordinator, p1: Participant, r: Round) :: (r in p1.commited ==> (forall (p2: Participant) :: preference(p2, r) == YES)); + +// supporting invariants from non-round proof +invariant a1: forall (e: eVoteResp) :: sent e ==> e.source is Participant; +invariant a2: forall (e: eVoteResp) :: sent e ==> e.vote == preference(e.source, e.round); +invariant a3a: forall (c: Coordinator, e: eCommit) :: sent e ==> e.round in c.commited; +invariant a3b: forall (c: Coordinator, e: eAbort) :: sent e ==> e.round in c.aborted; +invariant a4: forall (c: Coordinator, r: Round, p1: Participant) :: r in p1.commited ==> r in c.commited; +invariant a5: forall (p: Participant, c: Coordinator, r: Round) :: (r in c.yesVotes && p in c.yesVotes[r]) ==> preference(p, r) == YES; +invariant a6: forall (c: Coordinator, r: Round) :: r in c.commited ==> (forall (p2: Participant) :: preference(p2, r) == YES); + +// make sure that votes have been initialized +invariant a7a: forall (c: Coordinator, e: eVoteReq) :: sent e ==> e.round in c.yesVotes; +invariant a7b: forall (c: Coordinator, e: eVoteResp) :: sent e ==> e.round in c.yesVotes; + + diff --git a/Tutorial/6_TwoPhaseCommitVerification/Rounds/TwoPhaseCommitVerification.pproj b/Tutorial/6_TwoPhaseCommitVerification/Rounds/TwoPhaseCommitVerification.pproj new file mode 100644 index 000000000..d60d0d2f7 --- /dev/null +++ b/Tutorial/6_TwoPhaseCommitVerification/Rounds/TwoPhaseCommitVerification.pproj @@ -0,0 +1,8 @@ + +TwoPhaseCommitVerification + + ./PSrc/ + +./PGenerated/ +UCLID5 + diff --git a/Tutorial/6_TwoPhaseCommitVerification/Single/PSrc/System.p b/Tutorial/6_TwoPhaseCommitVerification/Single/PSrc/System.p new file mode 100644 index 000000000..a6322795d --- /dev/null +++ b/Tutorial/6_TwoPhaseCommitVerification/Single/PSrc/System.p @@ -0,0 +1,112 @@ +enum Vote {YES, NO} +type tVoteResp = (source: machine, vote: Vote); + +event eVoteReq; +event eVoteResp: tVoteResp; +event eAbort; +event eCommit; + +machine Coordinator +{ + var yesVotes: set[machine]; + + start state Init { + entry { + var p: machine; + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eVoteReq; + { + send p, eVoteReq; + } + goto WaitForResponses; + } + } + + state WaitForResponses { + on eVoteResp do (resp: tVoteResp) { + var p: machine; + + if (resp.vote == YES) { + yesVotes += (resp.source); + + if (yesVotes == participants()) { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eCommit; + { + send p, eCommit; + } + goto Committed; + } + + } else { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eAbort; + { + send p, eAbort; + } + goto Aborted; + } + } + } + + state Committed {ignore eVoteResp;} + state Aborted {ignore eVoteResp;} +} + +machine Participant { + start state Undecided { + on eVoteReq do { + send coordinator(), eVoteResp, (source = this, vote = preference(this)); + } + + on eCommit do { + goto Accepted; + } + + on eAbort do { + goto Rejected; + } + } + + state Accepted {ignore eVoteReq, eCommit, eAbort;} + state Rejected {ignore eVoteReq, eCommit, eAbort;} +} + +// using these to avoid initialization +pure participants(): set[machine]; +pure coordinator(): machine; +pure preference(m: machine) : Vote; + +// assumptions about how the system is setup and the pure functions above +init forall (m: machine) :: m == coordinator() == m is Coordinator; +init forall (m: machine) :: m in participants() == m is Participant; + +// making sure that our assumptions about pure functions are not pulled out from underneath us +invariant one_coordinator: forall (m: machine) :: m == coordinator() == m is Coordinator; +invariant participant_set: forall (m: machine) :: m in participants() == m is Participant; + +// set all the fields to their default values +init forall (c: Coordinator) :: c.yesVotes == default(set[machine]); + +// make sure we never get a message that we're not expecting +invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e; +invariant never_abort_to_coordinator: forall (e: event) :: e is eAbort && e targets coordinator() ==> !inflight e; +invariant never_req_to_coordinator: forall (e: event) :: e is eVoteReq && e targets coordinator() ==> !inflight e; +invariant never_resp_to_participant: forall (e: event, p: Participant) :: e is eVoteResp && e targets p ==> !inflight e; +invariant never_resp_to_init: forall (e: event, c: Coordinator) :: e is eVoteResp && e targets c && c is Init ==> !inflight e; +invariant req_implies_not_init: forall (e: event, c: Coordinator) :: e is eVoteReq && c is Init ==> !inflight e; + +// the main invariant we care about +invariant safety: forall (p1: Participant) :: p1 is Accepted ==> (forall (p2: Participant) :: preference(p2) == YES); + +// supporting invariants, based on the Kondo paper +invariant a1: forall (e: eVoteResp) :: inflight e ==> e.source in participants(); +invariant a2: forall (e: eVoteResp) :: inflight e ==> e.vote == preference(e.source); +invariant a3b: forall (e: eAbort) :: inflight e ==> coordinator() is Aborted; +invariant a3a: forall (e: eCommit) :: inflight e ==> coordinator() is Committed; +invariant a4: forall (p: Participant) :: p is Accepted ==> coordinator() is Committed; +invariant a5: forall (p: Participant, c: Coordinator) :: p in c.yesVotes ==> preference(p) == YES; +invariant a6: coordinator() is Committed ==> (forall (p: Participant) :: p in participants() ==> preference(p) == YES); \ No newline at end of file diff --git a/Tutorial/6_TwoPhaseCommitVerification/Single/TwoPhaseCommitVerification.pproj b/Tutorial/6_TwoPhaseCommitVerification/Single/TwoPhaseCommitVerification.pproj new file mode 100644 index 000000000..d60d0d2f7 --- /dev/null +++ b/Tutorial/6_TwoPhaseCommitVerification/Single/TwoPhaseCommitVerification.pproj @@ -0,0 +1,8 @@ + +TwoPhaseCommitVerification + + ./PSrc/ + +./PGenerated/ +UCLID5 + diff --git a/Tutorial/7_RingLeaderVerification/.gitignore b/Tutorial/7_RingLeaderVerification/.gitignore new file mode 100644 index 000000000..161a65f6d --- /dev/null +++ b/Tutorial/7_RingLeaderVerification/.gitignore @@ -0,0 +1,7 @@ +*.out +*.err +portfolio/ +Test.cs +pom.xml +*.csproj +PCheckerOutput/ diff --git a/Tutorial/7_RingLeaderVerification/PSrc/System.p b/Tutorial/7_RingLeaderVerification/PSrc/System.p new file mode 100644 index 000000000..9779f8100 --- /dev/null +++ b/Tutorial/7_RingLeaderVerification/PSrc/System.p @@ -0,0 +1,47 @@ +type tNominate = (voteFor: machine); + +event eNominate : tNominate; + +pure le(x: machine, y: machine): bool; +axiom forall (x: machine) :: le(x, x); +axiom forall (x: machine, y: machine) :: le(x, y) || le(y, x); +axiom forall (x: machine, y: machine, z: machine) :: (le(x, y) && le(y, z)) ==> le(x, z); +axiom forall (x: machine, y: machine) :: (le(x, y) && le(y, x)) ==> (x == y); + +pure btw(x: machine, y: machine, z: machine): bool; +axiom forall (w: machine, x: machine, y: machine, z: machine) :: (btw(w, x, y) && btw(w, y, z)) ==> btw(w, x, z); +axiom forall (x: machine, y: machine, z: machine) :: btw(x, y, z) ==> !btw(x, z, y); +axiom forall (x: machine, y: machine, z: machine) :: btw(x, y, z) || btw(x, z, y) || (x == y) || (x == z) || (y == z); +axiom forall (x: machine, y: machine, z: machine) :: btw(x, y, z) ==> btw(y, z, x); + +pure right(x: machine): machine; +axiom forall (x: machine) :: x != right(x); +axiom forall (x: machine, y: machine) :: (x != y && y != right(x)) ==> btw(x, right(x), y); + +machine Server { + start state Proposing { + entry { + send right(this), eNominate, (voteFor=this,); + } + on eNominate do (n: tNominate) { + if (n.voteFor == this) { + goto Won; + } else if (le(this, n.voteFor)) { + send right(this), eNominate, (voteFor=n.voteFor,); + } else { + send right(this), eNominate, (voteFor=this,); + } + } + } + state Won { + ignore eNominate; + } +} + +// voteFor is the running max +invariant NoBypass: forall (n: machine, m: machine, e: eNominate) :: (inflight e && e targets m && n is Server && btw(e.voteFor, n, m)) ==> le(n, e.voteFor); +invariant SelfPendingMax: forall (n: machine, m: machine, e: eNominate) :: (inflight e && e targets m && e.voteFor == m) ==> le(n, m); + +// Main theorems +invariant LeaderMax: forall (x: machine, y: machine) :: x is Won ==> le(y, x); +invariant UniqueLeader: forall (x: machine, y: machine) :: (x is Won && y is Won) ==> (le(x, y) && le(y, x)); \ No newline at end of file diff --git a/Tutorial/7_RingLeaderVerification/RingLeaderVerification.pproj b/Tutorial/7_RingLeaderVerification/RingLeaderVerification.pproj new file mode 100644 index 000000000..c74824350 --- /dev/null +++ b/Tutorial/7_RingLeaderVerification/RingLeaderVerification.pproj @@ -0,0 +1,8 @@ + +RingLeaderVerification + + ./PSrc/ + +./PGenerated/ +UCLID5 +