tla-rs 0.1.0

Rust implementation of the IronFleet verified distributed systems framework
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142

# -*- python -*-
import atexit
import os, os.path
import re
import shutil
import subprocess
import sys
import SCons.Util
import threading

Import("*")

# Retrieve tool-specific command overrides passed in by the user
AddOption('--verus-path',
  dest='verus_path',
  type='string',
  nargs=1,
  default=None,
  action='store',
  help='Specify the path to your local copy of the Verus repo')

AddOption('--no-verify',
  dest='no_verify',
  default=False,
  action='store_true',
  help="Don't verify, just build executables")

AddOption('--debug-build',
  dest='debug_build',
  default=False,
  action='store_true',
  help="Build executables in debug mode")

verus_path = GetOption('verus_path')
if verus_path is None:
  sys.stderr.write("ERROR:  Missing --verus-path= on command line\n")
  exit(-1)

#verus_variant = "debug" if GetOption('debug_build') else "release"
verus_variant = "release"
# verus_script = os.path.join(verus_path, f"source/target-verus/{verus_variant}/verus")
verus_script = verus_path
if sys.platform == 'win32':
    verus_script = verus_script + ".exe"
if not os.path.exists(verus_script):
  sys.stderr.write("ERROR:  Could not find %s\n" % (verus_script))
  exit(-1)

env = Environment(ENV=os.environ)

####################################################################
#
#   .NET binaries
#
####################################################################

def generate_dotnet_actions(source, target, env, for_signature):
  target_dir = os.path.dirname(str(target[0]))
  build_config = "Debug" if GetOption('debug_build') else "Release"
  return [
    ["dotnet", "build", "--configuration", build_config, "--output", target_dir, str(source[0])]
  ]

def get_dotnet_dependencies(target, source, env):
  csproj_file = str(source[0])
  source_dir = os.path.dirname(csproj_file)
  extra_dependencies = [os.path.join(source_dir, f) for f in os.listdir(source_dir) if re.search(r'\.cs$', f)]
  with open(csproj_file, 'r') as fh:
    for line in fh.readlines():
      m = re.search(r'<Compile\s+Include=\"([^\"]*)\"\s*/>', line)
      if m:
        raw_file_name = re.sub(r'\\', '/', m.group(1))
        file_name = os.path.normpath(os.path.join(source_dir, raw_file_name))
        extra_dependencies.append(file_name)
  return target, source + extra_dependencies

# Add env.DotnetBuild(), to generate dotnet build actions
def add_dotnet_builder(env):
  client_builder = Builder(generator = generate_dotnet_actions,
                           chdir=0,
                           emitter=get_dotnet_dependencies)
  env.Append(BUILDERS = {'DotnetBuild' : client_builder})


####################################################################
#
#   Verus binaries
#
####################################################################

def generate_verus_actions(source, target, env, for_signature):
  source_dir = os.path.dirname(str(source[0]))
  # [jonh] NB -C opt-level=3 is the default; I don't think it does
  # anything here.
  # https://users.rust-lang.org/t/do-rust-compilers-have-optimization-flags-like-c-compilers-have/48833/7
  opt_flag = ["-g"] if GetOption('debug_build') else ["-C", "opt-level=3"]
  cmd_line = [verus_script, "--crate-type=dylib", "--expand-errors"] + opt_flag + ["--compile", str(source[0])]
  if GetOption("no_verify"):
      cmd_line.append("--no-verify")
  return [ cmd_line ]

def get_verus_dependencies(target, source, env):
  source_dir = os.path.dirname(str(source[0]))

  extra_dependencies = []
  for root, _, files in os.walk(source_dir):
    for f in files:
      if f.endswith('.rs'):
        extra_dependencies.append(os.path.join(root, f))

  return target, source + extra_dependencies

# Add env.VerusBuild(), to generate Verus build actions
def add_verus_builder(env):
  client_builder = Builder(generator = generate_verus_actions,
                           chdir=0,
                           emitter=get_verus_dependencies)
  env.Append(BUILDERS = {'VerusBuild' : client_builder})
  
####################################################################
#
#   Put it all together
#
####################################################################

add_dotnet_builder(env)
add_verus_builder(env)

####################################################################
#
#   Create dependencies
#
####################################################################

# env.DotnetBuild('bin/IronLockServer.dll', 'csharp/IronLockServer/IronLockServer.csproj')
env.DotnetBuild('bin/IronRSLClient.dll', 'csharp/IronRSLClient/IronRSLClient.csproj')
env.DotnetBuild('bin/IronRSLServer.dll', 'csharp/IronRSLServer/IronRSLServer.csproj')
env.DotnetBuild('bin/IronRSLClientUDP.dll', 'csharp/IronRSLClientUDP/IronRSLClientUDP.csproj')
env.DotnetBuild('bin/IronRSLServerUDP.dll', 'csharp/IronRSLServerUDP/IronRSLServerUDP.csproj')
env.DotnetBuild('bin/CreateIronServiceCerts.dll', 'csharp/CreateIronServiceCerts/CreateIronServiceCerts.csproj')
env.DotnetBuild('bin/TestIoFramework.dll', 'csharp/TestIoFramework/TestIoFramework.csproj')
env.VerusBuild('liblib.so', 'src/lib.rs')