From d14b42117ae756df30514155861ccedef6f43006 Mon Sep 17 00:00:00 2001 From: oeb25 Date: Thu, 1 Feb 2024 15:27:31 +0100 Subject: [PATCH] update to future version of the api --- Graph.fs | 5 +++-- Interpreter.fs | 5 +++-- Parse.fs | 20 +++++++++++++++----- Program.fs | 37 +++++++++++++++++++------------------ ProgramVerification.fs | 6 +++--- Security.fs | 5 +++-- SignAnalysis.fs | 7 ++++--- 7 files changed, 50 insertions(+), 35 deletions(-) diff --git a/Graph.fs b/Graph.fs index 4be692b..1eab64d 100644 --- a/Graph.fs +++ b/Graph.fs @@ -8,9 +8,10 @@ open Types evaluation tools! *) -type Input = { determinism: Determinism } +type Input = { commands: string + determinism: Determinism } type Output = { dot: string } -let analysis (src: string) (input: Input) : Output = +let analysis (input: Input) : Output = failwith "Graph analysis not yet implemented" // TODO: start here diff --git a/Interpreter.fs b/Interpreter.fs index f1688e9..e04c284 100644 --- a/Interpreter.fs +++ b/Interpreter.fs @@ -12,7 +12,8 @@ type InterpreterMemory = arrays: Map> } type Input = - { determinism: Determinism + { commands: string + determinism: Determinism assignment: InterpreterMemory trace_length: int } @@ -43,7 +44,7 @@ let prepareConfiguration (c: Configuration) : Configuration = memory = c.memory } -let analysis (src: string) (input: Input) : Output = +let analysis (input: Input) : Output = failwith "Interpreter not yet implemented" // TODO: start here let execution_sequence: List> = failwith "TODO" let final: TerminationState = failwith "TODO" diff --git a/Parse.fs b/Parse.fs index 7ea66eb..e2b24d9 100644 --- a/Parse.fs +++ b/Parse.fs @@ -25,13 +25,23 @@ let parse parser src = eprintf "\n" Error(ParseError(pos, lastToken, e)) -let rec prettyPrint ast = +let rec prettyPrint ast : string = // TODO: start here failwith "GCL parser not yet implemented" -let analysis (src: string) : string = - match parse Parser.start (src) with +(* + This defines the input and output for the security analysis. Please do not + change the definitions below as they are needed for the validation and + evaluation tools! +*) + +type Input = { commands: string } + +type Output = { pretty: string } + +let analysis (input: Input) : Output = + match parse Parser.start input.commands with | Ok ast -> Console.Error.WriteLine("> {0}", ast) - prettyPrint ast - | Error e -> "Parse error: {0}" \ No newline at end of file + { pretty = prettyPrint ast } + | Error e -> { pretty = String.Format("Parse error: {0}", e) } diff --git a/Program.fs b/Program.fs index 3021959..ae72ba3 100644 --- a/Program.fs +++ b/Program.fs @@ -49,50 +49,51 @@ let main (args) = | Error e -> Console.Error.WriteLine("Parse error: {0}", e) 0 - | "parse" :: src :: _ -> - let output: string = Parse.analysis src + | ["Parse"; input ] -> + let input = JsonConvert.DeserializeObject input + let output: Parse.Output = Parse.analysis input Console.WriteLine("{0}", JsonConvert.SerializeObject output) 0 - | [ "graph"; src; input ] -> + | [ "Graph"; input ] -> let input = JsonConvert.DeserializeObject input - let output: Graph.Output = Graph.analysis src input + let output: Graph.Output = Graph.analysis input Console.WriteLine("{0}", JsonConvert.SerializeObject output) 0 - | [ "interpreter"; src; input ] -> + | [ "Interpreter"; input ] -> let input = JsonConvert.DeserializeObject input - let output: Interpreter.Output = Interpreter.analysis src input + let output: Interpreter.Output = Interpreter.analysis input Console.WriteLine("{0}", JsonConvert.SerializeObject output) 0 - | [ "program-verification"; src; input ] -> + | [ "ProgramVerification"; input ] -> let input = JsonConvert.DeserializeObject input - let output: ProgramVerification.Output = ProgramVerification.analysis src input + let output: ProgramVerification.Output = ProgramVerification.analysis input Console.WriteLine("{0}", JsonConvert.SerializeObject output) 0 - | [ "sign"; src; input ] -> + | [ "Sign"; input ] -> let input = JsonConvert.DeserializeObject input - let output: SignAnalysis.Output = SignAnalysis.analysis src input + let output: SignAnalysis.Output = SignAnalysis.analysis input Console.WriteLine("{0}", JsonConvert.SerializeObject output) 0 - | [ "security"; src; input ] -> + | [ "Security"; input ] -> let input = JsonConvert.DeserializeObject input - let output: Security.Output = Security.analysis src input + let output: Security.Output = Security.analysis input Console.WriteLine("{0}", JsonConvert.SerializeObject output) 0 | _ -> let commands = [ "calc " - "parse " - "graph " - "interpreter " - "program-verification " - "sign " - "security " ] + "parse " + "Graph " + "Interpreter " + "ProgramVerification " + "Sign " + "Security " ] Console.Error.WriteLine( "\x1B[1;31merror:\x1B[0m unrecognized input: \x1B[0;33m'{0}'\x1B[0m\n\n{1}\n\nAvailable commands:\n{2}", diff --git a/ProgramVerification.fs b/ProgramVerification.fs index 630ca56..b165c50 100644 --- a/ProgramVerification.fs +++ b/ProgramVerification.fs @@ -9,14 +9,14 @@ open Predicate.AST validation and evaluation tools! *) -type Input = unit +type Input = { commands: string } type Output = { verification_conditions: List } -let analysis (src: string) (input: Input) : Output = +let analysis (input: Input) : Output = let (P, C, Q) = - match Predicate.Parse.parse src with + match Predicate.Parse.parse input.commands with | Ok (AnnotatedCommand (P, C, Q)) -> P, C, Q | Error e -> failwith diff --git a/Security.fs b/Security.fs index dfb0b0f..c6d74c3 100644 --- a/Security.fs +++ b/Security.fs @@ -14,7 +14,8 @@ type Classification = arrays: Map } type Input = - { lattice: Flow list + { commands: string + lattice: Flow list classification: Classification } type Output = @@ -23,5 +24,5 @@ type Output = violations: Flow list } -let analysis (src: string) (input: Input) : Output = +let analysis (input: Input) : Output = failwith "Security analysis not yet implemented" // TODO: start here diff --git a/SignAnalysis.fs b/SignAnalysis.fs index 863ced2..0a592a0 100644 --- a/SignAnalysis.fs +++ b/SignAnalysis.fs @@ -3,7 +3,7 @@ module SignAnalysis open Types (* - This defines the input and output of the sign analysis. Please do not + This defines the input and output of the sign analysis. Please do not change the definitions below as they are needed for the validation and evaluation tools! *) @@ -18,7 +18,8 @@ type SignAssignment = arrays: Map> } type Input = - { determinism: Determinism + { commands: string + determinism: Determinism assignment: SignAssignment } type Output = @@ -27,5 +28,5 @@ type Output = nodes: Map> } -let analysis (src: string) (input: Input) : Output = +let analysis (input: Input) : Output = failwith "Sign analysis not yet implemented" // TODO: start here