Skip to content

Commit

Permalink
update to future version of the api
Browse files Browse the repository at this point in the history
  • Loading branch information
oeb25 committed Feb 1, 2024
1 parent 2e5629a commit d14b421
Show file tree
Hide file tree
Showing 7 changed files with 50 additions and 35 deletions.
5 changes: 3 additions & 2 deletions Graph.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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
5 changes: 3 additions & 2 deletions Interpreter.fs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,8 @@ type InterpreterMemory =
arrays: Map<string, List<int>> }

type Input =
{ determinism: Determinism
{ commands: string
determinism: Determinism
assignment: InterpreterMemory
trace_length: int }

Expand Down Expand Up @@ -43,7 +44,7 @@ let prepareConfiguration (c: Configuration<Node>) : Configuration<string> =
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<Configuration<Node>> = failwith "TODO"
let final: TerminationState = failwith "TODO"
Expand Down
20 changes: 15 additions & 5 deletions Parse.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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}"
{ pretty = prettyPrint ast }
| Error e -> { pretty = String.Format("Parse error: {0}", e) }
37 changes: 19 additions & 18 deletions Program.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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<Parse.Input> input
let output: Parse.Output = Parse.analysis input
Console.WriteLine("{0}", JsonConvert.SerializeObject output)

0
| [ "graph"; src; input ] ->
| [ "Graph"; input ] ->
let input = JsonConvert.DeserializeObject<Graph.Input> 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<Interpreter.Input> 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<ProgramVerification.Input> 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<SignAnalysis.Input> 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<Security.Input> 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 <EXPRESSION...>"
"parse <SRC>"
"graph <SRC> <INPUT>"
"interpreter <SRC> <INPUT>"
"program-verification <SRC> <INPUT>"
"sign <SRC> <INPUT>"
"security <SRC> <INPUT>" ]
"parse <INPUT>"
"Graph <INPUT>"
"Interpreter <INPUT>"
"ProgramVerification <INPUT>"
"Sign <INPUT>"
"Security <INPUT>" ]

Console.Error.WriteLine(
"\x1B[1;31merror:\x1B[0m unrecognized input: \x1B[0;33m'{0}'\x1B[0m\n\n{1}\n\nAvailable commands:\n{2}",
Expand Down
6 changes: 3 additions & 3 deletions ProgramVerification.fs
Original file line number Diff line number Diff line change
Expand Up @@ -9,14 +9,14 @@ open Predicate.AST
validation and evaluation tools!
*)

type Input = unit
type Input = { commands: string }

type Output =
{ verification_conditions: List<SerializedPredicate> }

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
Expand Down
5 changes: 3 additions & 2 deletions Security.fs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,8 @@ type Classification =
arrays: Map<string, string> }

type Input =
{ lattice: Flow list
{ commands: string
lattice: Flow list
classification: Classification }

type Output =
Expand All @@ -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
7 changes: 4 additions & 3 deletions SignAnalysis.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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!
*)
Expand All @@ -18,7 +18,8 @@ type SignAssignment =
arrays: Map<string, Set<Sign>> }

type Input =
{ determinism: Determinism
{ commands: string
determinism: Determinism
assignment: SignAssignment }

type Output =
Expand All @@ -27,5 +28,5 @@ type Output =
nodes: Map<string, Set<SignAssignment>> }


let analysis (src: string) (input: Input) : Output =
let analysis (input: Input) : Output =
failwith "Sign analysis not yet implemented" // TODO: start here

0 comments on commit d14b421

Please sign in to comment.