sukyoung / safe Goto Github PK

• My Program

/*
	Here are some example ways in which you can use node-fetch. Test each code fragment separately so that you don't get errors related to constant reassigning, etc.

	Top-level `await` support is required.
*/

import fetch from "node-fetch";

// Plain text or HTML
let response = await fetch("https://github.com/");
let body = await response.text();

console.log(body);

// JSON
response = await fetch("https://github.com/");
json = await response.json();

console.log(json);

// Simple Post
response = await fetch("https://httpbin.org/post", {
	method: "POST",
	body: "a=1",
});
json = await response.json();

console.log(json);

// Post with JSON
body = { a: 1 };

response = await fetch("https://httpbin.org/post", {
	method: "post",
	body: JSON.stringify(body),
	headers: { "Content-Type": "application/json" },
});
const json = await response.json();

console.log(json);

• ERR Msg

Why am I getting this error?

Thanks for your reply!

It seems to me that SAFE does not conform to ES5.1, Section 8.7.2 PutValue (V, W), [[Put]], Step 7.a.

For the following test program:

// 8.7.2 PutValue (V, W), [[Put]], Step 7.a

// 7. Else, this is a request to create an own property on the transient object O
//     a. If Throw is true, then throw a TypeError exception.

// For [[Put]] for a reference with a primitive base,
// if it does not have its own value, but a inherited data descriptor,
// then this assignment will create its own data descriptor which cannot be used later at all, because this object will immediately disappear after this assignment
// (at least there is no reference pointing to this object, so it's not accessible).
// Thus, if throw is true, then it throws TypeError.

"use strict";
1["x"] = 10; // TypeError

SAFE failed to throw a TypeError exception:

$ ./bin/jsaf interpret 07.js
Normal(10)

Is there anything that I'm missing?

function f(a) {
    arguments[0] = "changed";
    return a;
}

function g(a) {
    a = "changed";
    return arguments[0];
}

var ret1 = f('given');
var ret2 = g('given');

For chrome, firefox and IE, ret1 == ret2 == 'changed'.
However, SAFE analyzer says that ret1 == ret2 == 'given' at the end of the program.

I set the SAFE_HOME and then ran sbt compile. sbt compile ran successfully but when I ran sbt test, it failed. It is giving null pointer exception at line number 226 in CoreTest.scala and even after setting the $SAFE_HOME/bin in bashrc it does not recognize safe command. Even i tried to run directly inside bin directory.
Could you please help me?

It seems to me that SAFE does not conform to ES5.1, Section 10.2.1.1.3 SetMutableBinding (N,V,S), Step 4.

For the following test program:

// 10.2.1.1.3 SetMutableBinding (N,V,S), Step 4, if-condition is true

// 4. Else this must be an attempt to change the value of an immutable binding so if S if true throw a TypeError exception.

// In a strict mode, assigning an immutable binding throws TypeError.

// There are only two ways to create an immutable binding:
//   1. 'arguments' is an immutable binding in a strict mode function.
//   2. name of a recursive function expression (it should be a function 'expression', not a function 'declaration') is an immutable binding of the function body's environment.
// In the first case, assigning such binding raises a syntax error, in advance, in a strict mode code, thus it cannot reach here.
// Thus, assigning the second kind of binding is the only case that can reach here, and the below example represents this case.

// In the example below, 'g' is a name of recursive function expression, thus inside the function body, 'g' is a immutable binding.
// Note that 'g' is not visible outside of the function body, that is, it is not visible in a global scope.

"use strict";
var f = function g() {
  g = 0;
};
f(); // TypeError

SAFE failed to throw a TypeError exception:

$ ./bin/jsaf interpret 09.js
Normal(undefined)

Is there anything that I'm missing?

Hi,

I am new to SAFE. Recently, I am trying to import a preprocessed CFG into SAFE for improving its performance of bugs analysis. However, I noticed that the program uses the IR nodes during the phase CfgBuild. I was wondering whether these objects are essential in the analysis phase.
Besides, I realize that the origin CFG from SAFE includes some variables like the loop head and local variables. I was wondering whether those things are also critical.

Further, might I request any suggestions about the CFG importation? Is there anything else that is critical but not noticed by me?

Many thanks,
Yichao

sbt compile is failing on a linux machine with the error:

[error] (compile:buildParsers) Error opening http://central.maven.org/maven2/xtc/rats/2.4.0/rats-2.4.0.jar: java.io.IOException: Server returned HTTP response code: 501 for URL: http://central.maven.org/maven2/xtc/rats/2.4.0/rats-2.4.0.jar

Dear developers of SAFE, 

I notice that safe accepts multiple JS files as inputs, so I was wondering whether the SAFE is able to handle the model and some functions in NodeJS like module.exports and requires("...") to invoke some functions in different files. 

Besides, I am confused about how the CallInstructions are handled in SAFE. I noticed there are some methods like sematic.CI and semantics.getCallInfo. Those two functions require TracePartition as a parameter, but the output of sematic.getState(callBlock) always be Nil. I was wondering whether there are any development documents or examples of their usage.

Many thanks, 

In a Jan 17 comment, @jhnaldo writes:

We are currently developing JSAVER, a JavaScript static analyzer, based on the JavaScript syntax and semantics extracted from ECMAScript specification via JISET. While the current version of JSAVER is a prototype implementation, we checked that it can successfully analyze all applicable JavaScript programs in Test262: ECMAScript Test Suite (ECMA TR/104).

On the other hand, our team also has developed SAFE, a JavaScript static analyzer for ECMAScript 5.1, with abstract semantics designed by hand in several years.

I cannot find JSAVER. Is it shared publicly yet? So this SAFE tool seems to be the closest thing with an open issues list...

I have an idea for a static analysis tool to check for unexpected throws. Expected throws would be denoted as assert(cond) or assert.typeof(x, 'string') or assert.equal(a, b) or the like. If any code path could lead to a throw other than an explicit assert, the tool should report that as a problem. I expect this would be extremely valuable in establishing that input validation has been done thoroughly. For example, in issues such as:

• Agoric/agoric-sdk#4068

I would appreciate any thoughts you would like to share on how to go about making such a tool.

Feel free to write to me at [email protected] if you prefer that over a github issue such as this.

cc @erights

See line 30 of src/main/scala/kr/ac/kaist/safe/parser/Parser.scala and similar ones in other files.

On clicking the link for user manual from the repo readme it displays a 404 GitHub page.

It seems to me that SAFE does not conform to ES5.1, Section 8.7.2 PutValue (V, W), [[Put]], Step 2.a.

For the following test program:

// 8.7.2 PutValue (V, W), [[Put]], Step 2.a

// 2. If the result of calling the [[CanPut]] internal method of O with argument P is false, then
//     a. If Throw is true, then throw a TypeError exception.
//     b. ...

// For [[Put]] for a reference with a primitive base,
// if [[CanPut]] returns false, and Throw is true, then it throws TypeError.

// NOTE: In this example, [[CanPut]] returns false, because 'writable' is false.

"use strict";
Object.defineProperty(Number.prototype, "x", { "value" : 0, "writable" : false, "enumerable" : true, "configurable" : true });
1["x"] = 10; // TypeError

SAFE failed to throw a TypeError exception:

$ ./bin/jsaf interpret 02.js
Normal(10)

Is there anything that I'm missing?

I would expect safe bugDetect arity.js to detect some bugs in this case:

function add3(a, b, c) {
  return a + b + c;
}

add3(1, "x");

add3(1, 2, null, 4, 3);

but it just says:

$ safe bugDetect arity.js 
The command 'bugDetect' took 1656 ms.

I tried to analyse the html file given that the tool analyses DOM interactions in the HTML page. But when i run the commond

$safe bugDetect {respective html file}

I see a message saying that getElementById is not implemented. On checking the repository i don't find relevant files relating DOM modeller or Event modeller as mentioned in the SAFE paper.