Some dependencies confuse module resolution

[jryans]

I'm in the process of evaluating the SCV approach for some future projects, and I've noticed that certain forms confuse SCV's module resolution. For example, the following file:

#lang racket

(contract-random-generate integer?)

gives:

$ raco scv module-resolver.rkt
- dependency: /Applications/Racket v8.8/collects/racket/contract/private/generate.rkt for `contract-random-generate`
- dependency: /Users/jryans/Projects/Static Contract Verification/racket/guts.rkt for `value-contract`
open-input-file: cannot open input file
  path: /Users/jryans/Projects/Static Contract Verification/racket/guts.rkt
  system error: No such file or directory; errno=2
  context...:
   /Users/jryans/Projects/Static Contract Verification/racket/soft-contract/soft-contract/parse/expand.rkt:141:0: do-expand-file
   .../private/map.rkt:40:19: loop
   /Users/jryans/Projects/Static Contract Verification/racket/soft-contract/soft-contract/parse/private.rkt:146:4: parse-files
   /Users/jryans/Projects/Static Contract Verification/racket/soft-contract/soft-contract/parse/main.rkt:26:4: parse-files65
   /Users/jryans/Projects/Static Contract Verification/racket/soft-contract/soft-contract/verifier.rkt:49:2: havoc105
   /Users/jryans/Projects/Static Contract Verification/racket/soft-contract/soft-contract/cmdline.rkt:59:4
   /Applications/Racket v8.8/collects/racket/private/more-scheme.rkt:163:2: select-handler/no-breaks
   [repeats 1 more time]
   body of "/Users/jryans/Projects/Static Contract Verification/racket/soft-contract/soft-contract/cmdline.rkt"
   /Applications/Racket v8.8/collects/raco/raco.rkt:41:0
   body of "/Applications/Racket v8.8/collects/raco/raco.rkt"
   body of "/Applications/Racket v8.8/collects/raco/main.rkt"

The file guts.rkt is part of Racket itself in the racket/contract/private directory, but for some reason, SCV's module resolution seems to believe it should exist in the same directory as the input file, which of course fails.

This issue occurs with both Racket 8.8 and 7.8 (version used in SCV-CR).

I've tried to apply various local hacks to work around this, but I do not yet fully understand which step is actually failing, so someone with better knowledge of SCV and / or module resolution may have a better path forward here.

[philnguyen]

The "module resolution" mechanism was very hacky, just enough for running benchmarks. Here it wasn't supposed to follow through Racket's private stuff. The printing out of dependencies is for debugging, and what I used to do was having a large set of declarations of contracts for for "primitives" or "library functions" whenever I encounter one I don't want to pull in to analyze (e.g. https://github.com/philnguyen/soft-contract/blob/5e07dc2d622ee80b961f4e8aebd04ce950720239/soft-contract/primitives/prims-04-09.rkt)

[jryans]

Ah right, okay, so it sounds like this could be resolved by adding another primitive.

About this large set of primitives... Is it mainly there as a performance optimisation (by analysing only application code and avoiding Racket internals), or is it about implementation simplification (by avoiding the need to parse e.g. Racket language features and forms that only appear in Racket internals)? It might be a bit of both...? Anyway, I am just trying to understand the intention behind this part of SCV.

Thanks for taking a look! 😄

[samth]

It's trying to avoid figuring out the specification for things like third from its source, both for performance and accuracy reasons. But also contracts are analyzed directly without trying to look at their implementation because it's very hard to accurately analyze the generated code.