GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
441 stars 63 forks source link

`get_opt` no longer works effectively #1068

Open ghost opened 3 years ago

ghost commented 3 years ago

How do I invoke saw with an extra argument for get_opt?

$ cat opt.saw
print (get_opt 0);
print (get_opt 1);
print (get_opt 2);

$ saw opt.saw argument
Multiple files not yet supported.
brianhuffman commented 3 years ago

That's a very good question! We should probably reopen #143, because the feature is not very useful in its current state, is it?

Maybe the current design, where get_opt just takes a single Int parameter for the argument number, is not the right one. We probably need to design it to go along with a corresponding saw command-line flag that lets you supply arbitrary strings. How would you like it to work? We could keep the Int parameter, and have it select the string from the nth occurrence of a "user string" command line option. Or maybe the command-line option could support key/value pairs, and the saw-script function could take a key string instead of an int. Any of those would probably be pretty easy to implement.

ghost commented 3 years ago

A command-line flag to indicate that there are additional arguments seems reasonable, sort of like gdb's --args.

I like the idea of key/value pairs. The key string could give some contextual help when an argument is missing, more so than:

$ # same opt.saw as before, no third argument:
$ saw opt.saw
[00:36:23.445] Loading file "opt.saw"
[00:36:23.456] saw
[00:36:23.456] opt.saw
[00:36:23.456] Stack trace:
"get_opt" (opt.saw:3:8-3:15):
nth: index too large

On a related note, would it be possible to have a get_opt analogue for passing integers as command-line arguments? It would be useful for verifications like the llvm/dotprod_struct.saw example where the (vector) size is effectively an argument.

weaversa commented 3 years ago

Bit of a hack, but you can currently do:

$ saw opt.saw -v 0x1234

And skip over the -v strings. Might want to end the command with the verbosity you actually desire :-)

weaversa commented 3 years ago

Here's some magic to get environment variables:

/** part of `nul_terminated_value` string before `nul` (`\0`) */
let unterminate (nul_terminated_value: String) : TopLevel String = do {
    unterminated_value <- exec "echo" ["-n", nul_terminated_value] "";
    return unterminated_value;
};

/** value of environment variable identified by `key` */
let get_env (key: String) : TopLevel String = do {
    terminated_value <- exec "printenv" ["-0", key] "";
    unterminated_value <- unterminate terminated_value;
    return unterminated_value;
};
WeeknightMVP commented 3 years ago

@weaversa On Linux (and maybe macOS) anyway. One could perhaps define other implementations for Windows Command Prompt, Powershell, etc., but it would be more portable to write an executable script (e.g. in Haskell or Python, but this would introduce a dependency). Of course, just having native get_env and get_opt definitions would be convenient. But this would lead to requests for other String manipulations (split, strip, substr, etc.)... These were all considerations in my hesitation to share these definitions. In the end, this would just be better-in-python.

weaversa commented 3 years ago

@weaversa On Linux (and maybe macOS) anyway. One could perhaps define other implementations for Windows Command Prompt, Powershell, etc., but it would be more portable to write an executable script (e.g. in Haskell or Python, but this would introduce a dependency). Of course, just having native get_env and get_opt definitions would be convenient. But this would lead to requests for other String manipulations (split, strip, substr, etc.)... These were all considerations in my hesitation to share these definitions. In the end, this would just be better-in-python.

Well...there isn't a Windows build for SAW. Though, the commands likely work in the Docker container. :-)